FoxDifferential/Completed/DifferentialModule/TargetQuotient/Basic.lean
1import FoxDifferential.Completed.DifferentialModule.Map.Surjective
2import FoxDifferential.Completed.FiniteStage.PrimePower.Completion.Source.Index
4/-
5PUBLIC_PAGE_SNAPSHOT
6generated_at: 2026-05-27T09:47:29+09:00
7lean_source: lean4/FoxDifferential/Completed/DifferentialModule/TargetQuotient/Basic.lean
8translation_root: data/translation
9purpose: identifies the local data snapshot used to build pages/
10placement: after imports, never before imports
11-/
12/-!
13# Completed differential modules
15The completed differential module is organized separately from coefficient algebras; its universal and quotient maps are used by completed crossed differentials.
16-/
17namespace FoxDifferential
19noncomputable section
21open ProCGroups
22open ProCGroups.ProC
24universe u v
26variable (ℓ : ℕ) [Fact (0 < ℓ)]
27variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
28variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
31variable {X : Type u} [DecidableEq X]
33/-- Definition of finiteFoxStageTargetQuotientContinuousMonoidHom. -/
35 [TopologicalSpace (FreeGroup X)] [DiscreteTopology (FreeGroup X)]
36 (N : Subgroup (FreeGroup X)) [N.Normal]
37 [TopologicalSpace (finiteFoxStageTargetQuotient (X := X) N)] :
38 ContinuousMonoidHom (FreeGroup X) (finiteFoxStageTargetQuotient (X := X) N) where
39 toMonoidHom := QuotientGroup.mk' N
40 continuous_toFun := continuous_of_discreteTopology
42omit [DecidableEq X] in
43/-- Evaluation formula for finiteFoxStageTargetQuotientContinuousMonoidHom_apply. -/
44@[simp]
46 [TopologicalSpace (FreeGroup X)] [DiscreteTopology (FreeGroup X)]
47 (N : Subgroup (FreeGroup X)) [N.Normal]
48 [TopologicalSpace (finiteFoxStageTargetQuotient (X := X) N)]
49 (w : FreeGroup X) :
50 finiteFoxStageTargetQuotientContinuousMonoidHom (X := X) N w =
51 QuotientGroup.mk' N w := rfl
53omit [DecidableEq X] [Fact (0 < ℓ)] in
54/-- The completed free derivative source finite stage `[N,N]N^{ell^a}` refines every finite stage pulled back
55from the target quotient `F/N`. This is the order comparison that lets the completed
56group-algebra projection for `π : Z_ell[[F]] -> Z_ell[[F/N]]` be read from the completed free derivative source
57projection. -/
59 [TopologicalSpace (FreeGroup X)]
60 [DiscreteTopology (FreeGroup X)]
61 (N : Subgroup (FreeGroup X)) [N.Normal]
62 [TopologicalSpace (finiteFoxStageTargetQuotient (X := X) N)]
63 [IsTopologicalGroup (finiteFoxStageTargetQuotient (X := X) N)]
64 (hfinite : ∀ a : ℕ,
65 Finite (FreeGroup X ⧸
66 finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N (ℓ ^ a)))
68 (finiteFoxStageTargetQuotient (X := X) N)) :
69 completedGroupAlgebraComapIndex
70 (G := FreeGroup X) (H := finiteFoxStageTargetQuotient (X := X) N)
71 (finiteFoxStageTargetQuotientContinuousMonoidHom (X := X) N) j.2 ≤
73 (ℓ := ℓ) (X := X) N hfinite j.1 := by
74 change finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N (ℓ ^ j.1) ≤
75 Subgroup.comap
76 (finiteFoxStageTargetQuotientContinuousMonoidHom (X := X) N).toMonoidHom
77 (((OrderDual.ofDual j.2).1 :
78 OpenNormalSubgroup (finiteFoxStageTargetQuotient (X := X) N)) :
79 Subgroup (finiteFoxStageTargetQuotient (X := X) N))
80 intro g hg
81 change QuotientGroup.mk' N g ∈
82 (((OrderDual.ofDual j.2).1 :
83 OpenNormalSubgroup (finiteFoxStageTargetQuotient (X := X) N)) :
84 Subgroup (finiteFoxStageTargetQuotient (X := X) N))
85 have hgN : g ∈ N :=
86 finiteFoxCommutatorPowerSubgroup_le_normal (F := FreeGroup X) N (ℓ ^ j.1) hg
87 have hgq : QuotientGroup.mk' N g =
88 (1 : finiteFoxStageTargetQuotient (X := X) N) := by
89 simpa using (QuotientGroup.eq_one_iff (N := N) g).2 hgN
90 rw [hgq]
91 exact Subgroup.one_mem _
94end
96end FoxDifferential