TruncatedGroupAlgebra.lean

1 import PaperXII.ResidualAugmentation
2 import Mathlib.Algebra.CharP.Lemmas
3 import Mathlib.Algebra.CharP.Algebra
4 import Mathlib.Algebra.MvPolynomial.CommRing
5 import Mathlib.RingTheory.MvPolynomial.Basic
6 import Mathlib.RingTheory.MvPolynomial.Ideal
7 import Mathlib.Data.ZMod.Basic
8 import Mathlib.Algebra.BigOperators.Group.Finset.Pi
9 
10 set_option autoImplicit false
11 
12 /-! Paper XII, Theorem 5.2: explicit multivariable residual group-algebra presentation. -/
13 namespace PaperXII.TruncatedGroupAlgebra
14 
15 open scoped BigOperators MonoidAlgebra
16 
17 variable {k ι : Type*} [CommRing k] [Fintype ι] [DecidableEq ι]
18 variable (p : ℕ) [Fact p.Prime] [CharP k p] (n : ι → ℕ)
19 
20 /-- The actual product of cyclic groups in the chosen decomposition. -/
21 abbrev Delta := ∀ i, Multiplicative (ZMod (p ^ n i))
22 
23 /-- The standard generator of the indicated cyclic factor. -/
24 def gamma (i : ι) : Delta p n := Pi.mulSingle i (Multiplicative.ofAdd 1)
25 
26 /-- The ideal of the actual multivariable truncation relations. -/
27 noncomputable def relations : Ideal (MvPolynomial ι k) :=
28   Ideal.span (Set.range fun i => (MvPolynomial.X i : MvPolynomial ι k) ^ (p ^ n i))
29 
30 abbrev Truncated := MvPolynomial ι k ⧸ relations (k := k) p n
31 
32 omit [Fintype ι] [Fact p.Prime] in
33 theorem gamma_pow (i : ι) : gamma p n i ^ (p ^ n i) = 1 := by
34   rw [gamma, ← Pi.mulSingle_pow]
35   have h : Multiplicative.ofAdd (1 : ZMod (p ^ n i)) ^ (p ^ n i) = 1 := by
36     change (p ^ n i) • (1 : ZMod (p ^ n i)) = 0
37     simp [nsmul_eq_mul]
38   rw [h, Pi.mulSingle_one]
39 
40 /-- Polynomial evaluation at the augmentation generators. -/
41 noncomputable def presentation : MvPolynomial ι k →ₐ[k] k[Delta p n] :=
42   MvPolynomial.aeval fun i => MonoidAlgebra.single (gamma p n i) 1 - 1
43 
44 omit [Fintype ι] [Fact p.Prime] [CharP k p] in
45 theorem presentation_X (i : ι) :
46     presentation (k := k) p n (MvPolynomial.X i) =
47       MonoidAlgebra.single (gamma p n i) 1 - 1 := by
48   simp [presentation]
49 
50 omit [Fintype ι] in
51 theorem presentation_relation (i : ι) :
52     presentation (k := k) p n (MvPolynomial.X i ^ (p ^ n i)) = 0 := by
53   let : CharP k[Delta p n] p := charP_of_injective_algebraMap' k p
54   rw [map_pow, presentation_X, sub_pow_char_pow]
55   simp [MonoidAlgebra.single_pow, gamma_pow, ← MonoidAlgebra.one_def]
56 
57 omit [Fintype ι] in
58 theorem relations_le_ker :
59     relations (k := k) p n ≤ RingHom.ker (presentation (k := k) p n).toRingHom := by
60   rw [relations, Ideal.span_le]
61   rintro _ ⟨i, rfl⟩
62   exact presentation_relation p n i
63 
64 /-- The forward map from the actual truncated polynomial quotient. -/
65 noncomputable def forward : Truncated (k := k) p n →ₐ[k] k[Delta p n] :=
66   Ideal.Quotient.liftₐ _ (presentation p n) (fun _ h => relations_le_ker p n h)
67 
68 omit [Fintype ι] in
69 theorem forward_mk (f : MvPolynomial ι k) :
70     forward p n (Ideal.Quotient.mk _ f) = presentation p n f := rfl
71 
72 /-- The image of one plus a polynomial variable. -/
73 noncomputable def onePlusX (i : ι) : Truncated (k := k) p n :=
74   1 + Ideal.Quotient.mk _ (MvPolynomial.X i)
75 
76 omit [Fintype ι] [DecidableEq ι] in
77 theorem onePlusX_pow (i : ι) : onePlusX (k := k) p n i ^ (p ^ n i) = 1 := by
78   rw [onePlusX, ← map_one (Ideal.Quotient.mk (relations (k := k) p n)),
79     ← map_add, ← map_pow, add_pow_char_pow, one_pow, map_add, map_one]
80   have h : (MvPolynomial.X i : MvPolynomial ι k) ^ (p ^ n i) ∈ relations p n :=
81     Ideal.subset_span ⟨i, rfl⟩
82   rw [Ideal.Quotient.eq_zero_iff_mem.mpr h, add_zero]
83 
84 /-- A cyclic factor acts by powers of any element with the required relation. -/
85 noncomputable def cyclicMap {A : Type*} [Monoid A] (N : ℕ) [NeZero N]
86     (b : A) (h : b ^ N = 1) : Multiplicative (ZMod N) →* A where
87   toFun g := b ^ g.toAdd.val
88   map_one' := by simp
89   map_mul' g h' := by
90     change b ^ (g.toAdd + h'.toAdd).val = b ^ g.toAdd.val * b ^ h'.toAdd.val
91     rw [ZMod.val_add, ← pow_eq_pow_mod _ h, pow_add]
92 
93 theorem cyclicMap_generator {A : Type*} [Monoid A] (N : ℕ) [NeZero N]
94     (b : A) (h : b ^ N = 1) : cyclicMap N b h (Multiplicative.ofAdd 1) = b := by
95   change b ^ (1 : ZMod N).val = b
96   rw [ZMod.val_one_eq_one_mod, ← pow_eq_pow_mod _ h, pow_one]
97 
98 /-- The explicit monoid map underlying the inverse presentation. -/
99 noncomputable def groupMap : Delta p n →* Truncated (k := k) p n where
100   toFun g := ∏ i, cyclicMap (p ^ n i) (onePlusX p n i) (onePlusX_pow p n i) (g i)
101   map_one' := by simp
102   map_mul' g h := by simp [Finset.prod_mul_distrib]
103 
104 theorem groupMap_gamma (i : ι) :
105     groupMap (k := k) p n (gamma p n i) = onePlusX p n i := by
106   change (∏ j, cyclicMap (p ^ n j) (onePlusX p n j) (onePlusX_pow p n j)
107     (gamma p n i j)) = _
108   rw [Finset.prod_eq_single i]
109   · rw [gamma, Pi.mulSingle_eq_same, cyclicMap_generator]
110   · intro j _ hj
111     rw [gamma, Pi.mulSingle_eq_of_ne hj, map_one]
112   · simp
113 
114 /-- The inverse sends each group basis element to its explicit product of powers. -/
115 noncomputable def backward : k[Delta p n] →ₐ[k] Truncated (k := k) p n :=
116   MonoidAlgebra.lift k _ _ (groupMap p n)
117 
118 omit [DecidableEq ι] in
119 theorem backward_single (g : Delta p n) (a : k) :
120     backward p n (MonoidAlgebra.single g a) = a • groupMap p n g := by
121   simp [backward]
122 
123 theorem backward_presentation :
124     (backward (k := k) p n).comp (presentation p n) =
125       Ideal.Quotient.mkₐ k (relations p n) := by
126   ext i
127   simp [AlgHom.comp_apply, presentation_X, backward_single, groupMap_gamma, onePlusX]
128 
129 /-- Every group element is the product of the selected generators to its residue exponents. -/
130 theorem group_decomposition (g : Delta p n) :
131     (∏ i, gamma p n i ^ (g i).toAdd.val) = g := by
132   ext j
133   simp only [Finset.prod_apply, Pi.pow_apply]
134   rw [Finset.prod_eq_single j]
135   · simp only [gamma, Pi.mulSingle_eq_same]
136     change Multiplicative.ofAdd ((g j).toAdd.val • (1 : ZMod (p ^ n j))) = g j
137     simp [nsmul_eq_mul]
138   · intro i _ hij
139     rw [gamma, Pi.mulSingle_eq_of_ne (Ne.symm hij), one_pow]
140   · simp
141 
142 omit [Fintype ι] in
143 theorem forward_onePlusX (i : ι) :
144     forward (k := k) p n (onePlusX p n i) = MonoidAlgebra.single (gamma p n i) 1 := by
145   simp [onePlusX, forward_mk, presentation_X]
146 
147 theorem forward_groupMap (g : Delta p n) :
148     forward (k := k) p n (groupMap p n g) = MonoidAlgebra.single g 1 := by
149   change forward p n (∏ i, onePlusX p n i ^ (g i).toAdd.val) = _
150   simp only [map_prod, map_pow, forward_onePlusX, MonoidAlgebra.single_pow, one_pow]
151   rw [MonoidAlgebra.prod_single, group_decomposition]
152   simp
153 
154 theorem forward_backward :
155     (forward (k := k) p n).comp (backward p n) = AlgHom.id k k[Delta p n] := by
156   apply MonoidAlgebra.algHom_ext
157   · intro g
158     simp [AlgHom.comp_apply, backward_single, forward_groupMap]
159   · ext
160 
161 theorem backward_forward :
162     (backward (k := k) p n).comp (forward p n) =
163       AlgHom.id k (Truncated (k := k) p n) := by
164   ext x
165   obtain ⟨f, rfl⟩ := Ideal.Quotient.mk_surjective x
166   exact DFunLike.congr_fun (backward_presentation (k := k) p n) f
167 
168 /-- The full multivariable quotient presentation, with an explicitly proved inverse. -/
169 noncomputable def truncatedPolynomialEquiv :
170     Truncated (k := k) p n ≃ₐ[k] k[Delta p n] :=
171   AlgEquiv.ofAlgHom (forward p n) (backward p n) (forward_backward p n) (backward_forward p n)
172 
173 /-- The presentation sends each actual residue variable to the selected group generator minus one. -/
174 theorem truncatedPolynomialEquiv_X (i : ι) :
175     truncatedPolynomialEquiv (k := k) p n (Ideal.Quotient.mk _ (MvPolynomial.X i)) =
176       MonoidAlgebra.single (gamma p n i) 1 - 1 := by
177   exact presentation_X p n i
178 
179 omit [Fintype ι] [DecidableEq ι] in
180 /-- Zero constant coefficient is equivalent to membership in the variable ideal. -/
181 theorem constantCoeff_ker :
182     RingHom.ker (MvPolynomial.constantCoeff : MvPolynomial ι k →+* k) =
183       Ideal.span (Set.range (MvPolynomial.X : ι → MvPolynomial ι k)) := by
184   classical
185   ext f
186   rw [← Set.image_univ, MvPolynomial.mem_ideal_span_X_image]
187   change f.coeff 0 = 0 ↔ _
188   constructor
189   · intro hf m hm
190     have hm0 : m ≠ 0 := by
191       intro heq
192       subst m
193       exact (MvPolynomial.mem_support_iff.mp hm) hf
194     obtain ⟨i, hi⟩ := Finsupp.ne_iff.mp hm0
195     exact ⟨i, Set.mem_univ _, hi⟩
196   · intro hf
197     by_contra h
198     obtain ⟨i, _, hi⟩ := hf 0 (MvPolynomial.mem_support_iff.mpr h)
199     exact hi rfl
200 
201 omit [Fintype ι] [Fact p.Prime] [CharP k p] in
202 /-- Augmentation after polynomial presentation is the actual constant-coefficient map. -/
203 theorem augmentation_presentation :
204     (AuxiliaryGroupAlgebra.augmentation (R := k) (G := Delta p n)).toRingHom.comp
205       (presentation p n).toRingHom = MvPolynomial.constantCoeff := by
206   apply MvPolynomial.ringHom_ext
207   · intro a
208     simp [presentation, AuxiliaryGroupAlgebra.augmentation_single]
209   · intro i
210     simp [presentation_X, AuxiliaryGroupAlgebra.augmentation_single]
211 
212 /-- The selected augmentation generators generate the whole augmentation ideal. -/
213 theorem augmentationIdeal_eq :
214     AuxiliaryGroupAlgebra.augmentationIdeal (R := k) (G := Delta p n) =
215       Ideal.span (Set.range fun i => (MonoidAlgebra.single (gamma p n i) 1 - 1 : k[Delta p n])) := by
216   have hs : Function.Surjective (presentation (k := k) p n) := by
217     intro x
218     obtain ⟨y, hy⟩ := (truncatedPolynomialEquiv (k := k) p n).surjective x
219     obtain ⟨f, rfl⟩ := Ideal.Quotient.mk_surjective y
220     exact ⟨f, hy⟩
221   have hc : (AuxiliaryGroupAlgebra.augmentationIdeal (R := k) (G := Delta p n)).comap
222       (presentation p n).toRingHom = Ideal.span (Set.range (MvPolynomial.X : ι → MvPolynomial ι k)) := by
223     rw [AuxiliaryGroupAlgebra.augmentationIdeal, RingHom.comap_ker,
224       augmentation_presentation, constantCoeff_ker]
225   rw [← Ideal.map_comap_of_surjective (presentation p n).toRingHom hs
226     (AuxiliaryGroupAlgebra.augmentationIdeal (R := k) (G := Delta p n)), hc,
227     Ideal.map_span, ← Set.range_comp]
228   congr 2
229   funext i
230   exact presentation_X p n i
231 
232 /-- The canonical finite product has the required p-power order. -/
233 theorem delta_isPGroup : IsPGroup p (Delta p n) := by
234   apply IsPGroup.of_card (n := ∑ i, n i)
235   simp [Nat.card_eq_fintype_card, Delta, Fintype.card_pi, ← Finset.prod_pow_eq_pow_sum]
236 
237 variable {G : Type*} [CommGroup G]
238 
239 /-- Transport the explicit presentation along the supplied product decomposition. -/
240 noncomputable def equivalenceOfDecomposition (e : G ≃* Delta p n) :
241     Truncated (k := k) p n ≃ₐ[k] k[G] :=
242   (truncatedPolynomialEquiv p n).trans (MonoidAlgebra.domCongr k k e.symm)
243 
244 /-- The transported variables are precisely the chosen generators minus one. -/
245 theorem equivalenceOfDecomposition_X (e : G ≃* Delta p n) (i : ι) :
246     equivalenceOfDecomposition (k := k) p n e (Ideal.Quotient.mk _ (MvPolynomial.X i)) =
247       MonoidAlgebra.single (e.symm (gamma p n i)) 1 - 1 := by
248   simp [equivalenceOfDecomposition, truncatedPolynomialEquiv_X]
249 
250 omit [Fintype ι] [DecidableEq ι] [Fact p.Prime] [CharP k p] in
251 /-- Augmentation commutes with the chosen decomposition. -/
252 theorem augmentation_decomposition (e : G ≃* Delta p n) :
253     (AuxiliaryGroupAlgebra.augmentation (R := k) (G := G)).toRingHom.comp
254       (MonoidAlgebra.domCongr k k e.symm).toRingHom =
255         (AuxiliaryGroupAlgebra.augmentation (R := k) (G := Delta p n)).toRingHom := by
256   have h := AuxiliaryGroupAlgebra.augmentation_transfer (R := k) e.symm.toMonoidHom
257   exact congrArg AlgHom.toRingHom h
258 
259 /-- The chosen generators span the augmentation kernel after transport. -/
260 theorem augmentationIdeal_eq_of_decomposition (e : G ≃* Delta p n) :
261     AuxiliaryGroupAlgebra.augmentationIdeal (R := k) (G := G) =
262       Ideal.span (Set.range fun i => (MonoidAlgebra.single (e.symm (gamma p n i)) 1 - 1 : k[G])) := by
263   have hc : (AuxiliaryGroupAlgebra.augmentationIdeal (R := k) (G := G)).comap
264       (MonoidAlgebra.domCongr k k e.symm).toRingHom =
265         AuxiliaryGroupAlgebra.augmentationIdeal (R := k) (G := Delta p n) := by
266     rw [AuxiliaryGroupAlgebra.augmentationIdeal, RingHom.comap_ker,
267       augmentation_decomposition]
268   rw [← Ideal.map_comap_of_surjective (MonoidAlgebra.domCongr k k e.symm).toRingHom
269     (MonoidAlgebra.domCongr k k e.symm).surjective
270     (AuxiliaryGroupAlgebra.augmentationIdeal (R := k) (G := G)), hc,
271     augmentationIdeal_eq, Ideal.map_span, ← Set.range_comp]
272   congr 2
273   funext i
274   simp
275 
276 variable {K : Type*} [Field K] [CharP K p]
277 
278 /-- Locality for the actual group algebra with the supplied cyclic decomposition. -/
279 theorem isLocalRing_of_decomposition (e : G ≃* Delta p n) : IsLocalRing K[G] :=
280   ResidualAugmentation.isLocalRing ((delta_isPGroup p n).of_equiv e.symm)
281 
282 /-- Paper XII, Theorem 5.2: the full presentation, chosen-generator identities,
283 augmentation-ideal equality, and locality. No positive-rank or nontrivial-factor hypothesis
284 is needed. The inverse equivalence is proved above rather than supplied as an assumption. -/
285 theorem residual_augmentation_algebra (e : G ≃* Delta p n) :
286     (∃ E : Truncated (k := K) p n ≃ₐ[K] K[G],
287       ∀ i, E (Ideal.Quotient.mk _ (MvPolynomial.X i)) =
288         MonoidAlgebra.single (e.symm (gamma p n i)) 1 - 1) ∧
289     AuxiliaryGroupAlgebra.augmentationIdeal (R := K) (G := G) =
290       Ideal.span (Set.range fun i =>
291         (MonoidAlgebra.single (e.symm (gamma p n i)) 1 - 1 : K[G])) ∧
292     IsLocalRing K[G] := by
293   refine ⟨⟨equivalenceOfDecomposition p n e, equivalenceOfDecomposition_X p n e⟩, ?_,
294     isLocalRing_of_decomposition p n e⟩
295   exact augmentationIdeal_eq_of_decomposition p n e
296 
297 end PaperXII.TruncatedGroupAlgebra

Back to source controls