Source: ProCGroups.FoxDifferential.Completed.Comparison.QuotientFamily
1import ProCGroups.FoxDifferential.Completed.Comparison.DiscreteCompletion
3/-!
4# Fox differential: completed — comparison — quotient family
6The principal declarations in this module are:
8- `ZCFiniteStageQuotientBundle`
9 A bundled finite-stage quotient family for source-stage comparison theorems. The purpose is to
10 carry the topology and topological-group structure on the quotient target once, instead of
11 repeating these hypotheses at every comparison theorem.
12- `Target`
13 The target quotient carried by a finite-stage quotient bundle.
14- `targetFiniteInstance`
15 The finiteness instance certified by a genuine finite-stage quotient bundle.
16- `targetDiscreteTopology`
17 The genuine finite quotient stage has discrete topology.
18-/
20namespace FoxDifferential
22noncomputable section
24universe u
26section FiniteStageQuotientBundle
28variable {X : Type u} [DecidableEq X]
29variable (N : Subgroup (FreeGroup X)) [N.Normal]
31/--
32A bundled finite-stage quotient family for source-stage comparison theorems. The purpose is to
33carry the topology and topological-group structure on the quotient target once, instead of
34repeating these hypotheses at every comparison theorem.
35-/
36structure ZCFiniteStageQuotientBundle where
37 /-- Finiteness of the algebraic Fox-stage target quotient. -/
38 targetFinite : Finite (foxAlgebraicStageTargetQuotient (X := X) N)
40namespace ZCFiniteStageQuotientBundle
42variable {N}
43variable (C : ProCGroups.FiniteGroupClass.{u})
45/-- The target quotient carried by a finite-stage quotient bundle. -/
46abbrev Target (_B : ZCFiniteStageQuotientBundle N) : Type u :=
47 foxAlgebraicStageTargetQuotient (X := X) N
49omit [DecidableEq X] [N.Normal] in
50/-- The finiteness instance certified by a genuine finite-stage quotient bundle. -/
51theorem targetFiniteInstance (B : ZCFiniteStageQuotientBundle N) :
52 Finite (Target (N := N) B) :=
53 B.targetFinite
55/-- The canonical discrete topology on a genuine finite quotient stage.
57This keeps the historical projection-style name while removing the former arbitrary-topology
58field. -/
59@[reducible]
60def targetTopology (_B : ZCFiniteStageQuotientBundle N) :
61 TopologicalSpace (Target (N := N) _B) :=
62 ⊥
64omit [DecidableEq X] [N.Normal] in
65/-- The genuine finite quotient stage has discrete topology. -/
66theorem targetDiscreteTopology (B : ZCFiniteStageQuotientBundle N) :
67 @DiscreteTopology (Target (N := N) B) B.targetTopology := by
68 change @DiscreteTopology (Target (N := N) B) ⊥
69 exact discreteTopology_bot _
71omit [DecidableEq X] in
72/-- The canonical discrete topology makes the genuine finite quotient stage a topological group.
74This keeps the historical projection-style name while deriving the structure rather than accepting
75it as unrelated input data. -/
76theorem targetIsTopologicalGroup (B : ZCFiniteStageQuotientBundle N) :
77 @IsTopologicalGroup (Target (N := N) B) B.targetTopology inferInstance := by
78 letI : TopologicalSpace (Target (N := N) B) := B.targetTopology
79 letI : DiscreteTopology (Target (N := N) B) := B.targetDiscreteTopology
80 infer_instance
82/-- The canonical quotient morphism represented by a genuine finite-stage bundle. -/
83def quotientMap (_B : ZCFiniteStageQuotientBundle N) :
84 FreeGroup X →* Target (N := N) _B :=
85 QuotientGroup.mk' N
87omit [DecidableEq X] in
88/-- The canonical quotient morphism of a genuine finite-stage bundle is surjective. -/
89theorem quotientMap_surjective (B : ZCFiniteStageQuotientBundle N) :
90 Function.Surjective B.quotientMap :=
91 QuotientGroup.mk'_surjective N
93omit [DecidableEq X] in
94/-- Bundle an already known finite quotient using its canonical discrete topology. -/
95theorem ofFinite
96 (N : Subgroup (FreeGroup X)) [N.Normal]
97 [Finite (foxAlgebraicStageTargetQuotient (X := X) N)] :
98 ZCFiniteStageQuotientBundle N :=
99 ⟨inferInstance⟩
101/-- The completed pro-\(C\) stage indices for the bundled target quotient. -/
102abbrev Index (B : ZCFiniteStageQuotientBundle N) : Type u :=
103 letI : TopologicalSpace (Target (N := N) B) := B.targetTopology
104 ZCCompletedGroupAlgebraIndex C (Target (N := N) B)
106/-- The completed group algebra of the bundled target quotient. -/
107abbrev CompletedGroupAlgebra (B : ZCFiniteStageQuotientBundle N) : Type u :=
108 letI : TopologicalSpace (Target (N := N) B) := B.targetTopology
109 letI : IsTopologicalGroup (Target (N := N) B) := B.targetIsTopologicalGroup
110 ZCCompletedGroupAlgebra C (Target (N := N) B)
112/--
113The scalar stage attached to the quotient bundle is evaluated at the corresponding finite
114quotient and coefficient stage.
115-/
116theorem scalarStage_apply
117 (B : ZCFiniteStageQuotientBundle N)
118 (j : B.Index C) (w : FreeGroup X) :
119 letI : TopologicalSpace (Target (N := N) B) := B.targetTopology
120 letI : IsTopologicalGroup (Target (N := N) B) := B.targetIsTopologicalGroup
121 zcCompletedGroupAlgebraScalarStage C N j w =
122 (letI : Fact (0 < j.1.modulus) := ⟨j.1.positive⟩
123 modNCompletedGroupAlgebraStageMapInClass j.1.modulus
124 (zcFiniteStageTarget X N) C j.2
125 (foxAlgebraicStageCoefficient (X := X) N j.1.modulus w)) := by
126 letI : TopologicalSpace (Target (N := N) B) := B.targetTopology
127 letI : IsTopologicalGroup (Target (N := N) B) := B.targetIsTopologicalGroup
128 exact zcCompletedGroupAlgebraScalarStage_apply (C := C) (X := X) N j w
130/-- Completed derivative projection theorem, using the bundled quotient-family hypotheses. -/
131theorem derivative_finiteStageProjection
132 (B : ZCFiniteStageQuotientBundle N)
133 (j : B.Index C) (i : X) (w : FreeGroup X) :
134 letI : TopologicalSpace (Target (N := N) B) := B.targetTopology
135 letI : IsTopologicalGroup (Target (N := N) B) := B.targetIsTopologicalGroup
136 zcCompletedGroupAlgebraProjection C (zcFiniteStageTarget X N) j
137 (zcFreeGroupFoxDerivative C (QuotientGroup.mk' N) i w) =
138 (letI : Fact (0 < j.1.modulus) := ⟨j.1.positive⟩
139 modNCompletedGroupAlgebraStageMapInClass j.1.modulus
140 (zcFiniteStageTarget X N) C j.2
141 (foxAlgebraicStageDerivative (X := X) N j.1.modulus i w)) := by
142 letI : TopologicalSpace (Target (N := N) B) := B.targetTopology
143 letI : IsTopologicalGroup (Target (N := N) B) := B.targetIsTopologicalGroup
144 exact zcFreeGroupFoxDerivative_finiteStageProjection (C := C) (X := X) N j i w
146/-- Completed derivative-vector projection theorem, using the bundled quotient-family hypotheses. -/
147theorem derivativeVector_finiteStageProjection
148 (B : ZCFiniteStageQuotientBundle N)
149 (j : B.Index C) (w : FreeGroup X) :
150 letI : TopologicalSpace (Target (N := N) B) := B.targetTopology
151 letI : IsTopologicalGroup (Target (N := N) B) := B.targetIsTopologicalGroup
152 (fun i : X =>
153 zcCompletedGroupAlgebraProjection C (zcFiniteStageTarget X N) j
154 (zcFreeGroupFoxDerivativeVector C (QuotientGroup.mk' N) w i)) =
155 fun i : X =>
156 letI : Fact (0 < j.1.modulus) := ⟨j.1.positive⟩
157 modNCompletedGroupAlgebraStageMapInClass j.1.modulus
158 (zcFiniteStageTarget X N) C j.2
159 (foxAlgebraicStageDerivative (X := X) N j.1.modulus i w) := by
160 letI : TopologicalSpace (Target (N := N) B) := B.targetTopology
161 letI : IsTopologicalGroup (Target (N := N) B) := B.targetIsTopologicalGroup
162 exact zcFreeGroupFoxDerivativeVector_finiteStageProjection (C := C) (X := X) N j w
164/--
165Discrete-reduction derivative projection theorem, using the bundled quotient-family hypotheses.
166-/
167theorem derivative_finiteStageProjection_discreteReduction
168 (B : ZCFiniteStageQuotientBundle N)
169 (j : B.Index C) (i : X) (w : FreeGroup X) :
170 letI : TopologicalSpace (Target (N := N) B) := B.targetTopology
171 letI : IsTopologicalGroup (Target (N := N) B) := B.targetIsTopologicalGroup
172 zcCompletedGroupAlgebraProjection C (zcFiniteStageTarget X N) j
173 (zcFreeGroupFoxDerivative C (QuotientGroup.mk' N) i w) =
174 (letI : Fact (0 < j.1.modulus) := ⟨j.1.positive⟩
175 modNCompletedGroupAlgebraStageMapInClass j.1.modulus
176 (zcFiniteStageTarget X N) C j.2
177 (foxAlgebraicStageGroupRingReduction (X := X) N j.1.modulus
178 (FoxCalculus.relativeFreeGroupFoxDerivative
179 (H := zcFiniteStageTarget X N) X (QuotientGroup.mk' N) w i))) := by
180 letI : TopologicalSpace (Target (N := N) B) := B.targetTopology
181 letI : IsTopologicalGroup (Target (N := N) B) := B.targetIsTopologicalGroup
182 exact zcFreeGroupFoxDerivative_finiteStageProjection_discreteReduction
183 (C := C) (X := X) N i w j
185/--
186Discrete-reduction derivative-vector projection theorem, using the bundled quotient-family
187hypotheses.
188-/
189theorem derivativeVector_finiteStageProjection_discreteReduction
190 (B : ZCFiniteStageQuotientBundle N)
191 (j : B.Index C) (w : FreeGroup X) :
192 letI : TopologicalSpace (Target (N := N) B) := B.targetTopology
193 letI : IsTopologicalGroup (Target (N := N) B) := B.targetIsTopologicalGroup
194 (fun i : X =>
195 zcCompletedGroupAlgebraProjection C (zcFiniteStageTarget X N) j
196 (zcFreeGroupFoxDerivativeVector C (QuotientGroup.mk' N) w i)) =
197 fun i : X =>
198 letI : Fact (0 < j.1.modulus) := ⟨j.1.positive⟩
199 modNCompletedGroupAlgebraStageMapInClass j.1.modulus
200 (zcFiniteStageTarget X N) C j.2
201 (foxAlgebraicStageGroupRingReduction (X := X) N j.1.modulus
202 (FoxCalculus.relativeFreeGroupFoxDerivative
203 (H := zcFiniteStageTarget X N) X (QuotientGroup.mk' N) w i)) := by
204 letI : TopologicalSpace (Target (N := N) B) := B.targetTopology
205 letI : IsTopologicalGroup (Target (N := N) B) := B.targetIsTopologicalGroup
206 exact zcFreeGroupFoxDerivativeVector_finiteStageProjection_discreteReduction
207 (C := C) (X := X) N w j
209end ZCFiniteStageQuotientBundle
211end FiniteStageQuotientBundle
213end
215end FoxDifferential