CrowellExactSequence/Profinite/RelationReflection.lean
1import FoxDifferential.Completed.FreeProC.FiniteQuotientStages
2import FoxDifferential.Completed.Continuous.Universal.NaturalTopology
3import CrowellExactSequence.Profinite.FreeProCSourceData
5/-
6PUBLIC_PAGE_SNAPSHOT
7generated_at: 2026-05-27T09:47:29+09:00
8lean_source: lean4/CrowellExactSequence/Profinite/RelationReflection.lean
9translation_root: data/translation
10purpose: identifies the local data snapshot used to build pages/
11placement: after imports, never before imports
12-/
13/-!
17pro-`C` sources. The root Crowell exactness file should only import this once the reflection
18frontier theorem is proved here.
19-/
21namespace CrowellExactSequence
23noncomputable section
25open scoped Topology
26open ProCGroups.InverseSystems
27open ProCGroups.ProC
28open FoxDifferential
30universe u v
33/-- A pre-stage reduction is a finite relation exactly when its finite universal-module class is
34zero. -/
36 (C : ProCGroups.FiniteGroupClass.{u})
37 {G H : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
38 [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
39 (ψ : G →* H)
40 (i : ZCCompletedDifferentialModuleIndex C ψ)
41 (x : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) :
42 zcCompletedDifferentialModulePreStageMap C ψ i x ∈
44 (zcCompletedDifferentialModuleStageScalar C ψ i) ↔
46 (zcCompletedDifferentialModuleStageScalar C ψ i)).mkQ
47 (zcCompletedDifferentialModulePreStageMap C ψ i x) = 0) := by
48 constructor
49 · intro hx
50 exact
51 (Submodule.Quotient.mk_eq_zero
54 (x := zcCompletedDifferentialModulePreStageMap C ψ i x)).2 hx
55 · intro hx
56 exact
57 (Submodule.Quotient.mk_eq_zero
60 (x := zcCompletedDifferentialModulePreStageMap C ψ i x)).1 hx
63section FreeRelationReflection
65variable {ProC : ProCGroups.ProC.ProCGroupPredicate.{u}}
66variable {H : Type u}
67variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
68variable [T2Space H]
69variable [ProC.HasFiniteQuotientFormation]
70variable [ProC.HasFiniteQuotientFinite]
71variable [ProC.HasFiniteQuotientHereditary]
72variable [ProC.HasFiniteQuotientMelnikovFormation]
73variable [ProC.DeterminedByFiniteQuotients]
75omit [T2Space H] [ProC.HasFiniteQuotientFinite] [ProC.HasFiniteQuotientMelnikovFormation]
76 [ProC.DeterminedByFiniteQuotients] in
77/-- Nonempty finite stage index set for a continuous map out of a free pro-`C` group. -/
79 (sourceData : FreeProCSourceData ProC)
80 (psi : ContinuousMonoidHom sourceData.carrier H) :
81 Nonempty
83 ProC.finiteQuotientClass psi.toMonoidHom) := by
85 (C := ProC.finiteQuotientClass) (G := sourceData.carrier) (H := H)
86 (ProCGroupPredicate.finiteQuotientHereditary ProC) psi
88 (C := ProC.finiteQuotientClass) inferInstance),
89 zcCompletedGroupAlgebraTopIndex ProC.finiteQuotientClass H)⟩
91omit [T2Space H] [ProC.HasFiniteQuotientFinite] [ProC.HasFiniteQuotientMelnikovFormation]
92 [ProC.DeterminedByFiniteQuotients] in
93/-- Directedness of source/target/coefficient finite stages. -/
95 (sourceData : FreeProCSourceData ProC)
96 (psi : ContinuousMonoidHom sourceData.carrier H) :
97 Directed (· ≤ ·)
98 (id :
100 ProC.finiteQuotientClass psi.toMonoidHom →
102 ProC.finiteQuotientClass psi.toMonoidHom) :=
104 (C := ProC.finiteQuotientClass) (G := sourceData.carrier) (H := H)
105 (ProCGroupPredicate.finiteQuotientFormation ProC)
106 (ProCGroupPredicate.finiteQuotientHereditary ProC) psi
108/-- Chosen universe-lifted finite free basis. Use this exact family in reflection proofs. -/
109abbrev freeProCReflectionFamily
110 (sourceData : FreeProCSourceData ProC) {r : Nat}
111 (hbasis : Cardinal.mk sourceData.basis = r) : ULift.{u} (Fin r) → sourceData.carrier :=
112 freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis
114omit [T2Space H] [ProC.HasFiniteQuotientFormation] [ProC.HasFiniteQuotientFinite]
115 [ProC.HasFiniteQuotientHereditary] [ProC.HasFiniteQuotientMelnikovFormation]
116 [ProC.DeterminedByFiniteQuotients] in
117/-- The target images of the chosen basis topologically generate a surjective target. -/
119 (sourceData : FreeProCSourceData ProC) {r : Nat}
120 (hbasis : Cardinal.mk sourceData.basis = r)
121 (psi : ContinuousMonoidHom sourceData.carrier H)
122 (hpsi : Function.Surjective psi) :
124 (G := H)
125 (Set.range (fun i : ULift.{u} (Fin r) =>
126 psi (freeProCReflectionFamily (ProC := ProC) sourceData hbasis i))) := by
127 simpa [freeProCReflectionFamily] using
129 (ProC := ProC) sourceData hbasis psi hpsi
131/-- The free-group map onto the source quotient used by a differential-module finite stage. -/
133 (sourceData : FreeProCSourceData ProC) {r : Nat}
134 (hbasis : Cardinal.mk sourceData.basis = r)
135 (psi : ContinuousMonoidHom sourceData.carrier H)
137 ProC.finiteQuotientClass psi.toMonoidHom) :
138 FreeGroup (ULift.{u} (Fin r)) →*
140 ProC.finiteQuotientClass psi.toMonoidHom i :=
142 ProC.finiteQuotientClass psi.toMonoidHom i).comp
143 (FreeGroup.lift (freeProCReflectionFamily (ProC := ProC) sourceData hbasis))
145/-- The source kernel used by a differential-module stage, pulled back to the abstract free group
146on the chosen basis. -/
148 (sourceData : FreeProCSourceData ProC) {r : Nat}
149 (hbasis : Cardinal.mk sourceData.basis = r)
150 (psi : ContinuousMonoidHom sourceData.carrier H)
152 ProC.finiteQuotientClass psi.toMonoidHom) :
153 Subgroup (FreeGroup (ULift.{u} (Fin r))) :=
154 MonoidHom.ker
155 (freeProCRelationReflectionStageSourceHom (ProC := ProC) sourceData hbasis psi i)
158 (sourceData : FreeProCSourceData ProC) {r : Nat}
159 (hbasis : Cardinal.mk sourceData.basis = r)
160 (psi : ContinuousMonoidHom sourceData.carrier H)
162 ProC.finiteQuotientClass psi.toMonoidHom) :
163 (freeProCRelationReflectionStageKernel (ProC := ProC) sourceData hbasis psi i).Normal := by
165 infer_instance
167omit [IsTopologicalGroup H] [T2Space H] [ProC.HasFiniteQuotientFormation]
168 [ProC.HasFiniteQuotientFinite] [ProC.HasFiniteQuotientHereditary]
169 [ProC.HasFiniteQuotientMelnikovFormation] [ProC.DeterminedByFiniteQuotients] in
170/-- The chosen free basis surjects onto every finite source quotient stage. -/
172 (sourceData : FreeProCSourceData ProC) {r : Nat}
173 (hbasis : Cardinal.mk sourceData.basis = r)
174 (psi : ContinuousMonoidHom sourceData.carrier H)
176 ProC.finiteQuotientClass psi.toMonoidHom) :
177 Function.Surjective
178 (freeProCRelationReflectionStageSourceHom (ProC := ProC) sourceData hbasis psi i) := by
179 classical
180 let X : Type u := ULift.{u} (Fin r)
181 let ι : X → sourceData.carrier := freeProCReflectionFamily (ProC := ProC) sourceData hbasis
182 let Q : Type u :=
184 ProC.finiteQuotientClass psi.toMonoidHom i
185 letI : DiscreteTopology Q :=
186 QuotientGroup.discreteTopology i.source.1.toOpenSubgroup.isOpen'
187 let g : X → Q := fun x =>
189 ProC.finiteQuotientClass psi.toMonoidHom i (ι x)
190 have hsource :
192 (G := sourceData.carrier) (Set.range ι) := by
193 simpa [ι, freeProCReflectionFamily] using
194 freeProCChosenULiftFamilyOfBasisCard_generates (ProC := ProC) sourceData hbasis
195 have hquot_image :
197 (G := Q)
198 ((QuotientGroup.mk' (i.source.1 : Subgroup sourceData.carrier)) '' Set.range ι) := by
199 simpa [Q] using
201 (G := sourceData.carrier) (N := (i.source.1 : Subgroup sourceData.carrier)) hsource
202 have hrange :
203 ((QuotientGroup.mk' (i.source.1 : Subgroup sourceData.carrier)) '' Set.range ι) =
204 Set.range g := by
205 ext y
206 constructor
207 · rintro ⟨x, ⟨a, rfl⟩, rfl⟩
208 exact ⟨a, rfl⟩
209 · rintro ⟨a, rfl⟩
210 exact ⟨ι a, ⟨a, rfl⟩, rfl⟩
211 have hg :
212 ProCGroups.Generation.TopologicallyGenerates (G := Q) (Set.range g) := by
213 rw [← hrange]
214 exact hquot_image
215 have hsurj : Function.Surjective (FreeGroup.lift g) :=
216 ProCGroups.FiniteGeneration.freeGroup_lift_surjective_of_topologicallyGenerates_discrete
217 (G := Q) g hg
218 have hlift :
219 FreeGroup.lift g =
220 freeProCRelationReflectionStageSourceHom (ProC := ProC) sourceData hbasis psi i := by
221 apply FreeGroup.ext_hom
222 intro x
223 rw [FreeGroup.lift_apply_of]
224 change
226 ProC.finiteQuotientClass psi.toMonoidHom i (ι x) =
228 ProC.finiteQuotientClass psi.toMonoidHom i
229 ((FreeGroup.lift (freeProCReflectionFamily (ProC := ProC) sourceData hbasis))
230 (FreeGroup.of x))
231 rw [FreeGroup.lift_apply_of]
232 simpa [hlift] using hsurj
234/-- Identification of the source quotient stage with the corresponding free-group quotient. -/
236 (sourceData : FreeProCSourceData ProC) {r : Nat}
237 (hbasis : Cardinal.mk sourceData.basis = r)
238 (psi : ContinuousMonoidHom sourceData.carrier H)
240 ProC.finiteQuotientClass psi.toMonoidHom) :
242 (X := ULift.{u} (Fin r))
243 (freeProCRelationReflectionStageKernel (ProC := ProC) sourceData hbasis psi i) ≃*
245 ProC.finiteQuotientClass psi.toMonoidHom i :=
246 QuotientGroup.quotientKerEquivOfSurjective
247 (freeProCRelationReflectionStageSourceHom (ProC := ProC) sourceData hbasis psi i)
249 (ProC := ProC) sourceData hbasis psi i)
251omit [IsTopologicalGroup H] [T2Space H] [ProC.HasFiniteQuotientFormation]
252 [ProC.HasFiniteQuotientFinite] [ProC.HasFiniteQuotientHereditary]
253 [ProC.HasFiniteQuotientMelnikovFormation] [ProC.DeterminedByFiniteQuotients] in
254@[simp]
256 (sourceData : FreeProCSourceData ProC) {r : Nat}
257 (hbasis : Cardinal.mk sourceData.basis = r)
258 (psi : ContinuousMonoidHom sourceData.carrier H)
260 ProC.finiteQuotientClass psi.toMonoidHom)
261 (w : FreeGroup (ULift.{u} (Fin r))) :
262 freeProCRelationReflectionStageSourceEquiv (ProC := ProC) sourceData hbasis psi i
263 (QuotientGroup.mk'
264 (freeProCRelationReflectionStageKernel (ProC := ProC) sourceData hbasis psi i) w) =
265 freeProCRelationReflectionStageSourceHom (ProC := ProC) sourceData hbasis psi i w :=
266 rfl
268/-- The target finite Fox relation kernel attached to the target quotient of a
271 (sourceData : FreeProCSourceData ProC) {r : Nat}
272 (hbasis : Cardinal.mk sourceData.basis = r)
273 (psi : ContinuousMonoidHom sourceData.carrier H)
275 ProC.finiteQuotientClass psi.toMonoidHom) :
276 Subgroup (FreeGroup (ULift.{u} (Fin r))) :=
278 (C := ProC.finiteQuotientClass)
279 (fun x : ULift.{u} (Fin r) =>
280 psi (freeProCReflectionFamily (ProC := ProC) sourceData hbasis x))
281 i.target.2
284 (sourceData : FreeProCSourceData ProC) {r : Nat}
285 (hbasis : Cardinal.mk sourceData.basis = r)
286 (psi : ContinuousMonoidHom sourceData.carrier H)
288 ProC.finiteQuotientClass psi.toMonoidHom) :
289 (freeProCRelationReflectionTargetStageKernel (ProC := ProC) sourceData hbasis psi i).Normal :=
290 inferInstance
292omit [T2Space H] [ProC.HasFiniteQuotientFormation] [ProC.HasFiniteQuotientFinite]
293 [ProC.HasFiniteQuotientHereditary] [ProC.HasFiniteQuotientMelnikovFormation]
294 [ProC.DeterminedByFiniteQuotients] in
295/-- Target finite Fox kernels are antitone along differential-module stage refinement. -/
297 (sourceData : FreeProCSourceData ProC) {r : Nat}
298 (hbasis : Cardinal.mk sourceData.basis = r)
299 (psi : ContinuousMonoidHom sourceData.carrier H)
301 ProC.finiteQuotientClass psi.toMonoidHom} (hij : i ≤ j) :
302 freeProCRelationReflectionTargetStageKernel (ProC := ProC) sourceData hbasis psi j ≤
303 freeProCRelationReflectionTargetStageKernel (ProC := ProC) sourceData hbasis psi i := by
305 (C := ProC.finiteQuotientClass)
306 (fun x : ULift.{u} (Fin r) =>
307 psi (freeProCReflectionFamily (ProC := ProC) sourceData hbasis x))
308 hij.2.2
310/-- The canonical target quotient comparison map `H/U_i -> F_X/N_i`. -/
312 (sourceData : FreeProCSourceData ProC) {r : Nat}
313 (hbasis : Cardinal.mk sourceData.basis = r)
314 (psi : ContinuousMonoidHom sourceData.carrier H)
315 (hpsi : Function.Surjective psi)
317 ProC.finiteQuotientClass psi.toMonoidHom) :
318 CompletedGroupAlgebraQuotientInClass H ProC.finiteQuotientClass i.target.2 →*
320 (X := ULift.{u} (Fin r))
321 (freeProCRelationReflectionTargetStageKernel (ProC := ProC) sourceData hbasis psi i) := by
322 let φ : ULift.{u} (Fin r) → H := fun x =>
323 psi (freeProCReflectionFamily (ProC := ProC) sourceData hbasis x)
324 have hφgen :
325 ProCGroups.Generation.TopologicallyGenerates (G := H) (Set.range φ) := by
326 simpa [φ] using
327 freeProCReflectionFamily_target_generates (ProC := ProC) sourceData hbasis psi hpsi
328 letI : DiscreteTopology
329 (CompletedGroupAlgebraQuotientInClass H ProC.finiteQuotientClass i.target.2) :=
330 QuotientGroup.discreteTopology
331 (ProCGroups.openNormalSubgroup_isOpen (G := H)
332 ((OrderDual.ofDual i.target.2).1 : OpenNormalSubgroup H))
334 (C := ProC.finiteQuotientClass) φ i.target.2
336 (C := ProC.finiteQuotientClass) φ i.target.2 hφgen)
338omit [T2Space H] [ProC.HasFiniteQuotientFormation] [ProC.HasFiniteQuotientFinite]
339 [ProC.HasFiniteQuotientHereditary] [ProC.HasFiniteQuotientMelnikovFormation]
340 [ProC.DeterminedByFiniteQuotients] in
341@[simp 900]
343 (sourceData : FreeProCSourceData ProC) {r : Nat}
344 (hbasis : Cardinal.mk sourceData.basis = r)
345 (psi : ContinuousMonoidHom sourceData.carrier H)
346 (hpsi : Function.Surjective psi)
348 ProC.finiteQuotientClass psi.toMonoidHom)
349 (x : ULift.{u} (Fin r)) :
350 freeProCRelationReflectionTargetStageQMap (ProC := ProC) sourceData hbasis psi hpsi i
351 (QuotientGroup.mk
352 (psi (freeProCReflectionFamily (ProC := ProC) sourceData hbasis x))) =
353 QuotientGroup.mk'
354 (freeProCRelationReflectionTargetStageKernel (ProC := ProC) sourceData hbasis psi i)
355 (FreeGroup.of x) := by
356 let φ : ULift.{u} (Fin r) → H := fun x =>
357 psi (freeProCReflectionFamily (ProC := ProC) sourceData hbasis x)
358 change
360 (ProC := ProC) sourceData hbasis psi hpsi i (QuotientGroup.mk (φ x)) =
361 QuotientGroup.mk'
362 (freeProCRelationReflectionTargetStageKernel (ProC := ProC) sourceData hbasis psi i)
363 (FreeGroup.of x)
365 simp only [freeProCFiniteQuotientStageQMap_generator,
366 freeProCRelationReflectionTargetStageKernel, ContinuousMonoidHom.coe_toMonoidHom,
367 QuotientGroup.mk'_apply, φ]
369omit [T2Space H] [ProC.HasFiniteQuotientFormation] [ProC.HasFiniteQuotientFinite]
370 [ProC.HasFiniteQuotientHereditary] [ProC.HasFiniteQuotientMelnikovFormation]
371 [ProC.DeterminedByFiniteQuotients] in
372/-- Target quotient comparison maps commute with differential-module stage refinement. -/
374 (sourceData : FreeProCSourceData ProC) {r : Nat}
375 (hbasis : Cardinal.mk sourceData.basis = r)
376 (psi : ContinuousMonoidHom sourceData.carrier H)
377 (hpsi : Function.Surjective psi)
379 ProC.finiteQuotientClass psi.toMonoidHom} (hij : i ≤ j)
380 (q : CompletedGroupAlgebraQuotientInClass H ProC.finiteQuotientClass j.target.2) :
381 freeProCRelationReflectionTargetStageQMap (ProC := ProC) sourceData hbasis psi hpsi i
382 ((OpenNormalSubgroupInClass.map
383 (C := ProC.finiteQuotientClass) (G := H)
384 (U := OrderDual.ofDual i.target.2)
385 (V := OrderDual.ofDual j.target.2) hij.2.2) q) =
387 (X := ULift.{u} (Fin r))
389 (ProC := ProC) sourceData hbasis psi hij)
391 (ProC := ProC) sourceData hbasis psi hpsi j q) := by
392 let φ : ULift.{u} (Fin r) → H := fun x =>
393 psi (freeProCReflectionFamily (ProC := ProC) sourceData hbasis x)
394 have hφgen :
395 ProCGroups.Generation.TopologicallyGenerates (G := H) (Set.range φ) := by
396 simpa [φ] using
397 freeProCReflectionFamily_target_generates (ProC := ProC) sourceData hbasis psi hpsi
398 letI : DiscreteTopology
399 (CompletedGroupAlgebraQuotientInClass H ProC.finiteQuotientClass i.target.2) :=
400 QuotientGroup.discreteTopology
401 (ProCGroups.openNormalSubgroup_isOpen (G := H)
402 ((OrderDual.ofDual i.target.2).1 : OpenNormalSubgroup H))
403 letI : DiscreteTopology
404 (CompletedGroupAlgebraQuotientInClass H ProC.finiteQuotientClass j.target.2) :=
405 QuotientGroup.discreteTopology
406 (ProCGroups.openNormalSubgroup_isOpen (G := H)
407 ((OrderDual.ofDual j.target.2).1 : OpenNormalSubgroup H))
410 (C := ProC.finiteQuotientClass) φ hij.2.2
412 (C := ProC.finiteQuotientClass) φ i.target.2 hφgen)
414 (C := ProC.finiteQuotientClass) φ j.target.2 hφgen)
415 q
417/-- The target component map used by finite Fox semidirect stages. -/
419 (sourceData : FreeProCSourceData ProC) {r : Nat}
420 (hbasis : Cardinal.mk sourceData.basis = r)
421 (psi : ContinuousMonoidHom sourceData.carrier H)
422 (hpsi : Function.Surjective psi)
424 ProC.finiteQuotientClass psi.toMonoidHom) :
426 (X := ULift.{u} (Fin r))
427 (freeProCRelationReflectionTargetStageKernel (ProC := ProC) sourceData hbasis psi i) :=
429 (ProC := ProC) sourceData hbasis psi hpsi i).comp
431 (C := ProC.finiteQuotientClass) (G := H) i.target.2)
433omit [T2Space H] [ProC.HasFiniteQuotientFormation] [ProC.HasFiniteQuotientFinite]
434 [ProC.HasFiniteQuotientHereditary] [ProC.HasFiniteQuotientMelnikovFormation]
435 [ProC.DeterminedByFiniteQuotients] in
436@[simp 900]
438 (sourceData : FreeProCSourceData ProC) {r : Nat}
439 (hbasis : Cardinal.mk sourceData.basis = r)
440 (psi : ContinuousMonoidHom sourceData.carrier H)
441 (hpsi : Function.Surjective psi)
443 ProC.finiteQuotientClass psi.toMonoidHom)
444 (x : ULift.{u} (Fin r)) :
445 freeProCRelationReflectionTargetStageRight (ProC := ProC) sourceData hbasis psi hpsi i
446 (psi (freeProCReflectionFamily (ProC := ProC) sourceData hbasis x)) =
447 QuotientGroup.mk'
448 (freeProCRelationReflectionTargetStageKernel (ProC := ProC) sourceData hbasis psi i)
449 (FreeGroup.of x) := by
450 change
452 (ProC := ProC) sourceData hbasis psi hpsi i
453 (QuotientGroup.mk
454 (psi (freeProCReflectionFamily (ProC := ProC) sourceData hbasis x))) =
455 QuotientGroup.mk'
456 (freeProCRelationReflectionTargetStageKernel (ProC := ProC) sourceData hbasis psi i)
457 (FreeGroup.of x)
459 (ProC := ProC) sourceData hbasis psi hpsi i x
461/-- The finite Fox semidirect projection attached to one target quotient stage. -/
463 (sourceData : FreeProCSourceData ProC) {r : Nat}
464 (hbasis : Cardinal.mk sourceData.basis = r)
465 (psi : ContinuousMonoidHom sourceData.carrier H)
466 (hpsi : Function.Surjective psi)
468 ProC.finiteQuotientClass psi.toMonoidHom) :
469 ZCCompletedFoxSemidirect ProC.finiteQuotientClass (ULift.{u} (Fin r)) H →*
471 (X := ULift.{u} (Fin r))
472 (freeProCRelationReflectionTargetStageKernel (ProC := ProC) sourceData hbasis psi i)
473 i.target.1.modulus := by
474 letI : ∀ j : ZCCompletedDifferentialModuleIndex
475 ProC.finiteQuotientClass psi.toMonoidHom,
476 Fact (0 < j.target.1.modulus) :=
477 fun j => ProCGroups.Completion.ProCIntegerIndex.positiveFact j.target.1
478 exact
480 (ProC := ProC) (X := ULift.{u} (Fin r)) (H := H)
481 (Nstage := fun j =>
482 freeProCRelationReflectionTargetStageKernel (ProC := ProC) sourceData hbasis psi j)
483 (nstage := fun j => j.target.1.modulus)
484 (zcIndex := fun j => j.target)
485 (hmod := fun _ => dvd_rfl)
486 (qmap := fun j =>
488 (ProC := ProC) sourceData hbasis psi hpsi j)
489 i
491omit [T2Space H] [ProC.HasFiniteQuotientFormation] [ProC.HasFiniteQuotientFinite]
492 [ProC.HasFiniteQuotientHereditary] [ProC.HasFiniteQuotientMelnikovFormation]
493 [ProC.DeterminedByFiniteQuotients] in
494/-- Each target finite stage attached to the chosen free pro-`C` basis satisfies the finite Fox
495relation-boundary module exactness needed by the approximation theorem. -/
497 (sourceData : FreeProCSourceData ProC) {r : Nat}
498 (hbasis : Cardinal.mk sourceData.basis = r)
499 (psi : ContinuousMonoidHom sourceData.carrier H)
501 ProC.finiteQuotientClass psi.toMonoidHom) :
503 (X := ULift.{u} (Fin r))
504 (freeProCRelationReflectionTargetStageKernel (ProC := ProC) sourceData hbasis psi i)
505 i.target.1.modulus := by
506 exact
508 (X := ULift.{u} (Fin r))
509 (freeProCRelationReflectionTargetStageKernel (ProC := ProC) sourceData hbasis psi i)
510 i.target.1.modulus
512 (X := ULift.{u} (Fin r))
513 (freeProCRelationReflectionTargetStageKernel (ProC := ProC) sourceData hbasis psi i)
514 i.target.1.modulus)
516end FreeRelationReflection
518end
520end CrowellExactSequence