ProCGroups/FreeProC/Constructions.lean
1import ProCGroups.NormalSubgroups.SimpleQuotients.Compactness
2import ProCGroups.ProC.MaximalQuotients.Definitions
4/-
5PUBLIC_PAGE_SNAPSHOT
6generated_at: 2026-05-27T09:47:29+09:00
7lean_source: lean4/ProCGroups/FreeProC/Constructions.lean
8translation_root: data/translation
9purpose: identifies the local data snapshot used to build pages/
10placement: after imports, never before imports
11-/
12/-!
13# Free pro-C groups
15Develops free pro-C groups on spaces and pointed spaces, their universal properties, finite quotient characterizations, and standard comparison isomorphisms.
16-/
18open Set
19open ProCGroups.ProC
21namespace ProCGroups.FreeProC
23universe u
25section CoreResults
27variable {ProC : ProCGroupPredicate}
29/-- A maximal pro-`C'` quotient of a pointed free pro-`C` group is again pointed free
30on the same pointed space.
33class-inclusion hypothesis `ProC' ⇒ ProC`. -/
35 {ProC' : ProCGroupPredicate}
36 (hmono :
37 ∀ {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G],
38 ProC' (G := G) → ProC (G := G))
39 {X : Type u} [TopologicalSpace X] {x0 : X}
40 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
41 {Q : Type u} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
42 {ι : X → F}
43 (hF : IsPointedFreeProCGroupOn (ProC := ProC) X x0 F ι)
44 (π : F →* Q) (hπ : IsMaximalProCQuotient ProC' π) :
45 IsPointedFreeProCGroupOn (ProC := ProC') X x0 Q (fun x => π (ι x)) := by
46 refine ⟨hπ.isProC, hπ.continuous_π.comp hF.continuous_ι, ?_, ?_, ?_⟩
50 simpa [himage] using
51 (Generation.topologicallyGenerates_image_of_continuousSurjective
53 · intro G _ _ _ hG φ hφ hφ0 hgen
54 have hG' : ProC (G := G) := hmono hG
55 rcases hF.existsUnique_lift hG' φ hφ hφ0 hgen with ⟨f, hfprop, hfuniq⟩
56 rcases hπ.existsUnique_lift hG f hfprop.1 with ⟨q, hqprop, hquniq⟩
57 refine ⟨q, ?_, ?_⟩
58 · refine ⟨hqprop.1, ?_⟩
59 intro x
60 have hcomp_eval := congrArg (fun ψ : F →* G => ψ (ι x)) hqprop.2
61 simpa [MonoidHom.comp_apply, hfprop.2 x] using hcomp_eval
62 · intro q' hq'
63 have hq'comp :
65 apply hfuniq
66 refine ⟨hq'.1.comp hπ.continuous_π, ?_⟩
67 intro x
68 simpa [MonoidHom.comp_apply] using hq'.2 x
69 exact hquniq q' ⟨hq'.1, hq'comp⟩
71/-- Lemma-level perfect-kernel statement with an explicit quotient hypothesis.
73With the current abstract `ProC` interface, the standard argument needs two extra inputs made
74explicit here:
75- the comparison `ProC ⇒ ProCe`, so the `pro-`C quotient may also be used as a `pro-`C_e` target;
79from a pointed free `pro-`C_e` model to a pointed free `pro-`C` model is perfect. -/
81 {ProCe : ProCGroupPredicate}
82 (hmono :
83 ∀ {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G],
84 ProC (G := G) → ProCe (G := G))
85 {X : Type u} [TopologicalSpace X] {x0 : X}
86 {Fe : Type u} [Group Fe] [TopologicalSpace Fe] [IsTopologicalGroup Fe]
87 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
88 {ιe : X → Fe} {ι : X → F}
89 (hFe : IsPointedFreeProCGroupOn (ProC := ProCe) X x0 Fe ιe)
90 (hF : IsPointedFreeProCGroupOn (ProC := ProC) X x0 F ι)
91 (φ : Fe →* F) (hφ : Continuous φ)
92 (hcompat : ∀ x, φ (ιe x) = ι x)
93 (hquot : ProC (G := Fe ⧸ ⁅φ.ker, φ.ker⁆)) :
94 ProCGroups.NormalSubgroups.IsPerfectSubgroup φ.ker := by
95 let K : Subgroup Fe := φ.ker
96 let q : Fe →* Fe ⧸ ⁅K, K⁆ := QuotientGroup.mk' ⁅K, K⁆
97 let ψ : X → Fe ⧸ ⁅K, K⁆ := fun x => q (ιe x)
98 have hψ : Continuous ψ := continuous_quotient_mk'.comp hFe.continuous_ι
99 have hψ0 : ψ x0 = 1 := by
100 simp only [QuotientGroup.mk'_apply, hFe.map_base, QuotientGroup.mk_one, ψ, q]
101 have himage : q '' Set.range ιe = Set.range ψ := by
102 simpa [ψ, q, Function.comp] using (Set.range_comp q ιe).symm
103 have hgenψ : Generation.TopologicallyGenerates (G := Fe ⧸ ⁅K, K⁆) (Set.range ψ) := by
104 simpa [himage] using
105 (Generation.topologicallyGenerates_image_of_continuousSurjective
106 (G := Fe) (H := Fe ⧸ ⁅K, K⁆) q continuous_quotient_mk'
107 (QuotientGroup.mk'_surjective ⁅K, K⁆) hFe.generates_range)
108 rcases hF.existsUnique_lift hquot ψ hψ hψ0 hgenψ with ⟨σ, hσ, _⟩
109 have hquot_e : ProCe (G := Fe ⧸ ⁅K, K⁆) := hmono hquot
110 rcases hFe.existsUnique_lift hquot_e ψ hψ hψ0 hgenψ with ⟨τ, hτ, hτuniq⟩
111 have hq_eq : q = τ := by
112 exact hτuniq q ⟨continuous_quotient_mk', fun x => rfl⟩
113 have hσφ_eq : σ.comp φ = τ := by
114 refine hτuniq (σ.comp φ) ⟨hσ.1.comp hφ, ?_⟩
115 intro x
116 calc
117 (σ.comp φ) (ιe x) = σ (ι x) := by
118 simp only [MonoidHom.comp_apply, hcompat x]
119 _ = ψ x := hσ.2 x
120 have hfac : σ.comp φ = q := hσφ_eq.trans hq_eq.symm
121 have hKle : K ≤ ⁅K, K⁆ := by
122 intro k hk
123 have hkφ : φ k = 1 := by
124 simpa [K, MonoidHom.mem_ker] using hk
125 have hqk : q k = 1 := by
126 rw [← DFunLike.congr_fun hfac k]
128 exact (QuotientGroup.eq_one_iff (N := ⁅K, K⁆) k).1 hqk
129 simpa [K, ProCGroups.NormalSubgroups.IsPerfectSubgroup] using
130 (le_antisymm (Subgroup.commutator_le_self K) hKle)
132/-- Perfect-kernel statement using pro-`C` permanence data to build the commutator-kernel
133quotient internally. -/
135 {ProCe : ProCGroupPredicate}
136 [ProC.ClosedUnderCommutatorKernelQuotientsFrom ProCe]
137 (hmono :
138 ∀ {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G],
139 ProC (G := G) → ProCe (G := G))
140 {X : Type u} [TopologicalSpace X] {x0 : X}
141 {Fe : Type u} [Group Fe] [TopologicalSpace Fe] [IsTopologicalGroup Fe]
142 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
143 {ιe : X → Fe} {ι : X → F}
144 (hFe : IsPointedFreeProCGroupOn (ProC := ProCe) X x0 Fe ιe)
145 (hF : IsPointedFreeProCGroupOn (ProC := ProC) X x0 F ι)
146 (φ : Fe →* F) (hφ : Continuous φ)
147 (hcompat : ∀ x, φ (ιe x) = ι x) :
148 ProCGroups.NormalSubgroups.IsPerfectSubgroup φ.ker := by
149 let φₜ : Fe →ₜ* F := { toMonoidHom := φ, continuous_toFun := hφ }
150 have hquot : ProC (G := Fe ⧸ ⁅φ.ker, φ.ker⁆) := by
151 simpa [φₜ] using
152 (ProCGroupPredicate.quotient_by_kernel_commutator
154 exact
156 (ProC := ProC) (ProCe := ProCe) hmono hFe hF φ hφ hcompat hquot
158end CoreResults
160end ProCGroups.FreeProC