Module

QuotientMaps.lean

Nyll.ProCGroups.Topologies.QuotientMaps

20 declarations indexed from sourceView source ↗

Module documentation

Continuous maps between group quotients

This file develops algebraic and continuous equivalences induced by surjective homomorphisms, lifts and maps between quotient groups, congruences between quotients, and restrictions to preimages of subgroups.

Imports2

Mathlib.Topology.Algebra.Group.Quotient
Nyll.ProCGroups.Topologies.ContinuousMulEquiv

Imported by27

theorem

comap_eq_of_map_eq_of_ker_le

L34 ↗

ProCGroups.QuotientGroup.comap_eq_of_map_eq_of_ker_le

Documentation

The comap of a quotient subgroup is determined by the representative-level map when the kernel condition holds.

Source context 6 commands

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

open scoped Topology
universe u v
namespace ProCGroups
namespace QuotientGroup
section Algebra
variable {G : Type u} {H : Type v} [Group G] [Group H]

Lean source · statement

theorem comap_eq_of_map_eq_of_ker_le
    (f : G →* H) {N : Subgroup G} {M : Subgroup H}
    (hmap : N.map f = M) (hker : f.ker ≤ N) :
    M.comap f = N

theorem

map_ker_eq_bot_of_map_eq_of_ker_le

L47 ↗

ProCGroups.QuotientGroup.map_ker_eq_bot_of_map_eq_of_ker_le

Documentation

Under the kernel condition, the induced quotient map has trivial kernel for the corresponding representative-level map.

Source context 6 commands

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

open scoped Topology
universe u v
namespace ProCGroups
namespace QuotientGroup
section Algebra
variable {G : Type u} {H : Type v} [Group G] [Group H]

Lean source · statement

theorem map_ker_eq_bot_of_map_eq_of_ker_le
    (f : G →* H) {N : Subgroup G} {M : Subgroup H} [N.Normal] [M.Normal]
    (hNM : N ≤ M.comap f) (hmap : N.map f = M) (hker : f.ker ≤ N) :
    (QuotientGroup.map (N := N) (M := M) (f := f) hNM).ker = ⊥

def

mapMulEquivOfSurjective

L68 ↗

ProCGroups.QuotientGroup.mapMulEquivOfSurjective

Documentation

A surjective homomorphism induces an isomorphism on quotients whenever it maps the source normal subgroup onto the target normal subgroup and its kernel is contained in the source normal subgroup.

Source context 6 commands

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

open scoped Topology
universe u v
namespace ProCGroups
namespace QuotientGroup
section Algebra
variable {G : Type u} {H : Type v} [Group G] [Group H]

Lean source · statement

def mapMulEquivOfSurjective
    (f : G →* H) {N : Subgroup G} {M : Subgroup H} [N.Normal] [M.Normal]
    (hf : Function.Surjective f) (hmap : N.map f = M) (hker : f.ker ≤ N) :
    G ⧸ N ≃* H ⧸ M

theorem

mapMulEquivOfSurjective_apply_mk

L91 ↗

ProCGroups.QuotientGroup.mapMulEquivOfSurjective_apply_mk

Documentation

A surjective homomorphism induces the expected multiplicative equivalence on quotient groups.

Source context 6 commands

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

open scoped Topology
universe u v
namespace ProCGroups
namespace QuotientGroup
section Algebra
variable {G : Type u} {H : Type v} [Group G] [Group H]

Lean source · statement

