Source: ProCGroups.ProC.MaximalQuotients.Definitions
1import ProCGroups.ProC.OpenNormalSubgroups.ProCGroup
3/-!
4# Maximal pro-\(C\) quotients
6`IsMaximalProCQuotient C π` states that `π` is a continuous quotient map onto
7a profinite group with a pro-\(C\) basis and that every continuous map to a
8pro-\(C\) target factors through it uniquely.
9-/
11namespace ProCGroups.ProC
13universe u
15/-- Maximal pro-\(C\) quotient groups via their universal property. -/
16structure IsMaximalProCQuotient
17 (C : FiniteGroupClass)
18 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
19 {Q : Type u} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
20 [CompactSpace Q] [T2Space Q] [TotallyDisconnectedSpace Q]
21 (π : G →* Q) : Prop where
22 /-- The quotient \(Q\) has an open-normal basis whose finite quotients lie in \(C\). -/
23 hasOpenNormalBasisInClass : HasOpenNormalBasisInClass C Q
24 /-- The quotient homomorphism \(\pi\) is continuous. -/
25 continuous_π : Continuous π
26 /-- The quotient homomorphism \(\pi\) is surjective. -/
27 surjective_π : Function.Surjective π
28 /--
29 Every continuous homomorphism from \(G\) to a pro-\(C\) target factors uniquely and
30 continuously through \(Q\).
31 -/
32 existsUnique_lift :
33 ∀ {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
34 [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H],
35 HasOpenNormalBasisInClass C H →
36 ∀ (φ : G →* H), Continuous φ →
37 ∃! φbar : Q →* H, Continuous φbar ∧ φbar.comp π = φ
39end ProCGroups.ProC