Classical.Structures.Group.NormalClosure¶
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,⟦_⟧,closure-sound, inNormalClosure) 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 (
⟪_⟫,⟪⟫-dec,⟪⟫-mem,⟪⟫-least, inNormalClosureᵈ) 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
𝒢 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
of Setoid.Congruences.Presented.Decidable, Lemma L1 of the two-layer note), and the
group signature is finite finitary (Sig-Group-FiniteSignature 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 rule of
congruence generation, and Cg-least pushed across the correspondence.
Three points about the formal statement.
-
The level is forced, and it is the right one.
Sig-Grouphas zero signature levels, so the congruence generated by a pair list of a group at levelsα,ρlands atα ⊔ ρ. That is exactly the levelLat whichGroupSublattice 𝒢 ρ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 matrixCg-deccomputes 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 asdecodeDecof Setoid.Congruences.Finite.Decidable seals the same term for the same reason. -
Leastness needs no finiteness.
⟪⟫-leastholds for the generated congruence of any group; only the decision procedure consumes theFiniteAlgebrawitness. 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.
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 is an arbitrary carrier element, not
a term: normality closes a subgroup under conjugation by everything.
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 of
Classical.Structures.Group.Conjugation (syntax: _^ g), so that soundness
can consume a normality proof with no conversion.
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.
-- 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 𝒢 together with carrier-finiteness data
𝑭 for its underlying algebra. (The ᵈ superscript marks the
Layer-D presentation, as in the descent module this construction drives.)
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-algebra, and hence the normal subgroup it
corresponds to, sits at α ⊔ ρ.
-- The working level of the normal closure. L : Level L = α ⊔ ρ
The normal closure of y is the identity class of the congruence generated
by the single pair (y , ε). Being in the image of normalOf it is a
normal, equality-respecting subgroup with no further work. (The algebra implicit of
Cg and fromPairs is supplied by hand: a relation on
𝕌[ 𝑮 ] does not determine 𝑮.)
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
lies in ⟪ y ⟫ exactly when the generated congruence relates
x to ε, and that is one entry of the closure matrix.
-- 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
rule of Gen applied to the one listed pair.
-- y lies in its own normal closure. ⟪⟫-mem : (y : G) → y ∈ set ⟪ y ⟫ ⟪⟫-mem y = base (here (≈refl , ≈refl))
Leastness. If a normal subgroup 𝑵 contains y, then its
congruence relates y to ε, so it contains the presented
relation; Cg-least carries that to the generated congruence, and
normalOf — monotone, and inverse to congruenceOf —
brings the containment back to the subgroup side.
-- 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