---
layout: default
file: "src/Classical/Structures/Group/NormalClosure.lagda.md"
title: "Classical.Structures.Group.NormalClosure module"
date: "2026-08-30"
author: "the agda-algebras development team"
---

### The normal closure of an element

This is the [Classical.Structures.Group.NormalClosure][] module of the [Agda Universal Algebra Library][].

The **normal closure** of a set of elements of a group is the least normal subgroup
containing the set.  This module treats it twice, once per consumer, and the two
halves share no code:

+  **The witness-term language** (`ClosureTerm`{.AgdaDatatype},
   `⟦_⟧`{.AgdaFunction}, `closure-sound`{.AgdaFunction}, in
   `NormalClosure`{.AgdaModule}) does not construct the subgroup; it provides the
   replay language for membership claims about it, which is what a finite
   simplicity certificate consumes.
+  **The decidable construction** (`⟪_⟫`{.AgdaFunction}, `⟪⟫-dec`{.AgdaFunction},
   `⟪⟫-mem`{.AgdaFunction}, `⟪⟫-least`{.AgdaFunction}, in
   `NormalClosureᵈ`{.AgdaModule}) builds the closure of a single element of a
   *finite* group, with **decidable** membership, so it is a normal subgroup at
   Layer D of the two-layer discipline of [ADR-008][]; it is the engine of the
   minimal-normal descent of [Classical.Structures.Group.MinimalNormalDescent][].

#### The witness-term language

The point of the language is finite certification.  A simplicity certificate in
the sense of [Classical.Structures.Group.Simple][] must show, for a given seed,
that the seed's normal closure is everything; a certificate does that by
exhibiting, for each target element, a closure term that evaluates to it, and the
evaluations are decidable equalities over a finite carrier.  Soundness then
replays the certificate against an *arbitrary* normal subgroup containing the
seed, with no completeness theorem needed: only the two directions actually
consumed are stated.

The term datatype is parameterized by the carrier type alone, not by a group,
so that generated certificate data can be written down before (and independent
of) the group structure it will be replayed against; evaluation and soundness
live in the group-parameterized module below.

#### The decidable construction, in outline

The construction reuses machinery rather than rebuilding it.  A normal subgroup of
`𝒢`{.AgdaBound} is the same thing as a congruence of the underlying algebra
([Classical.Structures.Group.Congruences][]), the congruence generated by a finite list
of pairs of a finite finitary algebra has decidable membership (`Cg-DecCon`{.AgdaFunction}
of [Setoid.Congruences.Presented.Decidable][]), and the
group signature is finite finitary (`Sig-Group-FiniteSignature`{.AgdaFunction} of
[Classical.Signatures.Finite][]).  So

    ⟪ y ⟫ = normalOf (Cg (fromPairs [ (y , ε) ]))

and the three facts the descent needs — decidability, `y ∈ ⟪ y ⟫`, and leastness —
are, in order, L1's decision procedure, the `base`{.AgdaInductiveConstructor} rule of
congruence generation, and `Cg-least`{.AgdaFunction} pushed across the correspondence.

Three points about the formal statement.

+  **The level is forced, and it is the right one**.  `Sig-Group`{.AgdaFunction} has
   zero signature levels, so the congruence generated by a pair list of a group at
   levels `α`{.AgdaBound}, `ρ`{.AgdaBound} lands at `α ⊔ ρ`.  That is exactly the level
   `L`{.AgdaFunction} at which `GroupSublattice 𝒢 ρ`{.AgdaModule} of
   [Classical.Structures.Group.SubgroupLattice][] holds its elements, and hence the
   level of the normal subgroups that [Classical.Structures.Group.MinimalNormal][]
   quantifies over.  No level bookkeeping is needed downstream.

+  **The decision procedure is `abstract`**.  The closure matrix `Cg-dec`{.AgdaFunction}
   computes is an enormous symbolic term, and nothing below inspects it — only its
   *type* matters.  Sealing it keeps that term out of every goal in which a normal
   closure appears, exactly as `decodeDec`{.AgdaFunction} of
   [Setoid.Congruences.Finite.Decidable][] seals the same term for the same reason.

+  **Leastness needs no finiteness**.  `⟪⟫-least`{.AgdaFunction} holds for the
   generated congruence of any group; only the decision procedure consumes the
   `FiniteAlgebra`{.AgdaRecord} witness.  The two are nevertheless proved in one
   module, since the finiteness witness is what makes the notion useful and splitting
   would buy a generality no consumer wants.

