Module

LeftQuotientMaps.lean

Nyll.ProCGroups.ProC.Quotients.LeftQuotientMaps

9 declarations indexed from sourceView source ↗

Module documentation

Maps between left quotients

This file defines the canonical projection \(G/L \to G/H\) for nested subgroups and proves its formula, continuity, surjectivity, functoriality, and compatibility with the quotient action.

Imports1

Nyll.ProCGroups.ProC.Subgroups.Products

Imported by3

def

leftQuotientProjection

L29 ↗

ProCGroups.ProC.leftQuotientProjection

Documentation

The natural projection \(G/K \to G/H\) for closed subgroups K \(\leq\) H is viewed as a quotient-space map on left cosets.

Source context 5 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.ProC
universe u v
open InverseSystems

Lean source · statement

def leftQuotientProjection
    {G : Type u} [Group G] (K H : Subgroup G) (hKH : K ≤ H) :
    G ⧸ K → G ⧸ H

theorem

leftQuotientProjection_mk

L43 ↗

ProCGroups.ProC.leftQuotientProjection_mk

Documentation

The projection on left quotients sends the class of \(g\) modulo \(K\) to the class of \(g\) modulo \(H\).

Source context 6 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.ProC
universe u v
open InverseSystems
variable {G : Type u} [Group G]

Lean source · statement

theorem leftQuotientProjection_mk
    (K H : Subgroup G) (hKH : K ≤ H) (g : G) :
    leftQuotientProjection K H hKH (QuotientGroup.mk (s := K) g) =
      QuotientGroup.mk (s := H) g

theorem

continuous_leftQuotientProjection

L50 ↗

ProCGroups.ProC.continuous_leftQuotientProjection

Documentation

The natural map between nested left quotients is continuous.

Source context 6 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.ProC
universe u v
open InverseSystems
variable {G : Type u} [Group G]

Lean source · statement

theorem continuous_leftQuotientProjection
    [TopologicalSpace G]
    (K H : Subgroup G) (hKH : K ≤ H) :
    Continuous (leftQuotientProjection K H hKH : G ⧸ K → G ⧸ H)

theorem

leftQuotientProjection_id

L59 ↗

ProCGroups.ProC.leftQuotientProjection_id

Documentation

The left-quotient projection to itself is the identity.

Source context 6 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.ProC
universe u v
open InverseSystems
variable {G : Type u} [Group G]

Lean source · statement

theorem leftQuotientProjection_id
    (K : Subgroup G) :
    leftQuotientProjection K K le_rfl = id

theorem

leftQuotientProjection_comp

L68 ↗

ProCGroups.ProC.leftQuotientProjection_comp

Documentation

Left-quotient projections compose along chains of subgroup inclusions.

Source context 6 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.ProC
universe u v
open InverseSystems
variable {G : Type u} [Group G]

Lean source · statement

theorem leftQuotientProjection_comp
    (K H L : Subgroup G) (hKH : K ≤ H) (hHL : H ≤ L) :
    leftQuotientProjection H L hHL ∘ leftQuotientProjection K H hKH =
      leftQuotientProjection K L (hKH.trans hHL)

theorem

leftQuotientProjection_comp_apply

L81 ↗

ProCGroups.ProC.leftQuotientProjection_comp_apply

Documentation

Applying the projection map to a completed element returns its corresponding finite-stage coordinate.

Source context 6 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.ProC
universe u v
open InverseSystems
variable {G : Type u} [Group G]

Lean source · statement

theorem leftQuotientProjection_comp_apply
    (K H L : Subgroup G) (hKH : K ≤ H) (hHL : H ≤ L) (x : G ⧸ K) :
    leftQuotientProjection H L hHL (leftQuotientProjection K H hKH x) =
      leftQuotientProjection K L (hKH.trans hHL) x

theorem

leftQuotientProjection_comp_apply_symm

L88 ↗

ProCGroups.ProC.leftQuotientProjection_comp_apply_symm

Documentation

Symmetric pointwise form of the composition law for left-quotient projections.

Source context 6 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.ProC
universe u v
open InverseSystems
variable {G : Type u} [Group G]

Lean source · statement

theorem leftQuotientProjection_comp_apply_symm
    (K H L : Subgroup G) (hKH : K ≤ H) (hHL : H ≤ L) (x : G ⧸ K) :
    leftQuotientProjection K L (hKH.trans hHL) x =
      leftQuotientProjection H L hHL (leftQuotientProjection K H hKH x)

theorem

surjective_leftQuotientProjection

L95 ↗

ProCGroups.ProC.surjective_leftQuotientProjection

Documentation

The natural map between nested left quotients is surjective.

Source context 6 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.ProC
universe u v
open InverseSystems
variable {G : Type u} [Group G]

Lean source · statement

theorem surjective_leftQuotientProjection
    (K H : Subgroup G) (hKH : K ≤ H) :
    Function.Surjective (leftQuotientProjection K H hKH : G ⧸ K → G ⧸ H)

theorem

leftQuotientProjection_smul

L104 ↗

ProCGroups.ProC.leftQuotientProjection_smul

Documentation

Left-quotient projections are equivariant for the ambient left action of G.

Source context 6 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.ProC
universe u v
open InverseSystems
variable {G : Type u} [Group G]

Lean source · statement

theorem leftQuotientProjection_smul
    (K H : Subgroup G) (hKH : K ≤ H) (g : G) (x : G ⧸ K) :
    leftQuotientProjection K H hKH (g • x) =
      g • leftQuotientProjection K H hKH x

Module documentation

Maps between left quotients

Declarations