Category Theory in Foundations of Computer Science Andrzej Tarlecki

(Universal Algebra and)

Category Theory

in Foundations of Computer Science

Andrzej Tarlecki

Institute of Informatics

Faculty of Mathematics, Informatics and Mechanics University of Warsaw

http://www.mimuw.edu.pl/~tarlecki office: 4750 tarlecki@mimuw.edu.pl phone (office): (48)(22)(55) 44475

Universal algebra and category theory:

basic ideas, notions and some results

• Algebras, homomorphisms, equations: basic definitions and results

• Categories; examples and simple categorical definitions

• Limits and colimits

• Functors and natural transformations

• Adjunctions

• Cartesian closed categories

• Monads

• Institutions (abstract model theory, abstract specification theory)

BUT: Tell me what you want to learn!

Universal algebra and category theory:

basic ideas, notions and some results

• Algebras, homomorphisms, equations: basic definitions and results

• Categories; examples and simple categorical definitions

• Limits and colimits

• Functors and natural transformations

• Adjunctions

• Cartesian closed categories

• Monads

• Institutions (abstract model theory, abstract specification theory)

Universal algebra and category theory:

basic ideas, notions and some results

• Algebras, homomorphisms, equations: basic definitions and results

• Categories; examples and simple categorical definitions

• Limits and colimits

• Functors and natural transformations

• Adjunctions

• Cartesian closed categories

• Monads

• Institutions (abstract model theory, abstract specification theory)

BUT: Tell me what you want to learn!

Universal algebra and category theory:

basic ideas, notions and some results

• Algebras, homomorphisms, equations: basic definitions and results

• Categories; examples and simple categorical definitions

• Limits and colimits

• Functors and natural transformations

• Adjunctions

• Cartesian closed categories

• Monads

• Institutions (abstract model theory, abstract specification theory)

Universal algebra and category theory:

basic ideas, notions and some results

• Algebras, homomorphisms, equations: basic definitions and results

• Categories; examples and simple categorical definitions

• Limits and colimits

• Functors and natural transformations

• Adjunctions

• Cartesian closed categories

• Monads

• Institutions (abstract model theory, abstract specification theory)

BUT: Tell me what you want to learn!

Literature

Plenty of standard textbooks But this will be roughly based on:

• D.T. Sannella, A. Tarlecki.

Foundations of Algebraic Specifications and Formal Program Development. Springer, 2012.

− Chap. 1: Universal algebra

− Chap. 2: Simple equational specifications

− Chap. 3: Category theory

One motivation

Software systems (modules, programs, databases. . . ):

sets of data with operations on them

• Disregarding: code, efficiency, robustness, reliability, . . .

• Focusing on: CORRECTNESS

Universal algebra from rough analogy

module interface ; signature module; algebra

module specification; class of algebras

Category theory

A language to further abstract away from the standard notions of univer- sal algebra, to deal with their numer- ous variants needed in foundations of computer science.

One motivation

Software systems (modules, programs, databases. . . ):

sets of data with operations on them

• Disregarding: code, efficiency, robustness, reliability, . . .

• Focusing on: CORRECTNESS

Universal algebra from rough analogy

module interface ;signature module;algebra

Category theory

A language to further abstract away from the standard notions of univer- sal algebra, to deal with their numer- ous variants needed in foundations of

One motivation

Software systems (modules, programs, databases. . . ):

sets of data with operations on them

• Disregarding: code, efficiency, robustness, reliability, . . .

• Focusing on: CORRECTNESS

Universal algebra from rough analogy

module interface ;signature module;algebra

module specification;class of algebras

Category theory

A language to further abstract away from the standard notions of univer- sal algebra, to deal with their numer- ous variants needed in foundations of computer science.

Signatures

Algebraic signature:

Σ = (S, Ω)

• sort names: S

• operation names, classified by arities and result sorts: Ω = hΩ_w,si_w∈S^∗_,s∈S Alternatively:

Σ = (S, Ω, arity, sort )

with sort names S, operation names Ω, and arity and result sort functions

arity : Ω → S^∗ and sort : Ω → S.

• f : s₁ × . . . × s_n → s stands for s₁, . . . , s_n, s ∈ S and f ∈ Ω_s1...sn,s

• f : s₁ × . . . × s_n → s and f : s⁰₁ × . . . × s⁰_m → s⁰ — overloading allowed

Signatures

Algebraic signature:

Σ = (S, Ω)

• sort names: S

• operation names, classified by arities and result sorts: Ω = hΩ_w,si_w∈S^∗_,s∈S Alternatively:

Σ = (S, Ω, arity, sort )

with sort names S, operation names Ω, and arity and result sort functions

arity : Ω → S^∗ and sort : Ω → S.

• f : s₁ × . . . × s_n → s stands for s₁, . . . , s_n, s ∈ S and f ∈ Ω_s1...sn,s

• f : s₁ × . . . × s_n → s and f : s⁰₁ × . . . × s⁰_m → s⁰ — overloading allowed

Compare the two notions

Signatures

Algebraic signature:

Σ = (S, Ω)

• sort names: S

• operation names, classified by arities and result sorts: Ω = hΩ_w,si_w∈S^∗_,s∈S Alternatively:

Σ = (S, Ω, arity, sort )

with sort names S, operation names Ω, and arity and result sort functions

arity : Ω → S^∗ and sort : Ω → S.

