---
layout: default
file: "src/Examples/Classical/Groups/AlternatingGroup5.lagda.md"
title: "Examples.Classical.Groups.AlternatingGroup5 module"
date: "2026-08-30"
author: "the agda-algebras development team"
---
### Worked example: the alternating group `A₅`, certified simple
This is the [Examples.Classical.Groups.AlternatingGroup5][] module of the [Agda Universal Algebra Library][].
The alternating group `A₅` on five points is the smallest nonabelian simple group.
This module constructs it concretely, on the carrier `Fin 60` with propositional
equality, and certifies its simplicity by finite computation: the result is an
inhabitant of `IsSimple`{.AgdaFunction} of [Classical.Structures.Group.Simple][],
the nonabelian-simple bundle `IsNonabelianSimple`{.AgdaRecord}, the discharged
`NontrivialCenterless`{.AgdaRecord} of the same module, and, through the
correspondence of [Classical.Structures.Group.Congruences][], the congruence-level
`IsSimple`{.AgdaFunction} of [Setoid.Congruences.Simple][].
The raw data lives in the generated companion
[Examples.Classical.Groups.AlternatingGroup5.Tables][]: the 60 by 60 Cayley table
on the lexicographic even-permutation encoding (index 0 is the identity), the
inverse vector, the action of each element on the five points, and the simplicity
certificate. Nothing rests on the generator's authority: every claim in the data
is replayed here by decision procedures over the finite carrier.
#### Presentation choice, with measurements
Three presentations were candidates, and we naturally chose the one that is easily
integrated into our existing finite group theory framework and has good
computational properties.[^1]
We represent `A₅` by a Cayley table, exploiting the fact that `A₅` acts
faithfully on its five points: the action tables are data.
`assoc-from-action`{.AgdaFunction} of [Overture.Cayley][] derives associativity
from two quadratic decisions: `ActionHom?`{.AgdaFunction} and
`ActionFaithful?`{.AgdaFunction} of [Overture.Operations.Properties][].
The whole module type-checks in under ten seconds at under a gigabyte.
#### The simplicity certificate
The definition of "simple group" in implication form says that a group is simple
provided every normal subgroup containing a non-identity element is the whole
group. The certificate witnesses this in two stages decided by
`from-yes`{.AgdaFunction} below.
1. For each of the 59 non-identity elements `x`, the two generators
`s = (0 1 2 3 4)` and `t = (0 1 2)` are expressed as products of conjugates of
`x` and of its inverse (`a5-seed-words-s`{.AgdaFunction},
`a5-seed-words-t`{.AgdaFunction}); soundness of the term language puts both
generators in `N`.
2. Every element is expressed as a word in `s` and `t`
(`a5-gen-words`{.AgdaFunction}), so `N` contains everything.
<!--
```agda
{-# OPTIONS --without-K --exact-split --safe #-}
module Examples.Classical.Groups.AlternatingGroup5 where
open import Data.Fin.Base using ( Fin ; suc )
open import Data.Fin.Patterns using ( 0F ; 1F )
open import Data.Fin.Properties using ( _≟_ ; all? )
open import Data.Product using ( _,_ ; proj₁ )
open import Data.Vec.Base using ( lookup )
open import Level using ( 0ℓ )
open import Relation.Binary.PropositionalEquality using ( _≡_ ; refl ; subst )
open import Relation.Nullary.Negation.Core using ( contradiction )
open import Relation.Unary using ( _∈_ )
open import Overture.Cayley using ( ⟦_⟧ ; from-yes ; assoc-from-action )
open import Overture.Operations.Properties
using ( ActionHom? ; ActionFaithful?
; LeftIdentity? ; RightIdentity?
; LeftInverse? ; RightInverse? )
open import Classical.Small.Structures.Group using ( Group ; eqsToGroup )
open import Examples.Classical.Groups.AlternatingGroup5.Tables
using ( a5-mul-table ; a5-inv-vec ; a5-gen-s
; a5-act-table ; a5-gen-t ; a5-gen-words
; a5-seed-words-s ; a5-seed-words-t )
open import Classical.Structures.Group.Simple
using ( NontrivialCenterless
; nonabelianSimple→nontrivialCenterless )
open import Setoid.Algebras.Finite using ( FiniteAlgebra )
import Classical.Structures.Group as Polymorphic
import Setoid.Congruences.Simple as SimpleAlgebra
```
-->
#### The group `A₅`
The tables denote the operation, the inverse, and the point action.
```agda
_·_ : Fin 60 → Fin 60 → Fin 60
_·_ = ⟦ a5-mul-table ⟧
infixl 7 _·_
a5-inv : Fin 60 → Fin 60
a5-inv a = lookup a5-inv-vec a
a5-act : Fin 60 → Fin 5 → Fin 5
a5-act a q = lookup (lookup a5-act-table a) q
```
Associativity comes from the faithful action, per the presentation note; the
remaining four laws are linear decisions over the carrier.
```agda
·-assoc : ∀ a b c → a · b · c ≡ a · (b · c)
·-assoc = assoc-from-action _·_ a5-act (from-yes (ActionHom? _·_ a5-act))
(from-yes (ActionFaithful? a5-act))
a5-group : Group
a5-group = eqsToGroup (Fin 60) _·_ 0F a5-inv
·-assoc
(from-yes (LeftIdentity? _·_ 0F))
(from-yes (RightIdentity? _·_ 0F))
(from-yes (LeftInverse? _·_ 0F a5-inv))
(from-yes (RightInverse? _·_ 0F a5-inv))
```
The simplicity vocabulary, the normal-subgroup projections, and the
closure-term evaluator, all instantiated at `A₅`.
```agda
open Polymorphic.Simple a5-group 0ℓ using ( IsSimple ; NoncommutingPair
; IsNonabelianSimple
; ≈-dec→Stable-≈ε ; center
; Stable-≈ε ; center-trivial )
open Polymorphic.MinimalNormal a5-group 0ℓ using (isSubgroup ; isNormal)
open Polymorphic.NormalClosure a5-group using ( closure-sound )
renaming ( ⟦_⟧ to ⟦_⟧◃ )
```
#### Replaying the certificate
**The three decided checks**: the shared word table hits every element, and at
each non-identity element the two seed words evaluate to the generators.
```agda
genσ : Fin 2 → Fin 60
genσ 0F = a5-gen-s
genσ 1F = a5-gen-t
gen-words-ok : ∀ y → ⟦ lookup a5-gen-words y ⟧◃ genσ ≡ y
gen-words-ok = from-yes (all? (λ y → ⟦ lookup a5-gen-words y ⟧◃ genσ ≟ y))
seed-words-s-ok : ∀ i → ⟦ lookup a5-seed-words-s i ⟧◃ (λ _ → suc i) ≡ a5-gen-s
seed-words-s-ok =
from-yes (all? (λ i → ⟦ lookup a5-seed-words-s i ⟧◃ (λ _ → suc i) ≟ a5-gen-s))
seed-words-t-ok : ∀ i → ⟦ lookup a5-seed-words-t i ⟧◃ (λ _ → suc i) ≡ a5-gen-t
seed-words-t-ok =
from-yes (all? (λ i → ⟦ lookup a5-seed-words-t i ⟧◃ (λ _ → suc i) ≟ a5-gen-t))
```
**Simplicity, by replay**. A non-identity element of `Fin 60` is `suc i` for a
unique `i : Fin 59`, so the two certificate stages compose: soundness of the
closure terms puts the generators, and then every element, in `N`.
```agda
a5-isSimple : IsSimple
a5-isSimple N N-nsg (0F , x∈N , x≉ε) y = contradiction refl x≉ε
a5-isSimple N N-nsg ((suc i) , x∈N , x≉ε) y =
subst (_∈ N) (gen-words-ok y) (closure-sound sg nrm σ∈ (lookup a5-gen-words y))
where
sg : Polymorphic.IsSubgroup a5-group N
sg = isSubgroup N-nsg
nrm : Polymorphic.Conjugate.IsNormal a5-group N
nrm = isNormal N-nsg
s∈N : a5-gen-s ∈ N
s∈N = subst (_∈ N) (seed-words-s-ok i)
(closure-sound sg nrm (λ _ → x∈N) (lookup a5-seed-words-s i))
t∈N : a5-gen-t ∈ N
t∈N = subst (_∈ N) (seed-words-t-ok i)
(closure-sound sg nrm (λ _ → x∈N) (lookup a5-seed-words-t i))
σ∈ : ∀ j → genσ j ∈ N
σ∈ 0F = s∈N
σ∈ 1F = t∈N
```
#### The nonabelian-simple bundle and its consequences
The generators do not commute, which provides a pair to use as the nonabelianness
witness; the bundle then yields the positive triviality of the center, since `Fin 60`
has decidable equality.
```agda
a5-noncommuting : NoncommutingPair
a5-noncommuting = a5-gen-s , a5-gen-t , λ ()
a5-isNonabelianSimple : IsNonabelianSimple
a5-isNonabelianSimple = record { simple = a5-isSimple
; noncommuting = a5-noncommuting }
a5-Stable-≈ε : Stable-≈ε
a5-Stable-≈ε = ≈-dec→Stable-≈ε _≟_
a5-center-trivial : ∀ d → d ∈ center → d ≡ 0F
a5-center-trivial = center-trivial a5-Stable-≈ε a5-isNonabelianSimple
```
**An important consequence**: `A₅` discharges the
`NontrivialCenterless`{.AgdaRecord} record of
[Classical.Structures.Group.Simple][], so a consumer that needs a nontrivial
centerless base group can take `A₅` with the side condition witnessed rather
than assumed.
```agda
a5-nontrivialCenterless : NontrivialCenterless a5-group
a5-nontrivialCenterless =
nonabelianSimple→nontrivialCenterless a5-group a5-Stable-≈ε a5-isNonabelianSimple
```
#### The congruence-level notion
Through the normal-subgroup/congruence correspondence of
[Classical.Structures.Group.Congruences][], the certificate transports to the
congruence-level simplicity of [Setoid.Congruences.Simple][]: every congruence of
the underlying algebra that relates two distinct elements relates every pair. This
makes `A₅` the library's first concrete finite algebra certified simple at the
congruence level. The group-side and algebra-side notions share a name, so the
algebra-side module is imported qualified here.
```agda
open Polymorphic.GroupCongruences a5-group using ( simple→simpleAlgebra )
a5-isSimpleAlgebra : SimpleAlgebra.IsSimple (proj₁ a5-group) 0ℓ
a5-isSimpleAlgebra = simple→simpleAlgebra 0ℓ a5-isSimple
```
#### Finiteness
The carrier is its own enumeration, so the `FiniteAlgebra`{.AgdaRecord}
witness is immediate; downstream instantiations consume it wherever a finite
base group is an antecedent.
```agda
a5-finite : FiniteAlgebra (proj₁ a5-group)
a5-finite = record
{ _≟_ = _≟_
; card = 60
; enum = λ i → i
; enum-sur = λ x → x , refl }
```
#### Acceptance checks
The `Group-Op`{.AgdaModule} accessors interpret to the tabulated operation,
to `0F`{.AgdaInductiveConstructor}, and to the inverse vector on the nose;
discharged by `refl`{.AgdaInductiveConstructor}.
```agda
open Polymorphic.Group-Op a5-group using ( _∙_ ; ε ; _⁻¹ )
∙-is-· : ∀ (a b : Fin 60) → a ∙ b ≡ a · b
∙-is-· a b = refl
ε-is-0 : ε ≡ 0F
ε-is-0 = refl
⁻¹-is-inv : ∀ (a : Fin 60) → a ⁻¹ ≡ a5-inv a
⁻¹-is-inv a = refl
```
---
[^1]: The two candidate formalizations that were rejected:
+ **A Cayley table with all laws decided**, as in
[Examples.Classical.Groups.SymmetricGroup3][]. At `Fin 60` the associativity
decision ranges over `60³ = 216000` triples of table lookups; measured on this
module's table, `from-yes (Associative? _·_)` type-checks in 72 seconds at a
peak of 13.8 GB of memory, which makes it undesirable from a usability
perspective and would be a burden on the CI workflow.
+ **A permutation presentation** over `setoidEqsToGroup`{.AgdaFunction}, with
near-definitional laws. Rejected for a different reason: the carrier would be
a setoid of functions, so the certificate replay below would have to transport
memberships along pointwise equality through `respects`{.AgdaField} at every
step, and the group would not plug into the `Fin`-indexed finite machinery as
it stands.