NormResidueLatticeMap.lean

1 import PaperX.ResidueLatticeIdealPoints
2 import PaperX.NormResidueArithmetic
3 
4 /-! Exact descent from actual ideal-lattice residues to arithmetic residue norms.
5 The map need not be surjective; no codomain density is inferred from it. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperX.NormResidueLattice
9 open Ideal NumberField
10 open PaperX.IdealClassQuantitative PaperX.ResidueLattice PaperX.NormResidue
11 open scoped nonZeroDivisors
12 
13 variable (K : Type*) [Field K] [NumberField K]
14 
15 /-- The unique algebraic integer underlying a point of an actual integral ideal lattice. -/
16 def integerRepresentative (J : (Ideal (𝓞 K))⁰) (x : idealEuclideanLattice K J) : 𝓞 K :=
17   ((idealPointEquiv K J).symm x).1
18 
19 theorem integerRepresentative_point (J : (Ideal (𝓞 K))⁰) (x : idealEuclideanLattice K J) :
20     integerPoint K (integerRepresentative K J x) = x.1 :=
21   congrArg Subtype.val ((idealPointEquiv K J).apply_symm_apply x)
22 
23 theorem integerRepresentative_equiv (J : (Ideal (𝓞 K))⁰) (x : (J : Ideal (𝓞 K))) :
24     integerRepresentative K J (idealPointEquiv K J x) = x.1 :=
25   congrArg Subtype.val ((idealPointEquiv K J).symm_apply_apply x)
26 
27 /-- The true map on the ideal-lattice residue quotient, when M lies in the modulus ideal.
28 The domain is J/(J∩M); it is J/M when M≤J. -/
29 def residueToIntegerQuotient (M J : (Ideal (𝓞 K))⁰) (m : ℕ)
30     (hM : (M : Ideal (𝓞 K)) ≤ modulusIdeal (𝓞 K) m) :
31     IdealResidues K M J → 𝓞 K ⧸ modulusIdeal (𝓞 K) m :=
32   Quotient.lift (fun x : idealEuclideanLattice K J => Ideal.Quotient.mk (modulusIdeal (𝓞 K) m)
33     (integerRepresentative K J x)) (by
34       intro x y hxy
35       apply Ideal.Quotient.eq.mpr
36       apply hM
37       rw [← integerPoint_mem_iff K M, integerPoint_sub,
38         integerRepresentative_point, integerRepresentative_point]
39       exact (Submodule.Quotient.eq
40         ((idealEuclideanLattice K M).comap (idealEuclideanLattice K J).subtype)).mp
41           (Quotient.sound hxy))
42 
43 theorem residueToIntegerQuotient_mk (M J : (Ideal (𝓞 K))⁰) (m : ℕ)
44     (hM : (M : Ideal (𝓞 K)) ≤ modulusIdeal (𝓞 K) m)
45     (x : (J : Ideal (𝓞 K))) :
46     residueToIntegerQuotient K M J m hM
47       (Submodule.Quotient.mk (idealPointEquiv K J x)) =
48         Ideal.Quotient.mk (modulusIdeal (𝓞 K) m) x.1 := by
49   change Ideal.Quotient.mk _ (integerRepresentative K J (idealPointEquiv K J x)) = _
50   rw [integerRepresentative_equiv]
51 
52 /-- The actual signed element norm on the additive ideal-lattice residue quotient. -/
53 def residueNorm (M J : (Ideal (𝓞 K))⁰) (m : ℕ)
54     (hM : (M : Ideal (𝓞 K)) ≤ modulusIdeal (𝓞 K) m) :
55     IdealResidues K M J → ZMod m :=
56   fun c => integerQuotientNorm K m (residueToIntegerQuotient K M J m hM c)
57 
58 theorem residueNorm_mk (M J : (Ideal (𝓞 K))⁰) (m : ℕ)
59     (hM : (M : Ideal (𝓞 K)) ≤ modulusIdeal (𝓞 K) m)
60     (x : (J : Ideal (𝓞 K))) :
61     residueNorm K M J m hM (Submodule.Quotient.mk (idealPointEquiv K J x)) =
62       (Algebra.norm ℤ x.1 : ZMod m) := by
63   rw [residueNorm, residueToIntegerQuotient_mk, integerQuotientNorm_mk]
64 
65 end PaperX.NormResidueLattice

Back to source controls