Module

ContinuousMonoidHom.lean

Nyll.ProCGroups.Topologies.ContinuousMonoidHom

11 declarations indexed from sourceView source ↗

Module documentation

Continuous group homomorphisms

This file provides standard continuous homomorphisms involving subgroups and quotients, proves an open-mapping criterion for compact-to-Hausdorff surjections, and develops range restrictions. Kernels and ranges are shown closed under the expected separation hypotheses.

Imports2

Mathlib.Topology.Algebra.ContinuousMonoidHom
Mathlib.Topology.Algebra.Group.Quotient

Imported by14

theorem

continuous_of_isOpen_ker_to_discrete

L27 ↗

ProCGroups.MonoidHom.continuous_of_isOpen_ker_to_discrete

Documentation

A homomorphism from a topological group to a discrete group is continuous if its kernel is open.

Source context 3 commands

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

namespace ProCGroups
namespace MonoidHom
universe u v

Lean source · statement

theorem continuous_of_isOpen_ker_to_discrete
    {G : Type u} {Q : Type v}
    [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [Group Q] [TopologicalSpace Q] [DiscreteTopology Q]
    (f : G →* Q) (hker : IsOpen ((f.ker : Subgroup G) : Set G)) : Continuous f

def

subtype

L75 ↗

ProCGroups.ContinuousMonoidHom.subtype

Documentation

The inclusion of a subgroup, as a continuous monoid homomorphism for the subtype topology.

Source context 7 commands

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

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

Lean source · full declaration

def subtype (K : Subgroup G) : K →ₜ* G where
  toMonoidHom := K.subtype
  continuous_toFun := continuous_subtype_val

theorem

subtype_apply

L83 ↗

ProCGroups.ContinuousMonoidHom.subtype_apply

Documentation

The continuous homomorphism induced by a subgroup inclusion evaluates to the underlying subgroup element.

Source context 7 commands

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

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

Lean source · statement

theorem subtype_apply (K : Subgroup G) (x : K) :
    subtype K x = x

def

quotientMk

L91 ↗

ProCGroups.ContinuousMonoidHom.quotientMk

Documentation

The quotient projection \(G \to G/K\), bundled as a continuous monoid homomorphism for the quotient topology.

Source context 7 commands

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

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

Lean source · full declaration

def quotientMk (K : Subgroup G) [K.Normal] : G →ₜ* G ⧸ K where
  toMonoidHom := QuotientGroup.mk' K
  continuous_toFun := continuous_quotient_mk'

theorem

quotientMk_apply

L99 ↗

ProCGroups.ContinuousMonoidHom.quotientMk_apply

Documentation

The continuous quotient homomorphism evaluates by taking the quotient class of the input element.

Source context 7 commands

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

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

Lean source · statement

theorem quotientMk_apply (K : Subgroup G) [K.Normal] (x : G) :
    quotientMk K x = QuotientGroup.mk' K x

theorem

isOpenMap_of_surjective_compact_t2

L107 ↗

ProCGroups.ContinuousMonoidHom.isOpenMap_of_surjective_compact_t2

Documentation

A continuous surjective homomorphism from a compact group to a Hausdorff topological group is an open map.

Source context 7 commands

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

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

Lean source · statement

theorem isOpenMap_of_surjective_compact_t2
    [IsTopologicalGroup G] [CompactSpace G] [T2Space H]
    (f : G →ₜ* H) (hf : Function.Surjective f) :
    IsOpenMap f

def

rangeRestrict

L137 ↗

ProCGroups.ContinuousMonoidHom.rangeRestrict

Documentation

A continuous homomorphism restricts to its range with the induced subtype topology.

Source context 7 commands

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

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

Lean source · full declaration

def rangeRestrict (f : G →ₜ* H) : G →ₜ* f.toMonoidHom.range where
  toMonoidHom := f.toMonoidHom.rangeRestrict
  continuous_toFun := Continuous.subtype_mk f.continuous_toFun fun x => ⟨x, rfl⟩

theorem

rangeRestrict_apply

L145 ↗

ProCGroups.ContinuousMonoidHom.rangeRestrict_apply

Documentation

The range-restricted continuous homomorphism evaluates to the image element together with its range-membership certificate.

Source context 7 commands

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

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

Lean source · statement

theorem rangeRestrict_apply (f : G →ₜ* H) (x : G) :
    f.rangeRestrict x = f.toMonoidHom.rangeRestrict x

theorem

coe_rangeRestrict_apply

L153 ↗

ProCGroups.ContinuousMonoidHom.coe_rangeRestrict_apply

Documentation

Coercing the range-restricted homomorphism back to the codomain recovers the original homomorphism value.

Source context 7 commands

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

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

Lean source · statement

theorem coe_rangeRestrict_apply (f : G →ₜ* H) (x : G) :
    (f.rangeRestrict x : H) = f x

theorem

isClosed_ker

L158 ↗

ProCGroups.ContinuousMonoidHom.isClosed_ker

Documentation

The kernel of a continuous homomorphism to a \(T_1\) group is closed.

Source context 7 commands

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

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

Lean source · statement

theorem isClosed_ker [T1Space H] (f : G →ₜ* H) :
    IsClosed ((f.toMonoidHom.ker : Subgroup G) : Set G)

theorem

isClosed_range

L170 ↗

ProCGroups.ContinuousMonoidHom.isClosed_range

Documentation

The range of a continuous homomorphism from a compact space to a Hausdorff space is closed.

Source context 7 commands

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

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

Lean source · statement

theorem isClosed_range [CompactSpace G] [T2Space H] (f : G →ₜ* H) :
    IsClosed ((f.toMonoidHom.range : Subgroup H) : Set H)

Module documentation

Continuous group homomorphisms

Declarations