↑ Top


Types for Substructures of General Structures

This is the Base.Structures.Substructures module of the Agda Universal Algebra Library.


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

module Base.Structures.Substructures where

-- Imports from Agda and the Agda Standard Library ------------------------------------
open import Agda.Primitive   using () renaming ( Set to Type )
open import Data.Product     using ( _,_ ; Σ-syntax ; _×_ ) renaming ( proj₂ to snd )
open import Function         using ( _∘_ )
open import Level            using ( _⊔_ ; suc ; Level )
open import Relation.Binary  using ( REL )
open import Relation.Unary   using ( Pred ; _∈_ ; _⊆_ ;  )
open import Relation.Binary.PropositionalEquality
                             using ( _≡_ ; module ≡-Reasoning )

-- Imports from the Agda Universal Algebra Library -------------------------------------
open import Overture         using ( ∣_∣ ; ∥_∥ ; _⁻¹ )
open import Base.Functions   using ( IsInjective )
open import Base.Relations   using ( Im_⊆_ ; PredType )
open import Base.Equality    using ( swelldef )
open import Base.Terms       using ( Term ) -- ; _⟦_⟧ )

open import Base.Structures.Basic  using ( signature ; structure ; _ᵒ_ ; sigl )
                                   using ( siglˡ ; siglʳ )
open import Base.Structures.Homs   using ( hom )
open import Base.Structures.Terms  using ( _⟦_⟧ )

open structure ; open signature

private variable
 𝓞₀ 𝓥₀ 𝓞₁ 𝓥₁ ρ α ρᵃ β ρᵇ γ ρᶜ χ ι : Level
 𝐹 : signature 𝓞₀ 𝓥₀
 𝑅 : signature 𝓞₁ 𝓥₁

module _ {𝑨 : structure 𝐹 𝑅 {α}{ρᵃ}} {X : Type χ} where

 Subuniverses : Pred (Pred (carrier 𝑨) ρ) (sigl 𝐹  α  ρ)
 Subuniverses B =  f a  Im a  B  (f  𝑨) a  B

 -- Subuniverses as a record type
 record Subuniverse : Type (sigl 𝐹  α  suc ρ) where
  constructor mksub
  field
   sset  : Pred (carrier 𝑨) ρ
   isSub : sset  Subuniverses

 -- Subuniverse Generation
 data Sg (G : Pred (carrier 𝑨) ρ) : Pred (carrier 𝑨) (sigl 𝐹  α  ρ) where
  var :  {v}  v  G  v  Sg G
  app :  f a  Im a  Sg G  (f  𝑨) a  Sg G

(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 : {G : Pred (carrier 𝑨) ρ}  Sg G  Subuniverses
 sgIsSub = app

Next we prove by structural induction that Sg X is the smallest subuniverse of 𝑨 containing X.


 sgIsSmallest :  {G : Pred (carrier 𝑨) ρ}(B : Pred (carrier 𝑨) ρᵇ)
                B  Subuniverses    G  B    Sg G  B

 sgIsSmallest _ _ G⊆B (var Gx) = G⊆B Gx
 sgIsSmallest B B≤A G⊆B {.((f  𝑨) a)} (app f a SgGa) = Goal
  where
  IH : Im a  B
  IH i = sgIsSmallest B B≤A G⊆B (SgGa i)

  Goal : (f  𝑨) a  B
  Goal = B≤A f a IH

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


 ⋂s :  (I : Type ι){𝒜 : I  Pred (carrier 𝑨) ρ}
      (∀ i  𝒜 i  Subuniverses)   I 𝒜  Subuniverses

 ⋂s I σ f a ν = λ i  σ i f a  x  ν x i)

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

ν    : Im a ⊆ ⋂ I 𝒜
a    : arity 𝐹 f → carrier 𝑨
f    : symbol 𝐹
σ    : (i : I) → 𝒜 i ∈ Subuniverses
𝒜    : I → Pred (carrier 𝑨) ρ   (not in scope)

and we must prove (f ᵒ 𝑨) a ∈ ⋂ I 𝒜. Agda can fill in the proof term λ i → σ i f a (λ x → ν x i) automatically using C-c C-a.


 open Term
 -- subuniverses are closed under the action of term operations
 sub-term-closed :  (B : Pred (carrier 𝑨) ρ)  (B  Subuniverses)
                   (t : Term X)(b : X  (carrier 𝑨))
                   (Im b  B)  (𝑨  t ) b  B

 sub-term-closed _ _ ( x) b Bb = Bb x

 sub-term-closed B B≤A (node f t) b ν =
  B≤A f  z  (𝑨  t z ) b)  x  sub-term-closed B B≤A (t x) b ν)

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

