3.2. Relational systems and concrete categories
Let us formalize the concept of system, focusing for simplicity on those
with only one type. For any number n∈ℕ and any set E, let us denote
- En = E×...×E = EVn,
set of all n-tuples of
elements of E (n-ary product
or exponentiation).
- RelE(n) = ℘(En),
set of all n-ary relations in E
- OpE(n)
= EEn, set of all n-ary operations in E.
We then denote the set of all operations OpE = ∐n∈ℕ
OpE(n),
and that of all relations RelE = ∐n∈ℕ ℘(En).
Or, we could write OpE with ⋃n∈ℕ since the
OpE(n) are pairwise disjoint when E≠∅.
Languages
A language L is a set of symbols, with the data of the intended arity
ns∈ℕ of each s∈L. For any set E, let
LE = ∐s∈L
Ens
Then ∀A⊂E, ∀(s,x)∈LE,
(s,x) ∈ LA ⇔ Im x ⊂ A.
A relational language is a language L of relation symbols,
where each s∈L aims to be interpreted in any L-system E as
an ns-ary relation. These form a family called an L-structure
on E, element of
∏s∈L ℘(Ens)
⥬ ℘(LE).
For any function f : E → F, let Lf :
LE → LF defined by
(s,x) ↦ (s,f⚬x). Then
LIdE = IdLE
∀fncf,g, Im f
⊂ Dom g ⇒ L(g⚬f) =
Lg ⚬ Lf
Inj f ⇒ Inj Lf
Im Lf = LIm f
The latter comes by
finite choice applied to (AC1)⇒(AC7),
as arities of symbols are finite (otherwise it still goes for injective f,
or using AC).
We shall omit parenthesis in notations of direct and inverse images
in the way Lf⋆ = (Lf)⋆.
Then,∀A⊂E, Lf[LA]
= L(f[A])
∀B⊂F, Lf⋆(LB) =
L(f⋆(B))
Relational systems
A relational system with language L, or L-system, is the
data (E,E) of a set E with an L-structure E ⊂
LE.
The case of an algebraic language, whose symbols aim to represent operations,
will be studied in 3.3.
Most often, we shall only use one L-structure on each set, so that E
can be treated as implicit, determined by E. Precisely, let us imagine given a class of
L-systems where each E is the intersection of LE
with a fixed class of (s,x), denoted as a predicate s(x) for how it is
naturally curried: each symbol s∈L is interpreted in each system E as the
ns-ary relation sE somehow independent of E,
sE = {x∈Ens
| s(x)} = E⃗(s)
E = {(s,x)∈LE | s(x)} =
∐s∈L sE.
Morphisms
Between any L-systems E,F,
we define the set MorL(E,F) ⊂ FE
of L-morphisms from E to F
by ∀f∈FE,
f ∈ MorL(E,F) ⇔
∀(s,x)∈E, (s,f⚬x)∈F
⇔ (∀s∈L,∀x∈Ens,
s(x) ⇒ s(f⚬x))
⇔
Lf[E] ⊂ F ⇔ E ⊂
(Lf)⋆F.
Concrete categories
The concept of concrete category is what remains of a class of systems with their
morphisms, when we forget which are the structures that the morphisms are preserving
(as we will see this list of structures can be extended without affecting the sets of morphisms).
Let us formalize concrete categories as made of the following data (making this
slightly "more concrete" than the official concept of concrete category from other authors)
- a class of sets called objects ;
- a class of functions called morphisms; then for any objects
E,F, we define
Mor(E,F) = {f∈FE | f is a morphism}
satisfying the following axioms:
- Every morphism belongs to some Mor(E,F), i.e.
its domain is an object and its image is included in an object
(in practice, images of morphisms will be objects too);
- For any object E, IdE ∈ Mor(E,E)
;
- Any composite of morphisms is a morphism: for any 3 objects E,F,G
, ∀f ∈ Mor(E,F), ∀g∈Mor(F,G),
g⚬f ∈ Mor(E,G).
The last condition is easily verified for L-morphisms : ∀(s,x)∈E,
(s,f⚬x)∈F ∴ (s,g⚬f⚬x)∈G.
The simplest example is the category of sets where all sets are objects, and
Mor(E,F) = FE.
A category is small if its class of objects is a set.
The official concept of concrete category mainly differs from this by allowing different objects to
have the same base set : in the case of relational systems, such objects are systems consisting
of different choices of structures on the same set. The above version of the concept may
simulate this by taking disjoint copies of a given set for all structures we consider to use on it ;
but this construction does not match the use of subsets as objects in their own right.
We do not need to specify a fixed consistent formalization as long as we shall not play on
the ambiguity in any way which might lead to wrong conclusions. Generally speaking,
when we define a system and declare it an object of a category, we only need that some
copy of this system is an object.
For example, we shall speak of the category of all L-systems, which gives back
the category of sets when L is empty.
Preservation of some defined structures
A relational symbol s with the data of an interpretation sE ⊂
Ens in every object E of a given concrete
category, is said to be preserved if all morphisms of the category are also morphisms
for this symbol, i.e. ∀f∈Mor(E,F), ∀x∈sE,
f⚬x∈sF. From definitions, each symbol in a language
L is preserved in any category of L-systems.
In any given category of L-systems, or any concrete category with a given list L
of preserved interpreted symbols, any further invariant structure
whose defining formula only uses symbols in L and logical symbols
∧,∨,0,1,=,∃, is preserved.
Proof. For any L-morphism
f∈MorL(E,F),
- Substituting arguments of a s∈L by a map σ to n' other variables
(∀E,∀x∈En', s'(x) ⇔ s(x⚬σ)),
works :
s'(x) ⇒ s(x⚬σ) ⇒
s(f⚬x⚬σ) ⇒ s'(f⚬x).
- ∀s,s'∈L, ns = ns' ⇒
∀x∈Ens, (s(x) ∧ s'(x))
⇒ (s(f⚬x) ∧ s'(f⚬x))
- ∀s,s'∈L, ns = ns' ⇒
∀x∈Ens, (s(x) ∨ s'(x))
⇒ (s(f⚬x) ∨ s'(f⚬x))
- For 0 and 1 it is trivial
- ∀x,y∈E, x = y ⇒ f(x) = f(y)
- ∀x∈Ens,(∃y∈E,
s(x,y)) ⇒ (∃z=f(y)∈F,
s(f⚬x, z)) ∎
In particular:
- In the nullary case: for any f ∈ MorL(E,F),
if a ground formula with language L using only these logical symbols is true in
E, then it is also true in F.
- The graph of any operation defined by a term is expressible in this way,
and thus also preserved. But the proofs given by the above means are only a
schema of one proof for each "small" (concretely written) term. A single proof for the full
range of all terms will be given in 4.1.
However, morphisms may no more preserve structures defined with other
symbols (¬,⇒,∀).
The above cases of 0, 1, ∨ and ∧ are mere particular cases (the nullary and binary cases)
of the following:
- Any union of a family of preserved structures in a concrete category is a preserved structure.
- Any intersection of a family of preserved structures is also a preserved structure.
Categories of typed systems
While we introduced the notion of morphism in the case of systems
with a single type, it may be extended to systems with several types as
well. The domain (range of objects)
of a typed system may be formalized in set theory, either as a family of sets
E = (Ei)i∈τ, or as a set E
with a function tE : E → τ giving the type of each element.
The translation between both formalizations is obtained one way taking the sum, and in
the other way taking the fibers of tE (what we called an indexed partition
but allowing empty components).
Then the concept of morphism between systems E,F
with a common list τ of types (and interpreting the same language),
is respectively and equivalently formalized as follows (aside the condition of having to
preserve all structures):
- As a tuple or family of functions (fi)i∈τ,
where ∀i∈τ, fi : Ei → Fi
;
- As a τ-morphism f : E → F seeing τ as a list of unary relation
symbols (like for the use of classes
as notions in set theory), i.e. a function such
that tF ⚬ f = tE.
Set theory and foundations
of mathematics
1. First foundations of
mathematics
2. Set theory
3. Algebra 1
3.1. Galois
connections
3.2. Relational systems and concrete categories
3.3. Algebras
3.4. Special morphisms
3.5. Monoids and categories
3.6. Actions of monoids and categories
3.7. Invertibility and groups
3.8. Properties in categories
3.9. Initial and final objects
3.10. Products of systems
3.11. Basis
3.12. The category of relations
4. Arithmetic and first-order foundations
5. Second-order foundations
6. Foundations of Geometry
Other languages:
FR :
Systèmes
relationnels et catégories concrètes