• f : s₁ × . . . × s_n → s stands for s₁, . . . , s_n, s ∈ S and f ∈ Ω_s1...sn,s

• f : s₁ × . . . × s_n → s and f : s⁰₁ × . . . × s⁰_m → s⁰ — overloading allowed

Signatures

Algebraic signature:

Σ = (S, Ω)

• sort names: S

• operation names, classified by arities and result sorts: Ω = hΩ_w,si_w∈S^∗_,s∈S Alternatively:

Σ = (S, Ω, arity, sort )

with sort names S, operation names Ω, and arity and result sort functions

arity : Ω → S^∗ and sort : Ω → S.

• f : s₁ × . . . × s_n → s stands for s₁, . . . , s_n, s ∈ S and f ∈ Ω_s1...sn,s

• f : s₁ × . . . × s_n → s and f : s₁⁰ × . . . × s⁰_m → s⁰ — overloading allowed

Compare the two notions

Signatures

Algebraic signature:

Σ = (S, Ω)

• sort names: S

• operation names, classified by arities and result sorts: Ω = hΩ_w,si_w∈S^∗_,s∈S Alternatively:

Σ = (S, Ω, arity, sort )

with sort names S, operation names Ω, and arity and result sort functions

arity : Ω → S^∗ and sort : Ω → S.

• f : s₁ × . . . × s_n → s stands for s₁, . . . , s_n, s ∈ S and f ∈ Ω_s1...sn,s

• f : s × . . . × s → s and f : s⁰ × . . . × s⁰ → s⁰ — overloading allowed

Fix a signature Σ = (S, Ω) for a while.

Algebras

• Σ-algebra:

A = (|A|, hf_Ai_{f ∈Ω})

• carrier sets: |A| = h|A|_si_s∈S

• operations: f_A: |A|_s1 × . . . × |A|_sn → |A|_s, for f : s₁ × . . . × s_n → s

• the class of all Σ-algebras:

Alg(Σ)

Fix a signature Σ = (S, Ω) for a while.

Algebras

• Σ-algebra:

A = (|A|, hf_Ai_{f ∈Ω})

• carrier sets: |A| = h|A|_si_s∈S

• operations: f_A: |A|_s1 × . . . × |A|_sn → |A|_s, for f : s₁ × . . . × s_n → s

• the class of all Σ-algebras:

Alg(Σ)

Fix a signature Σ = (S, Ω) for a while.

Algebras

• Σ-algebra:

A = (|A|, hf_Ai_{f ∈Ω})

• carrier sets: |A| = h|A|_si_s∈S

• operations: f_A: |A|_s1 × . . . × |A|_sn → |A|_s, for f : s₁ × . . . × s_n → s BTW: constants: f_A: {hi} → |A|_s, i.e. f_A ∈ |A|_s, for f : s

• the class of all Σ-algebras:

Alg(Σ)

Fix a signature Σ = (S, Ω) for a while.

Algebras

• Σ-algebra:

A = (|A|, hf_Ai_{f ∈Ω})

• carrier sets: |A| = h|A|_si_s∈S

• operations: f_A: |A|_s1 × . . . × |A|_sn → |A|_s, for f : s₁ × . . . × s_n → s

• the class of all Σ-algebras:

Alg(Σ)

Can Alg(Σ) be empty? Finite?

Fix a signature Σ = (S, Ω) for a while.

Algebras

• Σ-algebra:

A = (|A|, hf_Ai_{f ∈Ω})

• carrier sets: |A| = h|A|_si_s∈S

• operations: f_A: |A|_s1 × . . . × |A|_sn → |A|_s, for f : s₁ × . . . × s_n → s

• the class of all Σ-algebras:

Alg(Σ)

Can Alg(Σ) be empty? Finite?

Can A ∈ Alg(Σ) have empty carriers?

Fix a signature Σ = (S, Ω) for a while.

Algebras

• Σ-algebra:

A = (|A|, hf_Ai_{f ∈Ω})

• carrier sets: |A| = h|A|_si_s∈S

• operations: f_A: |A|_s1 × . . . × |A|_sn → |A|_s, for f : s₁ × . . . × s_n → s

• the class of all Σ-algebras:

Alg(Σ)

Can Alg(Σ) be empty? Finite?

Intermezzo: many-sorted sets

Given a set (of sort names) S,

S-sorted set X = hX_si_s∈S is a family of sets X_s, s ∈ S. The usual set-theoretic concepts and notations apply component-wise.

For instance, given X = hX_si_s∈S, Y = hY_si_s∈S, Z = hZ_si_s∈S:

• X ∩ Y = hX_s ∩ Y_si_s∈S, X × Y = hX_s × Y_si_s∈S, etc

• X ⊆ Y iff X_s ⊆ Y_s, for s ∈ S

• R ⊆ X × Y means R = hR_s ⊆ X_s × Y_si_s∈S

• f : X → Y means f = hf_s: X_s → Y_si_s∈S

• for f : X → Y , g : Y → Z, f ;g = hf_s;g_s: X_s → Z_si_s∈S : X → Z

BTW: (f ;g)(x) = g(f (x)), where by abuse of notation for x ∈ X_s, f (x) = f_s(x)

Intermezzo: many-sorted sets

Given a set (of sort names) S,

S-sorted set X = hX_si_s∈S is a family of sets X_s, s ∈ S. The usual set-theoretic concepts and notations apply component-wise.

