Yamaguchi Lean 4 Library
ProCGroups.ProC.Quotients.LeftQuotientMaps
ProCGroups/ProC/Quotients/LeftQuotientMaps

ProCGroups.ProC.Quotients.LeftQuotientMaps

8 Theorem | 1 Definition

This module supplies the topological part of the construction. It checks continuity and stagewise neighborhood properties so that the completed object inherits the required topology.

Open this file on GitHub
import
Imported by

Declarations

Definition ProCGroups.ProC.leftQuotientProjection GitHub 
def leftQuotientProjection
    {G : Type u} [Group G] (K H : Subgroup G) (hKH : K ≤ H) :
    G ⧸ K → G ⧸ H :=
  Quotient.map' id <| by
    intro a b hab
    rw [QuotientGroup.leftRel_apply] at hab ⊢
    exact hKH hab

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

Theorem ProCGroups.ProC.leftQuotientProjection_mk GitHub 
@[simp] 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

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

Show proof
Theorem ProCGroups.ProC.continuous_leftQuotientProjection GitHub 
theorem continuous_leftQuotientProjection
    [TopologicalSpace G]
    (K H : Subgroup G) (hKH : K ≤ H) :
    Continuous (leftQuotientProjection K H hKH : G ⧸ K → G ⧸ H)

The natural map between nested left quotients is continuous.

Show proof
Theorem ProCGroups.ProC.leftQuotientProjection_id GitHub 
@[simp] theorem leftQuotientProjection_id
    (K : Subgroup G) :
    leftQuotientProjection K K le_rfl = id

The left-quotient projection to itself is the identity.

Show proof
Theorem ProCGroups.ProC.leftQuotientProjection_comp GitHub 
@[simp] 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)

Left-quotient projections compose along chains of subgroup inclusions.

Show proof
Theorem ProCGroups.ProC.leftQuotientProjection_comp_apply GitHub 
@[simp] 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

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

Show proof
Theorem ProCGroups.ProC.leftQuotientProjection_comp_apply_symm GitHub 
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)

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

Show proof
Theorem ProCGroups.ProC.surjective_leftQuotientProjection GitHub 
theorem surjective_leftQuotientProjection
    (K H : Subgroup G) (hKH : K ≤ H) :
    Function.Surjective (leftQuotientProjection K H hKH : G ⧸ K → G ⧸ H)

The natural map between nested left quotients is surjective.

Show proof
Theorem ProCGroups.ProC.leftQuotientProjection_smul GitHub 
@[simp] 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

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

Show proof