3.10. Produits de systèmes

Nous allons maintenant introduire la notion de produit d'une famille d'objets dans une catégorie, et ses usages particuliers dans diverses catégories concrètes. Cela généralise le concept de produit d'une famille d'ensembles, les deux coïncidant essentiellement dans le cas de la catégorie des ensembles.

On peut voir cela comme le concept dual de celui de produit de types dans une théorie donnée.
Le concept de produit d'un n-uplet de types, à savoir la condition pour qu'un type joue ce rôle, a été formalisé en 2.3 («Uplets» et «Axiome des uplets»). Il consistait à introduire ou distinguer un n-uplet de symboles de fonctions (servant de projections), un symbole d'opération n-aire (définisseur d'uplets) et des axiomes les rendant l'inverse l'un de l'autre. Mais on doit l'adapter au cadre de la théorie des catégories, plus faible que la théorie de la théorie. La formalisation en théorie des catégories garde les symboles de projection (qui sont des symboles de fonction), mais doit ré-exprimer le définisseur d'uplets en termes de "fonctions invariantes" uniquement. La solution est d’utiliser le concept de produit de fonctions (2.8). Le produit de toute famille de fonctions invariantes est également invariant (vu comme défini à l'aide du définisseur d'uplets). Cela conduit naturellement au concept standard de produit en théorie des catégories, que nous formaliserons ci-dessous.

Produits d'actions

Étant donné une famille d'actions (αi)iI d'une catégorie C, leur produit est une action β = ∏iI αi de C définie par

CX, Xβ = ∏iI Xαi
CX,Y, ∀f∈ Mor(X,Y), f β = ⨉iI f αi = ⊓iI f αi ⚬ πi
xXβ, ∀yYβ, f β(x) = y ⇔ ∀iI, f αi(xi) = yi

Les produits des familles de co-actions se définissent de la même manière.
L'action CM mentionnée en 3.6 était le produit M-aire constant de l'action primitive de C.

Produits dans les catégories

Un produit d'une famille (Ei)iI d'objets dans une catégorie C, noté CiI Ei, est un co-oeuf (P, π) du produit de co-actions ∏iI C(Ei).
Autrement dit, c'est la donnée d'un objet P et d'une famille π ∈ ∏iI Mor(P,Ei), rendant bijectives toutes les fonctions de la forme f ↦ (πif)iI où les f sont des morphismes de cible P:

CF, ⊓iI πi(F) : P(F) ↔ ∏iI Ei(F)

Leurs inverses définissent les produits de morphismes, généralisant la notion de produit de fonctions ⊓ à toute catégorie au-delà de la catégorie des ensembles :

⊓ : ∏iI Mor(F, Ei) ↔ Mor(F, P)

Les produits dans C de la famille vide (I = ∅) sont les objets finaux de C.

Produits dans les catégories concrètes

Dans une catégorie concrète C, un produit (P, π) d'une famille d'objets a une fonction naturelle vers le produit ensembliste, donnée par le produit de fonctions

⊓π : P → ∏iI Ei

Son image est l'ensemble d'arrivée commun de tous les produits ensemblistes de morphismes fi∈Mor(F, Ei) pour un objet F fixe et un iI variable.

