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).
_≥_ -- (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 𝑨.
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 𝒦