Module

TopologicalAbelianizationFunctoriality.lean

Nyll.ProCGroups.Abelian.TopologicalAbelianizationFunctoriality

29 declarations indexed from sourceView source ↗

Module documentation

Functorial topological abelianization

Topological abelianization defines a functor from topological groups to commutative topological groups. Its universal property is expressed directly as an equivalence of morphism types for \(T_1\) targets.

Imports4

Imported by22

def

topologicalAbelianizationFunctor

L31 ↗

ProCGroups.Abelian.topologicalAbelianizationFunctor

Documentation

Topological abelianization as a functor from topological groups to commutative topological groups.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open CategoryTheory
open scoped Topology commutatorElement
namespace ProCGroups.Abelian
universe u

Lean source · full declaration

def topologicalAbelianizationFunctor : TopGrp.{u} ⥤ CommTopGrp.{u} where
  obj G := CommTopGrp.of (TopologicalAbelianization G)
  map {G H} f := CommTopGrp.ofHom (TopologicalAbelianization.map f.hom)
  map_id G := by
    apply CommTopGrp.hom_ext
    exact TopologicalAbelianization.map_id G
  map_comp f g := by
    apply CommTopGrp.hom_ext
    exact TopologicalAbelianization.map_comp g.hom f.hom

theorem

topologicalAbelianizationFunctor_map_apply_mk

L45 ↗

ProCGroups.Abelian.topologicalAbelianizationFunctor_map_apply_mk

Documentation

The induced map on topological abelianizations sends a representative class to the class of its image.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open CategoryTheory
open scoped Topology commutatorElement
namespace ProCGroups.Abelian
universe u

Lean source · statement

theorem topologicalAbelianizationFunctor_map_apply_mk
    {G H : TopGrp.{u}} (f : G ⟶ H) (x : G) :
    topologicalAbelianizationFunctor.map f (TopologicalAbelianization.mk G x) =
      TopologicalAbelianization.mk H (f x)

def

topologicalAbelianizationHomEquiv

L55 ↗

ProCGroups.Abelian.topologicalAbelianizationHomEquiv

Documentation

Category-level Hom equivalence expressing the universal property of topological abelianization for commutative \(T_1\) targets.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open CategoryTheory
open scoped Topology commutatorElement
namespace ProCGroups.Abelian
universe u

Lean source · full declaration

def topologicalAbelianizationHomEquiv
    (G : TopGrp.{u}) (A : CommTopGrp.{u}) [T1Space A] :
    (topologicalAbelianizationFunctor.obj G ⟶ A) ≃
      (G ⟶ commTopGrpForgetToTopGrp.obj A) where
  toFun φ := TopGrp.ofHom (φ.hom.comp (TopologicalAbelianization.mkₜ G))
  invFun f := CommTopGrp.ofHom (TopologicalAbelianization.lift f.hom)
  left_inv φ := by
    apply CommTopGrp.hom_ext
    apply TopologicalAbelianization.hom_ext
    intro x
    rfl
  right_inv f := by
    apply TopGrp.hom_ext
    ext x
    rfl

theorem

topologicalAbelianizationHomEquiv_apply_hom

L75 ↗

ProCGroups.Abelian.topologicalAbelianizationHomEquiv_apply_hom

Documentation

The topological-abelianization hom equivalence evaluates a homomorphism by its induced map on representatives.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open CategoryTheory
open scoped Topology commutatorElement
namespace ProCGroups.Abelian
universe u

Lean source · statement

theorem topologicalAbelianizationHomEquiv_apply_hom
    (G : TopGrp.{u}) (A : CommTopGrp.{u}) [T1Space A]
    (φ : topologicalAbelianizationFunctor.obj G ⟶ A) :
    (topologicalAbelianizationHomEquiv G A φ).hom =
      φ.hom.comp (TopologicalAbelianization.mkₜ G)

theorem

topologicalAbelianizationHomEquiv_symm_apply_mk

