NormResidueAlgebra.lean

1 import Mathlib.NumberTheory.NumberField.Ideal.Basic
2 import Mathlib.Data.ZMod.Basic
3 
4 /-!
5 # The actual norm on a finite residue algebra
6 
7 The determinant of multiplication descends to reduction modulo an integer.
8 This construction uses a basis of the integral algebra and proves the value
9 on every representative, rather than assuming a norm label on a quotient.
10 -/
11 
12 noncomputable section
13 
14 namespace PaperX.NormResidue
15 
16 variable (S : Type*) [CommRing S]
17 
18 /-- The ideal generated by the rational integer modulus. -/
19 def modulusIdeal (m : ℕ) : Ideal S := Ideal.span {(m : S)}
20 
21 variable {S} {ι : Type*} [Fintype ι] [DecidableEq ι]
22 
23 /-- Multiplication matrices with coefficients reduced modulo `m`. -/
24 def residueMatrix (b : Module.Basis ι ℤ S) (m : ℕ) :
25     S →+* Matrix ι ι (ZMod m) :=
26   (Int.castRingHom (ZMod m)).mapMatrix.comp (Algebra.leftMulMatrix b).toRingHom
27 
28 theorem residueMatrix_modulus (b : Module.Basis ι ℤ S) (m : ℕ) :
29     residueMatrix b m (m : S) = 0 := by
30   rw [map_natCast]
31   ext i j
32   simp [Matrix.natCast_apply]
33 
34 theorem residueMatrix_eq_zero_of_mem (b : Module.Basis ι ℤ S) (m : ℕ)
35     {x : S} (hx : x ∈ modulusIdeal S m) : residueMatrix b m x = 0 := by
36   obtain ⟨y, rfl⟩ := Ideal.mem_span_singleton.mp hx
37   rw [map_mul, residueMatrix_modulus, zero_mul]
38 
39 /-- The actual multiplication representation of the residue algebra. -/
40 def quotientMatrix (b : Module.Basis ι ℤ S) (m : ℕ) :
41     S ⧸ modulusIdeal S m →+* Matrix ι ι (ZMod m) :=
42   Ideal.Quotient.lift _ (residueMatrix b m)
43     (fun _ hx => residueMatrix_eq_zero_of_mem b m hx)
44 
45 /-- The determinant norm of a residue class. -/
46 def quotientNorm (b : Module.Basis ι ℤ S) (m : ℕ) :
47     S ⧸ modulusIdeal S m →* ZMod m :=
48   Matrix.detMonoidHom.comp (quotientMatrix b m).toMonoidHom
49 
50 theorem quotientNorm_mk (b : Module.Basis ι ℤ S) (m : ℕ) (x : S) :
51     quotientNorm b m (Ideal.Quotient.mk (modulusIdeal S m) x) =
52       (Algebra.norm ℤ x : ZMod m) := by
53   change (residueMatrix b m x).det = _
54   rw [Algebra.norm_eq_matrix_det b]
55   exact ((Int.castRingHom (ZMod m)).map_det _).symm
56 
57 theorem norm_congr_of_sub_mem (b : Module.Basis ι ℤ S) (m : ℕ)
58     {x y : S} (h : x - y ∈ modulusIdeal S m) :
59     (Algebra.norm ℤ x : ZMod m) = (Algebra.norm ℤ y : ZMod m) := by
60   rw [← quotientNorm_mk b m x, ← quotientNorm_mk b m y]
61   exact congrArg (quotientNorm b m) ((Ideal.Quotient.mk_eq_mk_iff_sub_mem _ _).mpr h)
62 
63 theorem quotientNorm_basis_independent {κ : Type*} [Fintype κ] [DecidableEq κ]
64     (b : Module.Basis ι ℤ S) (c : Module.Basis κ ℤ S) (m : ℕ) :
65     quotientNorm b m = quotientNorm c m := by
66   ext q
67   obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective q
68   rw [quotientNorm_mk, quotientNorm_mk]
69 
70 end PaperX.NormResidue

Back to source controls