For instance, given X = hX_si_s∈S, Y = hY_si_s∈S, Z = hZ_si_s∈S:

• X ∩ Y = hX_s ∩ Y_si_s∈S, X × Y = hX_s × Y_si_s∈S, etc

• X ⊆ Y iff X_s ⊆ Y_s, for s ∈ S

• R ⊆ X × Y means R = hR_s ⊆ X_s × Y_si_s∈S

• f : X → Y means f = hf_s: X_s → Y_si_s∈S

• for f : X → Y , g : Y → Z, f ;g = hf_s;g_s: X_s → Z_si_s∈S : X → Z

Intermezzo: many-sorted sets

Given a set (of sort names) S,

S-sorted set X = hX_si_s∈S is a family of sets X_s, s ∈ S. The usual set-theoretic concepts and notations apply component-wise.

For instance, given X = hX_si_s∈S, Y = hY_si_s∈S, Z = hZ_si_s∈S:

• X ∩ Y = hX_s ∩ Y_si_s∈S, X × Y = hX_s × Y_si_s∈S, etc

• X ⊆ Y iff X_s ⊆ Y_s, for s ∈ S

• R ⊆ X × Y means R = hR_s ⊆ X_s × Y_si_s∈S

• f : X → Y means f = hf_s: X_s → Y_si_s∈S

• for f : X → Y , g : Y → Z, f ;g = hf_s;g_s: X_s → Z_si_s∈S : X → Z

BTW: (f ;g)(x) = g(f (x)), where by abuse of notation for x ∈ X_s, f (x) = f_s(x)

Intermezzo: many-sorted sets

Given a set (of sort names) S,

S-sorted set X = hX_si_s∈S is a family of sets X_s, s ∈ S. The usual set-theoretic concepts and notations apply component-wise.

For instance, given X = hX_si_s∈S, Y = hY_si_s∈S, Z = hZ_si_s∈S:

• X ∩ Y = hX_s ∩ Y_si_s∈S, X × Y = hX_s × Y_si_s∈S, etc

• X ⊆ Y iff X_s ⊆ Y_s, for s ∈ S

• R ⊆ X × Y means R = hR_s ⊆ X_s × Y_si_s∈S

• f : X → Y means f = hf_s: X_s → Y_si_s∈S

• for f : X → Y , g : Y → Z, f ;g = hf_s;g_s: X_s → Z_si_s∈S : X → Z

Subalgebras

Definition: For A, A_sub ∈ Alg(Σ), A_sub is a Σ-subalgebra of A, written A_sub ⊆ A, if

− |A_sub| ⊆ |A|, and

− for f : s₁ × . . . × s_n → s, and a₁ ∈ |A_sub|_s1, . . . , a_n ∈ |A_sub|_sn,

f_Asub(a₁, . . . , a_n) = f_A(a₁, . . . , a_n)

Subalgebras

• for A ∈ Alg(Σ), a Σ-subalgebra A_sub ⊆ A is given by subset |A_sub| ⊆ |A| closed under the operations:

− for f : s₁ × . . . × s_n → s and a₁ ∈ |A_sub|_s1, . . . , a_n ∈ |A_sub|_sn,

f_A(a₁, . . . , a_n) ∈ |A_sub| .

• for A ∈ Alg(Σ) and X ⊆ |A|, the subalgebra of A genereted by X, hAi_X, is the least subalgebra of A that contains X.

• A ∈ Alg(Σ) is reachable if hAi_∅ coincides with A.

Theorem: For any A ∈ Alg(Σ) and X ⊆ |A|, hAi_X exists.

Subalgebras

• for A ∈ Alg(Σ), a Σ-subalgebra A_sub ⊆ A is given by subset |A_sub| ⊆ |A| closed under the operations.

• for A ∈ Alg(Σ) and X ⊆ |A|, the subalgebra of A genereted by X, hAi_X, is the least subalgebra of A that contains X.

• A ∈ Alg(Σ) is reachable if hAi_∅ coincides with A.

Theorem: For any A ∈ Alg(Σ) and X ⊆ |A|, hAi_X exists.

Subalgebras

• for A ∈ Alg(Σ), a Σ-subalgebra A_sub ⊆ A is given by subset |A_sub| ⊆ |A| closed under the operations.

• for A ∈ Alg(Σ) and X ⊆ |A|, the subalgebra of A genereted by X, hAi_X, is the least subalgebra of A that contains X.

• A ∈ Alg(Σ) is reachable if hAi_∅ coincides with A.

Theorem: For any A ∈ Alg(Σ) and X ⊆ |A|, hAi_X exists.

Subalgebras

• for A ∈ Alg(Σ), a Σ-subalgebra A_sub ⊆ A is given by subset |A_sub| ⊆ |A| closed under the operations.

• for A ∈ Alg(Σ) and X ⊆ |A|, the subalgebra of A genereted by X, hAi_X, is the least subalgebra of A that contains X.

• A ∈ Alg(Σ) is reachable if hAi_∅ coincides with A.

Theorem: For any A ∈ Alg(Σ) and X ⊆ |A|, hAi_X exists.

Proof: Let X₀ = X, and for i ≥ 0,

X_i+1 = X_i ∪ {f_A(x₁, . . . , x_n) | f : s₁ × . . . × s_n → s, x₁ ∈ (X_i)_s1, . . . , x_n ∈ (X_i)_sn}.