L86 ↗

ProCGroups.Abelian.topologicalAbelianizationHomEquiv_symm_apply_mk

Documentation

The inverse topological-abelianization hom equivalence sends a coset representative to the corresponding homomorphism value.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open CategoryTheory
open scoped Topology commutatorElement
namespace ProCGroups.Abelian
universe u

Lean source · statement

theorem topologicalAbelianizationHomEquiv_symm_apply_mk
    (G : TopGrp.{u}) (A : CommTopGrp.{u}) [T1Space A]
    (f : G ⟶ commTopGrpForgetToTopGrp.obj A) (x : G) :
    (topologicalAbelianizationHomEquiv G A).symm f
      (TopologicalAbelianization.mk G x) = f x

def

topologicalAbelianizationTopMulEquiv

L97 ↗

ProCGroups.Abelian.topologicalAbelianizationTopMulEquiv

Documentation

The topological abelianization of the \(\top\) open subgroup is canonically the same as the topological abelianization of the ambient group.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open CategoryTheory
open scoped Topology commutatorElement
namespace ProCGroups.Abelian
universe u

Lean source · statement

def topologicalAbelianizationTopMulEquiv
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] :
    TopologicalAbelianization ↥((⊤ : OpenSubgroup G) : Subgroup G) ≃ₜ*
      TopologicalAbelianization G

theorem

topologicalAbelianizationTopMulEquiv_apply_mk

L110 ↗

ProCGroups.Abelian.topologicalAbelianizationTopMulEquiv_apply_mk

Documentation

The abelianization equivalence for a topological group equivalence sends representatives to representatives.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open CategoryTheory
open scoped Topology commutatorElement
namespace ProCGroups.Abelian
universe u

Lean source · statement

theorem topologicalAbelianizationTopMulEquiv_apply_mk
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    (x : ↥((⊤ : OpenSubgroup G) : Subgroup G)) :
    topologicalAbelianizationTopMulEquiv
        (G := G) (TopologicalAbelianization.mk ↥((⊤ : OpenSubgroup G) : Subgroup G) x) =
      TopologicalAbelianization.mk G x.1

def

quotientConjugationTopologicalAbelianizationMap

L125 ↗

ProCGroups.Abelian.quotientConjugationTopologicalAbelianizationMap

Documentation

The quotient G/N acts on the topological abelianization of N by conjugation.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open CategoryTheory
open scoped Topology commutatorElement
namespace ProCGroups.Abelian
universe u

Lean source · statement

def quotientConjugationTopologicalAbelianizationMap
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    (N : Subgroup G) [N.Normal] :
    (G ⧸ N) →* MulAut (TopologicalAbelianization N)

def

conjugationTopologicalAbelianizationContinuousAut

L149 ↗

ProCGroups.Abelian.conjugationTopologicalAbelianizationContinuousAut

Documentation

The continuous self-equivalence of topological abelianization induced by conjugation by a representative.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open CategoryTheory
open scoped Topology commutatorElement
namespace ProCGroups.Abelian
universe u

Lean source · statement

def conjugationTopologicalAbelianizationContinuousAut
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    (N : Subgroup G) [N.Normal] (g : G) :
    TopologicalAbelianization N ≃ₜ* TopologicalAbelianization N

theorem

conjugationTopologicalAbelianizationContinuousAut_toMulAut_apply_mk

L159 ↗

ProCGroups.Abelian.conjugationTopologicalAbelianizationContinuousAut_toMulAut_apply_mk

Documentation

The representative-wise continuous automorphism has the same underlying algebraic action as quotientConjugationTopologicalAbelianizationMap.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open CategoryTheory
open scoped Topology commutatorElement
namespace ProCGroups.Abelian
universe u

Lean source · statement

