Setoid.Subalgebras.Subdirect.Basic¶
Subdirect product basics¶
This is the Setoid.Subalgebras.Subdirect.Basic module of the Agda Universal Algebra Library.
A subdirect product of a family 𝒜 : I → Algebra is a subalgebra of the product
⨅ 𝒜 whose every coordinate projection is surjective — the subalgebra meets every
factor. A subdirect embedding of 𝑨 is a monomorphism 𝑨 ↪ ⨅ 𝒜 exhibiting 𝑨
as such a subdirect product. These are the structures underlying Birkhoff's subdirect
representation theorem: every algebra is a subdirect product of subdirectly irreducible
algebras.
Subdirect products and subdirect embeddings¶
Fix a candidate algebra 𝑩 and a factor family 𝒜. The i-th coordinate map
of a homomorphism h : 𝑩 → ⨅ 𝒜 is the composite projᵢ ∘ h : 𝑩 → 𝒜 i.
The homomorphism h : 𝑩 → ⨅ 𝒜 is a subdirect embedding when it is injective and
every coordinate map is surjective.
module _ {𝑆 : Signature 𝓞 𝓥}{I : Type ι}{𝑩 : Algebra {𝑆 = 𝑆} β ρᵇ}(𝒜 : I → Algebra {𝑆 = 𝑆} α ρ) where -- The i-th coordinate map projᵢ ∘ h of a hom into the product. coord : hom 𝑩 (⨅ 𝒜) → (i : I) → hom 𝑩 (𝒜 i) coord h i = ⊙-hom h (⨅-proj 𝒜 i) record IsSubdirectEmbedding (h : hom 𝑩 (⨅ 𝒜)) : Type (ι ⊔ α ⊔ ρ ⊔ β ⊔ ρᵇ) where field embed-inj : IsInjective (proj₁ h) proj-onto : (i : I) → IsSurjective (proj₁ (coord h i)) open IsSubdirectEmbedding public -- A subdirect embedding of 𝑩 into ⨅ 𝒜; i.e., 𝑩 is a subdirect product of 𝒜. SubdirectEmbedding : Type (𝓞 ⊔ 𝓥 ⊔ ι ⊔ α ⊔ ρ ⊔ β ⊔ ρᵇ) SubdirectEmbedding = Σ[ h ∈ hom 𝑩 (⨅ 𝒜) ] IsSubdirectEmbedding h -- A subdirect embedding is in particular a subalgebra inclusion 𝑩 ≤ ⨅ 𝒜. subdirect→≤ : SubdirectEmbedding → 𝑩 ≤ ⨅ 𝒜 subdirect→≤ (h , emb) = h , embed-inj emb
The bridge: a separating family of congruences gives a subdirect embedding¶
Now the constructive heart. Fix an algebra 𝑨 and a family of congruences
θ : I → Con 𝑨. Form the family of quotients i ↦ 𝑨 ╱ θ i and the natural map
into their product, assembled from the canonical quotient projections πhom (θ i).
module _ {𝑆 : Signature 𝓞 𝓥}{I : Type ι}{𝑨 : Algebra {𝑆 = 𝑆} α ρ}(θ : I → Con 𝑨 ℓ) where -- the family of quotient algebras and the natural map into their product 𝑨╱ : I → Algebra {𝑆 = 𝑆} α ℓ 𝑨╱ i = 𝑨 ╱ θ i natmap : hom 𝑨 (⨅ 𝑨╱) natmap = ⨅-hom-co 𝑨╱ (λ i → πhom 𝒾𝒹 (θ i))
The family separates points when the only pairs related by every θ i are the
≈-equal ones — i.e. the meet ⋂ θ is the diagonal 0ᴬ. This is exactly the
injectivity of the natural map: an element's image in the product is its tuple of
congruence classes, and two elements have the same tuple iff every θ i relates
them.
-- the meet ⋂ θ is the diagonal 0ᴬ: every θ i relating a,b forces a ≈ b. Separates : Type (ι ⊔ α ⊔ ρ ⊔ ℓ) Separates = ∀ {a b} → (∀ i → proj₁ (θ i) a b) → a ≈ b where open Setoid 𝔻[ 𝑨 ] using ( _≈_ ) -- Injectivity of the natural map is definitionally the separation property. natmap-injective : Separates → IsInjective (proj₁ natmap) natmap-injective = id natmap-separates : IsInjective (proj₁ natmap) → Separates natmap-separates = id _ : IsInjective (proj₁ natmap) ≡ Separates _ = refl
Each coordinate map projᵢ ∘ natmap is the canonical quotient epimorphism
𝑨 ↠ 𝑨 ╱ θ i, hence surjective — with no decidability or choice assumption on the
index.
natmap-proj-onto : (i : I) → IsSurjective (proj₁ (coord 𝑨╱ natmap i)) natmap-proj-onto i = IsEpi.isSurjective (proj₂ (πepi 𝒾𝒹 (θ i)))
Assembling injectivity and the surjective coordinate maps gives the subdirect embedding.
separating→subdirect : Separates → IsSubdirectEmbedding 𝑨╱ natmap separating→subdirect sep = record { embed-inj = natmap-injective sep ; proj-onto = natmap-proj-onto } separating→SubdirectEmbedding : Separates → SubdirectEmbedding 𝑨╱ separating→SubdirectEmbedding sep = natmap , separating→subdirect sep