Systèmes relationnels et categories concrètes

3.2. Systèmes relationnels et catégories concrètes

Formalisons le concept de système, précisément ceux à un seul type par mesure de simplicité. Pour tout entier naturel n∈ℕ et tout ensemble E, notons

Eⁿ = E×...×E = E^V_n, ensemble de tous les n-uplets d'éléments de E (produit n-aire ou exponentiation).
Rel_E⁽ⁿ⁾ = ℘(Eⁿ), ensemble de toutes les relations n-aires dans E
Op_E⁽ⁿ⁾ = E^Eⁿ, ensemble de toutes les opérations n-aires dans E.

On note alors l'ensemble de toutes les operations Op_E = ∐_n∈ℕ Op_E⁽ⁿ⁾, et celui de toutes les relations Rel_E = ∐_n∈ℕ ℘(Eⁿ). Ou, on pourrait écrire Op_E avec ⋃_n∈ℕ puisque les Op_E⁽ⁿ⁾ sont deux à deux disjoints lorsque E≠∅.

Langages

Un langage L est un ensemble de symboles, avec la donnée de l'arité voulue n_s∈ℕ pour chaque s∈L. Pour tout ensemble E, soit

^LE = ∐_s∈L E^n_s

Alors ∀A⊂E, ∀(s,x)∈^LE, (s,x) ∈ ^LA ⇔ Im x ⊂ A.

Un langage relationnel est un langage L de symboles de relation, où chaque s∈L vise à être interprété dans tout L-système E comme une relation n_s-aire. Ils forment une famille appelée une L-structure sur E, élément de

∏_s∈L ℘(E^n_s) ⥬ ℘(^LE).

Pour toute fonction f : E → F, soit ^Lf : ^LE → ^LF défini par (s,x) ↦ (s,f⚬x). Alors

^LId_E = Id_^LE
∀_fncf,g, Im f ⊂ Dom g ⇒ ^L(g⚬f) = ^Lg ⚬ ^Lf
Inj f ⇒ Inj ^Lf
Im ^Lf = ^LIm f

La dernière formule vient par choix fini appliqué à (AC1)⇒(AC7), les arités des symboles étant finies (sinon cela vaut encore pour les f injectives, ou avec AC).
On omettra les parenthèses dans les notations des images directes et inverses suivant ^Lf_⋆ = (^Lf)_⋆. Ainsi,

∀A⊂E, ^Lf[^LA] = ^L(f[A])
∀B⊂F, ^Lf_⋆(^LB) = ^L(f_⋆(B))

Systèmes relationnels

Un système relationnel de langage L, ou L-système, est la donnée (E,E) d'un ensemble E et d'une L-structure E⊂L⋆E.

Le cas d'un langage algébrique, dont les symboles visent à représenter des opérations, sera étudié en 3.3.

Le plus souvent, on n'utilisera qu'une L-structure sur chaque ensemble, de sorte que E peut être vu comme implicite, déterminé par E. Précisément, imaginons donnée une classe de L-systèmes où chaque E est l'intersection de ^LE avec une classe fixe de (s,x), notée comme prédicat s(x) pour sa currification naturelle: chaque symbole s∈L s'interprète dans chaque système E comme la relation n_s-aire s_E en quelque sorte indépendante de E,

s_E = {x∈E^n_s | s(x)} = E⃗(s)
E = {(s,x)∈^LE | s(x)} = ∐_s∈L s_E.

Morphismes

Entre deux L-systèmes E,F, on définit l'ensemble Mor_L(E,F) ⊂ F^E des L-morphismes de E vers F par ∀f∈F^E,

f ∈ Mor_L(E,F) ⇔ ∀(s,x)∈E, (s,f⚬x)∈F
⇔ (∀s∈L,∀x∈E^n_s, s(x) ⇒ s(f⚬x))
⇔ ^Lf[E] ⊂ F ⇔ E ⊂ (^Lf)_⋆F.

Catégories concrètes

