Definitions.lean

structure IsMaximalProCQuotient
    (C : FiniteGroupClass)
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    {Q : Type u} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
      [CompactSpace Q] [T2Space Q] [TotallyDisconnectedSpace Q]
    (π : G →* Q) : Prop where
  /-- The quotient \(Q\) has an open-normal basis whose finite quotients lie in \(C\). -/
  hasOpenNormalBasisInClass : HasOpenNormalBasisInClass C Q
  /-- The quotient homomorphism \(\pi\) is continuous. -/
  continuous_π : Continuous π
  /-- The quotient homomorphism \(\pi\) is surjective. -/
  surjective_π : Function.Surjective π
  /--
  Every continuous homomorphism from \(G\) to a pro-\(C\) target factors uniquely and
  continuously through \(Q\).
  -/
  existsUnique_lift :
    ∀ {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
      [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H],
      HasOpenNormalBasisInClass C H →
      ∀ (φ : G →* H), Continuous φ →
        ∃! φbar : Q →* H, Continuous φbar ∧ φbar.comp π = φ