Skip to content

FLRP.KurzweilNetter.A5

The Kurzweil–Netter theorem, closed at A₅

This is the FLRP.KurzweilNetter.A5 module of the Agda Universal Algebra Library.

Theorem. If a finite lattice is decidably representable, then so is its dual.

This module instantiates the base-group package of FLRP.KurzweilNetter.Duality's closed form at the certified alternating group A₅ of Examples.Classical.Groups.AlternatingGroup5, producing a closed inhabitant of KurzweilNetterDuality: no hypothesis remains.

The ingredients are as follows:

  • the group table and its laws by finite computation;
  • nonabelian simplicity by the certified IsNonabelianSimple bundle;
  • the carrier finiteness by the FiniteAlgebra witness;
  • Kurzweil surjectivity by the blockwise collapse.

Each is machine-checked upstream, so the duality theorem of Kurzweil and Netter is now fully proved in the agda-algebras library, with A₅ as the canonical witness that the parameterized proof's package is inhabitable.

The per-exponent surjectivity family is exported alongside, in the form the census consumers and any future instantiation-free arguments quote.

{-# OPTIONS --cubical-compatible --exact-split --safe #-}

module FLRP.KurzweilNetter.A5 where

open import Data.Nat.Base using ( ℕ )

-- Imports from the Agda Universal Algebra Library ------------------------------
open import Examples.Classical.Groups.AlternatingGroup5  using  ( a5-group ; a5-finite
                                                                ; a5-isNonabelianSimple )
open import FLRP.Assumptions                             using  ( KurzweilSurjectivityᵈAt
                                                                ; KurzweilNetterDuality )
open import FLRP.KurzweilNetter.Surjectivity             using  ( kurzweilSurjectivityᵈ )
open import FLRP.KurzweilNetter.Duality        using  ( kurzweilNetterDuality-ofSimple )

The instantiation

Kurzweil surjectivity holds at A₅ at every exponent; this is the family the Kurzweil–Netter route consumes, now closed.

-- Entry 4's working form, closed at A₅.
a5-kurzweilSurjectivityᵈ : (n : ℕ) → KurzweilSurjectivityᵈAt a5-group n
a5-kurzweilSurjectivityᵈ =
  kurzweilSurjectivityᵈ a5-group a5-finite a5-isNonabelianSimple

The theorem itself, with no remaining hypothesis.

-- The Kurzweil–Netter duality theorem: representable lattices are closed
-- under dualization, unconditionally.
kurzweilNetterDuality-A₅ : KurzweilNetterDuality
kurzweilNetterDuality-A₅ =
  kurzweilNetterDuality-ofSimple a5-group a5-finite a5-isNonabelianSimple