---
layout: default
file: "src/Classical/Structures/Group/Congruences.lagda.md"
title: "Classical.Structures.Group.Congruences module"
date: "2026-07-26"
author: "the agda-algebras development team"
---
### Normal subgroups and congruences of a group
This is the [Classical.Structures.Group.Congruences][] module of the [Agda Universal Algebra Library][].
The normal subgroups of a group `𝒢` correspond to the congruences of the underlying
`Sig-Group`-algebra. This module establishes that correspondence as an **order
isomorphism of posets**, between the congruence poset `(Con 𝑮 ℓ , ≑ , ⊑)` of
[Setoid.Congruences.Lattice][] and the poset `(NormalSubgroup ℓ , ≈ⁿ , ≤ⁿ)` of normal
subgroups under inclusion, which is built here.
Both sides carry more structure than a poset: at the absorbing level `L` the
congruences form a complete lattice ([Setoid.Congruences.CompleteLattice][]). The
corresponding **isomorphism of complete lattices** is
[Classical.Structures.Group.NormalSubgroupLattice][], which stands on the poset
isomorphism proved here. The split is deliberate: the correspondence below holds at
*every* relation level, whereas a lattice needs the single absorbing level at which
the join — a *generated* congruence — stays put, so bundling them would have narrowed
the theorem to the level the lattice happens to need.
The correspondence has two mutually inverse, order-preserving maps.
+ **`N ↦ θ_N`** (`congruenceOf`{.AgdaFunction}). A normal subgroup `N` maps to the
relation `NormalRel`{.AgdaFunction}` N`, defined by `x θ_N y ⟺ x ∙ y ⁻¹ ∈ N`.
We prove that this is an equivalence containing the setoid equality (for which
`N`{.AgdaBound} being an equality-respecting subgroup is enough) and
compatible with the three operations of `Sig-Group`{.AgdaFunction}, which is where
normality is consumed.
+ **`θ ↦ N_θ`** (`normalOf`{.AgdaFunction}). A congruence `θ`{.AgdaBound} maps to
the `θ`-class of the identity; we define the latter as
`IdentityClass`{.AgdaFunction} `θ`{.AgdaBound}, which represents the predicate
`{ x ∣ x θ ε }`. We prove it is a normal, equality-respecting subgroup.
The two maps are monotone and mutually inverse — up to `≑`{.AgdaFunction} on
congruences and mutual inclusion on normal subgroups — so together they are an
`OrderIso`{.AgdaRecord} of [Order.Iso][].
This is the bridge that `Classical.Structures.Group.MinimalNormal` was written
without: it lets us apply the library's `IsSubdirectlyIrreducible`{.AgdaFunction} of
[Setoid.Congruences.Monolith][] — a statement about `Con 𝑨`{.AgdaFunction} — to a
group, whose subdirect irreducibility the group theorist states as "there is a
least nontrivial normal subgroup". The final step of that identification,
`HasMonolithᵍ → HasMonolith`, is deliberately *not* taken here; see **What this module
does not do** below.
Four points about the formal statement deserve to be recorded up front, because in each
case the informal slogan "congruences are normal subgroups" conceals a choice that the
mechanized version has to make.
+ **The correspondence is level-uniform, not level-collapsing**. It relates
`Con 𝑮 ℓ`{.AgdaFunction} to `NormalSubgroup ℓ`{.AgdaFunction} for each *fixed*
relation level `ℓ`{.AgdaBound}, since `NormalRel`{.AgdaFunction} of a `Pred G ℓ` is
a `BinaryRel G ℓ` and `IdentityClass`{.AgdaFunction} of a `Con 𝑮 ℓ` is a
`Pred G ℓ`. It says nothing about congruences at one level versus normal subgroups
at another. Three instances matter downstream: `ℓ = ρ`, where the congruence side
is the `Con 𝑮 ρ` of `IsMonolith`{.AgdaRecord} and the subgroup side contains
`trivialSubgroup`{.AgdaFunction}, itself a `Subgroup ρ`; `ℓ = α ⊔ ρ ⊔ ℓ₀`, the
absorbing level of the congruence lattice, which is where
[Classical.Structures.Group.NormalSubgroupLattice][] instantiates it; and
`ℓ = α ⊔ ℓ₀`, the predicate level `L` at which `GroupSublattice 𝒢 ℓ₀`{.AgdaModule}
of [Classical.Structures.Group.SubgroupLattice][] holds its elements, for a
consumer that wants to compose with the *subgroup* lattice.
+ **Equality on each side is mutual containment, not propositional equality**. On the
congruence side this is `_≑_`{.AgdaFunction} of [Setoid.Congruences.Lattice][], for
the reasons given there (upgrading it would need propositional extensionality, which
`--safe --cubical-compatible` does not provide); on the subgroup side we take the
matching `_≈ⁿ_`{.AgdaFunction}. So `to∘from`{.AgdaField} and `from∘to`{.AgdaField}
are *bi-implications of membership*, not equalities of predicates.
+ **The round trip on subgroups uses the `respects`{.AgdaField} field**. Recovering
`N`{.AgdaBound} from `θ_N` produces `{ x ∣ x ∙ ε ⁻¹ ∈ N }`, and identifying that with
`N`{.AgdaBound} moves membership across `x ∙ ε ⁻¹ ≈ x`. A normal *subuniverse* that
does not respect the setoid equality therefore need not be recovered by the round
trip, exactly as in the respecting-interval finding of [FLRP.Bridge][]. This is why
`NormalSubgroup`{.AgdaFunction} is built on `IsSubgroup`{.AgdaRecord} (which carries
`respects`{.AgdaField}) rather than on bare `Subuniverses`{.AgdaFunction}.
+ **Normality is consumed only by compatibility, and it is consumed exactly**. For an
arbitrary equality-respecting subgroup `N`{.AgdaBound}, `NormalRel N`{.AgdaFunction}
is already an equivalence relation containing `_≈_`{.AgdaFunction}; this is
`SubgroupRel`{.AgdaModule} below, and it holds with no normality hypothesis. What
needs normality is compatibility with `∙-Op`{.AgdaInductiveConstructor} and
`⁻¹-Op`{.AgdaInductiveConstructor}, so the separation is stated rather than folded
into one monolithic lemma — and the converse `congruence→normal`{.AgdaFunction} is
proved, so that "the correspondence is with the *normal* subgroups" is a theorem of
the module and not a claim its prose makes on the development's behalf.
**On the choice of relation**. `x ∙ y ⁻¹ ∈ N` is the *right*-coset relation of
`N`{.AgdaBound}, whereas `Coset._∼_`{.AgdaFunction} of
[Classical.Structures.Group.Cosets][] — the relation [FLRP.Bridge][] uses — is the
*left*-coset relation `x ⁻¹ ∙ y ∈ N`. For a general subgroup the two need not agree;
for a normal subgroup they do, which we prove (`rel→coset`{.AgdaFunction},
`coset→rel`{.AgdaFunction}) rather than assume, so that either presentation may be used
downstream.
**What this module does not do**. Issue #508 also asks that
`HasMonolithᵍ`{.AgdaFunction} of `Classical.Structures.Group.MinimalNormal` be
transported to `HasMonolith`{.AgdaFunction}, that the `ᵍ` superscript be retired, and
that `𝒢₂` of `FLRP.Reductions` be restated. Those steps are held back until the pull
request that introduces `MinimalNormal` lands; everything above is independent of them.
The `Nonzero`{.AgdaFunction}/nontriviality equivalences proved here
(`nonzero→nontrivial`{.AgdaFunction} and friends) are precisely the ingredient that
transport will need beyond the isomorphism itself.
<!--
```agda
{-# OPTIONS --cubical-compatible --exact-split --safe #-}
module Classical.Structures.Group.Congruences where
open import Agda.Primitive using () renaming ( Set to Type )
open import Data.Fin.Patterns using ( 0F ; 1F )
open import Data.Product using ( _,_ ; _×_ ; Σ-syntax ; proj₁ ; swap )
open import Level using ( Level ; _⊔_ ; suc )
open import Relation.Binary using ( Setoid ; IsEquivalence
; IsPartialOrder )
renaming ( Rel to BinaryRel )
open import Relation.Binary.Bundles using ( Poset )
open import Relation.Binary.Definitions using ( _Respects_ )
open import Relation.Nullary using ( ¬_ )
open import Relation.Unary using ( Pred ; _∈_ ; _⊆_ )
import Algebra.Properties.Group as GroupProperties
import Relation.Binary.Reasoning.Setoid as SetoidReasoning
open import Classical.Bundles.Group using ( ⟨_⟩ᵍᵖ )
open import Classical.Signatures.Group using ( ∙-Op ; ε-Op ; ⁻¹-Op )
open import Classical.Structures.Group.Basic using ( Group ; module Group-Op )
open import Classical.Structures.Group.Conjugation using ( module Conjugate )
open import Classical.Structures.Group.Cosets using ( module Coset )
open import Classical.Structures.Group.Subgroups using ( IsSubgroup ; mkIsSubgroup
; trivialSubgroup
; interp-tuple-∙
; interp-tuple-ε
; interp-tuple-⁻¹ )
open import Order.Iso using ( OrderIso )
open import Setoid.Algebras.Basic using ( 𝕌[_] ; 𝔻[_] )
open import Setoid.Congruences.Basic using ( Con ; IsCongruence ; mkcon
; _∣≈_ ; is-compatible
; is-equivalence ; reflexive )
open import Setoid.Congruences.Lattice using ( _≑_ )
renaming ( _⊆_ to _⊑_ )
open import Setoid.Congruences.Monolith using ( BelowDiagonal ; Nonzero )
private variable α ρ ℓ : Level
```
-->
#### The ambient group
Everything below is developed inside one parameterized module, so that the group, its
carrier, its curried operations, and the conjugation vocabulary are fixed once.
```agda
module GroupCongruences {α ρ : Level} (𝒢 : Group α ρ) where
private
𝑮 = proj₁ 𝒢
G = 𝕌[ 𝑮 ]
open Setoid 𝔻[ 𝑮 ] using ( _≈_ )
renaming ( refl to ≈refl ; sym to ≈sym ; trans to ≈trans )
open SetoidReasoning 𝔻[ 𝑮 ]
open Group-Op 𝒢 using ( _∙_ ; ε ; _⁻¹ ; ∙-cong ; assoc-law
; idˡ-law ; idʳ-law ; invˡ-law ; invʳ-law )
open GroupProperties ⟨ 𝒢 ⟩ᵍᵖ using ( ε⁻¹≈ε ; ⁻¹-involutive ; ⁻¹-anti-homo-∙
; \\-leftDividesʳ )
open Conjugate 𝒢 using ( conj-syntax ; conj-ε ; IsNormal )
```
#### Four facts of group arithmetic
The correspondence rests on four small identities, each named so that no proof below
has to inline an equational chain about them. The first two say that `x ∙ y ⁻¹ ≈ ε`
is *equivalent* to `x ≈ y` — this is what makes the relation `x ∙ y ⁻¹ ∈ N` collapse to
the setoid equality exactly when `N` is trivial. The third is right-cancellation in the
form the round trip needs, and the fourth is the unit law that identifies `x ∙ ε ⁻¹`
with `x`.
```agda
∙⁻¹≈ε→≈ : ∀ {x y} → x ∙ y ⁻¹ ≈ ε → x ≈ y
∙⁻¹≈ε→≈ {x} {y} h = begin
x ≈˘⟨ idʳ-law x ⟩
x ∙ ε ≈˘⟨ ∙-cong ≈refl (invˡ-law y) ⟩
x ∙ (y ⁻¹ ∙ y) ≈˘⟨ assoc-law x (y ⁻¹) y ⟩
x ∙ y ⁻¹ ∙ y ≈⟨ ∙-cong h ≈refl ⟩
ε ∙ y ≈⟨ idˡ-law y ⟩
y ∎
≈→∙⁻¹≈ε : ∀ {x y} → x ≈ y → x ∙ y ⁻¹ ≈ ε
≈→∙⁻¹≈ε {x} {y} x≈y = ≈trans (∙-cong x≈y ≈refl) (invʳ-law y)
∙⁻¹∙ : ∀ x y → x ∙ y ⁻¹ ∙ y ≈ x
∙⁻¹∙ x y = begin
x ∙ y ⁻¹ ∙ y ≈⟨ assoc-law x (y ⁻¹) y ⟩
x ∙ (y ⁻¹ ∙ y) ≈⟨ ∙-cong ≈refl (invˡ-law y) ⟩
x ∙ ε ≈⟨ idʳ-law x ⟩
x ∎
∙ε⁻¹ : ∀ x → x ∙ ε ⁻¹ ≈ x
∙ε⁻¹ x = ≈trans (∙-cong ≈refl ε⁻¹≈ε) (idʳ-law x)
```
#### Normal subgroups as an ordered object
A **normal subgroup** of `𝒢`{.AgdaBound} at predicate level `ℓ`{.AgdaBound} is a
predicate on the carrier together with a proof that it is an equality-respecting
subgroup and a proof that it is closed under conjugation. This is
`Subgroup`{.AgdaFunction} of [Classical.Structures.Group.Subgroups][] with
`IsNormal`{.AgdaFunction} of [Classical.Structures.Group.Conjugation][] adjoined; it is
introduced here rather than there because normality is the *only* extra datum the
correspondence needs, and no earlier module had cause to bundle it.
Normal subgroups are ordered by inclusion of the underlying predicates, with equality
mutual inclusion — the same shape as `_⊑_`{.AgdaFunction} and `_≑_`{.AgdaFunction} on
congruences, so that the isomorphism below can be stated without any bridging
construction on either side.
```agda
NormalSubgroup : (ℓ : Level) → Type (α ⊔ ρ ⊔ suc ℓ)
NormalSubgroup ℓ = Σ[ N ∈ Pred G ℓ ] (IsSubgroup 𝒢 N × IsNormal N)
set : NormalSubgroup ℓ → Pred G ℓ
set (N , _ , _) = N
set-isSubgroup : (𝑵 : NormalSubgroup ℓ) → IsSubgroup 𝒢 (set 𝑵)
set-isSubgroup (_ , isSubgroup , _) = isSubgroup
set-normal : (𝑵 : NormalSubgroup ℓ) → IsNormal (set 𝑵)
set-normal (_ , _ , isNormal) = isNormal
infix 4 _≤ⁿ_ _≈ⁿ_
_≤ⁿ_ : NormalSubgroup ℓ → NormalSubgroup ℓ → Type (α ⊔ ℓ)
𝑴 ≤ⁿ 𝑵 = set 𝑴 ⊆ set 𝑵
_≈ⁿ_ : NormalSubgroup ℓ → NormalSubgroup ℓ → Type (α ⊔ ℓ)
𝑴 ≈ⁿ 𝑵 = 𝑴 ≤ⁿ 𝑵 × 𝑵 ≤ⁿ 𝑴
```
Calling the correspondence an *order* isomorphism presupposes that both sides really
are ordered, so the partial-order laws are proved rather than assumed. They are the
laws of `_⊆_`{.AgdaFunction} on predicates, and antisymmetry holds by construction:
`_≈ⁿ_`{.AgdaFunction} *is* mutual inclusion. This mirrors
`⊆-isPartialOrder`{.AgdaFunction} and `Con-Poset`{.AgdaFunction} on the congruence
side, down to the same implicit-argument discipline — `_≤ⁿ_`{.AgdaFunction} is a
defined relation, not an injective type former, so Agda cannot recover the endpoint
arguments of the helper lemmas from the expected field types and they are forwarded by
hand.
```agda
≤ⁿ-refl : {𝑵 : NormalSubgroup ℓ} → 𝑵 ≤ⁿ 𝑵
≤ⁿ-refl p = p
≤ⁿ-trans : {𝑳 𝑴 𝑵 : NormalSubgroup ℓ} → 𝑳 ≤ⁿ 𝑴 → 𝑴 ≤ⁿ 𝑵 → 𝑳 ≤ⁿ 𝑵
≤ⁿ-trans 𝑳≤𝑴 𝑴≤𝑵 p = 𝑴≤𝑵 (𝑳≤𝑴 p)
≈ⁿ-refl : {𝑵 : NormalSubgroup ℓ} → 𝑵 ≈ⁿ 𝑵
≈ⁿ-refl = (λ p → p) , (λ p → p)
≈ⁿ-sym : {𝑴 𝑵 : NormalSubgroup ℓ} → 𝑴 ≈ⁿ 𝑵 → 𝑵 ≈ⁿ 𝑴
≈ⁿ-sym = swap
≈ⁿ-trans : {𝑳 𝑴 𝑵 : NormalSubgroup ℓ} → 𝑳 ≈ⁿ 𝑴 → 𝑴 ≈ⁿ 𝑵 → 𝑳 ≈ⁿ 𝑵
≈ⁿ-trans (𝑳≤𝑴 , 𝑴≤𝑳) (𝑴≤𝑵 , 𝑵≤𝑴) = (λ p → 𝑴≤𝑵 (𝑳≤𝑴 p)) , (λ p → 𝑴≤𝑳 (𝑵≤𝑴 p))
≈ⁿ-isEquivalence : IsEquivalence (_≈ⁿ_ {ℓ})
≈ⁿ-isEquivalence {ℓ} = record
{ refl = λ {𝑵} → ≈ⁿ-refl {ℓ} {𝑵}
; sym = λ {𝑴} {𝑵} → ≈ⁿ-sym {ℓ} {𝑴} {𝑵}
; trans = λ {𝑳} {𝑴} {𝑵} → ≈ⁿ-trans {ℓ} {𝑳} {𝑴} {𝑵}
}
≤ⁿ-isPartialOrder : IsPartialOrder (_≈ⁿ_ {ℓ}) _≤ⁿ_
≤ⁿ-isPartialOrder {ℓ} = record
{ isPreorder = record { isEquivalence = ≈ⁿ-isEquivalence {ℓ}
; reflexive = proj₁
; trans = λ {𝑳} {𝑴} {𝑵} → ≤ⁿ-trans {ℓ} {𝑳} {𝑴} {𝑵}
}
; antisym = _,_
}
NormalSubgroup-Poset : (ℓ : Level) → Poset (α ⊔ ρ ⊔ suc ℓ) (α ⊔ ℓ) (α ⊔ ℓ)
NormalSubgroup-Poset ℓ = record { Carrier = NormalSubgroup ℓ
; _≈_ = _≈ⁿ_
; _≤_ = _≤ⁿ_
; isPartialOrder = ≤ⁿ-isPartialOrder
}
```
#### The relation attached to a subgroup
`NormalRel N`{.AgdaFunction} is the relation "`x` and `y` differ by an element of
`N`", written with the *right* quotient `x ∙ y ⁻¹`. It is defined for an arbitrary
predicate, so that the hypotheses each of its properties needs can be stated exactly.
```agda
NormalRel : Pred G ℓ → BinaryRel G ℓ
NormalRel N x y = x ∙ y ⁻¹ ∈ N
```
For an equality-respecting subgroup `N`{.AgdaBound} — with no normality hypothesis —
`NormalRel N`{.AgdaFunction} is an equivalence relation that contains the setoid
equality. Each clause is one closure property of `N`{.AgdaBound} transported along one
line of group arithmetic, exactly as in `Coset`{.AgdaModule} of
[Classical.Structures.Group.Cosets][] for the left-handed relation.
```agda
module SubgroupRel {ℓ : Level} (N : Pred G ℓ) (N-sg : IsSubgroup 𝒢 N) where
open IsSubgroup N-sg using ( respects ; ∙-closed ; ε-closed ; ⁻¹-closed )
infix 4 _∼_
_∼_ : BinaryRel G ℓ
_∼_ = NormalRel N
∼-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 (⁻¹-involutive y) ≈refl ⟩
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 }
≈⇒∼ : ∀ {x y} → x ≈ y → x ∼ y
≈⇒∼ x≈y = respects (≈sym (≈→∙⁻¹≈ε x≈y)) ε-closed
∼-resp : ∀ {x x' y y'} → x ≈ x' → y ≈ y' → x ∼ y → x' ∼ y'
∼-resp x≈x' y≈y' p = ∼-trans (∼-trans (≈⇒∼ (≈sym x≈x')) p) (≈⇒∼ y≈y')
```
#### From a normal subgroup to a congruence
Adding normality makes the relation compatible with the three operations of
`Sig-Group`{.AgdaFunction}, hence a congruence.
Compatibility with `∙-Op`{.AgdaInductiveConstructor} is the substantive clause and the
only one that uses normality in an essential way: from `x ∙ y ⁻¹ ∈ N` and
`u ∙ v ⁻¹ ∈ N` we must produce `(x ∙ u) ∙ (y ∙ v) ⁻¹ ∈ N`, and the two given elements do
not multiply to it — one of them must first be *moved past* `x`{.AgdaBound}, which is
precisely conjugation. Compatibility with `⁻¹-Op`{.AgdaInductiveConstructor} is one
conjugation as well; with `ε-Op`{.AgdaInductiveConstructor} it is reflexivity.
```agda
module NormalCon {ℓ : Level} (𝑵 : NormalSubgroup ℓ) where
private
N : Pred G ℓ
N = set 𝑵
open IsSubgroup (set-isSubgroup 𝑵) using ( respects ; ∙-closed )
open SubgroupRel N (set-isSubgroup 𝑵) public
normal : IsNormal N
normal = set-normal 𝑵
∼-∙ : ∀ {x y u v} → x ∼ y → u ∼ v → (x ∙ u) ∼ (y ∙ v)
∼-∙ {x} {y} {u} {v} p q = respects step (∙-closed (normal x q) p)
where
step : x ∙ (u ∙ v ⁻¹) ∙ x ⁻¹ ∙ (x ∙ y ⁻¹) ≈ x ∙ u ∙ (y ∙ v) ⁻¹
step = begin
x ∙ (u ∙ v ⁻¹) ∙ x ⁻¹ ∙ (x ∙ y ⁻¹) ≈⟨ assoc-law (x ∙ (u ∙ v ⁻¹)) (x ⁻¹) (x ∙ y ⁻¹) ⟩
x ∙ (u ∙ v ⁻¹) ∙ (x ⁻¹ ∙ (x ∙ y ⁻¹)) ≈⟨ ∙-cong ≈refl (\\-leftDividesʳ x (y ⁻¹)) ⟩
x ∙ (u ∙ v ⁻¹) ∙ y ⁻¹ ≈˘⟨ ∙-cong (assoc-law x u (v ⁻¹)) ≈refl ⟩
x ∙ u ∙ v ⁻¹ ∙ y ⁻¹ ≈⟨ assoc-law (x ∙ u) (v ⁻¹) (y ⁻¹) ⟩
x ∙ u ∙ (v ⁻¹ ∙ y ⁻¹) ≈˘⟨ ∙-cong ≈refl (⁻¹-anti-homo-∙ y v) ⟩
x ∙ u ∙ (y ∙ v) ⁻¹ ∎
∼-⁻¹ : ∀ {x y} → x ∼ y → x ⁻¹ ∼ y ⁻¹
∼-⁻¹ {x} {y} p = ∼-sym (respects step (normal (x ⁻¹) p))
where
step : x ⁻¹ ∙ (x ∙ y ⁻¹) ∙ (x ⁻¹) ⁻¹ ≈ y ⁻¹ ∙ (x ⁻¹) ⁻¹
step = ∙-cong (\\-leftDividesʳ x (y ⁻¹)) ≈refl
∼-compatible : 𝑮 ∣≈ _∼_
∼-compatible ∙-Op {u} {v} p = ∼-resp (≈sym (interp-tuple-∙ 𝒢 u))
(≈sym (interp-tuple-∙ 𝒢 v))
(∼-∙ (p 0F) (p 1F))
∼-compatible ε-Op {u} {v} p = ∼-resp (≈sym (interp-tuple-ε 𝒢 u))
(≈sym (interp-tuple-ε 𝒢 v))
∼-refl
∼-compatible ⁻¹-Op {u} {v} p = ∼-resp (≈sym (interp-tuple-⁻¹ 𝒢 u))
(≈sym (interp-tuple-⁻¹ 𝒢 v))
(∼-⁻¹ (p 0F))
∼-isCongruence : IsCongruence 𝑮 _∼_
∼-isCongruence = mkcon ≈⇒∼ ∼-isEquivalence ∼-compatible
```
For a normal subgroup the right-handed relation used here agrees with the left-handed
coset relation `Coset._∼_`{.AgdaFunction} of [Classical.Structures.Group.Cosets][],
which is the one [FLRP.Bridge][] builds on. Both directions are one application of
`∼-⁻¹`{.AgdaFunction} followed by an involutivity rewrite, so nothing about the
development depends on which of the two presentations a consumer prefers.
```agda
rel→coset : ∀ {x y} → x ∼ y → Coset._∼_ 𝒢 N (set-isSubgroup 𝑵) x y
rel→coset {x} {y} p = respects (∙-cong ≈refl (⁻¹-involutive y)) (∼-⁻¹ p)
coset→rel : ∀ {x y} → Coset._∼_ 𝒢 N (set-isSubgroup 𝑵) x y → x ∼ y
coset→rel {x} {y} p = ∼-resp (⁻¹-involutive x) (⁻¹-involutive y)
(∼-⁻¹ (respects (∙-cong ≈refl (≈sym (⁻¹-involutive y))) p))
```
The forward map of the correspondence packages the relation with its congruence proof.
```agda
congruenceOf : NormalSubgroup ℓ → Con 𝑮 ℓ
congruenceOf 𝑵 = NormalRel (set 𝑵) , NormalCon.∼-isCongruence 𝑵
```
#### From a congruence to a normal subgroup
In the other direction the ingredients are the curried consequences of a congruence's
compatibility: it is preserved by multiplication, by inversion, and hence by
conjugation. These are read off from `is-compatible`{.AgdaFunction} at the canonical
tuples, with no interpretation bridge needed — the curried accessors of
`Group-Op`{.AgdaModule} are *defined* by applying the interpreted symbol to exactly
those tuples.
```agda
module ConNormal {ℓ : Level} ((_θ_ , θcon) : Con 𝑮 ℓ) where
θ-refl : ∀ {x} → x θ x
θ-refl = IsEquivalence.refl (is-equivalence θcon)
θ-trans : ∀ {x y z} → x θ y → y θ z → x θ z
θ-trans = IsEquivalence.trans (is-equivalence θcon)
θ-reflexive : ∀ {x y} → x ≈ y → x θ y
θ-reflexive = reflexive θcon
θ-∙ : ∀ {x y u v} → x θ y → u θ v → (x ∙ u) θ (y ∙ v)
θ-∙ {x} {y} {u} {v} p q = is-compatible θcon ∙-Op λ { 0F → p ; 1F → q }
θ-⁻¹ : ∀ {x y} → x θ y → (x ⁻¹) θ (y ⁻¹)
θ-⁻¹ p = is-compatible θcon ⁻¹-Op (λ _ → p)
θ-conj : ∀ g {x y} → x θ y → x ^ g θ y ^ g
θ-conj g {x} {y} p = θ-∙ (θ-∙ (θ-refl {x = g}) p) (θ-refl {x = g ⁻¹})
```
The class of the identity is an equality-respecting subgroup, and it is normal.
Membership is `x θ ε`, so each subgroup law is one application of the corresponding
compatibility fact followed by a `≈`-step that renormalizes the right-hand side back to
`ε`{.AgdaFunction}: `ε ∙ ε ≈ ε`, `ε ⁻¹ ≈ ε`, and `conj g ε ≈ ε`.
```agda
IdentityClass : Pred G ℓ
IdentityClass x = x θ ε
IdentityClass-respects : IdentityClass Respects _≈_
IdentityClass-respects x≈y p = θ-trans (θ-reflexive (≈sym x≈y)) p
IdentityClass-ε : ε ∈ IdentityClass
IdentityClass-ε = θ-refl
IdentityClass-∙ : ∀ {x y} → x ∈ IdentityClass → y ∈ IdentityClass
→ x ∙ y ∈ IdentityClass
IdentityClass-∙ p q = θ-trans (θ-∙ p q) (θ-reflexive (idˡ-law ε))
IdentityClass-⁻¹ : ∀ {x} → x ∈ IdentityClass → x ⁻¹ ∈ IdentityClass
IdentityClass-⁻¹ p = θ-trans (θ-⁻¹ p) (θ-reflexive ε⁻¹≈ε)
IdentityClass-isSubgroup : IsSubgroup 𝒢 IdentityClass
IdentityClass-isSubgroup = mkIsSubgroup 𝒢 IdentityClass-respects IdentityClass-∙
IdentityClass-ε IdentityClass-⁻¹
IdentityClass-normal : IsNormal IdentityClass
IdentityClass-normal g p = θ-trans (θ-conj g p) (θ-reflexive (conj-ε g))
```
The backward map of the correspondence packages the class with its two proofs.
```agda
normalOf : Con 𝑮 ℓ → NormalSubgroup ℓ
normalOf θ = ConNormal.IdentityClass θ
, ConNormal.IdentityClass-isSubgroup θ
, ConNormal.IdentityClass-normal θ
```
#### Normality is necessary, not merely sufficient
`NormalCon`{.AgdaModule} shows normality *suffices* for `NormalRel N`{.AgdaFunction} to
be a congruence. The converse holds too, and is worth proving rather than asserting:
were it left as prose, the claim "the correspondence is with the *normal* subgroups"
would be doing work the formal development had not done, and nothing would rule out the
relation of some non-normal subgroup slipping into `Con 𝑮 ℓ`{.AgdaFunction}.
The proof needs no new group arithmetic. If `NormalRel N`{.AgdaFunction} is a
congruence, its identity class is normal by
`IdentityClass-normal`{.AgdaFunction} — and that class is
`{ x ∣ x ∙ ε ⁻¹ ∈ N }`, which `respects`{.AgdaField} identifies with
`N`{.AgdaBound} itself.
```agda
congruence→normal : {ℓ : Level} (N : Pred G ℓ) → IsSubgroup 𝒢 N
→ IsCongruence 𝑮 (NormalRel N) → IsNormal N
congruence→normal N N-sg isCon g {x} x∈N =
respects (∙ε⁻¹ (x ^ g))
(ConNormal.IdentityClass-normal (NormalRel N , isCon) g
(respects (≈sym (∙ε⁻¹ x)) x∈N))
where open IsSubgroup N-sg using ( respects )
```
#### Monotonicity
Both maps act by (co)restriction of the underlying predicates and relations, so
monotonicity is immediate in each direction.
```agda
normalOf-mono : (θ φ : Con 𝑮 ℓ) → θ ⊑ φ → normalOf θ ≤ⁿ normalOf φ
normalOf-mono _ _ θ⊑φ p = θ⊑φ p
congruenceOf-mono : (𝑴 𝑵 : NormalSubgroup ℓ) → 𝑴 ≤ⁿ 𝑵 → congruenceOf 𝑴 ⊑ congruenceOf 𝑵
congruenceOf-mono _ _ 𝑴≤𝑵 p = 𝑴≤𝑵 p
```
`OrderIso`{.AgdaRecord} asks only for monotonicity, not for the maps to be well defined
on equivalence classes, so that latter property — which "isomorphism of posets" is
usually taken to include — is recorded here rather than left implicit. It costs
nothing: each equivalence *is* mutual containment, so applying the matching
monotonicity twice suffices.
```agda
normalOf-cong : (θ φ : Con 𝑮 ℓ) → θ ≑ φ → normalOf θ ≈ⁿ normalOf φ
normalOf-cong θ φ (θ⊑φ , φ⊑θ) =
normalOf-mono θ φ θ⊑φ , normalOf-mono φ θ φ⊑θ
congruenceOf-cong : (𝑴 𝑵 : NormalSubgroup ℓ)
→ 𝑴 ≈ⁿ 𝑵 → congruenceOf 𝑴 ≑ congruenceOf 𝑵
congruenceOf-cong 𝑴 𝑵 (𝑴≤𝑵 , 𝑵≤𝑴) =
congruenceOf-mono 𝑴 𝑵 𝑴≤𝑵 , congruenceOf-mono 𝑵 𝑴 𝑵≤𝑴
```
#### Mutual inverseness
On congruences, `θ_{N_θ} ≑ θ`: the relation `θ_{N_θ}` holds at `(x , y)` when
`(x ∙ y ⁻¹) θ ε`, and multiplying on the right by `y`{.AgdaBound} converts that to
`x θ y` through `∙⁻¹∙`{.AgdaFunction} and the unit law — while multiplying `x θ y` on
the right by `y ⁻¹` converts it back through `invʳ-law`{.AgdaFunction}.
```agda
congruenceOf∘normalOf : (θ : Con 𝑮 ℓ) → congruenceOf (normalOf θ) ≑ θ
congruenceOf∘normalOf θ = fwd , bwd
where
open ConNormal θ
fwd : congruenceOf (normalOf θ) ⊑ θ
fwd {x} {y} p = θ-trans (θ-reflexive (≈sym (∙⁻¹∙ x y)))
(θ-trans (θ-∙ p θ-refl) (θ-reflexive (idˡ-law y)))
bwd : θ ⊑ congruenceOf (normalOf θ)
bwd {x} {y} p = θ-trans (θ-∙ p (θ-refl {y ⁻¹})) (θ-reflexive (invʳ-law y))
```
On normal subgroups, `N_{θ_N} ≈ⁿ N`: an element `x`{.AgdaBound} lies in `N_{θ_N}` when
`x ∙ ε ⁻¹ ∈ N`, and `x ∙ ε ⁻¹ ≈ x`, so the `respects`{.AgdaField} proof carried by the
subgroup identifies the two. **This is the step that consumes the
`respects`{.AgdaField} field**, and the sole place the correspondence would break for a
normal subuniverse not closed under the setoid equality.
```agda
normalOf∘congruenceOf : (𝑵 : NormalSubgroup ℓ) → normalOf (congruenceOf 𝑵) ≈ⁿ 𝑵
normalOf∘congruenceOf 𝑵 = fwd , bwd
where
open IsSubgroup (set-isSubgroup 𝑵) using ( respects )
fwd : normalOf (congruenceOf 𝑵) ≤ⁿ 𝑵
fwd {x} p = respects (∙ε⁻¹ x) p
bwd : 𝑵 ≤ⁿ normalOf (congruenceOf 𝑵)
bwd {x} p = respects (≈sym (∙ε⁻¹ x)) p
```
#### The order isomorphism
Assembling the four facts — two maps, both monotone, mutually inverse — gives the
correspondence as an `OrderIso`{.AgdaRecord} between the congruence containment order of
the group algebra and the inclusion order on normal subgroups. (The endpoint implicits
of the monotone maps are bound and forwarded explicitly: `Con`{.AgdaFunction} and
`NormalSubgroup`{.AgdaFunction} are defined functions, not injective type formers, so
Agda cannot recover them from the field types.)
```agda
NormalCongruenceIso : (ℓ : Level) → Type (α ⊔ ρ ⊔ suc ℓ)
NormalCongruenceIso ℓ =
OrderIso (_≑_ {𝑨 = 𝑮} {ℓ = ℓ}) (_⊑_ {𝑨 = 𝑮} {ℓ = ℓ}) (_≈ⁿ_ {ℓ}) (_≤ⁿ_ {ℓ})
normal-congruence-iso : (ℓ : Level) → NormalCongruenceIso ℓ
normal-congruence-iso ℓ = record
{ to = normalOf
; from = congruenceOf
; to-mono = λ {θ} {φ} → normalOf-mono θ φ
; from-mono = λ {𝑴} {𝑵} → congruenceOf-mono 𝑴 𝑵
; to∘from = normalOf∘congruenceOf
; from∘to = congruenceOf∘normalOf
}
```
The reverse isomorphism presents the normal subgroups of `𝒢`{.AgdaBound} as the
congruence poset of its underlying algebra — the form a representability argument wants.
```agda
NormalCongruenceIso⁻¹ : (ℓ : Level) → Type (α ⊔ ρ ⊔ suc ℓ)
NormalCongruenceIso⁻¹ ℓ =
OrderIso (_≈ⁿ_ {ℓ}) (_≤ⁿ_ {ℓ}) (_≑_ {𝑨 = 𝑮} {ℓ = ℓ}) (_⊑_ {𝑨 = 𝑮} {ℓ = ℓ})
normal-congruence-iso⁻¹ : (ℓ : Level) → NormalCongruenceIso⁻¹ ℓ
normal-congruence-iso⁻¹ ℓ = record
{ to = congruenceOf
; from = normalOf
; to-mono = λ {𝑴} {𝑵} → congruenceOf-mono 𝑴 𝑵
; from-mono = λ {θ} {φ} → normalOf-mono θ φ
; to∘from = congruenceOf∘normalOf
; from∘to = normalOf∘congruenceOf
}
```
#### Nonzero congruences and nontrivial normal subgroups
The order isomorphism alone does not say that the two sides agree on which elements are
*above the bottom*; that has to be proved, and it is what the monolith transport will
consume. The bottom of the subgroup side is `trivialSubgroup`{.AgdaFunction} of
[Classical.Structures.Group.Subgroups][] — the `≈`-class of the identity, which over a
setoid carrier is the right notion of the one-element subgroup — and the bottom of the
congruence side is the diagonal, whose "at the bottom" predicate is
`BelowDiagonal`{.AgdaFunction} of [Setoid.Congruences.Monolith][].
```agda
BelowTrivial : Pred G ℓ → Type (α ⊔ ρ ⊔ ℓ)
BelowTrivial N = N ⊆ proj₁ (trivialSubgroup 𝒢)
Nontrivialᴺ : Pred G ℓ → Type (α ⊔ ρ ⊔ ℓ)
Nontrivialᴺ N = ¬ BelowTrivial N
```
The two positive statements are equivalent on each side, constructively and in both
directions; `Nonzero`{.AgdaFunction} and `Nontrivialᴺ`{.AgdaFunction} are their
negations, so the equivalence of the negations follows by contraposition with no
classical input. We state the four positive implications first, since a downstream
proof usually wants one of them directly rather than the negated form.
```agda
below-trivial→below-diagonal : (𝑵 : NormalSubgroup ℓ)
→ BelowTrivial (set 𝑵) → BelowDiagonal 𝑮 (congruenceOf 𝑵)
below-trivial→below-diagonal 𝑵 N⊆1 p = ∙⁻¹≈ε→≈ (N⊆1 p)
below-diagonal→below-trivial : (𝑵 : NormalSubgroup ℓ)
→ BelowDiagonal 𝑮 (congruenceOf 𝑵) → BelowTrivial (set 𝑵)
below-diagonal→below-trivial 𝑵 θ⊆Δ {x} x∈N = θ⊆Δ (respects (≈sym (∙ε⁻¹ x)) x∈N)
where open IsSubgroup (set-isSubgroup 𝑵) using ( respects )
con-below-diagonal→below-trivial : (θ : Con 𝑮 ℓ)
→ BelowDiagonal 𝑮 θ → BelowTrivial (set (normalOf θ))
con-below-diagonal→below-trivial θ θ⊆Δ x∈N = θ⊆Δ x∈N
con-below-trivial→below-diagonal : (θ : Con 𝑮 ℓ)
→ BelowTrivial (set (normalOf θ)) → BelowDiagonal 𝑮 θ
con-below-trivial→below-diagonal θ N⊆1 {x} {y} p =
∙⁻¹≈ε→≈ (N⊆1 (θ-trans (θ-∙ p (θ-refl {y ⁻¹})) (θ-reflexive (invʳ-law y))))
where open ConNormal θ
```
Negating both sides gives the statement the monolith transport needs: under the
correspondence, a congruence is nonzero exactly when the matching normal subgroup is
nontrivial.
```agda
nonzero→nontrivial : (𝑵 : NormalSubgroup ℓ)
→ Nonzero 𝑮 (congruenceOf 𝑵) → Nontrivialᴺ (set 𝑵)
nonzero→nontrivial 𝑵 nz N⊆1 = nz (below-trivial→below-diagonal 𝑵 N⊆1)
nontrivial→nonzero : (𝑵 : NormalSubgroup ℓ)
→ Nontrivialᴺ (set 𝑵) → Nonzero 𝑮 (congruenceOf 𝑵)
nontrivial→nonzero 𝑵 nt θ⊆Δ = nt (below-diagonal→below-trivial 𝑵 θ⊆Δ)
con-nonzero→nontrivial : (θ : Con 𝑮 ℓ)
→ Nonzero 𝑮 θ → Nontrivialᴺ (set (normalOf θ))
con-nonzero→nontrivial θ nz N⊆1 = nz (con-below-trivial→below-diagonal θ N⊆1)
con-nontrivial→nonzero : (θ : Con 𝑮 ℓ)
→ Nontrivialᴺ (set (normalOf θ)) → Nonzero 𝑮 θ
con-nontrivial→nonzero θ nt θ⊆Δ = nt (con-below-diagonal→below-trivial θ θ⊆Δ)
```