TopologicalAbelianization.lean

def mkₜ
    (G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G] :
    G →ₜ* TopologicalAbelianization G

abbrev mk
    (G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G] :
    G →* TopologicalAbelianization G

theorem ker_mk
    (G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G] :
    (mk G).ker =
      Subgroup.closedCommutator G

theorem mk_eq_one_iff
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    {x : G} :
    mk G x = 1 ↔
      x ∈ Subgroup.closedCommutator G

theorem closedCommutator_eq_bot_of_commGroup_t1
    (G : Type u) [TopologicalSpace G] [CommGroup G] [IsTopologicalGroup G] [T1Space G] :
    Subgroup.closedCommutator G = ⊥

theorem surjective_mk
    (G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G] :
    Function.Surjective (mk G)

instance instT2SpaceTopologicalAbelianization
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] :
    T2Space (TopologicalAbelianization G)

def lift
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    {A : Type v} [TopologicalSpace A] [CommGroup A] [T1Space A]
    (f : G →ₜ* A) :
    TopologicalAbelianization G →ₜ* A

theorem lift_apply_mk
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    {A : Type v} [TopologicalSpace A] [CommGroup A] [T1Space A]
    (f : G →ₜ* A) (x : G) :
    lift f (mk G x) = f x

theorem hom_ext
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    {A : Type v} [TopologicalSpace A] [Group A]
    (φ ψ : TopologicalAbelianization G →ₜ* A)
    (h : ∀ x : G, φ (mk G x) = ψ (mk G x)) :
    φ = ψ

theorem lift_unique
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    {A : Type v} [TopologicalSpace A] [CommGroup A] [T1Space A]
    (f : G →ₜ* A)
    (φ : TopologicalAbelianization G →ₜ* A)
    (hφ : ∀ x : G, φ (mk G x) = f x) :
    φ = lift f

def homEquiv
    (G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    (A : Type v) [TopologicalSpace A] [CommGroup A] [T1Space A] :
    (TopologicalAbelianization G →ₜ* A) ≃ (G →ₜ* A) where
  toFun φ := φ.comp (mkₜ G)
  invFun f := lift f
  left_inv φ := by
    apply hom_ext
    intro x
    rfl
  right_inv f := by
    ext x
    rfl

theorem homEquiv_apply
    (G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    (A : Type v) [TopologicalSpace A] [CommGroup A] [T1Space A]
    (φ : TopologicalAbelianization G →ₜ* A) :
    homEquiv G A φ = φ.comp (mkₜ G)

theorem homEquiv_symm_apply_mk
    (G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    (A : Type v) [TopologicalSpace A] [CommGroup A] [T1Space A]
    (f : G →ₜ* A) (x : G) :
    (homEquiv G A).symm f (mk G x) = f x

def map
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    {H : Type v} [TopologicalSpace H] [Group H] [IsTopologicalGroup H]
    (f : G →ₜ* H) :
    TopologicalAbelianization G →ₜ* TopologicalAbelianization H

theorem map_apply_mk
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    {H : Type v} [TopologicalSpace H] [Group H] [IsTopologicalGroup H]
    (f : G →ₜ* H) (x : G) :
    map f (mk G x) =
      mk H (f x)

theorem map_comp_mk
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    {H : Type v} [TopologicalSpace H] [Group H] [IsTopologicalGroup H]
    (f : G →ₜ* H) :
    (map f).toMonoidHom.comp (mk G) =
      (mk H).comp f.toMonoidHom

theorem map_id
    (G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G] :
    map
        (ContinuousMonoidHom.id G) =
      ContinuousMonoidHom.id (TopologicalAbelianization G)

theorem map_comp
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    {H : Type v} [TopologicalSpace H] [Group H] [IsTopologicalGroup H]
    {K : Type _} [TopologicalSpace K] [Group K] [IsTopologicalGroup K]
    (g : H →ₜ* K) (f : G →ₜ* H) :
    map (g.comp f) =
      (map g).comp (map f)

def congr
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    {H : Type v} [TopologicalSpace H] [Group H] [IsTopologicalGroup H]
    (e : G ≃ₜ* H) :
    TopologicalAbelianization G ≃ₜ* TopologicalAbelianization H

theorem congr_apply_mk
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    {H : Type v} [TopologicalSpace H] [Group H] [IsTopologicalGroup H]
    (e : G ≃ₜ* H) (x : G) :
    congr e (mk G x) =
      mk H (e x)

theorem surjective_map_of_surjective
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    {H : Type v} [TopologicalSpace H] [Group H] [IsTopologicalGroup H]
    (f : G →ₜ* H) (hf : Function.Surjective f) :
    Function.Surjective (map f)

theorem injective_mk_of_commGroup
    {G : Type u} [TopologicalSpace G] [CommGroup G] [IsTopologicalGroup G] [T1Space G] :
    Function.Injective (mk G)

def continuousMulEquivOfCommGroup
    (G : Type u) [TopologicalSpace G] [CommGroup G] [IsTopologicalGroup G] [T1Space G] :
    _root_.TopologicalAbelianization G ≃ₜ* G