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 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 sL. For any set E, let

LE = ∐sL Ens

Then ∀AE, ∀(s,x)∈LE, (s,x) ∈ LA ⇔ Im xA.

A relational language is a language L of relation symbols, where each sL 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

sL ℘(Ens) ⥬ ℘(LE).

For any function f : EF, let Lf : LELF defined by (s,x) ↦ (s,fx). Then

LIdE = IdLE
fncf,g, Im f ⊂ Dom gL(gf) = LgLf
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,

AE, Lf[LA] = L(f[A])
BF, 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 ELE.

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 sL is interpreted in each system E as the ns-ary relation sE somehow independent of E,

sE = {xEns | s(x)} = E(s)
E = {(s,x)∈LE | s(x)} = ∐sL sE.

Morphisms

Between any L-systems E,F, we define the set MorL(E,F) ⊂ FE of L-morphisms from E to F by ∀fFE,

f ∈ MorL(E,F) ⇔ ∀(s,x)∈E, (s,fx)∈F
⇔ (∀sL,∀xEns, s(x) ⇒ s(fx))
Lf[E] ⊂ FE ⊂ (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)
satisfying the following axioms:
The last condition is easily verified for L-morphisms : ∀(s,x)∈E, (s,fx)∈F ∴ (s,gfx)∈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 sEEns 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), ∀xsE, fxsF. 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), In particular: 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:

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. Between systems E,F with a common list τ of types (and interpretations of a common list of structure symbols), morphisms can equivalently be conceived in the following 2 ways, apart from having to preserve all structures:

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