Then |hAi_X| = S

i≥0 X_i contains X (clearly) and is closed under the operations.

Moreover, if a subset of |A| contains X and is closed under the operations then it contains each X_i, i ≥ 0, and hence so defined |hAi_X| as well.

Subalgebras

• for A ∈ Alg(Σ), a Σ-subalgebra A_sub ⊆ A is given by subset |A_sub| ⊆ |A| closed under the operations.

• for A ∈ Alg(Σ) and X ⊆ |A|, the subalgebra of A genereted by X, hAi_X, is the least subalgebra of A that contains X.

• A ∈ Alg(Σ) is reachable if hAi_∅ coincides with A.

Theorem: For any A ∈ Alg(Σ) and X ⊆ |A|, hAi_X exists.

Proof: Let X₀ = X, and for i ≥ 0,

X_i+1 = X_i ∪ {f_A(x₁, . . . , x_n) | f : s₁ × . . . × s_n → s, x₁ ∈ (X_i)_s1, . . . , x_n ∈ (X_i)_sn}.

Then |hAi_X| = S

i≥0 X_i contains X (clearly) and is closed under the operations.

Moreover, if a subset of |A| contains X and is closed under the operations then it

Subalgebras

• for A ∈ Alg(Σ), a Σ-subalgebra A_sub ⊆ A is given by subset |A_sub| ⊆ |A| closed under the operations.

• for A ∈ Alg(Σ) and X ⊆ |A|, the subalgebra of A genereted by X, hAi_X, is the least subalgebra of A that contains X.

• A ∈ Alg(Σ) is reachable if hAi_∅ coincides with A.

Theorem: For any A ∈ Alg(Σ) and X ⊆ |A|, hAi_X exists.

Proof:

Lemma: The intersection of any family of subsets of |A| closed under the operations is closed under the operations as well.

Then |hAi_X| = T{|A_sub| | X ⊆ |A_sub|, A_sub ⊆ A} is closed under the operations and contains X. Moreover, it is contained in every subalgebra of A that contains X.

Subalgebras

• for A ∈ Alg(Σ), a Σ-subalgebra A_sub ⊆ A is given by subset |A_sub| ⊆ |A| closed under the operations.

• for A ∈ Alg(Σ) and X ⊆ |A|, the subalgebra of A genereted by X, hAi_X, is the least subalgebra of A that contains X.

• A ∈ Alg(Σ) is reachable if hAi_∅ coincides with A.

Theorem: For any A ∈ Alg(Σ) and X ⊆ |A|, hAi_X exists.

Proof:

Lemma: The intersection of any family of subsets of |A| closed under the operations is closed under the operations as well.

Then |hAi | = T{|A | | X ⊆ |A |, A ⊆ A} is closed under the operations and

Subalgebras

• for A ∈ Alg(Σ), a Σ-subalgebra A_sub ⊆ A is given by subset |A_sub| ⊆ |A| closed under the operations.

• for A ∈ Alg(Σ) and X ⊆ |A|, the subalgebra of A genereted by X, hAi_X, is the least subalgebra of A that contains X.

• A ∈ Alg(Σ) is reachable if hAi_∅ coincides with A.

Theorem: For any A ∈ Alg(Σ) and X ⊆ |A|, hAi_X exists.

Proof (idea):

• generate the generated subalgebra from X by closing it under operations in A; or

• the intersection of any family of subalgebras of A is a subalgebra of A.

Homomorphisms

• for A, B ∈ Alg(Σ), a Σ-homomorphism h : A → B is a function h : |A| → |B|

that preserves the operations:

− for f : s₁ × . . . × s_n → s and a₁ ∈ |A|_s1, . . . , a_n ∈ |A|_sn,

h_s(f_A(a₁, . . . , a_n)) = f_B(h_s1(a₁), . . . , h_sn(a_n))

|A|_s1 × . . . × |A|_sn

|B|_s1 × . . . × |B|_sn

|A|_s

|B|_s -

-

?

?

f_A

f_B

h_s1 × . . . × h_sn h_s

Homomorphisms

• for A, B ∈ Alg(Σ), a Σ-homomorphism h : A → B is a function h : |A| → |B|

that preserves the operations:

− for f : s₁ × . . . × s_n → s and a₁ ∈ |A|_s1, . . . , a_n ∈ |A|_sn,

h_s(f_A(a₁, . . . , a_n)) = f_B(h_s1(a₁), . . . , h_sn(a_n)) Theorem: Given a homomorphism h : A → B and subalgebras A_sub of A and B_sub of B, the image of A_sub under h, h(A_sub), is a subalgebra of B, and the coimage of B_sub under h, h⁻¹(B_sub), is a subalgebra of A.

Homomorphisms

• for A, B ∈ Alg(Σ), a Σ-homomorphism h : A → B is a function h : |A| → |B|

that preserves the operations:

− for f : s₁ × . . . × s_n → s and a₁ ∈ |A|_s1, . . . , a_n ∈ |A|_sn,

h_s(f_A(a₁, . . . , a_n)) = f_B(h_s1(a₁), . . . , h_sn(a_n)) Theorem: Given a homomorphism h : A → B and subalgebras A_sub of A and B_sub of B, the image of A_sub under h, h(A_sub), is a subalgebra of B, and the coimage of B_sub under h, h⁻¹(B_sub), is a subalgebra of A.

Proof: Check that:

