FoxDifferential/Completed/DifferentialModule/TargetQuotient/Surjective.lean
1import FoxDifferential.Completed.DifferentialModule.TargetQuotient.StageMap
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FoxDifferential/Completed/DifferentialModule/TargetQuotient/Surjective.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Completed differential modules
14The completed differential module is organized separately from coefficient algebras; its universal and quotient maps are used by completed crossed differentials.
15-/
16namespace FoxDifferential
18noncomputable section
20open ProCGroups
21open ProCGroups.ProC
23universe u v
25variable (ℓ : ℕ) [Fact (0 < ℓ)]
26variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
27variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
30variable {X : Type u} [DecidableEq X]
32omit [DecidableEq X] in
33/-- The quotient homomorphism `FreeGroup X -> FreeGroup X / N` is surjective.
35This specialized form is used to lift coefficients from `Z_ell[[F/N]]` to
36`Z_ell[[F]]` in the completed Fox derivative construction. -/
38 [TopologicalSpace (FreeGroup X)] [DiscreteTopology (FreeGroup X)]
39 (N : Subgroup (FreeGroup X)) [N.Normal]
40 [TopologicalSpace (finiteFoxStageTargetQuotient (X := X) N)] :
41 Function.Surjective
42 (finiteFoxStageTargetQuotientContinuousMonoidHom (X := X) N) := by
43 intro q
44 rcases QuotientGroup.mk'_surjective N q with ⟨w, rfl⟩
45 exact ⟨w, rfl⟩
47omit [DecidableEq X] in
48/-- The completed group-algebra map attached to `FreeGroup X -> FreeGroup X / N` is surjective.
50This is the coefficient-lifting input for the surjectivity half of `K/KI -> L`. -/
52 [TopologicalSpace (FreeGroup X)] [IsTopologicalGroup (FreeGroup X)]
53 [DiscreteTopology (FreeGroup X)]
54 (N : Subgroup (FreeGroup X)) [N.Normal]
55 [TopologicalSpace (finiteFoxStageTargetQuotient (X := X) N)]
56 [IsTopologicalGroup (finiteFoxStageTargetQuotient (X := X) N)] :
57 Function.Surjective
59 (ℓ := ℓ) (G := FreeGroup X)
60 (H := finiteFoxStageTargetQuotient (X := X) N)
61 (finiteFoxStageTargetQuotientContinuousMonoidHom (X := X) N)) := by
62 exact
64 (ℓ := ℓ) (G := FreeGroup X)
65 (H := finiteFoxStageTargetQuotient (X := X) N)
66 (finiteFoxStageTargetQuotientContinuousMonoidHom (X := X) N)
69/-- A noncomputable lift of a completed target-group-algebra coefficient to the source completed
70group algebra. The defining equation is `primePowerCompletedGroupAlgebraMap_targetQuotient_lift_spec`. -/
72 [TopologicalSpace (FreeGroup X)] [IsTopologicalGroup (FreeGroup X)]
73 [DiscreteTopology (FreeGroup X)]
74 (N : Subgroup (FreeGroup X)) [N.Normal]
75 [TopologicalSpace (finiteFoxStageTargetQuotient (X := X) N)]
76 [IsTopologicalGroup (finiteFoxStageTargetQuotient (X := X) N)]
77 (a : PrimePowerCompletedGroupAlgebra ℓ (finiteFoxStageTargetQuotient (X := X) N)) :
78 PrimePowerCompletedGroupAlgebra ℓ (FreeGroup X) :=
79 Classical.choose
81 (ℓ := ℓ) (X := X) N a)
83omit [DecidableEq X] in
84/-- The chosen coefficient lift maps back to the prescribed completed target coefficient. -/
85@[simp]
87 [TopologicalSpace (FreeGroup X)] [IsTopologicalGroup (FreeGroup X)]
88 [DiscreteTopology (FreeGroup X)]
89 (N : Subgroup (FreeGroup X)) [N.Normal]
90 [TopologicalSpace (finiteFoxStageTargetQuotient (X := X) N)]
91 [IsTopologicalGroup (finiteFoxStageTargetQuotient (X := X) N)]
92 (a : PrimePowerCompletedGroupAlgebra ℓ (finiteFoxStageTargetQuotient (X := X) N)) :
94 (ℓ := ℓ) (G := FreeGroup X)
95 (H := finiteFoxStageTargetQuotient (X := X) N)
96 (finiteFoxStageTargetQuotientContinuousMonoidHom (X := X) N)
98 (ℓ := ℓ) (X := X) N a) = a :=
99 Classical.choose_spec
101 (ℓ := ℓ) (X := X) N a)
104end
106end FoxDifferential