Skip to content

Setoid.Algebras.Products.Finite

Finiteness of finite powers

This is the Setoid.Algebras.Products.Finite module of the Agda Universal Algebra Library.

A finite power of a finite algebra is finite. This module discharges the FiniteAlgebra interface of Setoid.Algebras.Finite for the constant-family product β¨… (Ξ» (_ : Fin n) β†’ 𝑨) of Setoid.Algebras.Products β€” the power 𝑨ⁿ β€” from a finiteness witness for the base algebra 𝑨:

  • decidable equality is decided coordinatewise, by a finite conjunction of base-level decisions (all?);
  • the enumeration of the cardⁿ tuples is the standard library's positional base-card encoding finToFun, composed with the base enumeration coordinatewise;
  • surjectivity holds pointwise up to β‰ˆ β€” which is exactly the setoid equality of the product β€” with no appeal to function extensionality: the round-trip law finToFun-funToFin is itself pointwise.

The first consumer is the Kurzweil–Netter duality proof (issue #502), which needs the power Sᡐ of a finite group to be a finite algebra so that the coset algebra on Sᡐ/D inherits finiteness through cosetAlgebra-FiniteAlgebra of Classical.Structures.Group.GSet.

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

module Setoid.Algebras.Products.Finite where

-- Imports from the Agda Standard Library ---------------------------------------
open import Data.Fin.Base                          using ( Fin ; finToFun ; funToFin )
open import Data.Fin.Properties                    using ( all? ; finToFun-funToFin )
open import Data.Nat.Base                          using ( β„• ; _^_ )
open import Data.Product                           using ( _,_ ; proj₁ ; projβ‚‚ )
open import Level                                  using ( Level )
open import Relation.Binary                        using ( Setoid )
open import Relation.Binary.PropositionalEquality  using ( cong )

-- Imports from the Agda Universal Algebra Library ------------------------------
open import Overture                  using ( π“ž ; π“₯ ; Signature )
open import Setoid.Algebras.Basic     using ( Algebra ; π•Œ[_] ; 𝔻[_] )
open import Setoid.Algebras.Finite    using ( FiniteAlgebra )
open import Setoid.Algebras.Products  using ( β¨… )

private variable α ρ : Level

The finiteness witness for a power

module _ {𝑆 : Signature π“ž π“₯} {𝑨 : Algebra {𝑆 = 𝑆} Ξ± ρ} {n : β„•}
         (𝑭 : FiniteAlgebra 𝑨) where

  open Setoid 𝔻[ 𝑨 ] using ( _β‰ˆ_ ; trans ) renaming ( reflexive to β‰ˆ-reflexive )
  open FiniteAlgebra 𝑭 using ( _β‰Ÿ_ ; card ; enum ; enum-sur )

  private
    𝑷 : Algebra {𝑆 = 𝑆} Ξ± ρ
    𝑷 = β¨… {I = Fin n} (Ξ» _ β†’ 𝑨)

    -- The tuple encoded by an index: base enumeration after digit extraction.
    penum : Fin (card ^ n) β†’ π•Œ[ 𝑷 ]
    penum Ξ½ i = enum (finToFun Ξ½ i)

    -- The index encoding a tuple: the digits are the base indices of its values.
    pidx : π•Œ[ 𝑷 ] β†’ Fin (card ^ n)
    pidx x = funToFin Ξ» i β†’ enum-sur (x i) .proj₁

    -- The round trip hits the tuple coordinatewise, up to β‰ˆ.
    penum-pidx : (x : π•Œ[ 𝑷 ]) (i : Fin n) β†’ penum (pidx x) i β‰ˆ x i
    penum-pidx x i = trans
      (β‰ˆ-reflexive (cong enum (finToFun-funToFin (Ξ» j β†’ enum-sur (x j) .proj₁) i)))
      (enum-sur (x i) .projβ‚‚)

  -- A finite power of a finite algebra is finite.
  power-FiniteAlgebra : FiniteAlgebra 𝑷
  power-FiniteAlgebra = record
    { _β‰Ÿ_       = Ξ» x y β†’ all? (Ξ» i β†’ x i β‰Ÿ y i)
    ; card      = card ^ n
    ; enum      = penum
    ; enum-sur  = Ξ» x β†’ pidx x , penum-pidx x
    }