Source: ProCGroups.FoxDifferential.Completed.DifferentialModule.TargetQuotient.Surjective
1import ProCGroups.FoxDifferential.Completed.DifferentialModule.TargetQuotient.StageMap
3/-!
4# Fox differential: completed — differential module — target quotient — surjective
6The principal declarations in this module are:
8- `primePowerCompletedGroupAlgebraMap_targetQuotient_lift`
9 A noncomputable lift of a completed target group-algebra coefficient to the source completed group
10 algebra. The defining equation is
11 \(\mathrm{primePowerCompletedGroupAlgebraMap\_targetQuotient\_lift\_spec}\).
12- `foxAlgebraicStageTargetQuotientContinuousMonoidHom_surjective`
13 The quotient homomorphism \(\mathrm{FreeGroup}(X) \to \mathrm{FreeGroup}(X)/N\) is surjective.
14 This specialized form is used to lift coefficients from \(\mathbb{Z}_{\ell}\llbracket
15 F/N\rrbracket\) to \(\mathbb{Z}_{\ell}\llbracket F\rrbracket\) in the completed Fox derivative.
16- `primePowerCompletedGroupAlgebraMap_targetQuotient_surjective`
17 The completed group-algebra map attached to \(\mathrm{FreeGroup}(X) \to \mathrm{FreeGroup}(X)/N\)
18 is surjective. This is the coefficient-lifting input for the surjectivity half of \(K/KI \to L\).
19- `primePowerCompletedGroupAlgebraMap_targetQuotient_lift_spec`
20 The chosen coefficient lift maps back to the prescribed completed target coefficient.
21-/
23namespace FoxDifferential
25noncomputable section
27open ProCGroups
28open ProCGroups.ProC
30universe u v
32variable (ℓ : ℕ) [Fact (0 < ℓ)]
33variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
34variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
37variable {X : Type u} [DecidableEq X]
39omit [DecidableEq X] in
40/--
41The quotient homomorphism \(\mathrm{FreeGroup}(X) \to \mathrm{FreeGroup}(X)/N\) is surjective.
42This specialized form is used to lift coefficients from \(\mathbb{Z}_{\ell}\llbracket
43F/N\rrbracket\) to \(\mathbb{Z}_{\ell}\llbracket F\rrbracket\) in the completed Fox derivative.
44-/
45theorem foxAlgebraicStageTargetQuotientContinuousMonoidHom_surjective
46 [TopologicalSpace (FreeGroup X)] [DiscreteTopology (FreeGroup X)]
47 (N : Subgroup (FreeGroup X)) [N.Normal]
48 [TopologicalSpace (foxAlgebraicStageTargetQuotient (X := X) N)] :
49 Function.Surjective
50 (foxAlgebraicStageTargetQuotientContinuousMonoidHom (X := X) N) := by
51 intro q
52 rcases QuotientGroup.mk'_surjective N q with ⟨w, rfl⟩
53 exact ⟨w, rfl⟩
55omit [DecidableEq X] in
56/--
57The completed group-algebra map attached to \(\mathrm{FreeGroup}(X) \to
58\mathrm{FreeGroup}(X)/N\) is surjective. This is the coefficient-lifting input for the
59surjectivity half of \(K/KI \to L\).
60-/
61theorem primePowerCompletedGroupAlgebraMap_targetQuotient_surjective
62 [TopologicalSpace (FreeGroup X)] [IsTopologicalGroup (FreeGroup X)]
63 [DiscreteTopology (FreeGroup X)]
64 (N : Subgroup (FreeGroup X)) [N.Normal]
65 [TopologicalSpace (foxAlgebraicStageTargetQuotient (X := X) N)]
66 [IsTopologicalGroup (foxAlgebraicStageTargetQuotient (X := X) N)] :
67 Function.Surjective
68 (primePowerCompletedGroupAlgebraMap
69 (ℓ := ℓ) (G := FreeGroup X)
70 (H := foxAlgebraicStageTargetQuotient (X := X) N)
71 (foxAlgebraicStageTargetQuotientContinuousMonoidHom (X := X) N)) := by
72 exact
73 primePowerCompletedGroupAlgebraMap_surjective
74 (ℓ := ℓ) (G := FreeGroup X)
75 (H := foxAlgebraicStageTargetQuotient (X := X) N)
76 (foxAlgebraicStageTargetQuotientContinuousMonoidHom (X := X) N)
77 (foxAlgebraicStageTargetQuotientContinuousMonoidHom_surjective (X := X) N)
79/--
80A noncomputable lift of a completed target group-algebra coefficient to the source completed
81group algebra. The defining equation is
82\(\mathrm{primePowerCompletedGroupAlgebraMap\_targetQuotient\_lift\_spec}\).
83-/
84def primePowerCompletedGroupAlgebraMap_targetQuotient_lift
85 [TopologicalSpace (FreeGroup X)] [IsTopologicalGroup (FreeGroup X)]
86 [DiscreteTopology (FreeGroup X)]
87 (N : Subgroup (FreeGroup X)) [N.Normal]
88 [TopologicalSpace (foxAlgebraicStageTargetQuotient (X := X) N)]
89 [IsTopologicalGroup (foxAlgebraicStageTargetQuotient (X := X) N)]
90 (a : PrimePowerCompletedGroupAlgebra ℓ (foxAlgebraicStageTargetQuotient (X := X) N)) :
91 PrimePowerCompletedGroupAlgebra ℓ (FreeGroup X) :=
92 Classical.choose
93 (primePowerCompletedGroupAlgebraMap_targetQuotient_surjective
94 (ℓ := ℓ) (X := X) N a)
96omit [DecidableEq X] in
97/-- The chosen coefficient lift maps back to the prescribed completed target coefficient. -/
98@[simp]
99theorem primePowerCompletedGroupAlgebraMap_targetQuotient_lift_spec
100 [TopologicalSpace (FreeGroup X)] [IsTopologicalGroup (FreeGroup X)]
101 [DiscreteTopology (FreeGroup X)]
102 (N : Subgroup (FreeGroup X)) [N.Normal]
103 [TopologicalSpace (foxAlgebraicStageTargetQuotient (X := X) N)]
104 [IsTopologicalGroup (foxAlgebraicStageTargetQuotient (X := X) N)]
105 (a : PrimePowerCompletedGroupAlgebra ℓ (foxAlgebraicStageTargetQuotient (X := X) N)) :
106 primePowerCompletedGroupAlgebraMap
107 (ℓ := ℓ) (G := FreeGroup X)
108 (H := foxAlgebraicStageTargetQuotient (X := X) N)
109 (foxAlgebraicStageTargetQuotientContinuousMonoidHom (X := X) N)
110 (primePowerCompletedGroupAlgebraMap_targetQuotient_lift
111 (ℓ := ℓ) (X := X) N a) = a :=
112 Classical.choose_spec
113 (primePowerCompletedGroupAlgebraMap_targetQuotient_surjective
114 (ℓ := ℓ) (X := X) N a)
117end
119end FoxDifferential