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.
∀CX, Xβ =
∏i∈I Xαi
∀CX,Y, ∀f∈ Mor(X,Y),
f β = ⨉i∈I f αi
= ⊓i∈I f αi ⚬ πi
∀x∈Xβ, ∀y∈Yβ,
f β(x) = y ⇔ ∀i∈I,
f αi(xi) = yi
∀CF, ⊓i∈I πi(F) : P(F) ↔ ∏i∈I 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 :⊓ : ∏i∈I Mor(F, Ei) ↔ Mor(F, P)
Les produits dans C de la famille vide (I = ∅) sont les objets finaux de C.⊓π : P → ∏i∈I 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 i∈I 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 = ∏i∈I 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 = ∏i∈I 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)] = ∏i∈I Mor(F,Ei).
Le côté d'inclusion de cette égalité équivaut à ∀i∈I, πi ∈ Mor(P,Ei). En effet,Dans une catégorie concrète,
pour toute famille d'éléments
((Ei,xi))i∈I, si la famille d'objets
(Ei)i∈I 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.
∃!h∈Mor(Y, C∏Mor(X,M) M), ∀u∈Mor(X,M), πu∘h∘b = u.
Si de plus C est concrète, cette formule (∀u∈Mor(X,M), ∀x∈X, πu(h(b(x))) = u(x)) peut aussi s'écrire∀x∈X, h(b(x)) = πx|Mor(X,M)
P = ⋂i∈I Lπi⋆(Ei) = ∐s∈L ⊓[ ∏i∈I si]
Pour un produit binaire de L-systèmes G = E×F ces structures sontsG = {x⊓y | x∈sE ∧ y∈sF} = {z∈Gns | π0⚬z ∈sE ∧ π1⚬z ∈sF}
Pour vérifier qu'il forme un produit dans cette catégorie, pour tout L-système F et tout f = ⊓i∈I fi ∈ PF, à savoir ∀i∈I, fi = πi⚬f ∈ EiF,f ∈ MorL(F,P) ⇔
Lf[F] ⊂ P ⇔ ∀i∈I, Lf[F]
⊂ Lπi⋆(Ei)
⇔ ∀i∈I, fi ∈ MorL(F,Ei)
⇔ ⊓f ∈ ∏i∈I
MorL(F,Ei)
(∀i∈I, πi ∈ MorL(P,Ei)) ⇔ (∀i∈I, φi⚬Lπi = πi⚬φP) ⇔ φP = ⊓i∈I φi⚬Lπi
En effet, pour tout L-système F et tout f = ⊓i∈I fi ∈ PF,f ∈ MorL(F,P) ⇔
φP⚬Lf = f⚬φF
⇔ ∀i∈I, φi⚬Lfi =
φi⚬Lπi⚬Lf =
fi⚬φF
⇔ ∀i∈I, fi
∈ MorL(F,Ei)
⇔ ⊓f ∈
∏i∈I
MorL(F,Ei)
∀(x,y)∈LP×P, y = φP(x) ⇔ ∀i∈I, yi = φi(Lπi(x))
La structure φP d'un produit constant P = EI d'une L-algèbre E peut s'écrireLP∋(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.
Soit L un langage algébrique, et E, F deux L-systèmes.
Si F est algébrique alors
MorL(E,F) = {f∈FE | Gr f ∈ SubL(E×F)}
Ce résultat peut se décomposer en deux parties (dont les preuves sont laissées en exercice):(E injective ∧ H ⊂ G⋆(LH))
⇒ f ∈ MorL(E,F)
(E surjective ∧ f ∈ MorL(E,F)) ⇒ H
⊂ G⋆(LH)
∐t∈τ ∏i∈I Et,i.
Il est identifiable à un sous-ensemble de ∏i∈I Ei si I ≠ ∅ mais une copie de τ si I = ∅.Un large produit fibré d'une famille non-vide (fi)i∈I 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
∀i∈I, p'i ∘ h = pi
ce qui implique q' ∘ h = q.Une formalisation équivalente des larges produits fibrés élimine l'usage de q remplacé par fk ∘ pk pour un k∈I fixé (independamment de ce choix), voire tous:
∀i,k∈I, fi ∘ pi = fk ∘ pk.
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 f ∘ p0 = g ∘ p1.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 p0⊓p1 ∈ 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 :
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.
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.
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 i∈I.
Soit u∈Mor(X,A). Comme b est épique il suffit de montrer
(∃w∈Mor(Y,A), w∘b = u).
∃i∈I, ∃v∈Mor(Y,Ei), v∘b =
ϕi∘u
∀j∈I, ∃!w∈Mor(Y,Ej), w∘b =
ϕj∘u ∴ ej∘w∘b =
ej∘ϕj∘u
= a∘u = ei∘ϕi∘u = ei∘v∘b
∴ ej∘w = ei∘v.
Comme (A,a) est une intersection des
(Ej,ej),
∃w∈Mor(Y,A), a∘w = ei∘v
∴ a∘w∘b = ei∘v∘b =
ei∘ϕi∘u = a∘u ∴ w∘b = u.∎
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.
Other languages:
EN :
3.10. Products of systems