<!--
```agda
{-# OPTIONS --without-K --exact-split --safe #-}

module Classical.Structures.Group.NormalClosure where

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

-- Imports from the Agda Standard Library ---------------------------------------
open import Data.Fin.Base                 using  ( Fin )
open import Data.List.Base                using  ( [] ; _∷_ )
open import Data.List.Relation.Unary.Any  using  ( here )
open import Data.Nat.Base                 using  ( ℕ )
open import Data.Product                  using  ( _,_ ; proj₁ ; proj₂ )
open import Level                         using  ( Level ; _⊔_ )
open import Relation.Binary               using  ( Setoid )
open import Relation.Nullary              using  ( Dec )
open import Relation.Unary                using  ( Pred ; _∈_ )

-- Imports from the Agda Universal Algebra Library ------------------------------
open import Classical.Signatures.Finite             using  ( Sig-Group-FiniteSignature )
open import Classical.Structures.Group.Basic        using  ( Group ; module Group-Op )
open import Classical.Structures.Group.Congruences  using  ( module GroupCongruences )
open import Classical.Structures.Group.Conjugation  using  ( module Conjugate )
open import Classical.Structures.Group.Subgroups    using  ( IsSubgroup )
open import Setoid.Algebras.Basic                   using  ( 𝕌[_] ; 𝔻[_] )
open import Setoid.Algebras.Finite                  using  ( FiniteAlgebra )
open import Setoid.Congruences.Basic                using  ( Con )
open import Setoid.Congruences.Generation           using  ( Cg ; base ; Cg-least )
open import Setoid.Congruences.Presented            using  ( fromPairs ; Cg-DecCon )
```
-->

#### The witness terms

A closure term over a carrier `A` with `k` seeds denotes an element built from
the seeds by the four normal-subgroup closure operations.  The conjugating
element of `cnj`{.AgdaInductiveConstructor} is an arbitrary carrier element, not
a term: normality closes a subgroup under conjugation by *everything*.

```agda
data ClosureTerm {a : Level} (A : Type a) (k : ℕ) : Type a where
  one   : ClosureTerm A k
  seed  : Fin k → ClosureTerm A k
  inv   : ClosureTerm A k → ClosureTerm A k
  mul   : ClosureTerm A k → ClosureTerm A k → ClosureTerm A k
  cnj   : A → ClosureTerm A k → ClosureTerm A k
```

#### Evaluation and soundness

Evaluation interprets a term in a group, at an assignment of the seeds; the
conjugation case is exactly `conj`{.AgdaFunction} of
[Classical.Structures.Group.Conjugation][] (syntax: `_^ g`), so that soundness
can consume a normality proof with no conversion.

```agda
module NormalClosure {α ρ : Level} (𝒢@(𝑮 , _) : Group α ρ) where
  open Group-Op 𝒢   using  ( _∙_ ; ε ; _⁻¹ )
  open Conjugate 𝒢  using  ( conj-syntax ; IsNormal )

  -- Evaluate a closure term at an assignment of the seeds.
  ⟦_⟧ : {k : ℕ} → ClosureTerm 𝕌[ 𝑮 ] k → (Fin k → 𝕌[ 𝑮 ]) → 𝕌[ 𝑮 ]
  ⟦ one ⟧      σ = ε
  ⟦ seed i ⟧   σ = σ i
  ⟦ inv e ⟧    σ = ⟦ e ⟧ σ ⁻¹
  ⟦ mul e f ⟧  σ = ⟦ e ⟧ σ ∙ ⟦ f ⟧ σ
  ⟦ cnj g e ⟧  σ = ⟦ e ⟧ σ ^ g
```

**Soundness**.  A normal subgroup containing every seed contains the value of
every term.  The proof is structural, one closure property per constructor.

```agda
  -- A normal subgroup containing the seeds contains every term's value.
  closure-sound : {ℓ : Level} {N : Pred 𝕌[ 𝑮 ] ℓ}
    →  IsSubgroup 𝒢 N → IsNormal N
    →  {k : ℕ} {σ : Fin k → 𝕌[ 𝑮 ]} → (∀ i → σ i ∈ N)
    →  (e : ClosureTerm 𝕌[ 𝑮 ] k) → ⟦ e ⟧ σ ∈ N
  closure-sound sg nrm σ∈ one        = IsSubgroup.ε-closed sg
  closure-sound sg nrm σ∈ (seed i)   = σ∈ i
  closure-sound sg nrm σ∈ (inv e)    = IsSubgroup.⁻¹-closed sg (closure-sound sg nrm σ∈ e)
  closure-sound sg nrm σ∈ (mul e f)  = IsSubgroup.∙-closed sg  (closure-sound sg nrm σ∈ e)
                                                               (closure-sound sg nrm σ∈ f)
  closure-sound sg nrm σ∈ (cnj g e)  = nrm g (closure-sound sg nrm σ∈ e)
```

#### The decidable construction

Fix a finite group: a group `𝒢`{.AgdaBound} together with carrier-finiteness data
`𝑭`{.AgdaBound} for its underlying algebra.  (The `ᵈ` superscript marks the
Layer-D presentation, as in the descent module this construction drives.)