− h⁻¹(|B_sub|) is closed under the operations (in A) – easy!

− h(|A_sub|) is closed under the operations (in B) – just a tiny bit more difficult. . .

Homomorphisms

• for A, B ∈ Alg(Σ), a Σ-homomorphism h : A → B is a function h : |A| → |B|

that preserves the operations:

− for f : s₁ × . . . × s_n → s and a₁ ∈ |A|_s1, . . . , a_n ∈ |A|_sn,

h_s(f_A(a₁, . . . , a_n)) = f_B(h_s1(a₁), . . . , h_sn(a_n)) Theorem: Given a homomorphism h : A → B and subalgebras A_sub of A and B_sub of B, the image of A_sub under h, h(A_sub), is a subalgebra of B, and the coimage of B_sub under h, h⁻¹(B_sub), is a subalgebra of A.

Theorem: Given a homomorphism h : A → B and X ⊆ |A|, h(hAi_X) = hBi_h(X).

Homomorphisms

• for A, B ∈ Alg(Σ), a Σ-homomorphism h : A → B is a function h : |A| → |B|

that preserves the operations:

− for f : s₁ × . . . × s_n → s and a₁ ∈ |A|_s1, . . . , a_n ∈ |A|_sn,

h_s(f_A(a₁, . . . , a_n)) = f_B(h_s1(a₁), . . . , h_sn(a_n)) Theorem: Given a homomorphism h : A → B and subalgebras A_sub of A and B_sub of B, the image of A_sub under h, h(A_sub), is a subalgebra of B, and the coimage of B_sub under h, h⁻¹(B_sub), is a subalgebra of A.

Theorem: Given a homomorphism h : A → B and X ⊆ |A|, h(hAi_X) = hBi_h(X). Proof:

− h(hAi_X) ⊇ hBi_h(X), since h(hAi_X) is a subalgebra of B and contains h(X);

− hAi ⊆ h^{−1 −1}

Homomorphisms

• for A, B ∈ Alg(Σ), a Σ-homomorphism h : A → B is a function h : |A| → |B|

that preserves the operations:

− for f : s₁ × . . . × s_n → s and a₁ ∈ |A|_s1, . . . , a_n ∈ |A|_sn,

h_s(f_A(a₁, . . . , a_n)) = f_B(h_s1(a₁), . . . , h_sn(a_n)) Theorem: Given a homomorphism h : A → B and subalgebras A_sub of A and B_sub of B, the image of A_sub under h, h(A_sub), is a subalgebra of B, and the coimage of B_sub under h, h⁻¹(B_sub), is a subalgebra of A.

Theorem: Given a homomorphism h : A → B and X ⊆ |A|, h(hAi_X) = hBi_h(X). Theorem: If two homomorphisms h₁, h₂: A → B coincide on X ⊆ |A|, then they coincide on hAi_X.

Homomorphisms

• for A, B ∈ Alg(Σ), a Σ-homomorphism h : A → B is a function h : |A| → |B|

that preserves the operations:

− for f : s₁ × . . . × s_n → s and a₁ ∈ |A|_s1, . . . , a_n ∈ |A|_sn,

h_s(f_A(a₁, . . . , a_n)) = f_B(h_s1(a₁), . . . , h_sn(a_n)) Theorem: Given a homomorphism h : A → B and subalgebras A_sub of A and B_sub of B, the image of A_sub under h, h(A_sub), is a subalgebra of B, and the coimage of B_sub under h, h⁻¹(B_sub), is a subalgebra of A.

Theorem: Given a homomorphism h : A → B and X ⊆ |A|, h(hAi_X) = hBi_h(X). Theorem: If two homomorphisms h₁, h₂: A → B coincide on X ⊆ |A|, then they coincide on hAi_X.

Homomorphisms

• for A, B ∈ Alg(Σ), a Σ-homomorphism h : A → B is a function h : |A| → |B|

that preserves the operations:

− for f : s₁ × . . . × s_n → s and a₁ ∈ |A|_s1, . . . , a_n ∈ |A|_sn,

h_s(f_A(a₁, . . . , a_n)) = f_B(h_s1(a₁), . . . , h_sn(a_n)) Theorem: Given a homomorphism h : A → B and subalgebras A_sub of A and B_sub of B, the image of A_sub under h, h(A_sub), is a subalgebra of B, and the coimage of B_sub under h, h⁻¹(B_sub), is a subalgebra of A.

Theorem: Given a homomorphism h : A → B and X ⊆ |A|, h(hAi_X) = hBi_h(X). Theorem: If two homomorphisms h₁, h₂: A → B coincide on X ⊆ |A|, then they coincide on hAi_X.

Theorem: Identity function on the carrier of A ∈ Alg(Σ) is a homomorphism id_A: A → A. Composition of homomorphisms h : A → B and g : B → C is a homomorphism h;g : A → C.

Isomorphisms

• for A, B ∈ Alg(Σ), a Σ-isomorphism is any Σ-homomorphism i : A → B that has an inverse, i.e., a Σ-homomorphism i⁻¹: B → A such that i;i⁻¹ = id_A and i⁻¹;i = id_B.

A -B

6 

i

i⁻¹





^





id_A  id_B

• Σ-algebras are isomorphic if there exists an isomorphism between them.

Theorem: A Σ-homomorphism is a Σ-isomorphism iff it is bijective (“1-1” and

“onto”).

Isomorphisms

