โ†‘ Top


Subuniverses

This is the Subalgebras.Subuniverses module of the Agda Universal Algebra Library.

We start by defining a type that represents the important concept of subuniverse. Suppose ๐‘จ is an algebra. A subset B โŠ† โˆฃ ๐‘จ โˆฃ is said to be closed under the operations of ๐‘จ if for each ๐‘“ โˆˆ โˆฃ ๐‘† โˆฃ and all tuples ๐’ƒ : โˆฅ ๐‘† โˆฅ ๐‘“ โ†’ ๐ต the element (๐‘“ ฬ‚ ๐‘จ) ๐’ƒ belongs to B. If a subset B โŠ† ๐ด is closed under the operations of ๐‘จ, then we call B a subuniverse of ๐‘จ.

{-# OPTIONS --without-K --exact-split --safe #-}

open import Algebras.Basic using ( ๐“ž ; ๐“ฅ ; Signature )

module Subalgebras.Subuniverses {๐‘† : Signature ๐“ž ๐“ฅ} where

-- Imports from Agda and the Agda Standard Library -----------------------------
open import Agda.Primitive using ( _โŠ”_ ; lsuc ; Level ) renaming ( Set to Type )
open import Axiom.Extensionality.Propositional
                           using () renaming (Extensionality to funext)
open import Function.Base  using ( _โˆ˜_ )
open import Relation.Binary.PropositionalEquality
                           using ( module โ‰ก-Reasoning ; _โ‰ก_ )
open import Relation.Unary using ( Pred ; _โˆˆ_ ; _โŠ†_ ; โ‹‚ )

-- Imports from the Agda Universal Algebra Library -----------------------------
open import Overture.Preliminaries      using ( โˆฃ_โˆฃ ; โˆฅ_โˆฅ ; _โปยน )
open import Relations.Discrete          using ( Im_โŠ†_ )
open import Equality.Welldefined        using ( swelldef )
open import Algebras.Basic              using ( Algebra ; _ฬ‚_ )
open import Algebras.Products   {๐‘† = ๐‘†} using ( ov )
open import Terms.Basic         {๐‘† = ๐‘†} using ( Term ; โ„Š ; node )
open import Terms.Operations    {๐‘† = ๐‘†} using ( _โŸฆ_โŸง )
open import Homomorphisms.Basic {๐‘† = ๐‘†} using ( hom )

private variable ฮฑ ฮฒ ๐“ง : Level

We first show how to represent in Agda the collection of subuniverses of an algebra ๐‘จ. Since a subuniverse is viewed as a subset of the domain of ๐‘จ, we define it as a predicate on โˆฃ ๐‘จ โˆฃ. Thus, the collection of subuniverses is a predicate on predicates on โˆฃ ๐‘จ โˆฃ.

Subuniverses : (๐‘จ : Algebra ฮฑ ๐‘†) โ†’ Pred (Pred โˆฃ ๐‘จ โˆฃ ฮฒ) (๐“ž โŠ” ๐“ฅ โŠ” ฮฑ โŠ” ฮฒ)

Subuniverses ๐‘จ B = (๐‘“ : โˆฃ ๐‘† โˆฃ)(๐‘Ž : โˆฅ ๐‘† โˆฅ ๐‘“ โ†’ โˆฃ ๐‘จ โˆฃ) โ†’ Im ๐‘Ž โŠ† B โ†’ (๐‘“ ฬ‚ ๐‘จ) ๐‘Ž โˆˆ B

Subuniverses as records

Next we define a type to represent a single subuniverse of an algebra. If ๐‘จ is the algebra in question, then a subuniverse of ๐‘จ is a subset of (i.e., predicate over) the domain โˆฃ ๐‘จ โˆฃ that belongs to Subuniverses ๐‘จ.

record Subuniverse {๐‘จ : Algebra ฮฑ ๐‘†} : Type(ov ฮฒ โŠ” ฮฑ) where
 constructor mksub
 field       sset  : Pred โˆฃ ๐‘จ โˆฃ ฮฒ
             isSub : sset โˆˆ Subuniverses ๐‘จ

Subuniverse Generation

If ๐‘จ is an algebra and X โŠ† โˆฃ ๐‘จ โˆฃ a subset of the domain of ๐‘จ, then the subuniverse of ๐‘จ generated by X is typically denoted by Sg๐‘จ(X) and defined to be the smallest subuniverse of ๐‘จ containing X. Equivalently,

Sg๐‘จ(X) = โ‹‚ { U : U is a subuniverse of ๐‘จ and B โŠ† U }.

We define an inductive type, denoted by Sg, that represents the subuniverse generated by a given subset of the domain of a given algebra, as follows.

data Sg (๐‘จ : Algebra ฮฑ ๐‘†)(X : Pred โˆฃ ๐‘จ โˆฃ ฮฒ) : Pred โˆฃ ๐‘จ โˆฃ (๐“ž โŠ” ๐“ฅ โŠ” ฮฑ โŠ” ฮฒ)
 where
 var : โˆ€ {v} โ†’ v โˆˆ X โ†’ v โˆˆ Sg ๐‘จ X
 app : โˆ€ f a โ†’ Im a โŠ† Sg ๐‘จ X โ†’ (f ฬ‚ ๐‘จ) a โˆˆ Sg ๐‘จ X

(The inferred types in the app constructor are f : โˆฃ ๐‘† โˆฃ and a : โˆฅ ๐‘† โˆฅ ๐‘“ โ†’ โˆฃ ๐‘จ โˆฃ.)

Given an arbitrary subset X of the domain โˆฃ ๐‘จ โˆฃ of an ๐‘†-algebra ๐‘จ, the type Sg X does indeed represent a subuniverse of ๐‘จ. Proving this using the inductive type Sg is trivial, as we see here.

sgIsSub : {๐‘จ : Algebra ฮฑ ๐‘†}{X : Pred โˆฃ ๐‘จ โˆฃ ฮฒ} โ†’ Sg ๐‘จ X โˆˆ Subuniverses ๐‘จ
sgIsSub = app

Next we prove by structural induction that Sg X is the smallest subuniverse of ๐‘จ containing X.

sgIsSmallest : {๐“ก : Level}(๐‘จ : Algebra ฮฑ ๐‘†){X : Pred โˆฃ ๐‘จ โˆฃ ฮฒ}(Y : Pred โˆฃ ๐‘จ โˆฃ ๐“ก)
 โ†’             Y โˆˆ Subuniverses ๐‘จ  โ†’  X โŠ† Y  โ†’  Sg ๐‘จ X โŠ† Y

sgIsSmallest _ _ _ XinY (var Xv) = XinY Xv
sgIsSmallest ๐‘จ Y YsubA XinY (app f a SgXa) = Yfa
 where
 IH : Im a โŠ† Y
 IH i = sgIsSmallest ๐‘จ Y YsubA XinY (SgXa i)

 Yfa : (f ฬ‚ ๐‘จ) a โˆˆ Y
 Yfa = YsubA f a IH

When the element of Sg X is constructed as app f a SgXa, we may assume (the induction hypothesis) that the arguments in the tuple a belong to Y. Then the result of applying f to a also belongs to Y since Y is a subuniverse.

Subuniverse Lemmas

Here we formalize a few basic properties of subuniverses. First, the intersection of subuniverses is again a subuniverse.

โ‹‚s : {๐“˜ : Level}{๐‘จ : Algebra ฮฑ ๐‘†}{I : Type ๐“˜}{๐’œ : I โ†’ Pred โˆฃ ๐‘จ โˆฃ ฮฒ}
 โ†’   (โˆ€ i โ†’ ๐’œ i โˆˆ Subuniverses ๐‘จ) โ†’ โ‹‚ I ๐’œ โˆˆ Subuniverses ๐‘จ

โ‹‚s ฯƒ f a ฮฝ = ฮป i โ†’ ฯƒ i f a (ฮป x โ†’ ฮฝ x i)

In the proof above, we assume the following typing judgments:

 ฯƒ : โˆ€ i โ†’ ๐’œ i โˆˆ Subuniverses ๐‘จ
 f : โˆฃ ๐‘† โˆฃ
 a : โˆฅ ๐‘† โˆฅ ๐‘“ โ†’ โˆฃ ๐‘จ โˆฃ
 ฮฝ : Im ๐‘Ž โŠ† โ‹‚ I ๐’œ

and we must prove (f ฬ‚ ๐‘จ) a โˆˆ โ‹‚ I ๐’œ. In this case, Agda will fill in the proof term ฮป i โ†’ ฯƒ i f a (ฮป x โ†’ ฮฝ x i) automatically with the command C-c C-a.

Next, subuniverses are closed under the action of term operations.

sub-term-closed : {๐“ง : Level}{X : Type ๐“ง}(๐‘จ : Algebra ฮฑ ๐‘†){B : Pred โˆฃ ๐‘จ โˆฃ ฮฒ}
 โ†’                (B โˆˆ Subuniverses ๐‘จ) โ†’ (t : Term X)(b : X โ†’ โˆฃ ๐‘จ โˆฃ)
 โ†’                ((x : X) โ†’ (b x โˆˆ B)) โ†’ (๐‘จ โŸฆ t โŸง)b โˆˆ B

sub-term-closed ๐‘จ AB (โ„Š x) b Bb = Bb x

sub-term-closed ๐‘จ{B} ฯƒ (node f t)b ฮฝ =
  ฯƒ f  (ฮป z โ†’ (๐‘จ โŸฆ t z โŸง) b) ฮป x โ†’ sub-term-closed ๐‘จ{B} ฯƒ (t x) b ฮฝ

In the induction step of the foregoing proof, the typing judgments of the premise are the following:

๐‘จ   : Algebra ฮฑ ๐‘†
B   : Pred โˆฃ ๐‘จ โˆฃ ฮฒ
ฯƒ   : B โˆˆ Subuniverses ๐‘จ
f   : โˆฃ ๐‘† โˆฃ
t   : โˆฅ ๐‘† โˆฅ ๐‘“ โ†’ Term X
b   : X โ†’ โˆฃ ๐‘จ โˆฃ
ฮฝ   : โˆ€ x โ†’ b x โˆˆ B

and the given proof term establishes the goal ๐‘จ โŸฆ node f t โŸง b โˆˆ B.

Alternatively, we could express the preceeding fact using an inductive type representing images of terms.

data TermImage (๐‘จ : Algebra ฮฑ ๐‘†)(Y : Pred โˆฃ ๐‘จ โˆฃ ฮฒ) : Pred โˆฃ ๐‘จ โˆฃ (๐“ž โŠ” ๐“ฅ โŠ” ฮฑ โŠ” ฮฒ)
 where
 var : โˆ€ {y : โˆฃ ๐‘จ โˆฃ} โ†’ y โˆˆ Y โ†’ y โˆˆ TermImage ๐‘จ Y
 app : โˆ€ ๐‘“ ๐‘ก โ†’  ((x : โˆฅ ๐‘† โˆฅ ๐‘“) โ†’ ๐‘ก x โˆˆ TermImage ๐‘จ Y)  โ†’ (๐‘“ ฬ‚ ๐‘จ) ๐‘ก โˆˆ TermImage ๐‘จ Y

By what we proved above, it should come as no surprise that TermImage ๐‘จ Y is a subuniverse of ๐‘จ that contains Y.

TermImageIsSub : {๐‘จ : Algebra ฮฑ ๐‘†}{Y : Pred โˆฃ ๐‘จ โˆฃ ฮฒ} โ†’ TermImage ๐‘จ Y โˆˆ Subuniverses ๐‘จ
TermImageIsSub = app

Y-onlyif-TermImageY : {๐‘จ : Algebra ฮฑ ๐‘†}{Y : Pred โˆฃ ๐‘จ โˆฃ ฮฒ} โ†’ Y โŠ† TermImage ๐‘จ Y
Y-onlyif-TermImageY {a} Ya = var Ya

Since Sg ๐‘จ Y is the smallest subuniverse containing Y, we obtain the following inclusion.

SgY-onlyif-TermImageY : (๐‘จ : Algebra ฮฑ ๐‘†)(Y : Pred โˆฃ ๐‘จ โˆฃ ฮฒ) โ†’ Sg ๐‘จ Y โŠ† TermImage ๐‘จ Y
SgY-onlyif-TermImageY ๐‘จ Y = sgIsSmallest ๐‘จ (TermImage ๐‘จ Y) TermImageIsSub Y-onlyif-TermImageY

Next we prove the important fact that homomorphisms are uniquely determined by their values on a generating set.

open โ‰ก-Reasoning

hom-unique : swelldef ๐“ฅ ฮฒ โ†’ {๐‘จ : Algebra ฮฑ ๐‘†}{๐‘ฉ : Algebra ฮฒ ๐‘†}
             (X : Pred โˆฃ ๐‘จ โˆฃ ฮฑ)  (g h : hom ๐‘จ ๐‘ฉ)
 โ†’           ((x : โˆฃ ๐‘จ โˆฃ) โ†’ (x โˆˆ X โ†’ โˆฃ g โˆฃ x โ‰ก โˆฃ h โˆฃ x))
             -------------------------------------------------
 โ†’           (a : โˆฃ ๐‘จ โˆฃ) โ†’ (a โˆˆ Sg ๐‘จ X โ†’ โˆฃ g โˆฃ a โ‰ก โˆฃ h โˆฃ a)

hom-unique _ _ _ _ ฯƒ a (var x) = ฯƒ a x

hom-unique wd {๐‘จ}{๐‘ฉ} X g h ฯƒ fa (app ๐‘“ a ฮฝ) = Goal
 where
 IH : โˆ€ x โ†’ โˆฃ g โˆฃ (a x) โ‰ก โˆฃ h โˆฃ (a x)
 IH x = hom-unique wd{๐‘จ}{๐‘ฉ} X g h ฯƒ (a x) (ฮฝ x)

 Goal : โˆฃ g โˆฃ ((๐‘“ ฬ‚ ๐‘จ) a) โ‰ก โˆฃ h โˆฃ ((๐‘“ ฬ‚ ๐‘จ) a)
 Goal = โˆฃ g โˆฃ ((๐‘“ ฬ‚ ๐‘จ) a)   โ‰กโŸจ โˆฅ g โˆฅ ๐‘“ a โŸฉ
        (๐‘“ ฬ‚ ๐‘ฉ)(โˆฃ g โˆฃ โˆ˜ a ) โ‰กโŸจ wd (๐‘“ ฬ‚ ๐‘ฉ) (โˆฃ g โˆฃ โˆ˜ a) (โˆฃ h โˆฃ โˆ˜ a) IH โŸฉ
        (๐‘“ ฬ‚ ๐‘ฉ)(โˆฃ h โˆฃ โˆ˜ a)  โ‰กโŸจ ( โˆฅ h โˆฅ ๐‘“ a )โปยน โŸฉ
        โˆฃ h โˆฃ ((๐‘“ ฬ‚ ๐‘จ) a )  โˆŽ

In the induction step, the following typing judgments are assumed:

wd  : swelldef ๐“ฅ ฮฒ
๐‘จ   : Algebra ฮฑ ๐‘†
๐‘ฉ   : Algebra ฮฒ ๐‘†
X   : Pred โˆฃ ๐‘จ โˆฃ ฮฑ
g h  : hom ๐‘จ ๐‘ฉ
ฯƒ   : ฮ  x ๊ž‰ โˆฃ ๐‘จ โˆฃ , (x โˆˆ X โ†’ โˆฃ g โˆฃ x โ‰ก โˆฃ h โˆฃ x)
fa  : โˆฃ ๐‘จ โˆฃ
fa  = (๐‘“ ฬ‚ ๐‘จ) a
๐‘“   : โˆฃ ๐‘† โˆฃ
a   : โˆฅ ๐‘† โˆฅ ๐‘“ โ†’ โˆฃ ๐‘จ โˆฃ
ฮฝ   : Im a โŠ† Sg ๐‘จ X

and, under these assumptions, we proved โˆฃ g โˆฃ ((๐‘“ ฬ‚ ๐‘จ) a) โ‰ก โˆฃ h โˆฃ ((๐‘“ ฬ‚ ๐‘จ) a).


โ†‘ Subalgebras Subalgebras.Subalgebras โ†’