Examples.Classical.Groups.AlternatingGroup5¶
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 of Classical.Structures.Group.Simple,
the nonabelian-simple bundle IsNonabelianSimple, the discharged
NontrivialCenterless of FLRP.WreathNoGo,1 and, through the
correspondence of Classical.Structures.Group.Congruences, the congruence-level
IsSimple 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, exactly as in the certificate discipline of FLRP.Certificates.
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.2
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 of Overture.Cayley derives associativity
from two quadratic decisions: ActionHom? and
ActionFaithful? 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 below.
- For each of the 59 non-identity elements
x, the two generatorss = (0 1 2 3 4)andt = (0 1 2)are expressed as products of conjugates ofxand of its inverse (a5-seed-words-s,a5-seed-words-t); soundness of the term language puts both generators inN. - Every element is expressed as a word in
sandt(a5-gen-words), soNcontains everything.
The group A₅¶
The tables denote the operation, the inverse, and the point action.
-- The multiplication read off the Cayley table. _·_ : Fin 60 → Fin 60 → Fin 60 _·_ = ⟦ a5-mul-table ⟧ infixl 7 _·_ -- The inverse map. a5-inv : Fin 60 → Fin 60 a5-inv a = lookup a5-inv-vec a -- The action on the five points. 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.
-- Associativity, through the faithful point action. ·-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)) -- The group: the identity is the identity permutation, at index 0. 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₅.
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.
-- The seed assignment of the shared word table: seed 0 is s, seed 1 is t. genσ : Fin 2 → Fin 60 genσ 0F = a5-gen-s genσ 1F = a5-gen-t -- Decided: the word table expresses every element in the generators. 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)) -- Decided: at the i-th non-identity element, the s-word evaluates to s ... 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)) -- ... and the t-word to t. 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.
-- A₅ is simple: every normal subgroup containing a non-identity element -- is the whole group. 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 -- Stage 1: the generators lie in N, by the seed words at x = suc i. 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)) -- Stage 2 seeds: the word-table assignment lands in N. σ∈ : ∀ 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.
-- s and t do not commute: s · t and t · s are distinct table entries. a5-noncommuting : NoncommutingPair a5-noncommuting = a5-gen-s , a5-gen-t , λ () -- A₅ is nonabelian simple. a5-isNonabelianSimple : IsNonabelianSimple a5-isNonabelianSimple = record { simple = a5-isSimple ; noncommuting = a5-noncommuting } -- Identity equations are stable: the carrier equality is decidable. a5-Stable-≈ε : Stable-≈ε a5-Stable-≈ε = ≈-dec→Stable-≈ε _≟_ -- The center of A₅ is trivial, positively. a5-center-trivial : ∀ d → d ∈ center → d ≡ 0F a5-center-trivial = center-trivial a5-Stable-≈ε a5-isNonabelianSimple
An important consequence: A₅ discharges the NontrivialCenterless
record of FLRP.WreathNoGo, so it is an admissible base group for the Kurzweil
entries of FLRP.Assumptions with the nonabelian-simple side condition
witnessed rather than assumed.
-- A₅ is nontrivial and centerless, as FLRP.WreathNoGo consumes it. 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.
open Polymorphic.GroupCongruences a5-group using ( simple→simpleAlgebra ) -- A₅ is a simple algebra: the congruence-level notion, through the -- normal-subgroup/congruence correspondence. 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
witness is immediate; downstream instantiations consume it wherever a finite
base group is an antecedent.
-- A₅ is a finite algebra: Fin 60 enumerates itself. a5-finite : FiniteAlgebra (proj₁ a5-group) a5-finite = record { _≟_ = _≟_ ; card = 60 ; enum = λ i → i ; enum-sur = λ x → x , refl }
Acceptance checks¶
The Group-Op accessors interpret to the tabulated operation,
to 0F, and to the inverse vector on the nose;
discharged by refl.
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
-
This is what makes
A₅an admissible base group for the Kurzweil entries of FLRP.Assumptions. ↩ -
The two candidate formalizations that were rejected: + A Cayley table with all laws decided, as in Examples.Classical.Groups.SymmetricGroup3. At
Fin 60the associativity decision ranges over60³ = 216000triples 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, 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 throughrespectsat every step, and the group would not plug into theFin-indexed finite machinery as it stands.
- A permutation presentation over