theorem conjugationTopologicalAbelianizationContinuousAut_toMulAut_apply_mk
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    (N : Subgroup G) [N.Normal] (g : G) (n : N) :
    conjugationTopologicalAbelianizationContinuousAut (G := G) N g
      (TopologicalAbelianization.mk N n) =
        quotientConjugationTopologicalAbelianizationMap (G := G) (N := N)
          (QuotientGroup.mk' N g) (TopologicalAbelianization.mk N n)

theorem

quotientConjugationTopologicalAbelianizationMap_mk_apply_mk

L172 ↗

ProCGroups.Abelian.quotientConjugationTopologicalAbelianizationMap_mk_apply_mk

Documentation

The conjugation action on a quotient induces the expected map on topological abelianization representatives.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open CategoryTheory
open scoped Topology commutatorElement
namespace ProCGroups.Abelian
universe u

Lean source · statement

theorem quotientConjugationTopologicalAbelianizationMap_mk_apply_mk
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    (N : Subgroup G) [N.Normal] (g : G) (n : N) :
    quotientConjugationTopologicalAbelianizationMap (G := G) (N := N)
      (QuotientGroup.mk' N g) (TopologicalAbelianization.mk N n) =
        TopologicalAbelianization.mk N ((MulAut.conjNormal g) n)

theorem

quotientConjugationTopologicalAbelianizationMap_mk_eq_one_of_commutator_mem_closure

L186 ↗

ProCGroups.Abelian.quotientConjugationTopologicalAbelianizationMap_mk_eq_one_of_commutator_mem_closure

Documentation

If every commutator correction lies in the closed commutator subgroup, the induced conjugation action on the topological abelianization is trivial.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open CategoryTheory
open scoped Topology commutatorElement
namespace ProCGroups.Abelian
universe u

Lean source · statement

theorem quotientConjugationTopologicalAbelianizationMap_mk_eq_one_of_commutator_mem_closure
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    (N : Subgroup G) [N.Normal] {x : G}
    (hx :
      ∀ n : N,
        (((MulAut.conjNormal x) n) * n⁻¹ : N) ∈ Subgroup.closedCommutator N) :
    quotientConjugationTopologicalAbelianizationMap (G := G) (N := N)
      (QuotientGroup.mk' N x) = 1

theorem

quotientConjugationTopologicalAbelianizationMap_mk_apply_mk_eq_iff

L205 ↗

ProCGroups.Abelian.quotientConjugationTopologicalAbelianizationMap_mk_apply_mk_eq_iff

Documentation

The conjugation action fixes a representative exactly when the correction term lies in the closed commutator subgroup.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open CategoryTheory
open scoped Topology commutatorElement
namespace ProCGroups.Abelian
universe u

Lean source · statement

theorem quotientConjugationTopologicalAbelianizationMap_mk_apply_mk_eq_iff
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    {N : Subgroup G} [N.Normal] {x : G} {n : N} :
    quotientConjugationTopologicalAbelianizationMap (G := G) (N := N)
        (QuotientGroup.mk' N x) (TopologicalAbelianization.mk N n) =
      TopologicalAbelianization.mk N n ↔
    (((MulAut.conjNormal x) n) * n⁻¹ : N) ∈ Subgroup.closedCommutator N

theorem

quotientConjugationTopologicalAbelianizationMap_mk_eq_one_iff

L230 ↗

ProCGroups.Abelian.quotientConjugationTopologicalAbelianizationMap_mk_eq_one_iff

Documentation

The induced conjugation action is trivial exactly when every correction term lies in the closed commutator subgroup.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open CategoryTheory
open scoped Topology commutatorElement
namespace ProCGroups.Abelian
universe u

Lean source · statement

theorem quotientConjugationTopologicalAbelianizationMap_mk_eq_one_iff
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    {N : Subgroup G} [N.Normal] {x : G} :
    quotientConjugationTopologicalAbelianizationMap (G := G) (N := N)
        (QuotientGroup.mk' N x) = 1 ↔
      ∀ n : N,
        (((MulAut.conjNormal x) n) * n⁻¹ : N) ∈ Subgroup.closedCommutator N

theorem

quotientConjugationTopologicalAbelianizationMap_mk_eq_one_of_mem_center

L251 ↗

ProCGroups.Abelian.quotientConjugationTopologicalAbelianizationMap_mk_eq_one_of_mem_center

Documentation

Central elements act trivially on the topological abelianization of a normal subgroup.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open CategoryTheory
open scoped Topology commutatorElement
namespace ProCGroups.Abelian
universe u

Lean source · statement

theorem quotientConjugationTopologicalAbelianizationMap_mk_eq_one_of_mem_center
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    (N : Subgroup G) [N.Normal] {x : G} (hx : x ∈ Subgroup.center G) :
    quotientConjugationTopologicalAbelianizationMap (G := G) (N := N)
      (QuotientGroup.mk' N x) = 1

theorem

quotientConjAbMap_apply_mk_of_commute

L271 ↗

ProCGroups.Abelian.quotientConjAbMap_apply_mk_of_commute

Documentation

If a representative commutes with an element of N, then the induced action fixes its class in the topological abelianization.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open CategoryTheory
open scoped Topology commutatorElement
namespace ProCGroups.Abelian
universe u

Lean source · statement

theorem quotientConjAbMap_apply_mk_of_commute
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    (N : Subgroup G) [N.Normal] {g : G} {x : N}
    (hgx : g * (x : G) = (x : G) * g) :
    quotientConjugationTopologicalAbelianizationMap (G := G) (N := N)
      (QuotientGroup.mk' N g) (TopologicalAbelianization.mk N x) =
        TopologicalAbelianization.mk N x

def

subgroupImageInTopologicalAbelianization

L285 ↗

ProCGroups.Abelian.subgroupImageInTopologicalAbelianization

Documentation

The image of \(S\cap U\) in the topological abelianization of \(U\).

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open CategoryTheory
open scoped Topology commutatorElement
namespace ProCGroups.Abelian
universe u

Lean source · statement

def subgroupImageInTopologicalAbelianization
    {Q : Type u} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
    (S : Subgroup Q) (U : OpenNormalSubgroup Q) :
    Subgroup (TopologicalAbelianization ↥(U : Subgroup Q))

theorem

mem_subgroupImageInTopologicalAbelianization_iff

L296 ↗

ProCGroups.Abelian.mem_subgroupImageInTopologicalAbelianization_iff

Documentation

Membership in the subgroup image inside the topological abelianization is equivalent to the displayed coordinate condition.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open CategoryTheory
open scoped Topology commutatorElement
namespace ProCGroups.Abelian
universe u

Lean source · statement

theorem mem_subgroupImageInTopologicalAbelianization_iff
    {Q : Type u} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
    {S : Subgroup Q} {U : OpenNormalSubgroup Q}
    {y : TopologicalAbelianization ↥(U : Subgroup Q)} :
    y ∈ subgroupImageInTopologicalAbelianization (Q := Q) S U ↔
      ∃ x : ↥(U : Subgroup Q), (x : Q) ∈ S ∧ TopologicalAbelianization.mk _ x = y

theorem

subgroupImageInTopologicalAbelianization_mono_left

L308 ↗

ProCGroups.Abelian.subgroupImageInTopologicalAbelianization_mono_left

Documentation

Enlarging the ambient subgroup \(S\) enlarges its image in the abelianization of \(U\).

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open CategoryTheory
open scoped Topology commutatorElement
namespace ProCGroups.Abelian
universe u

Lean source · statement

theorem subgroupImageInTopologicalAbelianization_mono_left
    {Q : Type u} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
    {S T : Subgroup Q} (hST : S ≤ T) (U : OpenNormalSubgroup Q) :
    subgroupImageInTopologicalAbelianization (Q := Q) S U ≤
      subgroupImageInTopologicalAbelianization (Q := Q) T U

def

topologicalAbelianizationMapOfOpenNormalSubgroupLe

L325 ↗

ProCGroups.Abelian.topologicalAbelianizationMapOfOpenNormalSubgroupLe

Documentation

An inclusion of open normal subgroups induces the corresponding map on topological abelianizations.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open CategoryTheory
open scoped Topology commutatorElement
namespace ProCGroups.Abelian
universe u

Lean source · statement

def topologicalAbelianizationMapOfOpenNormalSubgroupLe
    {Q : Type u} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
    {U V : OpenNormalSubgroup Q} (hUV : (U : Subgroup Q) ≤ (V : Subgroup Q)) :
    TopologicalAbelianization ↥(U : Subgroup Q) →ₜ*
      TopologicalAbelianization ↥(V : Subgroup Q)

theorem

topologicalAbelianizationMapOfOpenNormalSubgroupLe_apply_mk

L340 ↗

ProCGroups.Abelian.topologicalAbelianizationMapOfOpenNormalSubgroupLe_apply_mk

Documentation

The induced map on topological abelianizations sends a representative class to the class of its image.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open CategoryTheory
open scoped Topology commutatorElement
namespace ProCGroups.Abelian
universe u

Lean source · statement

theorem topologicalAbelianizationMapOfOpenNormalSubgroupLe_apply_mk
    {Q : Type u} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
    {U V : OpenNormalSubgroup Q} (hUV : (U : Subgroup Q) ≤ (V : Subgroup Q))
    (x : ↥(U : Subgroup Q)) :
    topologicalAbelianizationMapOfOpenNormalSubgroupLe (Q := Q) hUV
      (TopologicalAbelianization.mk ↥(U : Subgroup Q) x) =
        TopologicalAbelianization.mk ↥(V : Subgroup Q) ⟨x.1, hUV x.2⟩

theorem

subgroupImageInTopologicalAbelianization_map_le_of_openNormalSubgroup_le

L350 ↗

ProCGroups.Abelian.subgroupImageInTopologicalAbelianization_map_le_of_openNormalSubgroup_le

Documentation

Under an inclusion U \(\leq\) V, the image from U maps into the image from V.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open CategoryTheory
open scoped Topology commutatorElement
namespace ProCGroups.Abelian
universe u

Lean source · statement

theorem subgroupImageInTopologicalAbelianization_map_le_of_openNormalSubgroup_le
    {Q : Type u} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
    (S : Subgroup Q) {U V : OpenNormalSubgroup Q}
    (hUV : (U : Subgroup Q) ≤ (V : Subgroup Q)) :
    (subgroupImageInTopologicalAbelianization (Q := Q) S U).map
        (topologicalAbelianizationMapOfOpenNormalSubgroupLe (Q := Q) hUV).toMonoidHom ≤
      subgroupImageInTopologicalAbelianization (Q := Q) S V

theorem

subgroupImageInTopologicalAbelianization_le_comap_of_openNormalSubgroup_le

L368 ↗

ProCGroups.Abelian.subgroupImageInTopologicalAbelianization_le_comap_of_openNormalSubgroup_le

Documentation

Comap form of subgroupImageInTopologicalAbelianization_map_le_of_openNormalSubgroup_le.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open CategoryTheory
open scoped Topology commutatorElement
namespace ProCGroups.Abelian
universe u

Lean source · statement

theorem subgroupImageInTopologicalAbelianization_le_comap_of_openNormalSubgroup_le
    {Q : Type u} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
    (S : Subgroup Q) {U V : OpenNormalSubgroup Q}
    (hUV : (U : Subgroup Q) ≤ (V : Subgroup Q)) :
    subgroupImageInTopologicalAbelianization (Q := Q) S U ≤
      (subgroupImageInTopologicalAbelianization (Q := Q) S V).comap
        (topologicalAbelianizationMapOfOpenNormalSubgroupLe (Q := Q) hUV).toMonoidHom

def

FiniteAbstractIndex

L385 ↗

ProCGroups.Abelian.OpenNormalAbelianizationImage.FiniteAbstractIndex

Documentation

The image of \(S\) has finite abstract index in the topological abelianization of every open normal supergroup of \(K\).

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open CategoryTheory
open scoped Topology commutatorElement
namespace ProCGroups.Abelian
universe u
namespace OpenNormalAbelianizationImage

Lean source · statement

def FiniteAbstractIndex
    {Q : Type u} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
    (S K : Subgroup Q) : Prop

def

closedSubgroupImageInTopologicalAbelianization

L396 ↗

ProCGroups.Abelian.OpenNormalAbelianizationImage.closedSubgroupImageInTopologicalAbelianization

Documentation

The topological closure of the image of \(S \cap U\) in the topological abelianization of \(U\).

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open CategoryTheory
open scoped Topology commutatorElement
namespace ProCGroups.Abelian
universe u
namespace OpenNormalAbelianizationImage

Lean source · statement

def closedSubgroupImageInTopologicalAbelianization
    {Q : Type u} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
    (S : Subgroup Q) (U : OpenNormalSubgroup Q) :
    Subgroup (TopologicalAbelianization ↥(U : Subgroup Q))

theorem

closedSubgroupImageInTopologicalAbelianization_eq_topologicalClosure

L406 ↗

ProCGroups.Abelian.OpenNormalAbelianizationImage.closedSubgroupImageInTopologicalAbelianization_eq_topologicalClosure

Documentation

The image of a closed subgroup in the topological abelianization is the corresponding topological closure.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open CategoryTheory
open scoped Topology commutatorElement
namespace ProCGroups.Abelian
universe u
namespace OpenNormalAbelianizationImage

Lean source · statement

theorem closedSubgroupImageInTopologicalAbelianization_eq_topologicalClosure
    {Q : Type u} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
    (S : Subgroup Q) (U : OpenNormalSubgroup Q) :
    closedSubgroupImageInTopologicalAbelianization (Q := Q) S U =
      (subgroupImageInTopologicalAbelianization (Q := Q) S U).topologicalClosure

def

OpenClosure

L414 ↗

ProCGroups.Abelian.OpenNormalAbelianizationImage.OpenClosure

Documentation

The closed image of \(S\) is open in every open normal supergroup of \(K\).

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open CategoryTheory
open scoped Topology commutatorElement
namespace ProCGroups.Abelian
universe u
namespace OpenNormalAbelianizationImage

Lean source · statement

def OpenClosure
    {Q : Type u} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
    (S K : Subgroup Q) : Prop

def

FiniteTopologicalIndex

L426 ↗

ProCGroups.Abelian.OpenNormalAbelianizationImage.FiniteTopologicalIndex

Documentation

The image of \(S\) is closed and has finite quotient in every open normal supergroup of \(K\).

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open CategoryTheory
open scoped Topology commutatorElement
namespace ProCGroups.Abelian
universe u
namespace OpenNormalAbelianizationImage

Lean source · statement

def FiniteTopologicalIndex
    {Q : Type u} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
    (S K : Subgroup Q) : Prop

theorem

finiteAbstractIndex_of_finiteTopologicalIndex

L439 ↗

ProCGroups.Abelian.OpenNormalAbelianizationImage.finiteAbstractIndex_of_finiteTopologicalIndex

Documentation

Finite topological index includes finite abstract index as its quotient-size component.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open CategoryTheory
open scoped Topology commutatorElement
namespace ProCGroups.Abelian
universe u
namespace OpenNormalAbelianizationImage

Lean source · statement

theorem finiteAbstractIndex_of_finiteTopologicalIndex
    {Q : Type u} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
    {S K : Subgroup Q}
    (h : FiniteTopologicalIndex (Q := Q) S K) :
    FiniteAbstractIndex (Q := Q) S K

Module documentation

Functorial topological abelianization

Declarations