3.10. Products of systems

We shall now introduce the concept of product of a family of objects in a category, and its particular uses in diverse concrete categories. This generalizes the concept of product of a family of sets, as both will essentially coincide in the case of the category of sets.

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.

Products of actions

Given a family of actions (αi)i∈I of a category C, their product is an action β = ∏i∈I αi of C defined by

∀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

Products of families of co-actions are defined in the same way.
The action CM mentioned in 3.6 was the constant M-ary product of the primitive action of C.

Products in categories

A product of a family (Ei)i∈I of objects in a category C, written C∏i∈I Ei, is a co-egg (P, π) of the product of co-actions ∏i∈I C(Ei).
In other words, it is the data of an object P with a family π ∈ ∏i∈I Mor(P,Ei) making bijective all functions of the form (f ↦ (πi∘f)i∈I) where the f are morphisms with target P :

∀CF, ⊓i∈I πi(F) : P(F) ↔ ∏i∈I Ei(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, Ei) ↔ Mor(F, P)

The products in C of the empty family (I = ∅) are the final objects of C.

Products in concrete categories

In a concrete category C, a product (P, π) of a family of objects has a natural function into the set theoretical product, given by the product of functions

⊓π : P → ∏i∈I Ei

Its image is the common target set of all set theoretical products of morphisms fi∈Mor(F, Ei) 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 Ei with its natural family of projections π = ⊓ IdP.
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 Ei 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,Ei).

The inclusion side of this equality is equivalent to (∀i∈I, πi ∈ Mor(P,Ei)). Indeed, By essential uniqueness of products, this also determines all Mor(P,F) from the category.

In a concrete category, for any family of elements ((Ei,xi))i∈I, if the family of objects (Ei)i∈I has a product (P, π) then the existence of a product of the (Ei,xi) 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

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

Products of modules

For any morphism b∈Mor(X,Y) in any category C, any product of b-modules is also a b-module.
Proof. Let (P, π) a product of a family (Ei)i∈I of b-modules. Then ∀f∈Mor(X,P), If C has products, the condition for an object M to be a b-module can be re-expressed as

∃!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)

Products of relational systems

In a category of all relational L-systems (with fixed L), any family of systems (Ei, Ei) has a product P given by the product of sets, with structure

P = ⋂i∈I Lπi⋆(Ei) = ∐s∈L ⊓[ ∏i∈I si]

For a binary product of L-systems G = E×F these structures are

sG = {x⊓y | x∈sE ∧ y∈sF} = {z∈Gns | π0⚬z ∈sE ∧ π1⚬z ∈sF}

To check that it forms a product in this category, for any L-system F and any f = ⊓i∈I fi ∈ PF, i.e. ∀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)

For a symbol s of trajectory of a tuple in a concrete category, sP ⊂ ⊓[ ∏i∈I si] with equality if ACI holds.

Products of algebras

With an algebraic language L, the product P = ∏i∈I Ei of a family of L-algebras (Ei, φi) has L-algebra structure φP defined by

(∀i∈I, πi ∈ MorL(P,Ei)) ⇔ (∀i∈I, φi⚬Lπi = πi⚬φP) ⇔ φP = ⊓i∈I φi⚬Lπi

Indeed, for any L-system F and any 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)

This comes as a particular case of product of relational systems :

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

The structure φP of a constant product P = EI of an L-algebra E can be written

LP∋(s,x) ↦ sE ⚬ ⊓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 ACI 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.

Graphs of morphisms

For any morphism f∈ Mor(E,F) in a category with products, the morphism IdE⊓f from E to a product G = E×F is a section, thus defining the graph of f as an embedded subobject of G if the category is concrete. Let us review some more specific properties of graphs of morphisms between systems.

Let L an algebraic language, and E, F two L-systems.
If F is algebraic then

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

This result may be split in two parts (whose proofs are left as exercises):
  1. (F serial ∧ Gr f ∈ SubL(E×F)) ⇒ f ∈ MorL(E,F)
  2. (F functional ∧ f ∈ MorL(E,F)) ⇒ Gr f ∈ SubL(E×F)
When both E,F are algebraic (and thus E×F too), these may be seen as deducible from previous results:
  1. (Gr f ∈ SubL(E×F) ∧ π0|Gr f ∈ MorL(Gr f, E)) ⇒ IdE⊓f = (π0|Gr f)-1 ∈ MorL(E, Gr f) ⊂ MorL(E, E×F).
  2. f ∈ MorL(E,F) ⇔ IdE⊓f ∈ MorL(E,E×F) ⇒ Gr f = Im(IdE⊓f ) ∈ SubL(E×F).∎
