CyclicQuotients.lean

1 import RealizationBoundaries.RadicalCounts
2 import Mathlib.Data.ZMod.QuotientRing
3 
4 /-! # Canonical cyclic coordinates for every integer quotient
5 
6 Chinese remainder identifies the product of distinct prime coordinates with
7 ZMod(rad m). Both the original quotient representative map and the transition
8 maps for divisibility of multipliers are retained explicitly.
9 -/
10 set_option autoImplicit false
11 noncomputable section
12 open scoped BigOperators
13 namespace RealizationBoundaries
14 
15 /-- The CRT equivalence is a ring equivalence on the coordinate target. -/
16 def divisorCrtEquiv {m : ℕ} (hm : 0 < m) :
17     ZMod (primeRadical m) ≃+* DivisorCoordinates m := by
18   letI : Finite (DivisorPrime m) := divisorPrime_finite hm
19   letI := Fintype.ofFinite (DivisorPrime m)
20   have hc : Pairwise (fun p q : DivisorPrime m => Nat.Coprime p.val.val q.val.val) := by
21     intro p q hpq
22     exact (Nat.coprime_primes p.val.property q.val.property).mpr
23       (fun h => hpq (Subtype.ext (Subtype.ext h)))
24   exact (ZMod.ringEquivCongr (divisorPrime_prod hm).symm).trans
25     (ZMod.prodEquivPi (fun p : DivisorPrime m => p.val.val) hc)
26 
27 /-- Integer representatives are reduced to their actual prime-coordinate residues. -/
28 @[simp] theorem divisorCrtEquiv_natCast {m : ℕ} (hm : 0 < m) (n : ℕ)
29     (p : DivisorPrime m) : divisorCrtEquiv hm (n : ZMod (primeRadical m)) p =
30       (n : Coordinate p.val) := by
31   exact congrArg (fun z : DivisorCoordinates m => z p) (map_natCast (divisorCrtEquiv hm) n)
32 
33 @[simp] theorem divisorCrtEquiv_intCast {m : ℕ} (hm : 0 < m) (n : ℤ)
34     (p : DivisorPrime m) : divisorCrtEquiv hm (n : ZMod (primeRadical m)) p =
35       (n : Coordinate p.val) := by
36   exact congrArg (fun z : DivisorCoordinates m => z p) (map_intCast (divisorCrtEquiv hm) n)
37 
38 /-- Complete cyclic identification of the actual quotient by m H_W. -/
39 def cyclicIntegerQuotientEquiv (W : Submodule ℚ TailSpace) {m : ℕ} (hm : 0 < m) :
40     (preimage W ⧸ multiples W m) ≃+ ZMod (primeRadical m) :=
41   (integerQuotientEquiv W hm).trans (divisorCrtEquiv hm).toAddEquiv.symm
42 
43 /-- The cyclic and product coordinates agree on every quotient element. -/
44 @[simp] theorem cyclicIntegerQuotientEquiv_coordinates (W : Submodule ℚ TailSpace) {m : ℕ}
45     (hm : 0 < m) (x : preimage W ⧸ multiples W m) :
46     divisorCrtEquiv hm (cyclicIntegerQuotientEquiv W hm x) = integerQuotientEquiv W hm x :=
47   (divisorCrtEquiv hm).toAddEquiv.apply_symm_apply _
48 
49 /-- The cyclic identification remembers the supplied original element. -/
50 @[simp] theorem cyclicIntegerQuotientEquiv_mk (W : Submodule ℚ TailSpace) {m : ℕ}
51     (hm : 0 < m) (x : preimage W) :
52     divisorCrtEquiv hm (cyclicIntegerQuotientEquiv W hm (QuotientAddGroup.mk x)) =
53       coordinateMap W m x := by
54   simp [cyclicIntegerQuotientEquiv]
55 
56 /-- Every root fiber can also be coordinatized by one cyclic radical residue. -/
57 def cyclicRootFiberEquiv (W : Submodule ℚ TailSpace) {m : ℕ} (hm : 0 < m)
58     (x : preimage W) (y : RootFiber W m x) : RootFiber W m x ≃ ZMod (primeRadical m) :=
59   (rootFiberEquiv W hm x y).trans (divisorCrtEquiv hm).symm.toEquiv
60 
61 /-- Explicit cyclic enumeration of all roots, as translated finite-support corrections. -/
62 theorem cyclicRootFiberEquiv_symm_natCast (W : Submodule ℚ TailSpace) {m : ℕ}
63     (hm : 0 < m) (x : preimage W) (y : RootFiber W m x) (n : ℕ) :
64     ((cyclicRootFiberEquiv W hm x y).symm (n : ZMod (primeRadical m))).val.val =
65       y.val.val + coordinateExtension m (fun p => (n : Coordinate p.val)) := by
66   change y.val.val + coordinateExtension m (divisorCrtEquiv hm (n : ZMod (primeRadical m))) = _
67   have he : divisorCrtEquiv hm (n : ZMod (primeRadical m)) =
68       (fun p : DivisorPrime m => (n : Coordinate p.val)) := by
69     funext p
70     exact divisorCrtEquiv_natCast hm n p
71   rw [he]
72 
73 /-- Divisibility reverses the inclusion of the original multiple subgroups. -/
74 theorem multiples_antitone (W : Submodule ℚ TailSpace) {m n : ℕ} (hmn : m ∣ n) :
75     multiples W n ≤ multiples W m := by
76   obtain ⟨k, rfl⟩ := hmn
77   rintro x ⟨y, rfl⟩
78   refine ⟨k • y, ?_⟩
79   change m • (k • y) = (m * k) • y
80   rw [mul_comm m k, mul_nsmul]
81 
82 /-- The genuine transition between quotient groups. -/
83 def quotientRestriction (W : Submodule ℚ TailSpace) {m n : ℕ} (hmn : m ∣ n) :
84     (preimage W ⧸ multiples W n) →+ (preimage W ⧸ multiples W m) :=
85   QuotientAddGroup.map (multiples W n) (multiples W m) (AddMonoidHom.id (preimage W))
86     (multiples_antitone W hmn)
87 
88 @[simp] theorem quotientRestriction_mk (W : Submodule ℚ TailSpace) {m n : ℕ}
89     (hmn : m ∣ n) (x : preimage W) :
90     quotientRestriction W hmn (QuotientAddGroup.mk x) = QuotientAddGroup.mk x := rfl
91 
92 /-- Coordinate restriction is the actual quotient transition, on every quotient element. -/
93 theorem integerQuotientEquiv_restriction (W : Submodule ℚ TailSpace) {m n : ℕ}
94     (hm : 0 < m) (hn : 0 < n) (hmn : m ∣ n) (x : preimage W ⧸ multiples W n) :
95     integerQuotientEquiv W hm (quotientRestriction W hmn x) =
96       coordinateRestriction hmn (integerQuotientEquiv W hn x) := by
97   induction x using QuotientAddGroup.induction_on with
98   | H x => rfl
99 
100 /-- Cyclic coordinates turn quotient transitions into the ordinary residue reduction. -/
101 theorem divisorCrtEquiv_restriction {m n : ℕ} (hm : 0 < m) (hn : 0 < n)
102     (hmn : m ∣ n) (z : ZMod (primeRadical n)) :
103     coordinateRestriction hmn (divisorCrtEquiv hn z) =
104       divisorCrtEquiv hm (ZMod.castHom (primeRadical_dvd_of_dvd hn hmn)
105         (ZMod (primeRadical m)) z) := by
106   let : NeZero (primeRadical n) := ⟨Nat.ne_of_gt (primeRadical_pos n)⟩
107   have he : (z.val : ZMod (primeRadical n)) = z := ZMod.natCast_zmod_val z
108   rw [← he]
109   simp only [map_natCast]
110   rfl
111 
112 /-- The complete commuting square in cyclic coordinates. -/
113 theorem cyclicIntegerQuotientEquiv_restriction (W : Submodule ℚ TailSpace) {m n : ℕ}
114     (hm : 0 < m) (hn : 0 < n) (hmn : m ∣ n) (x : preimage W ⧸ multiples W n) :
115     cyclicIntegerQuotientEquiv W hm (quotientRestriction W hmn x) =
116       ZMod.castHom (primeRadical_dvd_of_dvd hn hmn) (ZMod (primeRadical m))
117         (cyclicIntegerQuotientEquiv W hn x) := by
118   apply (divisorCrtEquiv hm).injective
119   rw [cyclicIntegerQuotientEquiv_coordinates, ← divisorCrtEquiv_restriction hm hn hmn,
120     cyclicIntegerQuotientEquiv_coordinates]
121   exact integerQuotientEquiv_restriction W hm hn hmn x
122 
123 end RealizationBoundaries

Back to source controls