theorem mapMulEquivOfSurjective_apply_mk
    (f : G →* H) {N : Subgroup G} {M : Subgroup H} [N.Normal] [M.Normal]
    (hf : Function.Surjective f) (hmap : N.map f = M) (hker : f.ker ≤ N) (g : G) :
    mapMulEquivOfSurjective (G := G) (H := H) f hf hmap hker (QuotientGroup.mk' N g) =
      QuotientGroup.mk' M (f g)

def

liftₜ

L107 ↗

ProCGroups.QuotientGroup.liftₜ

Documentation

The lifted continuous quotient map is induced by the quotient universal property.

Source context 8 commands

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

open scoped Topology
universe u v
namespace ProCGroups
namespace QuotientGroup
section Topology
variable {G : Type u} {H : Type v}
variable [Group G] [TopologicalSpace G]
variable [Group H] [TopologicalSpace H]

Lean source · statement

def liftₜ
    (N : Subgroup G) [N.Normal] (f : G →ₜ* H)
    (hN : N ≤ f.toMonoidHom.ker) :
    G ⧸ N →ₜ* H

def

mapContinuousMonoidHom

L121 ↗

ProCGroups.QuotientGroup.mapContinuousMonoidHom

Documentation

The continuous homomorphism induced on quotients by a continuous homomorphism.

Source context 8 commands

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

open scoped Topology
universe u v
namespace ProCGroups
namespace QuotientGroup
section Topology
variable {G : Type u} {H : Type v}
variable [Group G] [TopologicalSpace G]
variable [Group H] [TopologicalSpace H]

Lean source · statement

def mapContinuousMonoidHom
    (f : G →ₜ* H) {N : Subgroup G} {M : Subgroup H} [N.Normal] [M.Normal]
    (hNM : N ≤ M.comap f.toMonoidHom) :
    G ⧸ N →ₜ* H ⧸ M

def

mapₜ

L137 ↗

ProCGroups.QuotientGroup.mapₜ

Documentation

Continuous version of the quotient-group map.

Source context 8 commands

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

open scoped Topology
universe u v
namespace ProCGroups
namespace QuotientGroup
section Topology
variable {G : Type u} {H : Type v}
variable [Group G] [TopologicalSpace G]
variable [Group H] [TopologicalSpace H]

Lean source · statement

def mapₜ
    (N : Subgroup G) (M : Subgroup H) [N.Normal] [M.Normal]
    (f : G →ₜ* H) (hNM : N ≤ M.comap f.toMonoidHom) :
    G ⧸ N →ₜ* H ⧸ M

def

congrₜ

L144 ↗

ProCGroups.QuotientGroup.congrₜ

Documentation

Continuous equivalence between quotients induced by a continuous multiplicative equivalence.

Source context 8 commands

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

open scoped Topology
universe u v
namespace ProCGroups
namespace QuotientGroup
section Topology
variable {G : Type u} {H : Type v}
variable [Group G] [TopologicalSpace G]
variable [Group H] [TopologicalSpace H]

Lean source · statement

def congrₜ
    (N : Subgroup G) (M : Subgroup H) [N.Normal] [M.Normal]
    (e : G ≃ₜ* H) (h : N.map e.toMulEquiv.toMonoidHom = M) :
    G ⧸ N ≃ₜ* H ⧸ M

def

mapContinuousMulEquivOfSurjective

L169 ↗

ProCGroups.QuotientGroup.mapContinuousMulEquivOfSurjective

Documentation

Continuous version of the quotient-group multiplicative equivalence induced by a surjective map. The inverse is continuous by compact-to-Hausdorff automatic continuity, so the result is a topological-group isomorphism when the source quotient is compact and the target quotient is Hausdorff.

Source context 8 commands

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

open scoped Topology
universe u v
namespace ProCGroups
namespace QuotientGroup
section Topology
variable {G : Type u} {H : Type v}
variable [Group G] [TopologicalSpace G]
variable [Group H] [TopologicalSpace H]

Lean source · statement

def mapContinuousMulEquivOfSurjective
    (f : G →ₜ* H) {N : Subgroup G} {M : Subgroup H} [N.Normal] [M.Normal]
    [CompactSpace (G ⧸ N)] [T2Space (H ⧸ M)]
    (hf : Function.Surjective f) (hmap : N.map f.toMonoidHom = M)
    (hker : f.toMonoidHom.ker ≤ N) :
    G ⧸ N ≃ₜ* H ⧸ M

theorem

liftₜ_apply_mk

L198 ↗

ProCGroups.QuotientGroup.liftₜ_apply_mk

Documentation

The lifted continuous quotient map evaluates on quotient classes by applying the underlying map to representatives.

Source context 8 commands

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

open scoped Topology
universe u v
namespace ProCGroups
namespace QuotientGroup
section Topology
variable {G : Type u} {H : Type v}
variable [Group G] [TopologicalSpace G]
variable [Group H] [TopologicalSpace H]

Lean source · statement

theorem liftₜ_apply_mk
    (N : Subgroup G) [N.Normal] (f : G →ₜ* H)
    (hN : N ≤ f.toMonoidHom.ker) (g : G) :
    liftₜ (G := G) (H := H) N f hN (QuotientGroup.mk' N g) = f g

theorem

liftₜ_toMonoidHom

L205 ↗

ProCGroups.QuotientGroup.liftₜ_toMonoidHom

Documentation

The monoid homomorphism underlying liftₜ is the usual quotient lift.

Source context 8 commands

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

open scoped Topology
universe u v
namespace ProCGroups
namespace QuotientGroup
section Topology
variable {G : Type u} {H : Type v}
variable [Group G] [TopologicalSpace G]
variable [Group H] [TopologicalSpace H]

Lean source · statement

theorem liftₜ_toMonoidHom
    (N : Subgroup G) [N.Normal] (f : G →ₜ* H)
    (hN : N ≤ f.toMonoidHom.ker) :
    (liftₜ (G := G) (H := H) N f hN).toMonoidHom =
      QuotientGroup.lift N f.toMonoidHom hN

theorem

mapContinuousMonoidHom_apply_mk

L213 ↗

ProCGroups.QuotientGroup.mapContinuousMonoidHom_apply_mk

Documentation

The induced continuous monoid homomorphism sends a quotient class to the class of its image.

Source context 8 commands

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

open scoped Topology
universe u v
namespace ProCGroups
namespace QuotientGroup
section Topology
variable {G : Type u} {H : Type v}
variable [Group G] [TopologicalSpace G]
variable [Group H] [TopologicalSpace H]

Lean source · statement

theorem mapContinuousMonoidHom_apply_mk
    (f : G →ₜ* H) {N : Subgroup G} {M : Subgroup H} [N.Normal] [M.Normal]
    (hNM : N ≤ M.comap f.toMonoidHom) (g : G) :
    mapContinuousMonoidHom (G := G) (H := H) f (N := N) (M := M) hNM
        (QuotientGroup.mk' N g) =
      QuotientGroup.mk' M (f g)

theorem

mapₜ_apply_mk

L222 ↗

ProCGroups.QuotientGroup.mapₜ_apply_mk

Documentation

The continuous quotient map sends the class of \(g\) to the class of \(f(g)\).

Source context 8 commands

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

open scoped Topology
universe u v
namespace ProCGroups
namespace QuotientGroup
section Topology
variable {G : Type u} {H : Type v}
variable [Group G] [TopologicalSpace G]
variable [Group H] [TopologicalSpace H]

Lean source · statement

theorem mapₜ_apply_mk
    (N : Subgroup G) (M : Subgroup H) [N.Normal] [M.Normal]
    (f : G →ₜ* H) (hNM : N ≤ M.comap f.toMonoidHom) (g : G) :
    mapₜ (G := G) (H := H) N M f hNM (QuotientGroup.mk' N g) =
      QuotientGroup.mk' M (f g)

theorem

mapₜ_toMonoidHom

L230 ↗

ProCGroups.QuotientGroup.mapₜ_toMonoidHom

Documentation

The monoid homomorphism underlying mapₜ is the usual map between quotient groups.

Source context 8 commands

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

open scoped Topology
universe u v
namespace ProCGroups
namespace QuotientGroup
section Topology
variable {G : Type u} {H : Type v}
variable [Group G] [TopologicalSpace G]
variable [Group H] [TopologicalSpace H]

Lean source · statement

theorem mapₜ_toMonoidHom
    (N : Subgroup G) (M : Subgroup H) [N.Normal] [M.Normal]
    (f : G →ₜ* H) (hNM : N ≤ M.comap f.toMonoidHom) :
    (mapₜ (G := G) (H := H) N M f hNM).toMonoidHom =
      QuotientGroup.map (N := N) (M := M) (f := f.toMonoidHom) hNM

theorem

congrₜ_apply_mk

L241 ↗

ProCGroups.QuotientGroup.congrₜ_apply_mk

Documentation

The continuous quotient congruence map evaluates on quotient classes by applying the underlying map to representatives.

Source context 8 commands

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

open scoped Topology
universe u v
namespace ProCGroups
namespace QuotientGroup
section Topology
variable {G : Type u} {H : Type v}
variable [Group G] [TopologicalSpace G]
variable [Group H] [TopologicalSpace H]

Lean source · statement

theorem congrₜ_apply_mk
    (N : Subgroup G) (M : Subgroup H) [N.Normal] [M.Normal]
    (e : G ≃ₜ* H) (h : N.map e.toMulEquiv.toMonoidHom = M) (g : G) :
    congrₜ (G := G) (H := H) N M e h (QuotientGroup.mk' N g) =
      QuotientGroup.mk' M (e g)

theorem

mapContinuousMulEquivOfSurjective_apply_mk

L252 ↗

ProCGroups.QuotientGroup.mapContinuousMulEquivOfSurjective_apply_mk

Documentation

The induced continuous multiplicative equivalence sends a quotient class to the class of its image.

Source context 8 commands

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

open scoped Topology
universe u v
namespace ProCGroups
namespace QuotientGroup
section Topology
variable {G : Type u} {H : Type v}
variable [Group G] [TopologicalSpace G]
variable [Group H] [TopologicalSpace H]

Lean source · statement

theorem mapContinuousMulEquivOfSurjective_apply_mk
    (f : G →ₜ* H) {N : Subgroup G} {M : Subgroup H} [N.Normal] [M.Normal]
    [CompactSpace (G ⧸ N)] [T2Space (H ⧸ M)]
    (hf : Function.Surjective f) (hmap : N.map f.toMonoidHom = M)
    (hker : f.toMonoidHom.ker ≤ N) (g : G) :
    mapContinuousMulEquivOfSurjective (G := G) (H := H) f hf hmap hker
        (QuotientGroup.mk' N g) =
      QuotientGroup.mk' M (f g)

def

restrictPreimage

L275 ↗

ProCGroups.ContinuousMonoidHom.restrictPreimage

Documentation

A continuous homomorphism restricts to the preimage of a subgroup of the target.

Source context 8 commands

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

open scoped Topology
universe u v
namespace ProCGroups
namespace ContinuousMonoidHom
section RestrictPreimage
variable {G : Type u} {Q : Type v}
variable [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
variable [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]

Lean source · statement

def restrictPreimage (f : G →ₜ* Q) (H : Subgroup Q) :
    (H.comap f.toMonoidHom) →ₜ* H

theorem

restrictPreimage_surjective

L294 ↗

ProCGroups.ContinuousMonoidHom.restrictPreimage_surjective

Documentation

The restriction to a subgroup preimage is surjective if the original map is surjective.

Source context 9 commands

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

open scoped Topology
universe u v
namespace ProCGroups
namespace ContinuousMonoidHom
section RestrictPreimage
variable {G : Type u} {Q : Type v}
variable [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
variable [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
omit [IsTopologicalGroup G] [IsTopologicalGroup Q] in

Lean source · statement

theorem restrictPreimage_surjective (f : G →ₜ* Q) (hf : Function.Surjective f)
    (H : Subgroup Q) :
    Function.Surjective (restrictPreimage f H)

theorem

restrictPreimage_eq_one_iff

L306 ↗

ProCGroups.ContinuousMonoidHom.restrictPreimage_eq_one_iff

Documentation

The kernel of the restriction to a subgroup preimage is detected by the ambient map.

Source context 9 commands

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

open scoped Topology
universe u v
namespace ProCGroups
namespace ContinuousMonoidHom
section RestrictPreimage
variable {G : Type u} {Q : Type v}
variable [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
variable [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
omit [IsTopologicalGroup G] [IsTopologicalGroup Q] in

Lean source · statement

theorem restrictPreimage_eq_one_iff {f : G →ₜ* Q} {H : Subgroup Q}
    {x : H.comap f.toMonoidHom} :
    restrictPreimage f H x = 1 ↔ f x.1 = 1

def

preimageSubgroupQuotientMulEquivOfSurjective

L319 ↗

ProCGroups.ContinuousMonoidHom.preimageSubgroupQuotientMulEquivOfSurjective

Documentation

If the restricted map sends \(N\) onto \(M\) and its kernel is contained in \(N\), then the induced quotient map is an isomorphism.

Source context 8 commands

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

open scoped Topology
universe u v
namespace ProCGroups
namespace ContinuousMonoidHom
section RestrictPreimage
variable {G : Type u} {Q : Type v}
variable [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
variable [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]

Lean source · statement

def preimageSubgroupQuotientMulEquivOfSurjective
    (f : G →ₜ* Q) (hf : Function.Surjective f) (H : Subgroup Q)
    {N : Subgroup (H.comap f.toMonoidHom)} {M : Subgroup H} [N.Normal] [M.Normal]
    (hmap : N.map (restrictPreimage f H).toMonoidHom = M)
    (hker : (restrictPreimage f H).toMonoidHom.ker ≤ N) :
    (H.comap f.toMonoidHom) ⧸ N ≃* H ⧸ M

Module documentation

Continuous maps between group quotients

Declarations