FLRP.KurzweilNetter.Duality

The Kurzweil–Netter duality theorem

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

Theorem (Kurzweil 1985, Netter 1986). If a finite lattice is decidably representable, then so is its dual.

This module assembles the formal proof from its three prepared stages, following the argument of docs/papers/fin-lat-rep/SmallLatticeReps.tex § "Lattice duals: the theorem of Kurzweil and Netter" (after Pálfy's 2009 lectures). Given a representation 𝑳 ≅ DecCon 𝑨, proceed as follows:

1. present the carrier of 𝑨 by an irredundant enumeration Fin m (Setoid.Algebras.Finite.Irredundant), and its congruences as the partitions of Fin m invariant under the basic translations (FLRP.KurzweilNetter.Blocks, FLRP.KurzweilNetter.Translations, the translation criterion);

2. expand the coset algebra of the diagonal D ≤ Sᵐ by the lifted translations; its decidable congruence poset is the reversed poset of invariant partitions (FLRP.KurzweilNetter.Expansion, composing the WP-3 bridge DecCon (Sᵐ ↷ Sᵐ/D) ≅ [D , Sᵐ] of FLRP.Bridge with the decidable-instance passage of Kurzweil's interval isomorphism [D , Sᵐ] ≅ Eq(m)′ of FLRP.KurzweilNetter.Interval);

3. compose the two, and the original representation, into DecCon 𝑬 ≅ dualLattice 𝑳, the record dual-representation below.

What the proof assumes of the simple group

For now, we parameterize by the group S rather than instantiated at a concrete simple group, and the module parameters are the deliverable list of properties the argument actually uses:

• a finite carrier with decidable equality (𝑭ₛ: FiniteAlgebra), for finiteness of the power Sᵐ, decidable coset equality, and the membership deciders of the partition subgroups;

• a nontriviality witness s₀ with ¬ (s₀ ≈ ε), for the order reflection and injectivity of π ↦ K_π, and for extracting invariance from closure in the expansion step (the indicator tuples);

• Kurzweil surjectivity at every exponent, in the decidable form (KurzweilSurjectivityᵈAt𝒮 n, the working form of Entry 4 of FLRP.Assumptions): every decidable subgroup in [D , Sⁿ] is a partition subgroup. The semantic form is deliberately not consumed: it is unprovable outright (the no-go of FLRP.KurzweilNetter.Interval), while the decidable form is exactly what the construction's base-coset classes deliver.

Nonabelianness and simplicity of S enter only through the third item; they are what makes the surjectivity family true. Thus no simplicity predicate is needed anywhere in this module. Both follow-ons have landed with no change here: FLRP.KurzweilNetter.Surjectivity proves the family from the nonabelian-simplicity bundle and closes the theorem over the package (kurzweilNetterDuality-ofSimple), and FLRP.KurzweilNetter.A5 instantiates the package at the certified A₅ (kurzweilNetterDuality-A₅, a closed inhabitant).

What the proof does not assume

The manuscript reduces to unary operations by citing the unary-reduction theorem Con 𝑨 = Con ⟨A , Pol₁ 𝑨⟩ (not yet formalized). The formal proof here does not take that result as a hypothesis: the expansion lifts only the basic translations of 𝑨, and the translation criterion of FLRP.KurzweilNetter.Translations, a self-contained Mal'cev-style walk, shows these already determine the congruences.¹

Size

The construction represents dualLattice 𝑳 on the coset space Sᵐ / D of |S|ᵐ⁻¹ elements, which is at least 60ᵐ⁻¹ once 𝒮 is instantiated at A₅, so the census's dual entries become assumption-free in statement while remaining computationally out of reach: no concrete certificate algebra is materialized by this theorem.

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

module FLRP.KurzweilNetter.Duality where

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

-- Imports from the Agda Standard Library ---------------------------------------
open import Data.Nat.Base    using ( ℕ )
open import Data.Product     using ( _,_ ; proj₁ )
open import Level            using ( 0ℓ )
open import Function         using ( id ; _∘_ )
open import Relation.Binary  using ( Setoid )
open import Relation.Nullary using ( ¬_ )

-- Imports from the Agda Universal Algebra Library ------------------------------
open import Classical.Properties.Lattice        using  ( module Lattice-Order )
open import Classical.Small.Structures.Lattice  using  ( Lattice )
open import Classical.Structures.Group.Basic    using  ( Group ; module Group-Op )
open import Classical.Structures.Lattice.Dual   using  ( dualLattice
                                                       ; module LatticeDual )
open import FLRP.Assumptions                    using  ( KurzweilNetterDualityAt
                                                       ; KurzweilNetterDuality
                                                       ; KurzweilSurjectivityᵈAt )
open import Classical.Structures.Group.Simple   using  ( module Simple )
open import FLRP.KurzweilNetter.Surjectivity  using  ( kurzweilSurjectivityᵈ )
open import FLRP.KurzweilNetter.Blocks          using  ( module KNBlocks )
open import FLRP.KurzweilNetter.Expansion       using  ( module KNExpansion )
open import FLRP.KurzweilNetter.Translations    using  ( module KNTranslations )
open import FLRP.Representable                  using  ( Representableᵈ ; ConIsoᵈ
                                                       ; _⊆ᵈ_ ; _≑ᵈ_
                                                       ; module ConIsoᵈ-Consequences )
open import Order.Iso                           using  ( OrderIso ; OrderIso-trans )
open import Overture                            using  ( Signature )
open import Setoid.Algebras.Basic               using  ( Algebra ; 𝕌[_] ; 𝔻[_] )
open import Setoid.Algebras.Finite              using  ( FiniteAlgebra )
open import Setoid.Algebras.Finite.Irredundant  using  ( IrredundantEnumeration
                                                       ; irredundantEnumeration )
open import Setoid.Congruences.Finite.Basic     using  ( DecCon )
open import Setoid.Signatures.Finite            using  ( FiniteSignature )

The glue module

KNGlue assembles the composite over an abstract irredundant enumeration and an abstract surjectivity witness at its size, and glues the stages with the generic composition OrderIso-trans of Order.Iso rather than by hand. Both choices are measured type-checking requirements, not style: with the concrete irredundantEnumeration value substituted throughout, or with the composite's round trips elaborated inline, the conversion checker re-normalizes the whole construction at each step (profiled at over three minutes for this one module) whereas over inert parameters, with the composition checked once against abstract relations, the same content checks in seconds. The instantiation happens once, in KurzweilNetterProof at the bottom.

module KNGlue
  {𝑆          : Signature 0ℓ 0ℓ}
  {𝑨          : Algebra {𝑆 = 𝑆} 0ℓ 0ℓ}
  (𝑆fin       : FiniteSignature 𝑆)
  (𝑬ᵢ         : IrredundantEnumeration 𝑨)
  (𝒮@(𝑺 , _)  : Group 0ℓ 0ℓ)  (open Setoid 𝔻[ 𝑺 ] using (_≈_))
                              (open Group-Op 𝒮 using (ε))
  (𝑭ₛ         : FiniteAlgebra 𝑺)
  (s₀         : 𝕌[ 𝑺 ])
  (s₀≉ε       : ¬ s₀ ≈ ε)
  (surjm      : KurzweilSurjectivityᵈAt 𝒮 (IrredundantEnumeration.icard 𝑬ᵢ))
  (𝓛@(𝑳 , _)  : Lattice)
  (iso        : ConIsoᵈ 𝑨 𝓛)
  where

The three stages are instantiated. The irredundant enumeration fixes the exponent m, the translation toolkit supplies the family the expansion lifts, and the expansion module builds the representing algebra 𝑬 on Sᵐ/D.

  private
    open KNBlocks 𝑨 𝑬ᵢ using  ( pvOf ; blockRel-mono ; pvOf-mono ; blockRel-pvOf-out
                              ; blockRel-pvOf-in ; pvOf-blockRel )
    open KNTranslations 𝑨 𝑆fin 𝑬ᵢ using  ( trCount ; trFamily ; blockConᶠ
                                         ; pvOf-invariant-family)
    open ConIsoᵈ-Consequences {𝑆 = 𝑆} {𝑨} {𝓛} iso using ( to-cong≑ )

    open Setoid 𝔻[ 𝑳 ] using () renaming ( trans to ≈ᴸ-trans )
    open KNExpansion 𝒮 𝑭ₛ s₀ s₀≉ε  (IrredundantEnumeration.icard 𝑬ᵢ)
      trCount trFamily surjm using ( InvPart ; _≈ᵛ_ ; _≥ᵛ_ ; expandedAlgebra
                                         ; expansionIso ; Sig-Exp
                                         ; expandedAlgebra-FiniteAlgebra
                                         ; Sig-Exp-FiniteSignature )

The middle stage of the composite. The family-invariant partitions are the decidable congruences of 𝑨, by the translation toolkit — the congruence of an invariant partition one way, the invariant partition of a congruence the other.

    -- an invariant partition presents a congruence of the represented algebra ...
    midTo : InvPart → DecCon 𝑨 0ℓ
    midTo (pv , h) = blockConᶠ pv h

    -- ... and a congruence has an invariant partition.
    midFrom : DecCon 𝑨 0ℓ → InvPart
    midFrom d = pvOf d , pvOf-invariant-family d

The middle stage as an order isomorphism in its own right. The round trips are the two dictionary round trips of FLRP.KurzweilNetter.Blocks, with the relation of midTo definitionally the block relation of the partition, so both directions of each round trip are the prepared lemmas applied verbatim.

    infix  _⊇ᵈ_

    -- reversed congruence containment (the middle stages run dually)
    _⊇ᵈ_ : DecCon 𝑨 0ℓ → DecCon 𝑨 0ℓ → Type _
    d ⊇ᵈ e = e ⊆ᵈ d

    midIso : OrderIso _≈ᵛ_ _≥ᵛ_ (_≑ᵈ_ {𝑨 = 𝑨} {ℓ = 0ℓ}) _⊇ᵈ_
    midIso = record
      { to         = midTo
      ; from       = midFrom
      ; to-mono    = λ {(P , _)} {(Q , _)} ge → blockRel-mono {pu = Q} {pw = P} ge
      ; from-mono  = λ {d} {e} sup → pvOf-mono e d sup
      ; to∘from    = λ d → blockRel-pvOf-out d , blockRel-pvOf-in d
      ; from∘to    = λ P → pvOf-blockRel (midTo P) (proj₁ P) id id
      }

The lattice stage, dualized: the maps and round trips of the given representation, with the monotonicity directions flipped through the two flip lemmas of Classical.Structures.Lattice.Dual.

    I₀-dual : OrderIso _≑ᵈ_ _⊇ᵈ_  (Setoid._≈_ 𝔻[ dualLattice 𝓛 .proj₁ ])
                                  (Lattice-Order._≤_ (dualLattice 𝓛))
    I₀-dual = record
      { to         = to
      ; from       = from
      ; to-mono    = ≤ᵈ-unflip ∘ to-mono
      ; from-mono  = from-mono ∘ ≤ᵈ-flip
      ; to∘from    = to∘from
      ; from∘to    = from∘to
      }
      where
      open OrderIso iso
      open LatticeDual 𝓛 using (≤ᵈ-unflip ; ≤ᵈ-flip)

The junction data for composing the three stages: transitivity of the mutual containments, and the congruence of each map with respect to the middle equivalence it crosses; every one of them is monotonicity applied twice.

    ≑ᴱ-trans : {a b c : DecCon expandedAlgebra 0ℓ} → a ≑ᵈ b → b ≑ᵈ c → a ≑ᵈ c
    ≑ᴱ-trans (p₁ , p₂) (q₁ , q₂) = q₁ ∘ p₁ , p₂ ∘ q₂

    ≑ᴬ-trans : {a b c : DecCon 𝑨 0ℓ} → a ≑ᵈ b → b ≑ᵈ c → a ≑ᵈ c
    ≑ᴬ-trans (p₁ , p₂) (q₁ , q₂) = q₁ ∘ p₁ , p₂ ∘ q₂

    midTo-cong : {P Q : InvPart} → P ≈ᵛ Q → midTo P ≑ᵈ midTo Q
    midTo-cong {(P , _)} {(Q , _)} (uw , wu) =
      blockRel-mono {pu = P} {pw = Q} uw , blockRel-mono {pu = Q} {pw = P} wu

    midFrom-cong : {d e : DecCon 𝑨 0ℓ} → d ≑ᵈ e → midFrom d ≈ᵛ midFrom e
    midFrom-cong {d} {e} (p , q) = pvOf-mono d e p , pvOf-mono e d q

    open OrderIso expansionIso using ( from ; from-mono)

    KEfrom-cong : {P Q : InvPart} → P ≈ᵛ Q → from P ≑ᵈ from Q
    KEfrom-cong {P} {Q} (uw , wu) = from-mono {P} {Q} wu , from-mono {Q} {P} uw

    stage₁-from-cong : {d e : DecCon 𝑨 0ℓ}
      → d ≑ᵈ e → from (midFrom d) ≑ᵈ from (midFrom e)
    stage₁-from-cong {d} {e} de = KEfrom-cong {midFrom d} {midFrom e} (midFrom-cong de)

The composite isomorphism DecCon 𝑬 ≅ dualLattice 𝑳: by two applications of OrderIso-trans of Order.Iso; order reversal happens once, inside the expansion isomorphism; the middle stages run against the reversed orders, and the boundary lands in the dual lattice's meet order.

    stage₁ : OrderIso _≑ᵈ_ _⊆ᵈ_ _≑ᵈ_ _⊇ᵈ_
    stage₁ = OrderIso-trans expansionIso midIso
      (λ {P} {Q} → midTo-cong {P} {Q})
      (λ {P} {Q} → KEfrom-cong {P} {Q})
      (λ {a} {b} {c} → ≑ᴱ-trans {a} {b} {c})
      (λ {a} {b} {c} → ≑ᴬ-trans {a} {b} {c})

    dualConIso : ConIsoᵈ expandedAlgebra (dualLattice 𝓛)
    dualConIso = OrderIso-trans stage₁ I₀-dual to-cong≑ stage₁-from-cong
      (λ {a} {b} {c} → ≑ᴱ-trans {a} {b} {c}) ≈ᴸ-trans

The representation of the dual: the expanded coset algebra, its finiteness and finite signature from the expansion module, and the composite isomorphism.

  -- The dual of a decidably representable lattice is decidably representable.
  dual-representation : Representableᵈ (dualLattice 𝓛)
  dual-representation = record
    { sigᵈ      = Sig-Exp
    ; algᵈ      = expandedAlgebra
    ; finiteᵈ   = expandedAlgebra-FiniteAlgebra
    ; finsigᵈ   = Sig-Exp-FiniteSignature
    ; con-isoᵈ  = dualConIso
    }

The theorem

KurzweilNetterProof fixes the base group with exactly the three property witnesses of the deliverable list, and instantiates the glue at the canonical irredundant enumeration of each representation.

One reading note, on what is proved where: the definitions below inhabit KurzweilNetterDuality inside this parameterized module, so this module's own result is conditional on its package. The closed inhabitants live downstream (FLRP.KurzweilNetter.Surjectivity discharges the surjectivity family; FLRP.KurzweilNetter.A5 closes the theorem at A₅), and the registry's Entry 2 records the same reading.

module KurzweilNetterProof
  (𝒮@(𝑺 , _)  : Group 0ℓ 0ℓ)
  (𝑭ₛ         : FiniteAlgebra 𝑺)
  (s₀         : 𝕌[ 𝑺 ])
  (s₀≉ε       : ¬ (Setoid._≈_ 𝔻[ 𝑺 ] s₀ (Group-Op.ε 𝒮)))
  (surj       : (n : ℕ) → KurzweilSurjectivityᵈAt 𝒮 n)
  where

  -- Kurzweil–Netter duality at a lattice.
  kurzweilNetterDualityAt : (𝑳 : Lattice) → KurzweilNetterDualityAt 𝑳
  kurzweilNetterDualityAt 𝑳 r = dual-representation
    where
    open Representableᵈ r  -- sigᵈ, algᵈ, finiteᵈ, finsigᵈ, con-isoᵈ

    𝑬ᵢ : IrredundantEnumeration algᵈ
    𝑬ᵢ = irredundantEnumeration finiteᵈ
    open IrredundantEnumeration 𝑬ᵢ
    open KNGlue finsigᵈ 𝑬ᵢ 𝒮 𝑭ₛ s₀ s₀≉ε (surj icard) 𝑳 con-isoᵈ

  -- The Kurzweil–Netter duality theorem, conditional on the module's package.
  kurzweilNetterDuality : KurzweilNetterDuality
  kurzweilNetterDuality 𝑳 = kurzweilNetterDualityAt 𝑳

The theorem, closed over the simple-group package

The four witnesses of the parameterized proof were the deliverable list of the argument; FLRP.KurzweilNetter.Surjectivity proves the fourth from the first three, so the theorem closes over the package alone: a finite carrier and the nonabelian-simplicity bundle, with the nontriviality witness derived from the bundle's non-commuting pair. Nothing else is assumed; FLRP.KurzweilNetter.A5 instantiates the package at the certified A₅.

module _ (𝒮@(𝑺 , _)  : Group 0ℓ 0ℓ)
         (𝑭ₛ          : FiniteAlgebra 𝑺)
         (nas         : Simple.IsNonabelianSimple 𝒮 0ℓ)
  where

  open Simple 𝒮 0ℓ using ( elt ; elt≉ε )

  -- Kurzweil–Netter duality, from a finite nonabelian simple base group alone.
  kurzweilNetterDuality-ofSimple : KurzweilNetterDuality
  kurzweilNetterDuality-ofSimple =
    KurzweilNetterProof.kurzweilNetterDuality 𝒮 𝑭ₛ (elt nas) (elt≉ε nas)
      (kurzweilSurjectivityᵈ 𝒮 𝑭ₛ nas)

---

---

1. Issue #501 remains open as the full polynomial-clone statement; nothing here waits on it. ↩