Si C est régulier alors ce ⊓π est bijectif. Cela vaut plus généralement pour les actions de catégories, présentées sous la forme C(F) pour un certain objet F, en conséquence directe des définitions.
La bijectivité de ⊓π permet de donner le rôle de produit catégoriel (P, π) au produit d'ensembles P = ∏iI Ei avec sa famille naturelle de projections π = ⊓ IdP.
Alors en particulier, les objets finaux sont des singletons (même si parmi les objets peuvent se trouver d'autres singletons non isomorphes).

A l'inverse, si le produit en tant qu'ensembles P = ∏iI Ei d'objets dans une catégorie concrète C reçoit par ailleurs un rôle d'objet, alors la condition pour qu'il serve de produit dans C est que

F, ⊓[Mor(F,P)] = ∏iI Mor(F,Ei).

Le côté d'inclusion de cette égalité équivaut à ∀iI, πi ∈ Mor(P,Ei). En effet, Par l'unicité essentielle des produits, cela détermine aussi tous les Mor(P,F) par la catégorie.

Dans une catégorie concrète, pour toute famille d'éléments ((Ei,xi))iI, si la famille d'objets (Ei)iI a un produit (P, π) alors l'existence d'un produit des (Ei,xi) dans la catégorie des éléments équivaut à ∃!: ⊓π(x) et implique que ((P, ℩⊓π(x)),π) est un tel produit. (La preuve est directe et laissée en exercice)
Ainsi, si un produit ensembliste d'objets concrets sert également de produit catégoriel, alors le définisseur de famille y définit aussi les représentants des produits dans la catégorie des éléments.

Si C est une catégorie concrète avec des produits, l'énoncé que (M,e) est un œuf est ré-exprimable par

CE, ∃!f∈Mor(M,EE), f(e) = IdE.

Produits de modules

Pour tout morphisme b∈Mor(X,Y) dans une categorie C, tout produit de b-modules est aussi un b-module.
Preuve. Soit (P, π) un produit d'une famille (Ei)iI de b-modules. Alors ∀f∈Mor(X,P), Si C a des produits, la condition qu'un objet M soit un b-module est ré-exprimable comme

∃!h∈Mor(Y, CMor(X,M) M), ∀u∈Mor(X,M), πuhb = u.

Si de plus C est concrète, cette formule (∀u∈Mor(X,M), ∀xX, πu(h(b(x))) = u(x)) peut aussi s'écrire

xX, h(b(x)) = πx|Mor(X,M)

Produits de systèmes relationnels

Dans une catégorie de tous les L-systèmes relationnels (avec L fixe), toute famille de systèmes (Ei, Ei) a un produit P donné par le produit d'ensembles, de structure

P = ⋂iI Lπi(Ei) = ∐sL ⊓[ ∏iI si]

Pour un produit binaire de L-systèmes G = E×F ces structures sont

sG = {xy | xsEysF} = {zGns | π0z sE ∧ π1zsF}

Pour vérifier qu'il forme un produit dans cette catégorie, pour tout L-système F et tout f = ⊓iI fiPF, à savoir ∀iI, fi = πifEiF,

f ∈ MorL(F,P) ⇔ Lf[F] ⊂ P ⇔ ∀iI, Lf[F] ⊂ Lπi(Ei)
⇔ ∀iI, fi ∈ MorL(F,Ei) ⇔ ⊓f ∈ ∏iI MorL(F,Ei)

Pour un symbole s de trajectoire d'un uplet dans une catégorie concrète, sP ⊂ ⊓[ ∏iI si] avec égalité si ACI.

Produits d'algèbres

Avec un langage algébrique L, le produit P = ∏iI Ei d'une famille de L-algèbres (Ei, φi) a la structure de L-algèbre φP définie par

(∀iI, πi ∈ MorL(P,Ei)) ⇔ (∀iI, φiLπi = πi⚬φP) ⇔ φP = ⊓iI φiLπi

En effet, pour tout L-système F et tout f = ⊓iI fiPF,

f ∈ MorL(F,P) ⇔ φPLf = f⚬φF ⇔ ∀iI, φiLfi = φiLπiLf = fi⚬φF
⇔ ∀iI, fi ∈ MorL(F,Ei) ⇔ ⊓f ∈ ∏iI MorL(F,Ei)

Cela vient comme cas particulier de produit de systèmes relationnels :

∀(x,y)∈LP×Py = φP(x) ⇔ ∀iI, yi = φi(Lπi(x))

La structure φP d'un produit constant P = EI d'une L-algèbre E peut s'écrire

LP∋(s,x) ↦ sE ⚬ ⊓x

Le produit d'une famille d'actions d'un monoïde donné, cas particulier de produit d'actions d'une catégorie, est aussi un cas particulier de produit d'algèbres (précisément des modules parmi ceux-ci).

Parmi les systèmes, à part le cas des algèbres, tout produit d'algèbres partielles est une algèbre partielle; tout produit de systèmes injectifs est un système injectif; si ACI vaut alors tout produit sur I de systèmes sériels est sériel. Mais la surjectivité d'un système produit ne peut être assurée que si elle est réalisée par un seul symbole dans L.

Graphes de morphismes

Pour tout morphisme f∈ Mor(E,F) dans une catégorie avec produits, le morphisme IdEf de E vers un produit G = E×F est une section, défininissant ainsi le graphe de f comme sous-objet plongé de G si la catégorie est concrète. Examinons quelques propriétés plus précises des graphes de morphismes entre systèmes.

Soit L un langage algébrique, et E, F deux L-systèmes.
Si F est algébrique alors

MorL(E,F) = {fFE | Gr f ∈ SubL(E×F)}

Ce résultat peut se décomposer en deux parties (dont les preuves sont laissées en exercice):
  1. (F sériel ∧ Gr f ∈ SubL(E×F)) ⇒ f ∈ MorL(E,F)
  2. (F fonctionnel ∧ f ∈ MorL(E,F)) ⇒ Gr f ∈ SubL(E×F)
Lorsque E et F sont algébriques (et donc E×F aussi), on peut voir cela comme déductible de résultats précédents:
  1. (Gr f ∈ SubL(E×F) ∧ π0|Gr f ∈ MorL(Gr f, E)) ⇒ IdEf = (π0|Gr f)-1 ∈ MorL(E, Gr f) ⊂ MorL(E, E×F).
  2. f ∈ MorL(E,F) ⇔ IdEf ∈ MorL(E,E×F) ⇒ Gr f = Im(IdEf ) ∈ SubL(E×F).∎
et cela donne une autre preuve de la stabilité des égaliseurs D'autre part (sans condition d'algébraïcité), notant H = Gr fG = E×F, on a ∀fFE,

