Yamaguchi Lean 4 Library
FoxDifferential/Completed/CoefficientRings/CompletedGroupAlgebraPrimePower/InClass/Map.lean
FoxDifferential/Completed/CoefficientRings/CompletedGroupAlgebraPrimePower/InClass/Map/Source

FoxDifferential/Completed/CoefficientRings/CompletedGroupAlgebraPrimePower/InClass/Map.lean

1import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.InClass.System.Ring.Projection
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FoxDifferential/Completed/CoefficientRings/CompletedGroupAlgebraPrimePower/InClass/Map.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Completed coefficient algebras
14Coefficient algebras, residue stages, and completed group-algebra maps are kept as the scalar layer for completed Fox calculus.
15-/
16namespace FoxDifferential
18noncomputable section
20open ProCGroups.InverseSystems
21open ProCGroups.ProC
23universe u
25variable (ℓ : ℕ)
26variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
28section MapStageInClass
30variable {G0 H0 : Type u}
31variable [Group G0] [TopologicalSpace G0] [IsTopologicalGroup G0]
32variable [Group H0] [TopologicalSpace H0] [IsTopologicalGroup H0]
34/-- The finite-stage component of a class-restricted prime-power completed group-algebra map. -/
36 (C : ProCGroups.FiniteGroupClass.{u}) (hC : ProCGroups.FiniteGroupClass.Hereditary C)
37 (ψ : ContinuousMonoidHom G0 H0) (i : PrimePowerCompletedGroupAlgebraIndexInClass H0 C) :
39 (i.1, completedGroupAlgebraComapIndexInClass (G := G0) (H := H0) C hC ψ i.2) →+*
41 MonoidAlgebra.mapDomainRingHom (ModNCompletedCoeff (ℓ ^ i.1))
42 (completedGroupAlgebraComapQuotientMapInClass (G := G0) (H := H0) C hC ψ i.2)
44/-- Evaluation formula for primePowerCompletedGroupAlgebraMapStageInClass_of. -/
45@[simp]
47 (C : ProCGroups.FiniteGroupClass.{u}) (hC : ProCGroups.FiniteGroupClass.Hereditary C)
48 (ψ : ContinuousMonoidHom G0 H0) (i : PrimePowerCompletedGroupAlgebraIndexInClass H0 C)
49 (q : CompletedGroupAlgebraQuotientInClass G0 C
50 (completedGroupAlgebraComapIndexInClass (G := G0) (H := H0) C hC ψ i.2)) :
52 (MonoidAlgebra.of (ModNCompletedCoeff (ℓ ^ i.1)) _ q) =
53 MonoidAlgebra.of (ModNCompletedCoeff (ℓ ^ i.1)) _
54 (completedGroupAlgebraComapQuotientMapInClass (G := G0) (H := H0) C hC ψ i.2 q) := by
55 simp only [primePowerCompletedGroupAlgebraMapStageInClass, MonoidAlgebra.of, MonoidAlgebra.single,
56 MonoidHom.coe_mk, OneHom.coe_mk, MonoidAlgebra.mapDomainRingHom_apply, Finsupp.mapDomain_single]
58/-- 素冪係数で定めた 有限群クラスを固定した 標準写像が群環の単項基底元を有限商段階の対応する単項基底元へ送ることを述べる。 -/
60 (C : ProCGroups.FiniteGroupClass.{u}) (hC : ProCGroups.FiniteGroupClass.Hereditary C)
61 (ψ : ContinuousMonoidHom G0 H0) (i : PrimePowerCompletedGroupAlgebraIndexInClass H0 C)
62 (q : CompletedGroupAlgebraQuotientInClass G0 C
63 (completedGroupAlgebraComapIndexInClass (G := G0) (H := H0) C hC ψ i.2))
64 (a : ModNCompletedCoeff (ℓ ^ i.1)) :
66 (MonoidAlgebra.single q a) =
67 MonoidAlgebra.single
68 (completedGroupAlgebraComapQuotientMapInClass (G := G0) (H := H0) C hC ψ i.2 q) a := by
69 simp only [primePowerCompletedGroupAlgebraMapStageInClass, MonoidAlgebra.single,
70 MonoidAlgebra.mapDomainRingHom_apply, Finsupp.mapDomain_single]
72/-- Surjectivity of finite-stage class-restricted completed maps follows from surjectivity of the
73underlying continuous homomorphism. -/
75 (C : ProCGroups.FiniteGroupClass.{u}) (hC : ProCGroups.FiniteGroupClass.Hereditary C)
76 (ψ : ContinuousMonoidHom G0 H0) (hψ : Function.Surjective ψ)
78 Function.Surjective
79 (primePowerCompletedGroupAlgebraMapStageInClass (ℓ := ℓ) C hC ψ i) := by
80 intro x
81 induction x using Finsupp.induction with
82 | zero =>
83 exact ⟨0, by simp only [primePowerCompletedGroupAlgebraMapStageInClass, MonoidAlgebra.mapDomainRingHom_apply,
84 Finsupp.mapDomain_zero]⟩
85 | single_add q a x _ _ ih =>
86 rcases completedGroupAlgebraComapQuotientMapInClass_surjective_of_surjective
87 (G := G0) (H := H0) C hC ψ hψ i.2 q with
88 ⟨q', hq'⟩
89 rcases ih with ⟨y, hy⟩
90 refine ⟨(MonoidAlgebra.single q' a :
92 (i.1, completedGroupAlgebraComapIndexInClass (G := G0) (H := H0) C hC ψ i.2)) +
93 y, ?_⟩
96/-- Class-restricted finite-stage maps commute with the prime-power transition maps. -/
98 (C : ProCGroups.FiniteGroupClass.{u}) (hC : ProCGroups.FiniteGroupClass.Hereditary C)
99 (ψ : ContinuousMonoidHom G0 H0)
100 {i j : PrimePowerCompletedGroupAlgebraIndexInClass H0 C} (hij : i ≤ j) :
101 (primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := H0) C hij).comp
105 (show
106 (i.1, completedGroupAlgebraComapIndexInClass (G := G0) (H := H0) C hC ψ i.2) ≤
107 (j.1, completedGroupAlgebraComapIndexInClass (G := G0) (H := H0) C hC ψ j.2) from
108 ⟨hij.1,
109 completedGroupAlgebraComapIndexInClass_mono
110 (G := G0) (H := H0) C hC ψ hij.2⟩)) := by
111 apply RingHom.ext
112 intro x
113 refine MonoidAlgebra.induction_on
114 (p := fun x =>
115 ((primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := H0) C hij).comp
119 (show
120 (i.1, completedGroupAlgebraComapIndexInClass (G := G0) (H := H0) C hC ψ i.2) ≤
121 (j.1,
122 completedGroupAlgebraComapIndexInClass (G := G0) (H := H0) C hC ψ j.2) from
123 ⟨hij.1,
124 completedGroupAlgebraComapIndexInClass_mono
125 (G := G0) (H := H0) C hC ψ hij.2⟩))) x)
126 x ?_ ?_ ?_
127 · intro q
128 rw [RingHom.comp_apply, RingHom.comp_apply,
132 change
133 MonoidAlgebra.of (ModNCompletedCoeff (ℓ ^ i.1))
134 (CompletedGroupAlgebraQuotientInClass H0 C i.2)
135 ((OpenNormalSubgroupInClass.map
136 (C := C) (G := H0)
137 (U := OrderDual.ofDual i.2) (V := OrderDual.ofDual j.2) hij.2)
138 (completedGroupAlgebraComapQuotientMapInClass
139 (G := G0) (H := H0) C hC ψ j.2 q)) =
141 (MonoidAlgebra.of (ModNCompletedCoeff (ℓ ^ i.1))
142 (CompletedGroupAlgebraQuotientInClass G0 C
143 (completedGroupAlgebraComapIndexInClass (G := G0) (H := H0) C hC ψ i.2))
144 ((OpenNormalSubgroupInClass.map
145 (C := C) (G := G0)
146 (U := OrderDual.ofDual
147 (completedGroupAlgebraComapIndexInClass (G := G0) (H := H0) C hC ψ i.2))
148 (V := OrderDual.ofDual
149 (completedGroupAlgebraComapIndexInClass (G := G0) (H := H0) C hC ψ j.2))
150 (completedGroupAlgebraComapIndexInClass_mono
151 (G := G0) (H := H0) C hC ψ hij.2)) q))
153 exact congrArg (MonoidAlgebra.of (ModNCompletedCoeff (ℓ ^ i.1))
154 (CompletedGroupAlgebraQuotientInClass H0 C i.2))
155 (congrFun
156 (congrArg DFunLike.coe
157 (completedGroupAlgebraComapQuotientMapInClass_compatible
158 (G := G0) (H := H0) C hC ψ hij.2)) q)
159 · intro x y hx hy
160 rw [map_add, map_add, hx, hy]
161 · intro a x hx
162 rcases ZMod.intCast_surjective a with ⟨t, rfl⟩
163 rw [Algebra.smul_def, RingHom.map_mul, RingHom.map_mul, hx]
166 map_intCast, RingHom.coe_comp, RingHom.coe_coe, Function.comp_apply, MonoidAlgebra.mapDomainRingHom_apply]
168/-- The class-restricted prime-power completed group-algebra map induced by a continuous
169homomorphism, as an additive map on the inverse-limit subtype. -/
171 (C : ProCGroups.FiniteGroupClass.{u}) (hC : ProCGroups.FiniteGroupClass.Hereditary C)
172 (ψ : ContinuousMonoidHom G0 H0) :
175 toFun x := ⟨fun i =>
178 (ℓ := ℓ) (G := G0) C
179 (i.1, completedGroupAlgebraComapIndexInClass (G := G0) (H := H0) C hC ψ i.2) x), by
180 intro i j hij
181 let hsource :
182 (i.1, completedGroupAlgebraComapIndexInClass (G := G0) (H := H0) C hC ψ i.2) ≤
183 (j.1, completedGroupAlgebraComapIndexInClass (G := G0) (H := H0) C hC ψ j.2) :=
184 ⟨hij.1,
185 completedGroupAlgebraComapIndexInClass_mono (G := G0) (H := H0) C hC ψ hij.2⟩
186 have hx := x.2
187 (i.1, completedGroupAlgebraComapIndexInClass (G := G0) (H := H0) C hC ψ i.2)
188 (j.1, completedGroupAlgebraComapIndexInClass (G := G0) (H := H0) C hC ψ j.2)
189 hsource
190 change
191 primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G0) C hsource
193 (ℓ := ℓ) (G := G0) C
194 (j.1, completedGroupAlgebraComapIndexInClass (G := G0) (H := H0) C hC ψ j.2) x) =
196 (ℓ := ℓ) (G := G0) C
197 (i.1, completedGroupAlgebraComapIndexInClass (G := G0) (H := H0) C hC ψ i.2) x at hx
198 have hcompat := congrFun
199 (congrArg DFunLike.coe
201 (ℓ := ℓ) C hC ψ hij))
203 (ℓ := ℓ) (G := G0) C
204 (j.1, completedGroupAlgebraComapIndexInClass (G := G0) (H := H0) C hC ψ j.2) x)
205 rw [RingHom.comp_apply, RingHom.comp_apply] at hcompat
206 rw [hx] at hcompat
207 change
211 (ℓ := ℓ) (G := G0) C
212 (j.1, completedGroupAlgebraComapIndexInClass
213 (G := G0) (H := H0) C hC ψ j.2) x)) =
216 (ℓ := ℓ) (G := G0) C
217 (i.1, completedGroupAlgebraComapIndexInClass
218 (G := G0) (H := H0) C hC ψ i.2) x)
219 simpa using hcompat⟩
220 map_zero' := by
221 apply Subtype.ext
222 funext i
224 primePowerCompletedGroupAlgebraProjectionInClass_zero, MonoidAlgebra.mapDomainRingHom_apply, Finsupp.mapDomain_zero,
226 map_add' := by
227 intro x y
228 apply Subtype.ext
229 funext i
233/-- 素冪係数で定めた 有限群クラスを固定した 有限段階射影が関手的写像が有限段階射影と両立することを述べる。 -/
234@[simp]
236 (C : ProCGroups.FiniteGroupClass.{u}) (hC : ProCGroups.FiniteGroupClass.Hereditary C)
237 (ψ : ContinuousMonoidHom G0 H0) (i : PrimePowerCompletedGroupAlgebraIndexInClass H0 C)
243 (ℓ := ℓ) (G := G0) C
244 (i.1, completedGroupAlgebraComapIndexInClass (G := G0) (H := H0) C hC ψ i.2) x) := rfl
246end MapStageInClass
247end
249end FoxDifferential