---
layout: default
file: "src/Classical/Structures/Group/Cosets.lagda.md"
title: "Classical.Structures.Group.Cosets module"
date: "2026-07-11"
author: "the agda-algebras development team"
---
### 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 `𝑮`, we say that two elements, `x, y` in `𝑮`, lie in the same
**left coset**, and we write `x ∼ y`, 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 and packages the quotient
setoid, `cosetSetoid`{.AgdaFunction}, via the `_/_`{.AgdaFunction} 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 (`≈⇒∼`{.AgdaFunction}, well-definedness of the quotient map), and
left translation by any group element preserves the coset equality
(`∼-congˡ`{.AgdaFunction}, which will be the congruence proof of the action).
<!--
```agda
{-# OPTIONS --without-K --exact-split --safe #-}
module Classical.Structures.Group.Cosets where
open import Agda.Primitive using () renaming ( Set to Type )
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
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
```agda
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 4 _∼_
_∼_ : 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`.
+ Transitivity is closure under products, since `(x ⁻¹ ∙ y) ∙ (y ⁻¹ ∙ z) ≈ x ⁻¹ ∙ z`.
```agda
∼-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
Two facts are needed before the coset relation can be used as an equality.
`≈⇒∼`{.AgdaFunction} says the group's own setoid equality refines the coset
relation, which is what makes the quotient map well defined: equal elements land
in the same coset. `∼-congˡ`{.AgdaFunction} says left translation by any group
element preserves the coset relation, which is what lets `g ∙_` descend to the
coset space.
Both are proved the same way, by supplying `respects`{.AgdaFunction} with an
equality between the relevant `x ⁻¹ ∙ y` witnesses: for `≈⇒∼`{.AgdaFunction} that
witness reduces to `ε` and membership follows from `ε-closed`{.AgdaFunction}, and for
`∼-congˡ`{.AgdaFunction} the `g` cancels, so the translated witness equals the
original. `∼-congˡ`{.AgdaFunction} is what
[Classical.Structures.Group.GSet][] uses to build the coset algebra.
```agda
≈⇒∼ : ∀ {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)
∼-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`{.AgdaBound} is:
whether `x ∼ y` is, definitionally, whether the single product `x ⁻¹ ∙ y` lies in
`H`{.AgdaBound}.[^1]
```agda
∼-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][].
```agda
cosetSetoid : Setoid α ℓ
cosetSetoid = G / ∼-equivalence
```
---
[^1]: This is the Layer-D decision procedure that sits beside the semantic
relation, per the two-layer discipline of [ADR-008].