• for A, B ∈ Alg(Σ), a Σ-isomorphism is any Σ-homomorphism i : A → B that has an inverse, i.e., a Σ-homomorphism i⁻¹: B → A such that i;i⁻¹ = id_A and i⁻¹;i = id_B.

A -B

6 

i

i⁻¹





^





id_A  id_B

• Σ-algebras are isomorphic if there exists an isomorphism between them.

Theorem: A Σ-homomorphism is a Σ-isomorphism iff it is bijective (“1-1” and

“onto”).

Isomorphisms

• for A, B ∈ Alg(Σ), a Σ-isomorphism is any Σ-homomorphism i : A → B that has an inverse, i.e., a Σ-homomorphism i⁻¹: B → A such that i;i⁻¹ = id_A and i⁻¹;i = id_B.

A -B

6 

i

i⁻¹





^





id_A  id_B

• Σ-algebras are isomorphic if there exists an isomorphism between them.

Theorem: A Σ-homomorphism is a Σ-isomorphism iff it is bijective (“1-1” and

“onto”).

Isomorphisms

• for A, B ∈ Alg(Σ), a Σ-isomorphism is any Σ-homomorphism i : A → B that has an inverse, i.e., a Σ-homomorphism i⁻¹: B → A such that i;i⁻¹ = id_A and i⁻¹;i = id_B.

A -B

6 

i

i⁻¹





^





id_A  id_B

• Σ-algebras are isomorphic if there exists an isomorphism between them.

Theorem: A Σ-homomorphism is a Σ-isomorphism iff it is bijective (“1-1” and

“onto”).

Isomorphisms

• for A, B ∈ Alg(Σ), a Σ-isomorphism is any Σ-homomorphism i : A → B that has an inverse, i.e., a Σ-homomorphism i⁻¹: B → A such that i;i⁻¹ = id_A and i⁻¹;i = id_B.

A -B

6 

i

i⁻¹





^





id_A  id_B

• Σ-algebras are isomorphic if there exists an isomorphism between them.

Theorem: A Σ-homomorphism is a Σ-isomorphism iff it is bijective (“1-1” and

“onto”).

Isomorphisms

• for A, B ∈ Alg(Σ), a Σ-isomorphism is any Σ-homomorphism i : A → B that has an inverse, i.e., a Σ-homomorphism i⁻¹: B → A such that i;i⁻¹ = id_A and i⁻¹;i = id_B.

A -B

6 

i

i⁻¹





^





id_A  id_B

• Σ-algebras are isomorphic if there exists an isomorphism between them.

Theorem: A Σ-homomorphism is a Σ-isomorphism iff it is bijective (“1-1” and

“onto”).

Proof (“⇐=”): For f : s₁ × . . . × s_n → s and b₁ ∈ |B|_s1, . . . , b_n ∈ |B|_sn, i⁻¹_s (f_B(b₁, . . . , b_n)) = i_s⁻¹(f_B(i(i⁻¹(b₁)), . . . , i(i⁻¹(b_n)))) =

i⁻¹_s (i(f_A(i⁻¹(b₁), . . . , i⁻¹(b_n)))) = f_A(i⁻¹(b₁), . . . , i⁻¹(b_n))

Isomorphisms

• for A, B ∈ Alg(Σ), a Σ-isomorphism is any Σ-homomorphism i : A → B that has an inverse, i.e., a Σ-homomorphism i⁻¹: B → A such that i;i⁻¹ = id_A and i⁻¹;i = id_B.

A -B

6 

i

i⁻¹





^





id_A  id_B

• Σ-algebras are isomorphic if there exists an isomorphism between them.

Theorem: A Σ-homomorphism is a Σ-isomorphism iff it is bijective (“1-1” and

“onto”).

Theorem: Identities are isomorphisms, and any composition of isomorphisms is an isomorphism.

Congruences

• for A ∈ Alg(Σ), a Σ-congruence on A is an equivalence ≡ ⊆ |A| × |A| that is closed under the operations:

− for f : s₁ × . . . × s_n → s and a₁, a₁⁰ ∈ |A|_s1, . . . , a_n, a⁰_n ∈ |A|_sn,

if a₁ ≡_s1 a₁⁰ , . . . , a_n ≡_sn a⁰_n then f_A(a₁, . . . , a_n) ≡_s f_A(a⁰₁, . . . , a⁰_n).

Congruences

• for A ∈ Alg(Σ), a Σ-congruence on A is an equivalence ≡ ⊆ |A| × |A| that is closed under the operations:

− for f : s₁ × . . . × s_n → s and a₁, a₁⁰ ∈ |A|_s1, . . . , a_n, a⁰_n ∈ |A|_sn,

if a₁ ≡_s1 a₁⁰ , . . . , a_n ≡_sn a⁰_n then f_A(a₁, . . . , a_n) ≡_s f_A(a⁰₁, . . . , a⁰_n).

BTW:

equivalence

Congruences

• for A ∈ Alg(Σ), a Σ-congruence on A is an equivalence ≡ ⊆ |A| × |A| that is closed under the operations:

− for f : s₁ × . . . × s_n → s and a₁, a₁⁰ ∈ |A|_s1, . . . , a_n, a⁰_n ∈ |A|_sn,

if a₁ ≡_s1 a₁⁰ , . . . , a_n ≡_sn a⁰_n then f_A(a₁, . . . , a_n) ≡_s f_A(a⁰₁, . . . , a⁰_n).