```agda
module NormalClosureᵈ {α ρ : Level} (𝒢 : Group α ρ) (𝑭 : FiniteAlgebra (proj₁ 𝒢)) where
  private
    𝑮 = proj₁ 𝒢
    G = 𝕌[ 𝑮 ]

  open Setoid 𝔻[ 𝑮 ]  using  ()
                      renaming ( refl to ≈refl ; sym to ≈sym ; trans to ≈trans )
  open Group-Op 𝒢         using  ( ε ; ∙-cong ; ⁻¹-cong )
  open GroupCongruences 𝒢 using  ( NormalSubgroup ; set ; set-isSubgroup ; _≤ⁿ_
                                 ; ≤ⁿ-trans ; NormalRel ; congruenceOf ; normalOf
                                 ; normalOf-mono ; normalOf∘congruenceOf ; ∙ε⁻¹ )
```

The level at which the whole construction lives: the congruence generated by a pair
list of a `Sig-Group`{.AgdaFunction}-algebra, and hence the normal subgroup it
corresponds to, sits at `α ⊔ ρ`.

```agda
  -- The working level of the normal closure.
  L : Level
  L = α ⊔ ρ
```

The normal closure of `y`{.AgdaBound} is the identity class of the congruence generated
by the single pair `(y , ε)`.  Being in the image of `normalOf`{.AgdaFunction} it is a
normal, equality-respecting subgroup with no further work.  (The algebra implicit of
`Cg`{.AgdaFunction} and `fromPairs`{.AgdaFunction} is supplied by hand: a relation on
`𝕌[ 𝑮 ]`{.AgdaFunction} does not determine `𝑮`{.AgdaFunction}.)

```agda
  private
    -- The congruence generated by the single pair (y , ε).
    genCon : G → Con 𝑮 L
    genCon y = Cg {𝑨 = 𝑮} (fromPairs {𝑨 = 𝑮} ((y , ε) ∷ []))

  -- The normal closure of y: the identity class of the congruence generated by
  -- the pair (y , ε).
  ⟪_⟫ : G → NormalSubgroup L
  ⟪ y ⟫ = normalOf (genCon y)
```

Membership is decidable, by L1 of [Setoid.Congruences.Presented.Decidable][]: `x`{.AgdaBound}
lies in `⟪ y ⟫`{.AgdaFunction} exactly when the generated congruence relates
`x`{.AgdaBound} to `ε`{.AgdaFunction}, and that is one entry of the closure matrix.

```agda
  -- Membership in a normal closure is decidable (the term is sealed; see above).
  abstract
    ⟪⟫-dec : (y x : G) → Dec (x ∈ set ⟪ y ⟫)
    ⟪⟫-dec y x = proj₂ (Cg-DecCon 𝑭 Sig-Group-FiniteSignature ((y , ε) ∷ [])) x ε
```

The generator belongs to its own closure: this is the `base`{.AgdaInductiveConstructor}
rule of `Gen`{.AgdaDatatype} applied to the one listed pair.

```agda
  -- y lies in its own normal closure.
  ⟪⟫-mem : (y : G) → y ∈ set ⟪ y ⟫
  ⟪⟫-mem y = base (here (≈refl , ≈refl))
```

Leastness.  If a normal subgroup `𝑵`{.AgdaBound} contains `y`{.AgdaBound}, then its
congruence relates `y`{.AgdaBound} to `ε`{.AgdaFunction}, so it contains the presented
relation; `Cg-least`{.AgdaFunction} carries that to the generated congruence, and
`normalOf`{.AgdaFunction} — monotone, and inverse to `congruenceOf`{.AgdaFunction} —
brings the containment back to the subgroup side.

```agda
  -- The normal closure of y is inside every normal subgroup containing y.
  ⟪⟫-least : (y : G) (𝑵 : NormalSubgroup L) → y ∈ set 𝑵 → ⟪ y ⟫ ≤ⁿ 𝑵
  ⟪⟫-least y 𝑵 y∈N =
    ≤ⁿ-trans  {𝑳 = ⟪ y ⟫} {𝑴 = normalOf (congruenceOf 𝑵)} {𝑵 = 𝑵}
              (normalOf-mono  (genCon y)
                              (congruenceOf 𝑵)
                              (Cg-least (congruenceOf 𝑵) pairs⊆))
              (proj₁ (normalOf∘congruenceOf 𝑵))
    where
    open IsSubgroup (set-isSubgroup 𝑵) using ( respects )

    -- The one listed pair is related by the congruence of 𝑵, since y ∈ N.
    pairs⊆ : ∀ {u v} → fromPairs {𝑨 = 𝑮} ((y , ε) ∷ []) u v → NormalRel (set 𝑵) u v
    pairs⊆ {u} {v} (here (u≈y , v≈ε)) =
      respects (≈sym (≈trans (∙-cong u≈y (⁻¹-cong v≈ε)) (∙ε⁻¹ y))) y∈N
```