It can be thought of as the dual
concept to that of product of types in a given theory.
The concept of product of an n-tuple of types, namely the condition for a type
to play this role, was formalized in 2.3
("Tuples" and "Tuples axiom"). It consisted in introducing or distinguishing an
n-tuple of function symbols (serving as projections), an n-ary operation symbol
(tuples definer), and axioms making both the inverse of each other. But, it needs to be adapted to the
framework of category theory, weaker than one-theory theory. The formalization in category theory
keeps the projection symbols (which are function symbols), but needs to re-express the tuples
definer in terms of "invariant functions"
alone. The solution is to use the concept of product
of functions (2.8). The product of any family of invariant functions is also invariant (thinking of
it as defined using the tuples definer). This naturally leads to the standard concept
of product in category theory, which we shall formalize below.
∀_{C}X, X^{β} =
∏_{i∈I} X^{αi}
∀_{C}X,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}(x_{i}) = y_{i}
∀_{C}F, ⊓_{i∈I} π_{i}^{(F)} : P^{(F)} ↔ ∏_{i∈I} E_{i}^{(F)}
Their inverses define the products of morphisms, generalizing the concept of product of functions ⊓ to any category beyond the category of sets :⊓ : ∏_{i∈I} Mor(F, E_{i}) ↔ Mor(F, P)
The products in C of the empty family (I = ∅) are the final objects of C.⊓π : P → ∏_{i∈I} E_{i}
Its image is the common target set of all set theoretical products of morphisms f_{i}∈Mor(F, E_{i}) for a fixed object F and variable i∈I.
If C is regular then this ⊓π is bijective. This generally holds for acting categories, obviously
from definitions when written as C^{(F)} for some object F.
The bijectivity of ⊓π lets the role of categorical product (P,π) be played by the product of sets
∏_{i∈I} E_{i} with its natural family of projections
π = ⊓ Id_{P}.
Then in particular, final objets are singletons (even
if among objects there may be other, non-isomorphic singletons).
On the other hand, if the product as sets P = ∏_{i∈I} E_{i} of objects in a concrete category C is otherwise given a role of object, then the condition for it to serve as the product in C is that
∀F, ⊓[Mor(F,P)] = ∏_{i∈I} Mor(F,E_{i}).
The inclusion side of this equality is equivalent to (∀i∈I, π_{i} ∈ Mor(P,E_{i})). Indeed,In a concrete category, for any family of
elements
((E_{i},x_{i}))_{i∈I}, if the family of
objects (E_{i})_{i∈I} has a product (P, π) then the
existence of a product of the (E_{i},x_{i}) in the category of
elements is equivalent to ∃!: ⊓π_{•}(x) and implies that
((P, ℩⊓π_{•}(x)),π) is such a product.
(The proof is straightforward and left as an exercise)
Thus, if a set-product of concrete objects also serves as their categorical product then the family
definer is also what provides the representatives there of the products in the
category of elements.
In a concrete category C with products, the claim that (M,e) is an egg can be re-expressed as
∀_{C}E, ∃!f∈Mor(M,E^{E}), f(e) = Id_{E}.
∃!h∈Mor(Y, ^{C}∏_{Mor(X,M)} M), ∀u∈Mor(X,M), π_{u}∘h∘b = u.
If moreover C is concrete, this formula (∀u∈Mor(X,M), ∀x∈X, π_{u}(h(b(x))) = u(x)) can also be written∀x∈X, h(b(x)) = π_{x|Mor(X,M)}
P = ⋂_{i∈I} ^{L}π_{i⋆}(E_{i}) = ∐_{s∈L} ⊓[ ∏_{i∈I} s_{i}]
For a binary product of L-systems G = E×F these structures ares_{G} = {x⊓y | x∈s_{E} ∧ y∈s_{F}} = {z∈G^{ns} | π_{0}⚬z ∈s_{E} ∧ π_{1}⚬z ∈s_{F}}
To check that it forms a product in this category, for any L-system F and any f = ⊓_{i∈I} f_{i} ∈ P^{F}, i.e. ∀i∈I, f_{i} = π_{i}⚬f ∈ E_{i}^{F},f ∈ Mor_{L}(F,P) ⇔
^{L}f[F] ⊂ P ⇔ ∀i∈I,
^{L}f[F]
⊂ ^{L}π_{i⋆}(E_{i})
⇔ ∀i∈I, f_{i} ∈ Mor_{L}(F,E_{i})
⇔ ⊓f ∈ ∏_{i∈I}
Mor_{L}(F,E_{i})
(∀i∈I, π_{i} ∈ Mor_{L}(P,E_{i})) ⇔ (∀i∈I, φ_{i}⚬^{L}π_{i} = π_{i}⚬φ_{P}) ⇔ φ_{P} = ⊓_{i∈I} φ_{i}⚬^{L}π_{i}
Indeed, for any L-system F and any f = ⊓_{i∈I} f_{i} ∈ P^{F},f ∈ Mor_{L}(F,P) ⇔
φ_{P}⚬^{L}f = f⚬φ_{F}
⇔ ∀i∈I, φ_{i}⚬^{L}f_{i} =
φ_{i}⚬^{L}π_{i}⚬^{L}f =
f_{i}⚬φ_{F}
⇔ ∀i∈I, f_{i}
∈ Mor_{L}(F,E_{i})
⇔ ⊓f ∈
∏_{i∈I}
Mor_{L}(F,E_{i})
∀(x,y)∈^{L}P×P, y = φ_{P}(x) ⇔ ∀i∈I, y_{i} = φ_{i}(^{L}π_{i}(x))
The structure φ_{P} of a constant product P = E^{I} of an L-algebra E can be written^{L}P∋(s,x) ↦ s_{E} ⚬ ⊓x
The product of a family of actions of a given monoid, particular case of product of actions of a category, is also a particular case of product of algebras (precisely modules among these).Among systems, aside the case of algebras, any product of partial algebras is a partial algebra ; any product of injective systems is an injective system ; if AC_{I} holds then any product over I of serial systems is serial. But the surjectivity of a product system cannot be ensured unless it is achieved by a single symbol in L.
Let L an algebraic language, and E, F two L-systems.
If F is algebraic then
Mor_{L}(E,F) = {f∈F^{E} | Gr f ∈ Sub_{L}(E×F)}
This result may be split in two parts (whose proofs are left as exercises):(E injective ∧ H ⊂ G^{⋆}(^{L}H))
⇒ f ∈ Mor_{L}(E,F)
(E surjective ∧ f ∈ Mor_{L}(E,F)) ⇒ H
⊂ G^{⋆}(^{L}H)
∐_{t∈τ} ∏_{i∈I} E_{t,i}.
This is identifiable to a subset of ∏_{i∈I} E_{i} if I ≠ ∅ but a copy of τ if I = ∅.A wide pullback or wide fiber product of a nonempty family (f_{i})_{i∈I} of morphisms f_{i} ∈ Mor(E_{i} , T) to a fixed object T in a category C, is their product in the overcategory C/T. So it is a final object of the category whose objects are the triples of
∀i∈I, p'_{i} ∘ h = p_{i}
which implies q' ∘ h = q.An equivalent formalization of wide pullbacks eliminates the use of q replaced by f_{k} ∘ p_{k} for a fixed k∈I (independently of this choice), or all of them:
∀i,k∈I, f_{i} ∘ p_{i} = f_{k} ∘ p_{k}.
Hence the simpler definition in the binary case (when I is a pair): a pullback or fiber product of two morphisms f ∈ Mor(E, T), g ∈ Mor(F, T), is a co-egg of the sub-co-action of the product co-action C_{(E)}×C_{(F)}, giving to each X the set of all (p_{0},p_{1}) ∈ Mor(X, E)× Mor(X, F) such that f ∘ p_{0} = g ∘ p_{1}.In terms of co-actions, this is an equalizer inside a product. So, the same can be said in terms of categories when (E, F) has a product (G, π_{0}, π_{1}) where π_{0}∈ Mor(G, E), π_{1}∈ Mor(G, F). Namely, the pullback of (f,g) is identifiable with the subobject Eq(f∘π_{0},g∘π_{1}) of G, that is the sub-co-action C_{(f∘π0=g∘π1)} of C_{(G)} made of the p_{0}⊓p_{1} ∈ Mor(X, G) for the (p_{0},p_{1}) that fit the above condition.
Thus, any category with binary products and equalizers also has pullbacks; and in any concrete category where the underlying sets of products and equalizers are the set-like versions of these (such in as categories of all algebras or all systems over a given language), the same goes for its pullbacks obtained from these. In particular, any category of all typed algebras with a given set τ of types, has products given by the wide pullback over τ (which plays the role of final object of such a category).
Conversely, any category with binary products and pullbacks also has equalizers: any equalizer e = Eq(f, g) where f, g∈ Mor(E, F) can be extracted from a pullback in two ways:
There is a special use of pullbacks, namely to construct fiber bundles, where in the pullback (p_{0}, p_{1}) of (f,g), f and p_{1} serve as the components of a single morphism along two types, while g and p_{0} interpret a single function symbol in two systems.
In any concrete category, any intersection of quasi-embedded subobjects is quasi-embedded, with image the greatest image of a morphism into the intersection of images of given subobjects.
The proof for case 2. comes from the fact any wide pullback can be expressed as an intersection
of equalizers inside a product (which anyway exist as co-actions). This can be lengthily written
as follows.
Let us denote (A,a) this intersection, with
ϕ_{i}∈Mor(A,E_{i}) such that
a = e_{i}∘ϕ_{i} for each i∈I.
Let u∈Mor(X,A). As b is epic we just need to prove
(∃w∈Mor(Y,A), w∘b = u).
∃i∈I, ∃v∈Mor(Y,E_{i}), v∘b =
ϕ_{i}∘u
∀j∈I, ∃!w∈Mor(Y,E_{j}), w∘b =
ϕ_{j}∘u ∴ e_{j}∘w∘b =
e_{j}∘ϕ_{j}∘u
= a∘u = e_{i}∘ϕ_{i}∘u = e_{i}∘v∘b
∴ e_{j}∘w = e_{i}∘v.
As (A,a) is an intersection of the (E_{j},e_{j}),
∃w∈Mor(Y,A), a∘w = e_{i}∘v
∴ a∘w∘b = e_{i}∘v∘b =
e_{i}∘ϕ_{i}∘u = a∘u ∴ w∘b = u.∎
In any category of relational systems, subobjects of a system (F, F) are bijectively represented by its subsystems (E, E) in the sense that E⊂F ∧ E⊂F, with the monomorphism Id_{E} : E↪F. Then, the intersection of a family of subobjects (E_{i}, E_{i}) of (F, F) is represented by (⋂_{I∈I} E_{i}, ⋂_{I∈I} E_{i}) if we use the cateogry of all systems with a given language, or more generally if this system belongs to the considered category (which will be usually the case for categories defined as those of systems which are modules for some morphisms). This has two important special cases :
As first noted in 2.9 for a binary relation symbol, an intersection of preimages of structures by some functions from a given set, coincides with the preimage of the product structure by the product function.
Other languages:
FR : 3.10. Produits de systèmes