BTW:

equivalence

≈ ⊆ X × X

− reflexivity: x ≈ x

− symmetry: if x ≈ y then y ≈ x

− transitivity: if x ≈ y and y ≈ z then x ≈ z Then:

− equivalence class: [x]_≈ = {y ∈ X | y ≈ x}

− quotient set: X/≈ = {[x]_≈ | x ∈ X}

Congruences

• for A ∈ Alg(Σ), a Σ-congruence on A is an equivalence ≡ ⊆ |A| × |A| that is closed under the operations:

− for f : s₁ × . . . × s_n → s and a₁, a₁⁰ ∈ |A|_s1, . . . , a_n, a⁰_n ∈ |A|_sn,

if a₁ ≡_s1 a₁⁰ , . . . , a_n ≡_sn a⁰_n then f_A(a₁, . . . , a_n) ≡_s f_A(a⁰₁, . . . , a⁰_n).

Congruences

• for A ∈ Alg(Σ), a Σ-congruence on A is an equivalence ≡ ⊆ |A| × |A| that is closed under the operations:

− for f : s₁ × . . . × s_n → s and a₁, a₁⁰ ∈ |A|_s1, . . . , a_n, a⁰_n ∈ |A|_sn,

if a₁ ≡_s1 a₁⁰ , . . . , a_n ≡_sn a⁰_n then f_A(a₁, . . . , a_n) ≡_s f_A(a⁰₁, . . . , a⁰_n).

(a₁, . . . , a_n)

(a⁰₁, . . . , a⁰_n)

f_A(a₁, . . . , a_n)

f_A(a⁰₁, . . . , a⁰_n)

≡6_s1 · · · ≡_sn

?

6

?

-

- f_A

f_A

≡_s 6

?

Congruences

• for A ∈ Alg(Σ), a Σ-congruence on A is an equivalence ≡ ⊆ |A| × |A| that is closed under the operations:

− for f : s₁ × . . . × s_n → s and a₁, a₁⁰ ∈ |A|_s1, . . . , a_n, a⁰_n ∈ |A|_sn,

if a₁ ≡_s1 a₁⁰ , . . . , a_n ≡_sn a⁰_n then f_A(a₁, . . . , a_n) ≡_s f_A(a⁰₁, . . . , a⁰_n).

(a₁, . . . , a_n)

(a⁰₁, . . . , a⁰_n)

f_A(a₁, . . . , a_n)

f_A(a⁰₁, . . . , a⁰_n)

≡6_s1 · · · ≡_sn

?

6

?

-

- f_A

f_A

≡_s 6

?

Congruences

• for A ∈ Alg(Σ), a Σ-congruence on A is an equivalence ≡ ⊆ |A| × |A| that is closed under the operations:

− for f : s₁ × . . . × s_n → s and a₁, a₁⁰ ∈ |A|_s1, . . . , a_n, a⁰_n ∈ |A|_sn,

if a₁ ≡_s1 a₁⁰ , . . . , a_n ≡_sn a⁰_n then f_A(a₁, . . . , a_n) ≡_s f_A(a⁰₁, . . . , a⁰_n).

(a₁, . . . , a_n)

(a⁰₁, . . . , a⁰_n)

f_A(a₁, . . . , a_n)

f_A(a⁰₁, . . . , a⁰_n)

≡6_s1 · · · ≡_sn

?

6

?

-

- f_A

f_A

≡_s 6

?

Congruences

• for A ∈ Alg(Σ), a Σ-congruence on A is an equivalence ≡ ⊆ |A| × |A| that is closed under the operations:

− for f : s₁ × . . . × s_n → s and a₁, a₁⁰ ∈ |A|_s1, . . . , a_n, a⁰_n ∈ |A|_sn,

if a₁ ≡_s1 a₁⁰ , . . . , a_n ≡_sn a⁰_n then f_A(a₁, . . . , a_n) ≡_s f_A(a⁰₁, . . . , a⁰_n).

Theorem: For any relation R ⊆ |A| × |A| on the carrier of a Σ-algebra A, there exists the least congruence on A that conatins R.

Congruences

• for A ∈ Alg(Σ), a Σ-congruence on A is an equivalence ≡ ⊆ |A| × |A| that is closed under the operations:

− for f : s₁ × . . . × s_n → s and a₁, a₁⁰ ∈ |A|_s1, . . . , a_n, a⁰_n ∈ |A|_sn,

if a₁ ≡_s1 a₁⁰ , . . . , a_n ≡_sn a⁰_n then f_A(a₁, . . . , a_n) ≡_s f_A(a⁰₁, . . . , a⁰_n).

Theorem: For any relation R ⊆ |A| × |A| on the carrier of a Σ-algebra A, there exists the least congruence on A that conatins R.

Proof (idea):

• generate the least congruence from R by closing it under reflexivity, symmetry, transitivity and the operations in A; or

• the intersection of any family of congruences on A is a congruence on A.

Congruences

• for A ∈ Alg(Σ), a Σ-congruence on A is an equivalence ≡ ⊆ |A| × |A| that is closed under the operations:

− for f : s₁ × . . . × s_n → s and a₁, a₁⁰ ∈ |A|_s1, . . . , a_n, a⁰_n ∈ |A|_sn,