ν    : Im b ⊆ B
b    : X → carrier 𝑨
t    : arity 𝐹 f → Term X
f    : symbol 𝐹
B≤A  : B ∈ Subuniverses
B    : Pred (carrier 𝑨) ρ
𝑨    : structure 𝐹 𝑅

and the given proof term establishes the goal op 𝑨 f (λ i → (𝑨 ⟦ t i ⟧) b) ∈ B

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


 data TermImage (B : Pred (carrier 𝑨) ρ) : Pred (carrier 𝑨) (sigl 𝐹  α  ρ)
  where
  var :  {b : carrier 𝑨}  b  B  b  TermImage B
  app :  f ts  ((i : (arity 𝐹) f)  ts i  TermImage B)   (f  𝑨) ts  TermImage B

 -- `TermImage B` is a subuniverse of 𝑨 that contains B.
 TermImageIsSub : {B : Pred (carrier 𝑨) ρ}  TermImage B  Subuniverses
 TermImageIsSub = app

 B-onlyif-TermImageB : {B : Pred (carrier 𝑨) ρ}  B  TermImage B
 B-onlyif-TermImageB Ba = var Ba

 -- Since `Sg B` is the smallest subuniverse containing B, we obtain the following inclusion.
 SgB-onlyif-TermImageB : (B : Pred (carrier 𝑨) ρ)  Sg B  TermImage B
 SgB-onlyif-TermImageB B = sgIsSmallest  (TermImage B)
                                         TermImageIsSub B-onlyif-TermImageB

 module _ {𝑩 : structure 𝐹 𝑅 {β}{ρᵇ}} where
  private
   A = carrier 𝑨
   B = carrier 𝑩

  -- Homomorphisms are uniquely determined by their values on a generating set.
  hom-unique :  swelldef (siglʳ 𝐹) β  (G : Pred A ρ)  (g h : hom 𝑨 𝑩)
               ((x : A)  (x  G   g  x   h  x))
                -------------------------------------------------
               (a : A)  (a  Sg G   g  a   h  a)

  hom-unique _ G g h σ a (var Ga) = σ a Ga
  hom-unique wd G g h σ .((f  𝑨) a) (app f a SgGa) = Goal
   where
   IH :  x   g  (a x)   h  (a x)
   IH x = hom-unique wd G g h σ (a x) (SgGa x)
   open ≡-Reasoning
   Goal :  g  ((f  𝑨) a)   h  ((f  𝑨) a)
   Goal =   g  ((f  𝑨) a)    ≡⟨ snd  g  f a 
           (f  𝑩)( g   a )  ≡⟨ wd (f  𝑩) ( g   a) ( h   a) IH 
           (f  𝑩)( h   a)   ≡⟨ (snd  h  f a)⁻¹ 
            h  ((f  𝑨) a )   

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

SgGa : Im a ⊆ Sg G
a    : arity 𝐹 f → carrier 𝑨
f    : symbol 𝐹
σ    : (x : A) → x ∈ G → ∣ g ∣ x ≡ ∣ h ∣ x
h    : hom 𝑨 𝑩
g    : hom 𝑨 𝑩
G    : Pred A ρ
wd   : swelldef (siglʳ 𝐹) β
𝑩    : structure 𝐹 𝑅

and, under these assumptions, we proved ∣ g ∣ ((f ᵒ 𝑨) a) ≡ ∣ h ∣ ((f ᵒ 𝑨) a).

Substructures


_≥_  -- (alias for supstructure (aka parent structure; aka overstructure))
 _IsSupstructureOf_ :  structure 𝐹 𝑅 {α}{ρᵃ}  structure 𝐹 𝑅 {β}{ρᵇ}
                      Type (sigl 𝐹  sigl 𝑅  α  ρᵃ  β  ρᵇ)

𝑨 IsSupstructureOf 𝑩 = Σ[ h  hom 𝑩 𝑨 ] IsInjective  h 


_≤_  -- (alias for subalgebra relation))
 _IsSubstructureOf_ :  structure 𝐹 𝑅 {α}{ρᵃ}  structure 𝐹 𝑅 {β}{ρᵇ}
                      Type (sigl 𝐹  sigl 𝑅  α  ρᵃ  β  ρᵇ )

𝑨 IsSubstructureOf 𝑩 = Σ[ h  hom 𝑨 𝑩 ] IsInjective  h 

-- Syntactic sugar for sup/sub-algebra relations.
𝑨  𝑩 = 𝑨 IsSupstructureOf 𝑩
𝑨  𝑩 = 𝑨 IsSubstructureOf 𝑩


