Classical.Structures.Group.Cosets

Cosets and the coset space G/H

This is the Classical.Structures.Group.Cosets module of the Agda Universal Algebra Library.

For a subgroup H of a group 𝑮, two elements lie in the same left coset exactly when x ⁻¹ ∙ y ∈ H. In the setoid discipline the coset space G/H is not a new carrier of equivalence classes but the same carrier with a coarser setoid equality: the relation _∼_ just described.

This module proves _∼_ is an equivalence relation — each axiom is one subgroup closure property plus one line of group arithmetic — and packages the quotient setoid cosetSetoid via the _/_ construction of Setoid.Relations.Quotients.

Two further lemmas prepare the ground for the coset action of Classical.Structures.Group.GSet: the original setoid equality refines the coset equality (≈⇒∼, well-definedness of the quotient map), and left translation by any group element preserves the coset equality (∼-congˡ, which will be the congruence proof of the action).

{-# OPTIONS --cubical-compatible --exact-split --safe #-}

module Classical.Structures.Group.Cosets where

open import Agda.Primitive using () renaming ( Set to Type )

-- Imports from the Agda Standard Library ---------------------------------------
open import Data.Product     using ( _,_ ; proj₁ )
open import Level            using ( Level )
open import Relation.Binary  using ( Setoid ; IsEquivalence )
open import Relation.Nullary using ( Dec )
open import Relation.Unary   using ( Pred ; _∈_ )

import Algebra.Properties.Group as GroupProperties
import Relation.Binary.Reasoning.Setoid as SetoidReasoning

-- Imports from the Agda Universal Algebra Library ------------------------------
open import Overture                              using ( Equivalence )
open import Classical.Bundles.Group               using ( ⟨_⟩ᵍᵖ )
open import Classical.Structures.Group.Basic      using ( Group ; module Group-Op )
open import Classical.Structures.Group.Subgroups  using ( IsSubgroup )
open import Setoid.Algebras.Basic                 using ( Algebra ; 𝕌[_] ; 𝔻[_] )
open import Setoid.Relations.Quotients            using ( _/_ )

The coset relation

module Coset {α ρ : Level} (𝒢 : Group α ρ) {ℓ : Level}
  (H : Pred 𝕌[ proj₁ 𝒢 ] ℓ) (H-isSubgroup : IsSubgroup 𝒢 H)
  where

  private
    𝑮 = proj₁ 𝒢
    G = 𝕌[ 𝑮 ]

  open Setoid 𝔻[ 𝑮 ]            using ( _≈_ )
                                renaming ( refl to ≈refl ; sym to ≈sym ; trans to ≈trans )
  open SetoidReasoning 𝔻[ 𝑮 ]
  open Group-Op 𝒢               using  ( _∙_ ; ε ; _⁻¹ ; ∙-cong ; ⁻¹-cong
                                       ; assoc-law ; invˡ-law )
  open GroupProperties ⟨ 𝒢 ⟩ᵍᵖ  using  ( ⁻¹-involutive ; ⁻¹-anti-homo-∙
                                       ; \\-leftDividesˡ ; \\-leftDividesʳ )
  open IsSubgroup H-isSubgroup  using  ( respects ; ∙-closed ; ε-closed ; ⁻¹-closed )

  infix  _∼_

  -- x and y lie in the same left coset of H when x ⁻¹ ∙ y ∈ H.
  _∼_ : G → G → Type ℓ
  x ∼ y = x ⁻¹ ∙ y ∈ H

_∼_ is an equivalence relation

Reflexivity is ε ∈ H transported along x ⁻¹ ∙ x ≈ ε; symmetry is closure of H under inverses, since (x ⁻¹ ∙ y) ⁻¹ ≈ y ⁻¹ ∙ x; and transitivity is closure under products, since (x ⁻¹ ∙ y) ∙ (y ⁻¹ ∙ z) ≈ x ⁻¹ ∙ z.

  ∼-refl : ∀ {x} → x ∼ x
  ∼-refl {x} = respects (≈sym (invˡ-law x)) ε-closed

  ∼-sym : ∀ {x y} → x ∼ y → y ∼ x
  ∼-sym {x} {y} x∼y = respects inv-eq (⁻¹-closed x∼y)
    where
    inv-eq : (x ⁻¹ ∙ y) ⁻¹ ≈ y ⁻¹ ∙ x
    inv-eq = begin
      (x ⁻¹ ∙ y) ⁻¹     ≈⟨ ⁻¹-anti-homo-∙ (x ⁻¹) y ⟩
      y ⁻¹ ∙ (x ⁻¹) ⁻¹  ≈⟨ ∙-cong ≈refl (⁻¹-involutive x) ⟩
      y ⁻¹ ∙ x          ∎

  ∼-trans : ∀ {x y z} → x ∼ y → y ∼ z → x ∼ z
  ∼-trans {x} {y} {z} x∼y y∼z = respects prod-eq (∙-closed x∼y y∼z)
    where
    prod-eq : (x ⁻¹ ∙ y) ∙ (y ⁻¹ ∙ z) ≈ x ⁻¹ ∙ z
    prod-eq = begin
      (x ⁻¹ ∙ y) ∙ (y ⁻¹ ∙ z)  ≈⟨ assoc-law (x ⁻¹) y (y ⁻¹ ∙ z) ⟩
      x ⁻¹ ∙ (y ∙ (y ⁻¹ ∙ z))  ≈⟨ ∙-cong ≈refl (\\-leftDividesˡ y z) ⟩
      x ⁻¹ ∙ z                 ∎

  ∼-isEquivalence : IsEquivalence _∼_
  ∼-isEquivalence = record { refl = ∼-refl ; sym = ∼-sym ; trans = ∼-trans }

  ∼-equivalence : Equivalence G {ℓ}
  ∼-equivalence = _∼_ , ∼-isEquivalence

Compatibility lemmas

  -- The setoid equality refines the coset equality (the quotient map is well defined).
  ≈⇒∼ : ∀ {x y} → x ≈ y → x ∼ y
  ≈⇒∼ {x} {y} x≈y = respects (≈sym unit-eq) ε-closed
    where
    unit-eq : x ⁻¹ ∙ y ≈ ε
    unit-eq = ≈trans (∙-cong (⁻¹-cong x≈y) ≈refl) (invˡ-law y)

  -- Left translation by any group element preserves the coset equality.
  ∼-congˡ : ∀ g {x y} → x ∼ y → (g ∙ x) ∼ (g ∙ y)
  ∼-congˡ g {x} {y} x∼y = respects (≈sym transl-eq) x∼y
    where
    transl-eq : (g ∙ x) ⁻¹ ∙ (g ∙ y) ≈ x ⁻¹ ∙ y
    transl-eq = begin
      (g ∙ x) ⁻¹ ∙ (g ∙ y)     ≈⟨ ∙-cong (⁻¹-anti-homo-∙ g x) ≈refl ⟩
      x ⁻¹ ∙ g ⁻¹ ∙ (g ∙ y)    ≈⟨ assoc-law (x ⁻¹) (g ⁻¹) (g ∙ y) ⟩
      x ⁻¹ ∙ (g ⁻¹ ∙ (g ∙ y))  ≈⟨ ∙-cong ≈refl (\\-leftDividesʳ g y) ⟩
      x ⁻¹ ∙ y                 ∎

Decidability

The coset relation is decidable exactly when membership in H is: whether x ∼ y is, definitionally, whether the single product x ⁻¹ ∙ y lies in H. This is the Layer-D decision procedure that sits beside the semantic relation, per the two-layer discipline (ADR-008; audit A2 of docs/notes/flrp-wp7-audits.md).

  -- With decidable membership in H, the coset relation is decidable.
  ∼-dec : (∀ x → Dec (x ∈ H)) → ∀ x y → Dec (x ∼ y)
  ∼-dec H-dec x y = H-dec (x ⁻¹ ∙ y)

The quotient setoid G/H

The coset space is the carrier of 𝒢 under the coset equality, assembled by the quotient construction of Setoid.Relations.Quotients.

  cosetSetoid : Setoid α ℓ
  cosetSetoid = G / ∼-equivalence