(E injective ∧ HG(LH)) ⇒ f ∈ MorL(E,F)
(E surjective ∧ f ∈ MorL(E,F)) ⇒ HG(LH)

Produits fibrés

Une sorte importante de catégories concrètes avec des produits dont les ensembles sous-jacents diffèrent des produits d'ensembles, est formée des catégories de systèmes typés. L'effet d'un produit catégoriel entre une certaine sorte de systèmes ayant plusieurs types, est dual de celui d'un produit entre types d'une théorie interprétée à travers plusieurs systèmes : il se comporte comme un produit d'ensembles pour chaque type pris séparément.
Reprenant les notations de 3.2, avec un ensemble τ de types et une famille d'objets concrets typés Ei = ∐t∈τ Et,i pour chaque iI, leur produit aura pour ensemble de base

t∈τiI Et,i.

Il est identifiable à un sous-ensemble de ∏iI Ei si I ≠ ∅ mais une copie de τ si I = ∅.
Notre autre formalisation de la catégorie des ensembles typés exprimait ses objets sous la forme (E, hE) où hE : E → τ, et les morphismes de (E, hE) vers (F, hF) sont les f : EF tels que hFf = hE. C'est une catégorie de co-éléments Set/τ.

Un large produit fibré d'une famille non-vide (fi)iI de morphismes fi ∈ Mor(Ei , T) vers une objet fixe T dans une categorie C, est leur produit dans C/T. C'est donc un objet final de la categorie dont les objets sont les triplets de