and it gives another proof of the stability of equalizers On the other hand (with no algebraicity condition), denoting H = Gr f ⊂ G = E×F, we have ∀f∈FE,

(E injective ∧ H ⊂ G⋆(LH)) ⇒ f ∈ MorL(E,F)
(E surjective ∧ f ∈ MorL(E,F)) ⇒ H ⊂ G⋆(LH)

Fiber products

An important kind of concrete categories with products whose underlying sets differ from the products of sets, are the categories of typed systems. The effect of a categorical product between systems of a given kind which has multiple types, is dual to that of a product between types in a theory interpreted across multiple systems: it behaves as a product of sets for each type taken separately.
So, re-using the notations of 3.2, given a set τ of types and a family of typed concrete objects Ei = ∐t∈τ Et,i for each i∈I, their product will have base set

∐t∈τ ∏i∈I Et,i.

This is identifiable to a subset of ∏i∈I Ei if I ≠ ∅ but a copy of τ if I = ∅.
Our other formalization of the category of typed sets expressed its objects in the form (E, hE) where hE : E → τ, and morphisms from (E, hE) to (F, hF) are the f : E → F such that hF ⚬ f = hE. As already mentioned, such a category (with a fixed list τ of types) is an overcategory Set/τ of the category of sets.

A wide pullback or wide fiber product of a nonempty family (fi)i∈I of morphisms fi ∈ Mor(Ei , 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

and whose morphisms from such an object to a similar (P', q', (p'i)i∈I) are the h ∈ Mor(P, P') such that

∀i∈I, p'i ∘ h = pi

which implies q' ∘ h = q.
Indeed since I ≠ ∅, with a chosen k∈I we have q' ∘ h = fk ∘ p'k ∘ h = fk ∘ pk = q.

An equivalent formalization of wide pullbacks eliminates the use of q replaced by fk ∘ pk for a fixed k∈I (independently of this choice), or all of them:

∀i,k∈I, fi ∘ pi = fk ∘ pk.

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 (p0,p1) ∈ Mor(X, E)× Mor(X, F) such that f ∘ p0 = g ∘ p1.

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 p0⊓p1 ∈ Mor(X, G) for the (p0,p1) 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:

Products can themselves come as particular cases of wide pullbacks in categories with final objects.

There is a special use of pullbacks, namely to construct fiber bundles, where in the pullback (p0, p1) of (f,g), f and p1 serve as the components of a single morphism along two types, while g and p0 interpret a single function symbol in two systems.

Intersections of subobjects

Applying the concept of wide pullback to families of monomorphisms fi ∈ Mor(Ei , F), gives an operation between subobjects of F, called their intersection.
Indeed, the resulting morphism to F is also monic, it is related to the "inclusion" between subobjects the same way an intersection of sets is characterized from set inclusion, and it coincides with the operation of intersection between sub-co-actions.

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.

Intersections of submodules

For a given b∈Mor(X,Y), an intersection of a family of b-submodules (Ei,ei) of F indexed by I can be deduced to be also a b-submodule under either additional assumption:
  1. if F is a b-module ;
  2. or, if I ≠ ∅ and b is epic.
The simple proof with 1. is that an intersection of stable subsets is stable.
A more complex proof would use the above result on products of modules in the category of co-elements of C(F). This requires to prove that the condition for a subobject of F to be a b-submodule in C, is equivalent to it being a bh-module in the category of co-elements of C(F) for every h∈Mor(Y,F), where bh is the copy of b in Mor((X,h∘b), (Y,h)).

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,Ei) such that a = ei∘ϕ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,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.
As (A,a) is an intersection of the (Ej,ej),
∃w∈Mor(Y,A), a∘w = ei∘v ∴ a∘w∘b = ei∘v∘b = ei∘ϕi∘u = a∘u ∴ w∘b = u.∎

Intersections of subsystems

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 IdE : E↪F. Then, the intersection of a family of subobjects (Ei, Ei) of (F, F) is represented by (⋂I∈I Ei, ⋂I∈I Ei) 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 :

In the latter case, for a bijective b, the fact an intersection of b-module structures is a b-module structure can be seen as a case of the fact any intersection of stable subsets is stable.

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.

Set theory and foundations of mathematics
1. First foundations of mathematics
2. Set theory
3. Algebra 1
4. Arithmetic and first-order foundations
5. Second-order foundations
6. Foundations of Geometry

Other languages:
FR : 3.10. Produits de systèmes