Source: ProCGroups.FoxDifferential.Completed.DifferentialModule.TargetQuotient.Basic
1import ProCGroups.FoxDifferential.Completed.DifferentialModule.Map.Surjective
2import ProCGroups.FoxDifferential.Completed.FiniteStage.PrimePower.Completion.Source.Index
4/-!
5# Fox differential: completed — differential module — target quotient — basic
7The principal declarations in this module are:
9- `foxAlgebraicStageTargetQuotientContinuousMonoidHom`
10 The completed Fox-differential map is continuous with respect to the inverse-limit topology on the
11 completed coefficient modules.
12- `foxAlgebraicStageTargetQuotientContinuousMonoidHom_apply`
13 The finite-stage target quotient homomorphism sends a word to its quotient class modulo \(N\).
14- `foxAlgebraicStagePrimePowerSourceCompletedIndex_le_targetQuotientComap`
15 The completed free derivative source finite stage \([N,N]N^{ell^a}\) refines every finite stage
16 pulled back from the target quotient \(F/N\). This order comparison lets the completed
17 group-algebra projection for \(\pi: \mathbb{Z}_{\ell}\llbracket F\rrbracket \to
18 \mathbb{Z}_{\ell}\llbracket F/N\rrbracket\) be computed from the completed free derivative source
19 projection.
20-/
22namespace FoxDifferential
24noncomputable section
26open ProCGroups
27open ProCGroups.ProC
29universe u v
31variable (ℓ : ℕ) [Fact (0 < ℓ)]
32variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
33variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
36variable {X : Type u} [DecidableEq X]
38/--
39The completed Fox-differential map is continuous with respect to the inverse-limit topology on
40the completed coefficient modules.
41-/
42def foxAlgebraicStageTargetQuotientContinuousMonoidHom
43 [TopologicalSpace (FreeGroup X)] [DiscreteTopology (FreeGroup X)]
44 (N : Subgroup (FreeGroup X)) [N.Normal]
45 [TopologicalSpace (foxAlgebraicStageTargetQuotient (X := X) N)] :
46 ContinuousMonoidHom (FreeGroup X) (foxAlgebraicStageTargetQuotient (X := X) N) where
47 toMonoidHom := QuotientGroup.mk' N
48 continuous_toFun := continuous_of_discreteTopology
50omit [DecidableEq X] in
51/--
52The finite-stage target quotient homomorphism sends a word to its quotient class modulo \(N\).
53-/
54@[simp]
55theorem foxAlgebraicStageTargetQuotientContinuousMonoidHom_apply
56 [TopologicalSpace (FreeGroup X)] [DiscreteTopology (FreeGroup X)]
57 (N : Subgroup (FreeGroup X)) [N.Normal]
58 [TopologicalSpace (foxAlgebraicStageTargetQuotient (X := X) N)]
59 (w : FreeGroup X) :
60 foxAlgebraicStageTargetQuotientContinuousMonoidHom (X := X) N w =
61 QuotientGroup.mk' N w := rfl
63omit [DecidableEq X] [Fact (0 < ℓ)] in
64/--
65The completed free derivative source finite stage \([N,N]N^{ell^a}\) refines every finite stage
66pulled back from the target quotient \(F/N\). This order comparison lets the completed
67group-algebra projection for \(\pi: \mathbb{Z}_{\ell}\llbracket F\rrbracket \to
68\mathbb{Z}_{\ell}\llbracket F/N\rrbracket\) be computed from the completed free derivative
69source projection.
70-/
71theorem foxAlgebraicStagePrimePowerSourceCompletedIndex_le_targetQuotientComap
72 [TopologicalSpace (FreeGroup X)]
73 [DiscreteTopology (FreeGroup X)]
74 (N : Subgroup (FreeGroup X)) [N.Normal]
75 [TopologicalSpace (foxAlgebraicStageTargetQuotient (X := X) N)]
76 [IsTopologicalGroup (foxAlgebraicStageTargetQuotient (X := X) N)]
77 (hfinite : ∀ a : ℕ,
78 Finite (FreeGroup X ⧸
79 foxCommutatorPowerSubgroup (F := FreeGroup X) N (ℓ ^ a)))
80 (j : PrimePowerCompletedGroupAlgebraIndex
81 (foxAlgebraicStageTargetQuotient (X := X) N)) :
82 completedGroupAlgebraComapIndex
83 (G := FreeGroup X) (H := foxAlgebraicStageTargetQuotient (X := X) N)
84 (foxAlgebraicStageTargetQuotientContinuousMonoidHom (X := X) N) j.2 ≤
85 foxAlgebraicStagePrimePowerSourceCompletedIndex
86 (ℓ := ℓ) (X := X) N hfinite j.1 := by
87 change foxCommutatorPowerSubgroup (F := FreeGroup X) N (ℓ ^ j.1) ≤
88 Subgroup.comap
89 (foxAlgebraicStageTargetQuotientContinuousMonoidHom (X := X) N).toMonoidHom
90 (((OrderDual.ofDual j.2).1 :
91 OpenNormalSubgroup (foxAlgebraicStageTargetQuotient (X := X) N)) :
92 Subgroup (foxAlgebraicStageTargetQuotient (X := X) N))
93 intro g hg
94 change QuotientGroup.mk' N g ∈
95 (((OrderDual.ofDual j.2).1 :
96 OpenNormalSubgroup (foxAlgebraicStageTargetQuotient (X := X) N)) :
97 Subgroup (foxAlgebraicStageTargetQuotient (X := X) N))
98 have hgN : g ∈ N :=
99 foxCommutatorPowerSubgroup_le_normal (F := FreeGroup X) N (ℓ ^ j.1) hg
100 have hgq : QuotientGroup.mk' N g =
101 (1 : foxAlgebraicStageTargetQuotient (X := X) N) := by
102 simpa using (QuotientGroup.eq_one_iff (N := N) g).2 hgN
103 rw [hgq]
104 exact Subgroup.one_mem _
107end
109end FoxDifferential