import Mathlib.NumberTheory.NumberField.Ideal.Basic
import Mathlib.Data.ZMod.Basic

/-!
# The actual norm on a finite residue algebra

The determinant of multiplication descends to reduction modulo an integer.
This construction uses a basis of the integral algebra and proves the value
on every representative, rather than assuming a norm label on a quotient.
-/

noncomputable section

namespace PaperX.NormResidue

variable (S : Type*) [CommRing S]

/-- The ideal generated by the rational integer modulus. -/
def modulusIdeal (m : ℕ) : Ideal S := Ideal.span {(m : S)}

variable {S} {ι : Type*} [Fintype ι] [DecidableEq ι]

/-- Multiplication matrices with coefficients reduced modulo `m`. -/
def residueMatrix (b : Module.Basis ι ℤ S) (m : ℕ) :
    S →+* Matrix ι ι (ZMod m) :=
  (Int.castRingHom (ZMod m)).mapMatrix.comp (Algebra.leftMulMatrix b).toRingHom

theorem residueMatrix_modulus (b : Module.Basis ι ℤ S) (m : ℕ) :
    residueMatrix b m (m : S) = 0 := by
  rw [map_natCast]
  ext i j
  simp [Matrix.natCast_apply]

theorem residueMatrix_eq_zero_of_mem (b : Module.Basis ι ℤ S) (m : ℕ)
    {x : S} (hx : x ∈ modulusIdeal S m) : residueMatrix b m x = 0 := by
  obtain ⟨y, rfl⟩ := Ideal.mem_span_singleton.mp hx
  rw [map_mul, residueMatrix_modulus, zero_mul]

/-- The actual multiplication representation of the residue algebra. -/
def quotientMatrix (b : Module.Basis ι ℤ S) (m : ℕ) :
    S ⧸ modulusIdeal S m →+* Matrix ι ι (ZMod m) :=
  Ideal.Quotient.lift _ (residueMatrix b m)
    (fun _ hx => residueMatrix_eq_zero_of_mem b m hx)

/-- The determinant norm of a residue class. -/
def quotientNorm (b : Module.Basis ι ℤ S) (m : ℕ) :
    S ⧸ modulusIdeal S m →* ZMod m :=
  Matrix.detMonoidHom.comp (quotientMatrix b m).toMonoidHom

theorem quotientNorm_mk (b : Module.Basis ι ℤ S) (m : ℕ) (x : S) :
    quotientNorm b m (Ideal.Quotient.mk (modulusIdeal S m) x) =
      (Algebra.norm ℤ x : ZMod m) := by
  change (residueMatrix b m x).det = _
  rw [Algebra.norm_eq_matrix_det b]
  exact ((Int.castRingHom (ZMod m)).map_det _).symm

theorem norm_congr_of_sub_mem (b : Module.Basis ι ℤ S) (m : ℕ)
    {x y : S} (h : x - y ∈ modulusIdeal S m) :
    (Algebra.norm ℤ x : ZMod m) = (Algebra.norm ℤ y : ZMod m) := by
  rw [← quotientNorm_mk b m x, ← quotientNorm_mk b m y]
  exact congrArg (quotientNorm b m) ((Ideal.Quotient.mk_eq_mk_iff_sub_mem _ _).mpr h)

theorem quotientNorm_basis_independent {κ : Type*} [Fintype κ] [DecidableEq κ]
    (b : Module.Basis ι ℤ S) (c : Module.Basis κ ℤ S) (m : ℕ) :
    quotientNorm b m = quotientNorm c m := by
  ext q
  obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective q
  rw [quotientNorm_mk, quotientNorm_mk]

end PaperX.NormResidue