Module

ContinuousMulEquiv.lean

Nyll.ProCGroups.Topologies.ContinuousMulEquiv

7 declarations indexed from sourceView source ↗

Module documentation

Continuous multiplicative equivalences

This file constructs continuous multiplicative equivalences from inverse homomorphisms and from compact-to-Hausdorff bijections. It also gives the topological first-isomorphism equivalence from a quotient by the kernel to the range of a continuous homomorphism.

Imports3

Mathlib.GroupTheory.QuotientGroup.Basic
Mathlib.Topology.Algebra.ContinuousMonoidHom
Nyll.ProCGroups.Topologies.ContinuousMonoidHom

Imported by25

def

ofHomInv

L32 ↗

ProCGroups.ContinuousMulEquiv.ofHomInv

Documentation

Build a continuous multiplicative equivalence from inverse continuous homomorphisms.

Source context 7 commands

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

namespace ProCGroups
namespace ContinuousMulEquiv
universe u v
section
variable {G : Type u} {H : Type v}
variable [Group G] [Group H]
variable [TopologicalSpace G] [TopologicalSpace H]

Lean source · statement

def ofHomInv
    (f : G →ₜ* H) (g : H →ₜ* G)
    (hleft : Function.LeftInverse g f)
    (hright : Function.RightInverse g f) :
    G ≃ₜ* H

theorem

ofHomInv_apply

L47 ↗

ProCGroups.ContinuousMulEquiv.ofHomInv_apply

Documentation

The continuous equivalence is evaluated by the corresponding comparison formula.

Source context 7 commands

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

namespace ProCGroups
namespace ContinuousMulEquiv
universe u v
section
variable {G : Type u} {H : Type v}
variable [Group G] [Group H]
variable [TopologicalSpace G] [TopologicalSpace H]

Lean source · statement

theorem ofHomInv_apply
    (f : G →ₜ* H) (g : H →ₜ* G)
    (hleft : Function.LeftInverse g f)
    (hright : Function.RightInverse g f) (x : G) :
    ofHomInv f g hleft hright x = f x

def

ofBijectiveCompactToT2

L60 ↗

ProCGroups.ContinuousMulEquiv.ofBijectiveCompactToT2

Documentation

Upgrade a bijective continuous homomorphism from a compact topological group to a Hausdorff topological group to a continuous multiplicative equivalence.

Source context 3 commands

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

namespace ProCGroups
namespace ContinuousMulEquiv
universe u v

Lean source · statement

def ofBijectiveCompactToT2
    {G : Type u} {H : Type v}
    [Group G] [TopologicalSpace G]
    [Group H] [TopologicalSpace H]
    [CompactSpace G] [T2Space H]
    (φ : G →* H) (hφcont : Continuous φ)
    (hφ : Function.Bijective φ) :
    G ≃ₜ* H

theorem

ofBijectiveCompactToT2_apply

L79 ↗

ProCGroups.ContinuousMulEquiv.ofBijectiveCompactToT2_apply

Documentation

The composite map is computed pointwise by applying the constituent coordinate formulas in succession.

Source context 3 commands

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

namespace ProCGroups
namespace ContinuousMulEquiv
universe u v

Lean source · statement

theorem ofBijectiveCompactToT2_apply
    {G : Type u} {H : Type v}
    [Group G] [TopologicalSpace G]
    [Group H] [TopologicalSpace H]
    [CompactSpace G] [T2Space H]
    (φ : G →* H) (hφcont : Continuous φ)
    (hφ : Function.Bijective φ) (x : G) :
    ofBijectiveCompactToT2 φ hφcont hφ x = φ x

def

quotientKerContinuousMulEquivRange

L100 ↗

ProCGroups.ContinuousMonoidHom.quotientKerContinuousMulEquivRange

Documentation

The first isomorphism theorem for continuous monoid homomorphisms from a compact group to a Hausdorff group, with the quotient and range carrying their induced topologies.

Source context 3 commands

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

namespace ProCGroups
namespace ContinuousMonoidHom
universe u v

Lean source · statement

def quotientKerContinuousMulEquivRange
    {G : Type u} {H : Type v}
    [Group G] [TopologicalSpace G] [CompactSpace G]
    [Group H] [TopologicalSpace H] [T2Space H]
    (f : G →ₜ* H) :
    (G ⧸ (f.toMonoidHom.ker : Subgroup G)) ≃ₜ* f.toMonoidHom.range

theorem

quotientKerContinuousMulEquivRange_mk

L117 ↗

ProCGroups.ContinuousMonoidHom.quotientKerContinuousMulEquivRange_mk

Documentation

The quotient-by-kernel equivalence to the range sends a representative to its image.

Source context 3 commands

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

namespace ProCGroups
namespace ContinuousMonoidHom
universe u v

Lean source · statement

theorem quotientKerContinuousMulEquivRange_mk
    {G : Type u} {H : Type v}
    [Group G] [TopologicalSpace G] [CompactSpace G]
    [Group H] [TopologicalSpace H] [T2Space H]
    (f : G →ₜ* H) (g : G) :
    quotientKerContinuousMulEquivRange f
        (QuotientGroup.mk' (f.toMonoidHom.ker : Subgroup G) g) =
      f.toMonoidHom.rangeRestrict g

theorem

coe_quotientKerContinuousMulEquivRange_mk

L131 ↗

ProCGroups.ContinuousMonoidHom.coe_quotientKerContinuousMulEquivRange_mk

Documentation

Coercing the quotient-by-kernel equivalence to the codomain gives the original homomorphism value.

Source context 3 commands

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

namespace ProCGroups
namespace ContinuousMonoidHom
universe u v

Lean source · statement

theorem coe_quotientKerContinuousMulEquivRange_mk
    {G : Type u} {H : Type v}
    [Group G] [TopologicalSpace G] [CompactSpace G]
    [Group H] [TopologicalSpace H] [T2Space H]
    (f : G →ₜ* H) (g : G) :
    (quotientKerContinuousMulEquivRange f
        (QuotientGroup.mk' (f.toMonoidHom.ker : Subgroup G) g) : H) = f g

Module documentation

Continuous multiplicative equivalences

Declarations

ofHomInv

ofHomInv_apply

ofBijectiveCompactToT2

ofBijectiveCompactToT2_apply

quotientKerContinuousMulEquivRange

quotientKerContinuousMulEquivRange_mk

coe_quotientKerContinuousMulEquivRange_mk