record SubstructureOf : Type (sigl 𝐹  sigl 𝑅  suc (α  ρᵃ  β  ρᵇ)) where
 field
  struc       : structure 𝐹 𝑅 {α}{ρᵃ}
  substruc    : structure 𝐹 𝑅 {β}{ρᵇ}
  issubstruc  : substruc  struc



module _ {𝐹 : signature 𝓞₀ 𝓥₀}{𝑅 : signature 𝓞₁ 𝓥₁} where

 Substructure :  structure 𝐹 𝑅 {α}{ρᵃ}  {β ρᵇ : Level}
                Type (sigl 𝐹  sigl 𝑅  α  ρᵃ  suc (β  ρᵇ))

 Substructure 𝑨 {β}{ρᵇ} = Σ[ 𝑩  (structure 𝐹 𝑅 {β}{ρᵇ}) ] 𝑩  𝑨

 {- For 𝑨 : structure 𝐹 𝑅 {α}{ρᵃ}, inhabitant of `Substructure 𝑨` is
    a pair `(𝑩 , p) : Substructure 𝑨`  providing
    + a structure, `𝑩 : structure 𝐹 𝑅 {β}{ρᵇ}`, and
    + a proof, `p : 𝑩 ≤ 𝑨`, that 𝑩 is a substructure of 𝐴. -}


 IsSubstructureREL :   {α}{ρᵃ}{β}{ρᵇ}
                     REL (structure 𝐹 𝑅 {α}{ρᵃ})(structure 𝐹 𝑅 {β}{ρᵇ}) ρ
                     Type (sigl 𝐹  sigl 𝑅  suc (α  ρᵃ  β  ρᵇ))

 IsSubstructureREL {α = α}{ρᵃ}{β}{ρᵇ} R =   {𝑨 : structure 𝐹 𝑅 {α}{ρᵃ}}
                                             {𝑩 : structure 𝐹 𝑅 {β}{ρᵇ}}  𝑨  𝑩

From now on we will use 𝑩 ≤ 𝑨 to express the assertion that 𝑩 is a subalgebra of 𝑨.

Substructures of a class of algebras

Suppose 𝒦 : Pred (Algebra α 𝑆) γ denotes a class of 𝑆-algebras and 𝑩 : structure 𝐹 𝑅 {β}{ρᵇ} denotes an arbitrary 𝑆-algebra. Then we might wish to consider the assertion that 𝑩 is a subalgebra of an algebra in the class 𝒦. The next type we define allows us to express this assertion as 𝑩 IsSubstructureOfClass 𝒦.


 _≤c_  -- (alias for substructure-of-class relation)
  _IsSubstructureOfClass_ :  structure 𝐹 𝑅 {β}{ρᵇ}  Pred (structure 𝐹 𝑅 {α}{ρᵃ}) ρ
                            Type (sigl 𝐹  sigl 𝑅  suc (α  ρᵃ)  β  ρᵇ  ρ)

 𝑩 IsSubstructureOfClass 𝒦 = Σ[ 𝑨  PredType 𝒦 ] ((𝑨  𝒦) × (𝑩  𝑨))

 𝑩 ≤c 𝒦 = 𝑩 IsSubstructureOfClass 𝒦

 record SubstructureOfClass : Type (sigl 𝐹  sigl 𝑅  suc (α  ρ  β  ρᵇ  ρᵃ)) where
  field
   class : Pred (structure 𝐹 𝑅 {α}{ρᵃ}) ρ
   substruc : structure 𝐹 𝑅 {β}{ρᵇ}
   issubstrucofclass : substruc ≤c class


 record SubstructureOfClass' : Type (sigl 𝐹  sigl 𝑅  suc (α  ρ  β  ρᵇ  ρᵃ)) where
  field
   class : Pred (structure 𝐹 𝑅 {α}{ρᵃ}) ρ
   classalgebra    : structure 𝐹 𝑅 {α}{ρᵃ}
   isclassalgebra  : classalgebra  class
   subalgebra      : structure 𝐹 𝑅 {β}{ρᵇ}
   issubalgebra    : subalgebra  classalgebra

 -- The collection of subalgebras of algebras in class 𝒦.
 SubstructuresOfClass :  Pred (structure 𝐹 𝑅 {α}{ρᵃ}) ρ  {β ρᵇ : Level}
                        Type (sigl 𝐹  sigl 𝑅  suc (α  ρᵃ  β  ρᵇ)  ρ)

 SubstructuresOfClass 𝒦 {β}{ρᵇ} = Σ[ 𝑩  structure 𝐹 𝑅 {β}{ρᵇ} ] 𝑩 ≤c 𝒦

← Base.Structures.Terms Base.Structures.EquationalLogic →