Le concept de catégorie concrète est ce qui reste d'une classe de systèmes et leurs morphismes, oubliant quelles sont les structures que les morphismes préservent (cette liste de structures pouvant s'étendre sans affecter les ensembles de morphismes). Formalisons les catégories concrètes comme constituées des données suivantes (les rendant légèrement "plus concrètes" que le concept officiel de catégorie concrète d'autres auteurs)

une classe d'ensembles appelés objets ;
une classe de fonctions appelées morphismes; puis pour tous objets E,F, on définit
Mor(E,F) = {f∈F^E | f est un morphisme}

satisfaisant les axiomes suivants:

Tout morphisme appartient à un certain Mor(E,F) : son domaine est un objet et son image est incluse dans un objet (en pratique, les images des morphismes sont aussi des objets);
Pour tout objet E, Id_E ∈ Mor(E,E) ;
Tout composé de morphismes est un morphisme: pour 3 objets E,F,G , ∀f ∈ Mor(E,F), ∀g∈Mor(F,G), g⚬f ∈ Mor(E,G).

La dernière condition se vérifie facilement pour les L-morphismes : ∀(s,x)∈E, (s,f⚬x)∈F ∴ (s,g⚬f⚬x)∈G.
L'exemple le plus simple est la catégorie des ensembles, où tous les ensembles sont des objets, et Mor(E,F) = F^E.

Une catégorie est petite si sa classe d'objets est un ensemble.

Le concept officiel de catégorie concrète diffère principalement de cela en permettant à différents objets d'avoir le même ensemble de base: dans le cas des systèmes relationnels, ces objets sont des systèmes constitués de différents choix de structures sur le même ensemble. La version ci-dessus du concept peut simuler cela en prenant des copies disjointes d'un ensemble donné pour toutes les structures utilisées dessus; mais cette construction ne correspond pas à l'utilisation de sous-ensembles comme objets à part entière. Il reste inutile spécifier une formalisation cohérente fixe tant qu'on jouera pas sur l'ambiguïté qui pourrait conduire à de fausses conclusions. Généralement, lorsqu'un système est défini et déclaré objet d'une catégorie, on a seulement besoin qu'une copie de ce système soit un objet.
Par exemple, on parlera de la catégorie de tous les L-systèmes, qui restitue la catégorie des ensembles lorsque L est vide.

Préservation de structures définissables

Un symbole relationnel s avec la donnée d'une interprétation s_E⊂E^n_s dans chaque objet E d'une catégorie concrète donnée, est dit préservé si tous les morphismes de la catégorie sont aussi des morphismes pour ce symbole : ∀f∈Mor(E,F), ∀x∈s_E, f⚬x∈s_F. Par définition, chaque symbole d'un langage L est préservé dans toute catégorie de L-systèmes.
Dans toute catégorie de L-systèmes, ou toute catégorie concrète avec une liste L de symboles interprétés préservés, toute autre structure invariante définie par une formule n'utilise que les symboles de L et les symboles logiques ∧,∨,0,1,=,∃ est préservée.
En effet, pour tout L-morphisme f ∈ Mor_L(E,F),

Substituer les arguments d'un s∈L par une fonction σ vers n' autres variables (∀E,∀x∈E^n', s'(x)⇔s(x⚬σ)), fonctionne :
s'(x) ⇒ s(x⚬σ) ⇒ s(f⚬x⚬σ) ⇒ s'(f⚬x).
∀s,s'∈L, n_s = n_s' ⇒ ∀x∈E^n_s, (s(x) ∧ s'(x)) ⇒ (s(f⚬x) ∧ s'(f⚬x))
∀s,s'∈L, n_s = n_s' ⇒ ∀x∈E^n_s, (s(x) ∨ s'(x)) ⇒ (s(f⚬x)∨s'(f⚬x))
Pour 0 et 1 c'est trivial
∀x,y∈E, x = y ⇒ f(x) = f(y)
∀x∈E^n_s,(∃y∈E, s(x,y)) ⇒ (∃z=f(y)∈F, s(f⚬x, z)) ∎

En particulier:

Dans le cas nullaire: pour tout f ∈ Mor_L(E,F), si une formule close de langage L n'utilisant que ces symboles logiques est vraie dans E, elle est alors vraie dans F.
Le graphe de toute opération définie par un terme est exprimable ainsi, et donc également préservé. Mais les preuves données par les moyens ci-dessus ne sont qu'un schéma d'une preuve pour chaque «petit» terme (écrit concrètement). Une preuve unique pour l'ensemble de tous les termes sera donnée en 4.1.

Cependant les morphismes peuvent ne plus préserver les structures définies à l'aide d'autres symboles (¬,⇒,∀).

Les cas de 0, 1, ∨ et ∧ ne sont que des cas particuliers (nullaires et binaires) de ceci:

Toute union d'une famille de structures préservées dans une catégorie concrète est une structure préservée.
Toute intersection d'une famille de structures préservées est aussi une structure préservée.

Catégories de systèmes typés

La notion de morphisme a été introduite pour des systèmes avec un seul type, mais peut s'étendre à des systèmes à plusieurs types. Le domaine (celui des objets) d'un système typé peut se formaliser en théorie des ensembles, soit comme une famille d'ensembles E = (E_i)_i∈τ, soit comme un ensemble E avec une fonction t_E : E → τ donnant le type de chaque élément. La traduction entre les deux formalisations s'obtient dans un sens en prenant la somme, et dans l'autre en prenant les fibres de t_E (ce qu'on a appelé une partition indexée mais autorisant des composantes vides).
Cela mène à formaliser le concept de morphisme entre systèmes E,F avec une même liste τ de types (et interprétant un même langage), des deux manières respectives et équivalentes suivantes (en plus de devoir préserver toutes les structures) :

Comme uplet (ou famille) de fonctions (f_t)_t∈τ, où ∀i∈τ, f_i : E_i → F_i
Comme τ-morphisme f : E → F voyant τ comme liste de symboles de relations unaires (comme pour l'usage de classes comme notions en théorie des ensembles); autrement dit une fonction telle que t_F ⚬ f = t_E.

Théorie des ensembles et fondements des mathématiques
1. Premiers fondements des mathématiques
2. Théorie des ensembles
3. Algèbre

3.1. Correspondance de Galois
3.2. Systèmes relationnels et catégories concrètes
3.3. Algèbres
3.4. Morphismes particuliers
3.5. Monoïdes et catégories
3.6. Actions de monoides et de catégories
3.7. Inversibilité et groupes
3.8. Propriétés dans les catégories
3.9. Objets initiaux et finaux
3.10. Produits de systèmes
3.11. Bases

4. Arithmetic and first-order foundations
5. Second-order foundations
6. Foundations of Geometry

Other languages:
EN : 3.2. Relational systems and concrete categories