Source: ProCGroups.FoxDifferential.Completed.Comparison.SourceProjection
1import ProCGroups.FoxDifferential.Completed.Continuous.Naturality
2import ProCGroups.FoxDifferential.Completed.Comparison.QuotientFamily
4/-!
5# Fox differential: completed — comparison — source projection
7The principal declarations in this module are:
9- `freeProCZCCompletedFoxBoundary_finiteStageProjection`
10 Finite-stage projection of the source-shaped completed Fox boundary map.
11- `freeProCZCCompletedFoxBoundary_finiteStageProjection_stage`
12 Finite-stage projection of the source-shaped completed Fox boundary map, with generator boundaries
13 written in the selected finite pro-`C` quotient.
14- `zcFreeFoxCoordinatesMap_finiteStageProjection`
15 Componentwise finite-stage projection formula for target maps on completed Fox coordinates.
16- `freeProCZCCompletedFoxBoundary_mapTarget_finiteStageProjection_stage`
17 Finite-stage projection of target naturality for source-shaped completed Fox boundary maps.
18-/
20namespace FoxDifferential
22noncomputable section
24open scoped BigOperators
26universe u
28section SourceBoundaryProjection
30variable (C : ProCGroups.FiniteGroupClass.{u})
31variable {X H : Type u} [Fintype X]
32variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
34/-- Finite-stage projection of the source-shaped completed Fox boundary map. -/
35theorem freeProCZCCompletedFoxBoundary_finiteStageProjection
36 (φ : X → H) (v : ZCFreeFoxCoordinates C (X := X) (H := H))
37 (j : ZCCompletedGroupAlgebraIndex C H) :
38 zcCompletedGroupAlgebraProjection C H j
39 (freeProCZCCompletedFoxBoundary C φ v) =
40 ∑ x : X,
41 zcCompletedGroupAlgebraProjection C H j (v x) *
42 zcCompletedGroupAlgebraProjection C H j (zcGroupLike C H (φ x) - 1) := by
43 rw [freeProCZCCompletedFoxBoundary_apply, zcCompletedGroupAlgebraProjection_sum]
44 apply Finset.sum_congr rfl
45 intro x _
46 simp only [zcCompletedGroupAlgebraProjection, zcCompletedGroupAlgebraProjection_mul,
47 zcCompletedGroupAlgebraProjection_sub, zcCompletedGroupAlgebraProjection_groupLike,
48 MonoidAlgebra.of_apply,
49 zcCompletedGroupAlgebraProjection_one]
51/-- Finite-stage projection of the source-shaped completed Fox boundary map, with generator
52boundaries written in the selected finite pro-`C` quotient. -/
53theorem freeProCZCCompletedFoxBoundary_finiteStageProjection_stage
54 (φ : X → H) (v : ZCFreeFoxCoordinates C (X := X) (H := H))
55 (j : ZCCompletedGroupAlgebraIndex C H) :
56 zcCompletedGroupAlgebraProjection C H j
57 (freeProCZCCompletedFoxBoundary C φ v) =
58 ∑ x : X,
59 zcCompletedGroupAlgebraProjection C H j (v x) *
60 (MonoidAlgebra.of (ModNCompletedCoeff j.1.modulus)
61 (CompletedGroupAlgebraQuotientInClass H C j.2)
62 (QuotientGroup.mk (φ x)) - 1) := by
63 simpa [zcCompletedGroupAlgebraProjection] using
64 freeProCZCCompletedFoxBoundary_finiteStageProjection
65 (C := C) (X := X) (H := H) φ v j
67end SourceBoundaryProjection
69section TargetProjectionNaturality
71variable (C : ProCGroups.FiniteGroupClass.{u})
72variable (hC : ProCGroups.FiniteGroupClass.Hereditary C)
73variable {X H K : Type u} [Fintype X]
74variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
75variable [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
77omit [Fintype X] in
78/-- Componentwise finite-stage projection formula for target maps on completed Fox coordinates. -/
79theorem zcFreeFoxCoordinatesMap_finiteStageProjection
80 (η : H →ₜ* K)
81 (v : ZCFreeFoxCoordinates C (X := X) (H := H))
82 (j : ZCCompletedGroupAlgebraIndex C K) (x : X) :
83 zcCompletedGroupAlgebraProjection C K j
84 (zcFreeFoxCoordinatesMap (X := X) C hC η v x) =
85 zcCompletedGroupAlgebraMapStage C hC η j
86 (zcCompletedGroupAlgebraProjection C H
87 (j.1, completedGroupAlgebraComapIndexInClass
88 (G := H) (H := K) C hC η j.2) (v x)) := by
89 simp only [zcFreeFoxCoordinatesMap, zcCompletedGroupAlgebraProjection_map]
91/-- Finite-stage projection of target naturality for source-shaped completed Fox boundary maps. -/
92theorem freeProCZCCompletedFoxBoundary_mapTarget_finiteStageProjection_stage
93 (η : H →ₜ* K) (φ : X → H)
94 (v : ZCFreeFoxCoordinates C (X := X) (H := H))
95 (j : ZCCompletedGroupAlgebraIndex C K) :
96 zcCompletedGroupAlgebraProjection C K j
97 (zcCompletedGroupAlgebraMap C hC η (freeProCZCCompletedFoxBoundary C φ v)) =
98 ∑ x : X,
99 zcCompletedGroupAlgebraMapStage C hC η j
100 (zcCompletedGroupAlgebraProjection C H
101 (j.1, completedGroupAlgebraComapIndexInClass
102 (G := H) (H := K) C hC η j.2) (v x)) *
103 (MonoidAlgebra.of (ModNCompletedCoeff j.1.modulus)
104 (CompletedGroupAlgebraQuotientInClass K C j.2)
105 (QuotientGroup.mk (η (φ x))) - 1) := by
106 rw [freeProCZCCompletedFoxBoundary_mapTarget]
107 rw [freeProCZCCompletedFoxBoundary_finiteStageProjection_stage]
108 apply Finset.sum_congr rfl
109 intro x _
110 rw [zcFreeFoxCoordinatesMap_finiteStageProjection]
112end TargetProjectionNaturality
114section GenuineFiniteQuotientStage
116variable {X : Type u} [DecidableEq X]
117variable {N : Subgroup (FreeGroup X)} [N.Normal]
119omit [DecidableEq X] in
120/-- A quotient bundle certifies that every associated pro-`C` completed group-algebra stage is
121actually finite. This is the canonical finite-stage consumer of
122`ZCFiniteStageQuotientBundle`; the unbundled comparison lemmas remain purely algebraic. -/
123theorem ZCFiniteStageQuotientBundle.finite_completedGroupAlgebraStage
124 (C : ProCGroups.FiniteGroupClass.{u})
125 (B : ZCFiniteStageQuotientBundle N)
126 (j : B.Index C) :
127 letI : TopologicalSpace B.Target := B.targetTopology
128 letI : IsTopologicalGroup B.Target := B.targetIsTopologicalGroup
129 Finite (ZCCompletedGroupAlgebraStage C B.Target j) := by
130 letI : TopologicalSpace B.Target := B.targetTopology
131 letI : IsTopologicalGroup B.Target := B.targetIsTopologicalGroup
132 letI : Fact (0 < j.1.modulus) := ⟨j.1.positive⟩
133 exact
134 finite_modNCompletedGroupAlgebraStageInClass
135 (n := j.1.modulus) (G := B.Target) C j.2
137end GenuineFiniteQuotientStage
139end
141end FoxDifferential