## 3.10. Products of systems

### Products of actions

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

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

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)iI of objects in a category C, written CiI Ei, is a co-egg (P, π) of the product of co-actions C(Ei), thus made of an object P with π ∈ ∏iI Mor(P,Ei) such that all f ↦ (πif)iI are bijective :

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

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

The product in the category of sets, coincides with the product of sets (⊓ : ∏iI EiFPF).

### Products in concrete categories

In many concrete categories, any family of objects has a product (P, π) whose role can usually be played by the product of sets P = ∏iI Ei with its natural family of projections π = ⊓ IdP.
Then in particular, final objets are singletons (even if other, non-isomorphic singletons may be objects).
Namely, given any product (P, π), this preferable convention is possible when ⊓π : P ↔ ∏iI Ei, transferring the role of P to ∏iI Ei by this bijection. (Its injectivity already implies for any F, Inj ⊓iI πi(F)).
Our main exceptions will be categories of typed systems: with a set τ of types, a product of objects with base sets Ei = ∐t∈τ Et,i will have base set

t∈τiI Et,i.

This is identifiable to a subset of ∏iI Ei if I ≠ ∅ but a copy of τ if I = ∅.

On the other hand, if the product as sets P = ∏iI 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)] = ∏iI Mor(F,Ei).

The inclusion side of this equality is equivalent to (∀iI, πi ∈ Mor(P,Ei)). Indeed,
i)iI = ⊓ IdP ∈ ⊓[Mor(P,P)] ⊂ ∏iI Mor(P,Ei) ⇒ ∀iI, πi ∈ Mor(P,Ei).
Conversely (simple reason) : ∀iI, πi ∈ Mor(P,Ei) ⇒ ∀f∈Mor(F,P), πif ∈ Mor(F,Ei).
Other presentation : ∀F, ⊓[Mor(F,P)] = Im ⊓iI πi(F) ⊂ ∏iI Mor(F,Ei). ∎
By essential uniqueness of products, this also determines all Mor(P,F) from the category.

If C is a concrete category with products, the statement of (M,e) being 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)iI of b-modules. Then ∀f∈Mor(X,P),
(∀iI, ∃!g∈Mor(Y, Ei), gb = πif)
∴ ∃!h∈Mor(Y,P), ∀iI, πihb = πif.
By Inj ⊓iI πi(X) we conclude ∃!h∈Mor(Y,P), hb = f. ∎
If C has products, the condition for an object M to be a b-module can be re-expressed as

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

If moreover C is concrete, this formula (∀u∈Mor(X,M), ∀xX, πu(h(b(x))) = u(x)) can also be written

xX, 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 = iI Lπi*(Ei) = ∐sL ⊓[ ∏iI si]

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

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

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

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

### Products of algebras

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

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

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

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

∀(x,y)∈LP×Py = φP(x) ⇔ ∀iI, 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.

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.

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