FoxDifferential/Completed/FiniteStage/Basic.lean
1import FoxDifferential.Completed.CoefficientRings.AugmentationIdealPrimePower.SubtypeLinear
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FoxDifferential/Completed/FiniteStage/Basic.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Finite-stage completed Fox calculus
14Finite quotient stages are used to compare completed Fox boundaries, derivatives, and relation modules with explicit finite group-algebra calculations.
15-/
16namespace FoxDifferential
18noncomputable section
20open ProCGroups.InverseSystems
21open ProCGroups.ProC
23universe u v
25variable (ℓ : ℕ) [Fact (0 < ℓ)]
26variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
27variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
29section ModNStageMapScalar
31variable (n : ℕ) [Fact (0 < n)]
33omit [Fact (0 < n)] in
34/-- The finite-stage completed group-algebra projection preserves coefficient algebra maps. -/
35@[simp]
37 (U : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) (c : ModNCompletedCoeff n) :
39 (algebraMap (ModNCompletedCoeff n) (ModNCompletedGroupRing n G) c) =
40 algebraMap (ModNCompletedCoeff n) (ModNCompletedGroupAlgebraStage n G U) c := by
41 rcases ZMod.intCast_surjective c with ⟨t, rfl⟩
42 simp only [modNCompletedGroupAlgebraStageMap, map_intCast]
44end ModNStageMapScalar
46section FiniteFoxCommutatorPowerQuotient
48variable {F : Type u} [Group F]
50/-- Relators defining the finite Fox source quotient: commutators in `N` and `n`th powers in
51`N`. -/
52def finiteFoxCommutatorPowerRelatorSet (N : Subgroup F) (n : ℕ) : Set F :=
53 {g | (∃ a ∈ N, ∃ b ∈ N, ⁅a, b⁆ = g) ∨ ∃ a ∈ N, a ^ n = g}
55/-- Normal subgroup generated by commutators in `N` and `n`th powers in `N`. -/
56def finiteFoxCommutatorPowerSubgroup (N : Subgroup F) (n : ℕ) : Subgroup F :=
57 Subgroup.normalClosure (finiteFoxCommutatorPowerRelatorSet (F := F) N n)
59/-- The finite Fox commutator-power subgroup is normal by construction. -/
61 (N : Subgroup F) (n : ℕ) :
62 (finiteFoxCommutatorPowerSubgroup (F := F) N n).Normal := by
63 dsimp [finiteFoxCommutatorPowerSubgroup]
64 infer_instance
66/-- The finite Fox commutator-power relator set is contained in `N`. -/
68 (N : Subgroup F) (n : ℕ) :
69 finiteFoxCommutatorPowerRelatorSet (F := F) N n ⊆ N := by
70 intro g hg
71 rcases hg with ⟨a, ha, b, hb, rfl⟩ | ⟨a, ha, rfl⟩
72 · rw [commutatorElement_def]
73 exact N.mul_mem (N.mul_mem (N.mul_mem ha hb) (N.inv_mem ha)) (N.inv_mem hb)
74 · exact N.pow_mem ha n
76/-- The finite Fox commutator-power subgroup is contained in `N` when `N` is normal. -/
78 (N : Subgroup F) [N.Normal] (n : ℕ) :
79 finiteFoxCommutatorPowerSubgroup (F := F) N n ≤ N := by
80 exact Subgroup.normalClosure_le_normal
81 (finiteFoxCommutatorPowerRelatorSet_subset (F := F) N n)
83/-- Natural quotient map `F/[N,N]N^n → F/N`. -/
85 (N : Subgroup F) [N.Normal] (n : ℕ) :
86 F ⧸ finiteFoxCommutatorPowerSubgroup (F := F) N n →* F ⧸ N :=
87 QuotientGroup.map _ _ (MonoidHom.id F)
88 (finiteFoxCommutatorPowerSubgroup_le_normal (F := F) N n)
90/-- Evaluation of the natural quotient map `F/[N,N]N^n → F/N` on a representative. -/
91@[simp]
93 (N : Subgroup F) [N.Normal] (n : ℕ) (g : F) :
94 finiteFoxCommutatorPowerQuotientMapToNormalQuotient (F := F) N n
95 (QuotientGroup.mk'
96 (finiteFoxCommutatorPowerSubgroup (F := F) N n) g) =
97 QuotientGroup.mk' N g := by
98 rfl
100/-- The natural quotient map `F/[N,N]N^n → F/N` is surjective. -/
102 (N : Subgroup F) [N.Normal] (n : ℕ) :
103 Function.Surjective
104 (finiteFoxCommutatorPowerQuotientMapToNormalQuotient (F := F) N n) := by
105 intro y
106 rcases QuotientGroup.mk'_surjective N y with ⟨g, rfl⟩
107 exact ⟨QuotientGroup.mk'
108 (finiteFoxCommutatorPowerSubgroup (F := F) N n) g, rfl⟩
110/-- Group-algebra map induced by the natural quotient `F/[N,N]N^n → F/N`. -/
112 (N : Subgroup F) [N.Normal] (n : ℕ) :
113 MonoidAlgebra (ModNCompletedCoeff n)
114 (F ⧸ finiteFoxCommutatorPowerSubgroup (F := F) N n) →+*
115 MonoidAlgebra (ModNCompletedCoeff n) (F ⧸ N) :=
116 MonoidAlgebra.mapDomainRingHom (ModNCompletedCoeff n)
117 (finiteFoxCommutatorPowerQuotientMapToNormalQuotient (F := F) N n)
119/-- Algebra-hom version of the group-algebra map induced by
120`F/[N,N]N^n → F/N`. -/
122 (N : Subgroup F) [N.Normal] (n : ℕ) :
123 MonoidAlgebra (ModNCompletedCoeff n)
124 (F ⧸ finiteFoxCommutatorPowerSubgroup (F := F) N n) →ₐ[
126 MonoidAlgebra (ModNCompletedCoeff n) (F ⧸ N) :=
127 MonoidAlgebra.mapDomainAlgHom (ModNCompletedCoeff n) (ModNCompletedCoeff n)
128 (finiteFoxCommutatorPowerQuotientMapToNormalQuotient (F := F) N n)
130/-- The algebra-hom and ring-hom versions of the finite Fox quotient map agree on values. -/
131@[simp]
133 (N : Subgroup F) [N.Normal] (n : ℕ)
134 (x : MonoidAlgebra (ModNCompletedCoeff n)
135 (F ⧸ finiteFoxCommutatorPowerSubgroup (F := F) N n)) :
136 finiteFoxCommutatorPowerGroupAlgebraAlgHom (F := F) N n x =
137 finiteFoxCommutatorPowerGroupAlgebraMap (F := F) N n x := rfl
139/-- Augmentation map on the finite Fox source group algebra. -/
141 (N : Subgroup F) (n : ℕ) :
142 MonoidAlgebra (ModNCompletedCoeff n)
143 (F ⧸ finiteFoxCommutatorPowerSubgroup (F := F) N n) →ₐ[
144 ModNCompletedCoeff n] ModNCompletedCoeff n :=
145 MonoidAlgebra.lift (ModNCompletedCoeff n) (ModNCompletedCoeff n)
146 (F ⧸ finiteFoxCommutatorPowerSubgroup (F := F) N n)
147 (1 : (F ⧸ finiteFoxCommutatorPowerSubgroup (F := F) N n) →*
150/-- The source augmentation sends every quotient group basis element to `1`. -/
151@[simp]
153 (N : Subgroup F) (n : ℕ)
154 (q : F ⧸ finiteFoxCommutatorPowerSubgroup (F := F) N n) :
156 (MonoidAlgebra.of (ModNCompletedCoeff n)
157 (F ⧸ finiteFoxCommutatorPowerSubgroup (F := F) N n) q) =
158 1 := by
159 simp only [finiteFoxCommutatorPowerSourceGroupAlgebraAugmentation, MonoidAlgebra.of_apply,
160 MonoidAlgebra.lift_single, MonoidHom.one_apply, smul_eq_mul, mul_one]
162/-- Evaluation of the finite Fox source-to-target group-algebra map on a represented word. -/
163@[simp]
165 (N : Subgroup F) [N.Normal] (n : ℕ) (g : F) :
166 finiteFoxCommutatorPowerGroupAlgebraMap (F := F) N n
167 (MonoidAlgebra.of (ModNCompletedCoeff n)
168 (F ⧸ finiteFoxCommutatorPowerSubgroup (F := F) N n)
169 (QuotientGroup.mk'
170 (finiteFoxCommutatorPowerSubgroup (F := F) N n) g)) =
171 MonoidAlgebra.of (ModNCompletedCoeff n) (F ⧸ N) (QuotientGroup.mk' N g) := by
172 simp only [finiteFoxCommutatorPowerGroupAlgebraMap, MonoidAlgebra.of, MonoidAlgebra.single,
173 QuotientGroup.mk'_apply, MonoidHom.coe_mk, OneHom.coe_mk, MonoidAlgebra.mapDomainRingHom_apply,
174 Finsupp.mapDomain_single]
175 simpa using congrArg
176 (fun q : F ⧸ N => Finsupp.single q (1 : ModNCompletedCoeff n))
177 (finiteFoxCommutatorPowerQuotientMapToNormalQuotient_mk (F := F) N n g)
179/-- Evaluation of the finite Fox source-to-target group-algebra map on a quotient basis
180element. -/
181@[simp]
183 (N : Subgroup F) [N.Normal] (n : ℕ)
184 (q : F ⧸ finiteFoxCommutatorPowerSubgroup (F := F) N n) :
185 finiteFoxCommutatorPowerGroupAlgebraMap (F := F) N n
186 (MonoidAlgebra.of (ModNCompletedCoeff n)
187 (F ⧸ finiteFoxCommutatorPowerSubgroup (F := F) N n) q) =
188 MonoidAlgebra.of (ModNCompletedCoeff n) (F ⧸ N)
189 (finiteFoxCommutatorPowerQuotientMapToNormalQuotient (F := F) N n q) := by
190 rcases QuotientGroup.mk'_surjective
191 (finiteFoxCommutatorPowerSubgroup (F := F) N n) q with ⟨g, rfl⟩
195omit [Fact (0 < ℓ)] in
196/-- Evaluation of the finite Fox source-to-target group-algebra map on a single coefficient
197basis term. -/
198@[simp]
200 (N : Subgroup F) [N.Normal] (n : ℕ)
201 (q : F ⧸ finiteFoxCommutatorPowerSubgroup (F := F) N n)
202 (a : ModNCompletedCoeff n) :
203 finiteFoxCommutatorPowerGroupAlgebraMap (F := F) N n
204 (MonoidAlgebra.single q a) =
205 MonoidAlgebra.single
206 (finiteFoxCommutatorPowerQuotientMapToNormalQuotient (F := F) N n q) a := by
208 exact Finsupp.mapDomain_single
210end FiniteFoxCommutatorPowerQuotient
212end
214end FoxDifferential