if a₁ ≡_s1 a₁⁰ , . . . , a_n ≡_sn a⁰_n then f_A(a₁, . . . , a_n) ≡_s f_A(a⁰₁, . . . , a⁰_n).

Theorem: For any relation R ⊆ |A| × |A| on the carrier of a Σ-algebra A, there exists the least congruence on A that conatins R.

Theorem: For any Σ-homomorphism h : A → B, the kernel of h, K(h) ⊆ |A| × |A|, where a K(h) a⁰ iff h(a) = h(a⁰), is a Σ-congruence on A.

Proof: For f : s₁ × . . . × s_n → s and a₁, a⁰₁ ∈ |A|_s1, . . . , a_n, a⁰_n ∈ |A|_sn, if a₁ K(h)_s

1 a⁰₁, . . . , a_n K(h)_s

n a⁰_n then f_A(a₁, . . . , a_n) K(h)_s f_A(a⁰₁, . . . , a⁰_n), since h (f (a , . . . , a )) = f (h (a ), . . . , h (a )) = f (h (a⁰ ), . . . , h (a⁰ )) =

Congruences

• for A ∈ Alg(Σ), a Σ-congruence on A is an equivalence ≡ ⊆ |A| × |A| that is closed under the operations:

− for f : s₁ × . . . × s_n → s and a₁, a₁⁰ ∈ |A|_s1, . . . , a_n, a⁰_n ∈ |A|_sn,

if a₁ ≡_s1 a₁⁰ , . . . , a_n ≡_sn a⁰_n then f_A(a₁, . . . , a_n) ≡_s f_A(a⁰₁, . . . , a⁰_n).

Theorem: For any relation R ⊆ |A| × |A| on the carrier of a Σ-algebra A, there exists the least congruence on A that conatins R.

Theorem: For any Σ-homomorphism h : A → B, the kernel of h, K(h) ⊆ |A| × |A|, where a K(h) a⁰ iff h(a) = h(a⁰), is a Σ-congruence on A.

Proof: For f : s₁ × . . . × s_n → s and a₁, a₁⁰ ∈ |A|_s1, . . . , a_n, a⁰_n ∈ |A|_sn, if a₁ K(h)_s

1 a⁰₁, . . . , a_n K(h)_s

n a⁰_n then f_A(a₁, . . . , a_n) K(h)_s f_A(a⁰₁, . . . , a⁰_n), since h_s(f_A(a₁, . . . , a_n)) = f_B(h_s1(a₁), . . . , h_sn(a_n)) = f_B(h_s1(a⁰₁), . . . , h_sn(a⁰_n)) =

h_s(f_A(a⁰₁, . . . , a⁰_n)).

Congruences

• for A ∈ Alg(Σ), a Σ-congruence on A is an equivalence ≡ ⊆ |A| × |A| that is closed under the operations:

− for f : s₁ × . . . × s_n → s and a₁, a₁⁰ ∈ |A|_s1, . . . , a_n, a⁰_n ∈ |A|_sn,

if a₁ ≡_s1 a₁⁰ , . . . , a_n ≡_sn a⁰_n then f_A(a₁, . . . , a_n) ≡_s f_A(a⁰₁, . . . , a⁰_n).

Theorem: For any relation R ⊆ |A| × |A| on the carrier of a Σ-algebra A, there exists the least congruence on A that conatins R.

Theorem: For any Σ-homomorphism h : A → B, the kernel of h, K(h) ⊆ |A| × |A|, where a K(h) a⁰ iff h(a) = h(a⁰), is a Σ-congruence on A.

Proof: For f : s₁ × . . . × s_n → s and a₁, a⁰₁ ∈ |A|_s1, . . . , a_n, a⁰_n ∈ |A|_sn, if a₁ K(h)_s

1 a⁰₁, . . . , a_n K(h)_s

n a⁰_n then f_A(a₁, . . . , a_n) K(h)_s f_A(a⁰₁, . . . , a⁰_n), since h (f (a , . . . , a )) = f (h (a ), . . . , h (a )) = f (h (a⁰ ), . . . , h (a⁰ )) =

Quotients

• for A ∈ Alg(Σ) and Σ-congruence ≡ ⊆ |A| × |A| on A, the quotient algebra A/≡ is built in the natural way on the equivalence classes of ≡:

− for s ∈ S, |A/≡|_s = {[a]_≡ | a ∈ |A|_s}, with [a]_≡ = {a⁰ ∈ |A|_s | a ≡_s a⁰}

− for f : s₁ × . . . × s_n → s and a₁ ∈ |A|_s1, . . . , a_n ∈ |A|_sn,

f_A/≡([a₁]_≡, . . . , [a_n]_≡) = [f_A(a₁, . . . , a_n)]_≡ Theorem: The above is well-defined.

Quotients

• for A ∈ Alg(Σ) and Σ-congruence ≡ ⊆ |A| × |A| on A, the quotient algebra A/≡ is built in the natural way on the equivalence classes of ≡:

− for s ∈ S, |A/≡|_s = {[a]_≡ | a ∈ |A|_s}, with [a]_≡ = {a⁰ ∈ |A|_s | a ≡_s a⁰}

− for f : s₁ × . . . × s_n → s and a₁ ∈ |A|_s1, . . . , a_n ∈ |A|_sn,

f_A/≡([a₁]_≡, . . . , [a_n]_≡) = [f_A(a₁, . . . , a_n)]_≡ Theorem: The above is well-defined.