TotallyDisconnectedQuotients.lean

theorem totallyDisconnectedSpace_of_isClosed
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
    (N : Subgroup G) [N.Normal] (hN : IsClosed (N : Set G)) :
    TotallyDisconnectedSpace (G ⧸ N)

instance Subgroup.Normal.connectedComponentOfOne
    (G : Type*) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    (Subgroup.connectedComponentOfOne G).Normal where
  conj_mem x hx g := by
    change g * x * g⁻¹ ∈ connectedComponent (1 : G)
    simpa only [mul_one, mul_inv_cancel] using
      (IsTopologicalGroup.continuous_conj g).mapsTo_connectedComponent
        (1 : G) hx

theorem totallyDisconnectedSpace_quotient_connectedComponentOfOne
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    TotallyDisconnectedSpace
      (G ⧸ Subgroup.connectedComponentOfOne G)

theorem connectedComponentOfOne_le_ker
    {G H : Type*}
    [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
    [TotallyDisconnectedSpace H]
    (f : G →ₜ* H) :
    Subgroup.connectedComponentOfOne G ≤ f.ker