Source: ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.InClass.Augmentation
1import ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.InClass.StageCoeffMap
3/-!
4# Fox differential: coefficient rings — mod-\(n\) completed group algebra — in class — augmentation
6The principal declarations in this module are:
8- `modNCompletedGroupAlgebraStageAugmentationInClass`
9 The augmentation on one class-restricted residue-coefficient finite stage.
10- `modNCompletedGroupAlgebraStageAugmentationInClass_of`
11 The class-indexed finite-stage \(n\)-modular augmentation sends every group-like basis element to
12 \(1\).
13- `modNCompletedGroupAlgebraStageAugmentationInClass_single`
14 The class-indexed finite-stage \(n\)-modular augmentation sends a singleton basis element to its
15 coefficient.
16- `modNCompletedGroupAlgebraStageAugmentationInClass_compatible`
17 Class-indexed finite-stage \(n\)-modular augmentations are compatible with group-quotient
18 transition maps.
19-/
21namespace FoxDifferential
23noncomputable section
25open ProCGroups.InverseSystems
26open ProCGroups.ProC
28universe u
30variable (n : ℕ) [Fact (0 < n)]
31variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
33/-- The augmentation on one class-restricted residue-coefficient finite stage. -/
34def modNCompletedGroupAlgebraStageAugmentationInClass
35 (C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C) :
36 ModNCompletedGroupAlgebraStageInClass n G C U →+* ModNCompletedCoeff n :=
37 MonoidAlgebra.lift (ModNCompletedCoeff n) (ModNCompletedCoeff n)
38 (CompletedGroupAlgebraQuotientInClass G C U)
39 (1 : CompletedGroupAlgebraQuotientInClass G C U →* ModNCompletedCoeff n)
41omit [Fact (0 < n)] in
42/--
43The class-indexed finite-stage \(n\)-modular augmentation sends every group-like basis element
44to \(1\).
45-/
46@[simp]
47theorem modNCompletedGroupAlgebraStageAugmentationInClass_of
48 (C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C)
49 (q : CompletedGroupAlgebraQuotientInClass G C U) :
50 modNCompletedGroupAlgebraStageAugmentationInClass n G C U
51 (MonoidAlgebra.of (ModNCompletedCoeff n) _ q) = 1 := by
52 change
53 MonoidAlgebra.lift (ModNCompletedCoeff n) (ModNCompletedCoeff n)
54 (CompletedGroupAlgebraQuotientInClass G C U)
55 (1 : CompletedGroupAlgebraQuotientInClass G C U →*
56 ModNCompletedCoeff n)
57 (MonoidAlgebra.single q 1) = 1
58 rw [MonoidAlgebra.lift_single, MonoidHom.one_apply, one_smul]
60omit [Fact (0 < n)] in
61/--
62The class-indexed finite-stage \(n\)-modular augmentation sends a singleton basis element to its
63coefficient.
64-/
65@[simp]
66theorem modNCompletedGroupAlgebraStageAugmentationInClass_single
67 (C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C)
68 (q : CompletedGroupAlgebraQuotientInClass G C U) (a : ModNCompletedCoeff n) :
69 modNCompletedGroupAlgebraStageAugmentationInClass n G C U
70 (MonoidAlgebra.single q a) = a := by
71 change
72 MonoidAlgebra.lift (ModNCompletedCoeff n) (ModNCompletedCoeff n)
73 (CompletedGroupAlgebraQuotientInClass G C U)
74 (1 : CompletedGroupAlgebraQuotientInClass G C U →*
75 ModNCompletedCoeff n)
76 (MonoidAlgebra.single q a) = a
77 rw [MonoidAlgebra.lift_single, MonoidHom.one_apply, smul_eq_mul, mul_one]
79omit [Fact (0 < n)] in
80/--
81Class-indexed finite-stage \(n\)-modular augmentations are compatible with group-quotient
82transition maps.
83-/
84@[simp 900]
85theorem modNCompletedGroupAlgebraStageAugmentationInClass_compatible
86 (C : ProCGroups.FiniteGroupClass.{u})
87 {U V : CompletedGroupAlgebraIndexInClass G C} (hUV : U ≤ V) :
88 (modNCompletedGroupAlgebraStageAugmentationInClass n G C U).comp
89 (modNCompletedGroupAlgebraTransitionInClass n G C hUV) =
90 modNCompletedGroupAlgebraStageAugmentationInClass n G C V := by
91 apply RingHom.ext
92 intro x
93 induction x using MonoidAlgebra.induction_linear with
94 | zero =>
95 simp only [map_zero]
96 | add x y hx hy =>
97 simp only [map_add, hx, hy]
98 | single q a =>
99 rw [RingHom.comp_apply]
100 change
101 MonoidAlgebra.lift (ModNCompletedCoeff n) (ModNCompletedCoeff n)
102 (CompletedGroupAlgebraQuotientInClass G C U)
103 (1 : CompletedGroupAlgebraQuotientInClass G C U →*
104 ModNCompletedCoeff n)
105 (MonoidAlgebra.mapDomain
106 (OpenNormalSubgroupInClass.map
107 (C := C) (G := G)
108 (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV)
109 (MonoidAlgebra.single q a)) =
110 MonoidAlgebra.lift (ModNCompletedCoeff n) (ModNCompletedCoeff n)
111 (CompletedGroupAlgebraQuotientInClass G C V)
112 (1 : CompletedGroupAlgebraQuotientInClass G C V →*
113 ModNCompletedCoeff n)
114 (MonoidAlgebra.single q a)
115 rw [MonoidAlgebra.mapDomain_single, MonoidAlgebra.lift_single,
116 MonoidAlgebra.lift_single, MonoidHom.one_apply, smul_eq_mul, mul_one]
117 simp
119omit [Fact (0 < n)] in
120/--
121Composing the class-indexed finite-stage \(n\)-modular augmentation with the dense stage map
122gives the ordinary \(n\)-modular group-algebra augmentation.
123-/
124@[simp 900]
125theorem modNCompletedGroupAlgebraStageAugmentationInClass_comp_stageMap
126 (C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C) :
127 (modNCompletedGroupAlgebraStageAugmentationInClass n G C U).comp
128 (modNCompletedGroupAlgebraStageMapInClass n G C U) =
129 MonoidAlgebra.lift (ModNCompletedCoeff n) (ModNCompletedCoeff n) G
130 (1 : G →* ModNCompletedCoeff n) := by
131 apply RingHom.ext
132 intro x
133 induction x using MonoidAlgebra.induction_linear with
134 | zero =>
135 simp only [map_zero]
136 | add x y hx hy =>
137 simp only [map_add, hx, hy]
138 | single g a =>
139 rw [RingHom.comp_apply]
140 change
141 modNCompletedGroupAlgebraStageAugmentationInClass n G C U
142 (MonoidAlgebra.mapDomain
143 (openNormalSubgroupInClassProj (C := C) (G := G) U)
144 (MonoidAlgebra.single g a)) =
145 MonoidAlgebra.lift (ModNCompletedCoeff n) (ModNCompletedCoeff n) G
146 (1 : G →* ModNCompletedCoeff n) (MonoidAlgebra.single g a)
147 rw [MonoidAlgebra.mapDomain_single,
148 modNCompletedGroupAlgebraStageAugmentationInClass_single,
149 MonoidAlgebra.lift_single, MonoidHom.one_apply, smul_eq_mul, mul_one]
151omit [Fact (0 < n)] in
152/--
153Stage augmentations commute with coefficient reduction on class-restricted finite quotient
154stages.
155-/
156@[simp 900]
157theorem modNCompletedGroupAlgebraStageAugmentationInClass_comp_stageCoeffMap
158 (C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C)
159 {m : ℕ} (hnm : n ∣ m) :
160 (modNCompletedGroupAlgebraStageAugmentationInClass n G C U).comp
161 (modNCompletedGroupAlgebraStageCoeffMapInClass
162 (n := n) (m := m) (G := G) C U hnm) =
163 (modNCompletedCoeffMap (n := n) (m := m) hnm).comp
164 (modNCompletedGroupAlgebraStageAugmentationInClass m G C U) := by
165 apply RingHom.ext
166 intro x
167 induction x using MonoidAlgebra.induction_linear with
168 | zero =>
169 simp only [map_zero]
170 | add x y hx hy =>
171 simp only [map_add, hx, hy]
172 | single q a =>
173 rw [RingHom.comp_apply, RingHom.comp_apply,
174 modNCompletedGroupAlgebraStageCoeffMapInClass_single_apply,
175 modNCompletedGroupAlgebraStageAugmentationInClass_single,
176 modNCompletedGroupAlgebraStageAugmentationInClass_single]
178end
180end FoxDifferential