ProCGroups.Topologies.ContinuousMonoidHom

8 Theorem | 3 Definition

This module develops the maps induced by continuous homomorphisms. It organizes the relevant quotient pullbacks and finite-stage maps, then proves the compatibility statements needed for the completed construction.

Open this file on GitHub

import

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

Imported by

Theorem MonoidHom.continuous_of_isOpen_ker_to_discrete GitHub

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

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

Show proof

Definition ContinuousMonoidHom.subtype GitHub

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

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

Theorem ContinuousMonoidHom.subtype_apply GitHub

@[simp] theorem subtype_apply (K : Subgroup G) (x : K) :
    subtype K x = x

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

Show proof

Definition ContinuousMonoidHom.quotientMk GitHub

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

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

Theorem ContinuousMonoidHom.quotientMk_apply GitHub

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

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

Show proof

Theorem ContinuousMonoidHom.isOpenMap_of_surjective_compact_t2 GitHub

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

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

Show proof

Definition ContinuousMonoidHom.rangeRestrict GitHub

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⟩

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

Theorem ContinuousMonoidHom.rangeRestrict_apply GitHub

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

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

Show proof

Theorem ContinuousMonoidHom.coe_rangeRestrict_apply GitHub

@[simp] theorem coe_rangeRestrict_apply (f : G →ₜ* H) (x : G) :
    (f.rangeRestrict x : H) = f x

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

Show proof

Theorem ContinuousMonoidHom.isClosed_ker GitHub

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

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

Show proof

Theorem ContinuousMonoidHom.isClosed_range GitHub

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

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

Show proof

ProCGroups.Topologies.ContinuousMonoidHom

Declarations