Yamaguchi Lean 4 Library
ProCGroups.ProC.MaximalQuotients.Definitions
ProCGroups/ProC/MaximalQuotients/Definitions

ProCGroups.ProC.MaximalQuotients.Definitions

1 Structure

This module proves the universal-property part of the construction. It packages finite-stage data into completed maps and shows the required extension and uniqueness statements.

Open this file on GitHub
import
Imported by

Declarations

Structure ProCGroups.ProC.IsMaximalProCQuotient GitHub 
structure IsMaximalProCQuotient
    (ProC : ProCGroupPredicate)
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    {Q : Type u} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
    (π : G →* Q) : Prop where
  isProC : ProC (G := Q)
  continuous_π : Continuous π
  surjective_π : Function.Surjective π
  existsUnique_lift :
    ∀ {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H],
      ProC (G := H) →
      ∀ (φ : G →* H), Continuous φ →
        ∃! φbar : Q →* H, Continuous φbar ∧ φbar.comp π = φ

Maximal pro-\(C\) quotient groups via their universal property.