et où les morphismes d'un tel objet vers un autre (P', q', (p'i)iI) sont les h ∈ Mor(P, P') tels que

iI, p'ih = pi

ce qui implique q'h = q.
En effet comme I ≠ ∅, fixant un kI on a q'h = fkp'kh = fkpk = q.

Une formalisation équivalente des larges produits fibrés élimine l'usage de q remplacé par fkpk pour un kI fixé (independamment de ce choix), voire tous:

i,kI, fipi = fkpk.

D'où la définition plus simple dans le cas binaire (où I est une paire): un produit fibré de deux morphismes f ∈ Mor(E, T), g ∈ Mor(F, T), est un co-oeuf de la sous-co-action de la co-action produit C(E)×C(F), donnant à chaque X l'ensemble de tous les (p0,p1) ∈ Mor(X, E)× Mor(X, F) tels que fp0 = gp1.

En termes de co-actions, c'est un égaliseur dans un produit. Ainsi, il en va autant en termes de catégories lorsque (E, F) a un produit (G, π0, π1) où π0∈ Mor(G, E), π1∈ Mor(G, F). A savoir, le produit fibré de (f,g) est identifiable au sous-objet Eq(f∘π0,g∘π1) de G, c'est-à-dire la sous-co-action C(f∘π0=g∘π1) de C(G) faite des p0p1 ∈ Mor(X, G) pour les (p0,p1) remplissant la condition ci-dessus.

Ainsi, toute catégorie avec des produits binaires et des égaliseurs a aussi des produits fibrés ; et dans toute catégorie concrète où les ensembles sous-jacents de produits et d'égaliseurs sont les versions ensemblistes de ceux-ci (notamment dans les catégories de toutes les algèbres ou de tous les systèmes sur un langage donné), il en va de même pour les produits fibrés obtenus à partir de ceux-ci. En particulier, toute catégorie de toutes les algèbres typées avec un ensemble τ de types donné, a des produits donnés par le large produit fibré sur τ (qui joue le rôle d'objet final d'une telle catégorie).

Réciproquement, toute catégorie avec des produits binaires et des produits fibrés a aussi des égaliseurs : tout égaliseur e = Eq(f, g) où f, g∈ Mor(E, F) peut être extrait d'un produit fibré de deux manières :

Les produits peuvent eux-mêmes être restitués comme cas particuliers de larges produits fibrés dans les catégories avec objets finaux.

Il existe une utilisation particulière des produits fibrés, à savoir pour construire des espaces fibrés, où dans le produit fibré (p0, p1) de (f,g), f et p1 servent de composants d'un même morphisme suivant deux types, tandis que g et p0 interprètent un même symbole de fonction dans deux systèmes.

Intersections de sous-objets

Le concept de large produit fibré appliqué aux familles de monomorphismes fi ∈ Mor(Ei , F), définit une opération entre sous-objets de F, appelée leur intersection.
En effet, le morphisme vers F qui en résulte est aussi monique, il a le même lien au concept d'"inclusion" entre sous-objets, que celui de l'intersection d'ensembles à l'inclusion entre ensembles, et il coïncide avec l'intersection entre sous-co-actions.

Dans toute categorie concrete, toute intersection de sous-objets quasi-plongés est quasi-plongée, d'image la plus grande image d'un morphisme vers l'intersection des images des sous-objets donnés.

Intersections de sous-modules

Pour un b∈Mor(X,Y) donné, on peut montrer qu'une intersection d'une famille de b-sous-modules (Ei,ei) de F indexée par I est aussi un b-sous-module, sous l'une ou l'autre hypothèse supplémentaire :
  1. si F est un b-module ;
  2. ou, si I ≠ ∅ et b est épique.
La simple preuve pour le cas 1, est qu'une intersection de parties stables est stable.
Une preuve plus complexe utiliserait le résultat ci-dessus sur les produits de modules dans la catégorie des co-éléments de C(F). Pour cela, il faut montrer que la condition pour qu'un sous-objet de F soit un b-sous-module dans C, équivaut à ce qu'il soit un bh-module dans la catégorie des co-éléments de C(F) pour tout h∈Mor(Y,F), où bh est la copie de b dans Mor((X,hb), (Y,h)).

La preuve pour le cas 2 vient du fait que tout large produit fibré est exprimable comme une intersection d'égaliseurs dans un produit, qui existe au moins en termes de co-actions.
Notons (A,a) cette intersection, avec ϕi∈Mor(A,Ei) tel que a = ei∘ϕi pour chaque iI.
Soit u∈Mor(X,A). Comme b est épique il suffit de montrer (∃w∈Mor(Y,A), wb = u).
iI, ∃v∈Mor(Y,Ei), vb = ϕiu
jI, ∃!w∈Mor(Y,Ej), wb = ϕjuejwb = ej∘ϕju = au = ei∘ϕiu = eivbejw = eiv.
Comme (A,a) est une intersection des (Ej,ej),
w∈Mor(Y,A), aw = eivawb = eivb = ei∘ϕiu = auwb = u.∎

Intersections de sous-systèmes

Dans toute categorie de systèmes relationnels, les sous-objets d'un système (F, F) sont bijectivement representés par ses sous-systèmes (E, E) au sens de EFEF, avec le monomorphisme IdE : EF. Alors l'intersection d'une famille de sous-objets (Ei, Ei) de (F, F) est représentée par (⋂II Ei, ⋂II Ei) dans le cas de la catégorie de tous les systèmes de langage donné, ou plus généralement si ce système appartient à la catégorie considérée (ce qui sera généralement le cas pour des catégories définies comme celles de systèmes modules pour certains morphismes). Cela a deux cas particuliers importants : Dans le dernier cas, pour un b bijectif, le fait qu'une intersection de structures de b-modules soit une structure de b-module peut être vu comme un cas du fait que toute intersection de parties stables est stable.

Comme remarqué en 2.9 pour un symbole de relation binaire, une intersection de préimages de structures par une famille de fonctions d'un ensemble donné, coïncide avec la préimage de la structure produit par la fonction produit.


Théorie des ensembles et fondements des mathématiques
1. Premiers fondements des mathématiques
2. Théorie des ensembles
3. Algèbre
4. Arithmetic and first-order foundations
5. Second-order foundations
6. Foundations of Geometry

Other languages:
EN : 3.10. Products of systems