Theory and Applications of Categories, Vol. 32, No. 19, 2017, pp. 682–718.

A PRESENTATION OF BASES FOR PARAMETRIZED ITERATIVITY

JIŘÍ ADÁMEK, STEFAN MILIUS AND JIŘÍ VELEBIL

One for the money Two for the show Three to get ready And four to go.

Nursery rhyme

Abstract. Finitary monads on a locally finitely presentable category 𝒜 are wellknown to possess a presentation by signatures and equations. Here we prove that, analogously, bases on 𝒜, i.e., finitary functors from 𝒜 to the category of finitary monads on 𝒜, possess a presentation by parametrized signatures and equations.

1. Introduction

It is known since the classical work by Michael Barr [9] that free algebras for an endofunctor H (equivalently, the parametrized initial algebras μX.(HX + A)) yield the object assignment of a monad, in fact, the free monad on H. Similarly, the parametrized final coalgebras T A = νX.(HX + A) yield a monad as shown by Larry Moss [18]. This monad is completely iterative in the sense of Calvin Elgot, Stephen Bloom and Ralph Tindell [10]. We have proven in [1] that T is in fact the free completely iterative monad on H.

It was an idea of Tarmo Uustalu [22] that monad structures from parametrized initial algebras and final coalgebras can be obtained more generally from what he called a parametrized monad (in lieu of an endofunctor). A parametrized monad on a category 𝒜 is a functor □ which assigns to every object X of 𝒜 a monad X □ − on 𝒜, the leading example being X □ A = HX + A with the monad structure given by coproduct. He showed that the initial algebras μX.(X □ A) and the final coalgebra νX.(X □ A) yield monads, the latter being completely iterative.

Subsequently, we introduced a “finitary” form of parametrized monads, called bases [5], which are finitary functors

□ : 𝒜 ⟶ Mnd_{f} (𝒜)

Stefan Milius acknowledges support by the Deutsche Forschungsgemeinschaft (DFG) under project MI 717/5-1.

Received by the editors 2016-04-20 and, in final form, 2017-05-03.

Transmitted by Stephen Lack. Published on 2017-05-05.

2010 Mathematics Subject Classification: 08C05, 18C20, 18C35.

Key words and phrases: parametrized monads, bases, algebra, presentation.

\begin{matrix}c \\ ◯ \end{matrix} Jiří Adámek, Stefan Milius and Jiří Velebil, 2017. Permission to copy for private use granted.

from a locally finitely presentable category 𝒜 to the category of finitary monads on 𝒜. A leading example is X □ A = HX + A for a finitary endofunctor H. We used bases as the starting point of an extensive study of parametrized iterativity [5, 6, 7], generalizing and extending classical work on iterative algebras for a signature of Evelyn Nelson [19] and Jerzy Tiuryn [21] as well as our own work on iterative algebras for endofunctors [4].

The present paper does not study parametric iterativity of algebras for a base; here we concentrate on bases as such. We generalize the result of Max Kelly and John Power [13] that every finitary monad on 𝒜 has an equational presentation (using the appropriate concept of a signature in a locally finitely presentable category) to bases. For that we introduce parametrized signatures and equations.

In the rest of this introduction we explain the approach of Max Kelly and John Power to signatures in general categories, specializing it to the case of finitary signatures since this is the only case of interest for bases. In Sections 2–5 we then generalize this approach to parametrized signatures and in Section 6 we discuss the special case where 𝒜 = Set.

Throughout the paper 𝒜 denotes a locally finitely presentable category in the sense of Peter Gabriel and Friedrich Ulmer, see [11] or [8]. Let 𝒜_{fp} be a small full subcategory representing all finitely presentable objects.

1.1. Definition. A signature Σ is a collection of objects Σ(m) of 𝒜 indexed by m in 𝒜_{fp}. A morphism h : Σ ⟶ Γ of signatures is a collection of morphisms h_{m} : Σ(m) ⟶ Γ(m).

Thus, the category of signatures is simply the functor category

Sig(𝒜) = [|𝒜_{fp}|, 𝒜],

where |𝒜_{fp}| denotes the discrete category given by the objects of 𝒜_{fp}. This is, in the case where 𝒜 = Set, the classical concept; also the concept of a Σ-algebra is the classical one for 𝒜 = Set. That is, a set A together with m-ary operations indexed by Σ(m) for all m in ℕ. We can view the latter as a function from Set(m, A) × Σ(m) into A. For general categories we use M • X to denote a coproduct of M copies of X. We are lead to the following

1.2. Definition. A Σ-algebra is a pair (A, a) where A is an object of 𝒜 and a is a morphism

a : ∐_{m∈|𝒜_{fp}|} 𝒜 (m, A) • Σ(m) ⟶ A

A homomorphism into another Σ-algebra (B, b) is a morphism h : A ⟶ B such that the component of h · a corresponding to f : m ⟶ A composed with h is precisely the component of b corresponding to h · f : m ⟶ B.

We obtain the category of Σ-algebras and homomorphisms.

Recall from [15] that finitary monads are monadic over signatures. In more detail, if Mnd_{f} (𝒜) is the category of finitary monads and monad morphisms, we have a canonical forgetful functor

U′ : Mnd_{f} (𝒜) ⟶ Sig(𝒜)

taking a monad T to the signature

U′(T) = Σ, where Σ(m) = T m.  (1.1)

This functor preserves filtered colimits, since they are formed objectwise in Mnd_{f} (𝒜). Every signature Σ generates a free finitary monad, i.e., U′ has a left adjoint

F′ : Sig(𝒜) ⟶ Mnd_{f} (𝒜)  (1.2)

Moreover, U′ is a monadic functor. In particular, every finitary monad T has a presentation as a coequaliser of two morphisms between free monads:

\xymatrix{F′Γ \ar[r]^{λ} \ar[r]_{ρ} & F′Σ \ar[r]^{c} & T}

The finitary monad of F′ ⊣ U′ on the category Sig(𝒜) signatures is denoted by (−)^{∗}. Observe that since Mnd_{f} (𝒜) is finitary monadic over the (obviously cocomplete) category Sig(𝒜), it is a cocomplete category, too. Indeed, this category is finitary monadic over the category Fin[𝒜 , 𝒜] of all finitary endofunctors on 𝒜 (see e.g. [15]).

1.3. Example. If 𝒜 = Set then for every signature Σ the n-ary operation symbols of Σ^{∗} are precisely the Σ-terms on n variables.

A beautiful characterisation of Eilenberg-Moore algebras for T was given in [13, 14]: these algebras are precisely the algebras for Σ that satisfy the equations specified by the above pair (λ, ρ). The technique is to associate with every object B of 𝒜 a finitary monad ⟨B, B⟩ on 𝒜 such that, for any finitary monad T, we have a bijection

\frac{T B ⟶ B}{T ⟶ ⟨B, B⟩}

between Eilenberg-Moore algebras on B and monad morphisms from T to ⟨B, B⟩. We recall this technique, introduced by Anders Kock [14], in Section 4. Analogously, with every morphism f : B ⟶ C of 𝒜 one can associate a finitary monad {f, f} on 𝒜 such that, given a finitary monad T, we have a bijection

\frac{f : B ⟶ C}{T ⟶ \{f, f\}}

between homomorphisms f of Eilenberg-Moore algebras for T and monad morphisms from T to {f, f}. To prove the above equational presentation of algebras for T one then simply employs the universal property of coequalizers.

We mimic this technique for bases. Using results of [15] we prove that the category of all bases on a locally finitely presentable category 𝒜 is monadic over the appropriate category of parametrized signatures in 𝒜. This allows us to prove that every base is a coequalizer of a parallel pair of base morphisms between free bases. Then we associate with every object B a base ⟨⟨B, B⟩⟩ with the analogous universal property of ⟨B, B⟩ above w.r.t. bases, and with every morphism f a base {{f, f}} with the analogous property w.r.t. base morphisms. This allows us to derive an equational presentation of algebras for a base.

Index of notations.

Categories  Functors  Special symbols

(order by appearance)

𝒜_{fp}, 2.1  E, 2.1  □, 2.4
Alg □, 4.2  F, (3.4)  ˆ(−), 2.1
Base(𝒜), 2.6  F′, (1.2)  •, 2.10
Fin[𝒜 , ℬ], 2.2  J, 3.5  ⋔, 2.10
IdxSig(𝒜), 3.16  U_{sig}, 3.17  ∘, 2.8
Mon([𝒜_{fp}, 𝒜]), 2.2  F_{sig}, 3.17  ⊗, 2.11
Mnd_{f} (𝒜), 2.2  U′_{fun}, 3.18  Σ, 3.1, 3.3
ParFin(𝒜), 2.7  F′_{fun}, 3.18  ♢, 3.7
Sig(𝒜), 1.1  □_{Σ}, 3.8, 3.9

Σ^{(i)}, Σ^{(X)}, 3.9

Σ^{@}, 3.13

Acknowledgement. We are very grateful to the referee whose careful reading and numerous suggestions helped us improving our presentation.

2. Bases as monoids

The approach to bases we develop in this section is inspired by the treatment of monads in [12, 13, 15]. In fact, the notions introduced below are slight modifications of notions introduced in the abovementioned papers to the finitary and parametrized cases.

2.1. Notation. In the rest of the paper, 𝒜 is a locally finitely presentable category. That is, a cocomplete category having a small full subcategory E : 𝒜_{fp} ⟶ 𝒜 of finitely presentable objects such that 𝒜 is the closure of 𝒜_{fp} under filtered colimits. (An object is called finitely presentable if its hom-functor preserves filtered colimits.) By |𝒜_{fp}| we denote the set of objects of 𝒜_{fp} and we treat |𝒜_{fp}| as a (small) discrete category.

2.2. Remark. The category 𝒜 is a free cocompletion of 𝒜_{fp} under filtered colimits, see [8]. We thus have, for every category ℬ with filtered colimits, an equivalence between

(1) the category Fin[𝒜 , ℬ] of finitary functors from 𝒜 to ℬ, and

(2) the functor category [𝒜_{fp}, ℬ].

This equivalence is given by restriction and left Kan extension along the full embedding E : 𝒜_{fp} ⟶ 𝒜.

Thus, below we often define a finitary functor by specifying its values on finitely presentable objects only, and we often use the same symbol to denote a finitary functor on 𝒜 and its restriction 𝒜_{fp} ⟶ 𝒜.

Moreover, the equivalence Fin[𝒜 , 𝒜] ≃ [𝒜_{fp}, 𝒜] makes [𝒜_{fp}, 𝒜] a monoidal category whose monoidal structure corresponds to composition in Fin[𝒜 , 𝒜]. This yields an equivalence of

(1) the category Mnd_{f} (𝒜) of finitary monads on 𝒜, and

(2) the category Mon([𝒜_{fp}, 𝒜]) of monoids in [𝒜_{fp}, 𝒜].

The objects of Mon([𝒜_{fp}, 𝒜]) have been identified in [3], completely analogous to the famous presentation of monads by Ernie Manes [17], as finitary Kleisli triples. A finitary Kleisli triple (T, η, ˆ(−)) consists of

(i) An object-assignment X ⟼ T X for every finitely presentable object X.

(ii) A collection of arrows η_{X} : X ⟶ T X indexed by finitely presentable objects.

(iii) An assignment ˆ(−) called extension sending every arrow s : X ⟶ T Y, X and Y finitely presentable, to an arrow ŝ : T X ⟶ T Y subject to the following three axioms:

(a) η̂_{X} = id_{T X}, for every finitely presentable X.

(b) ŝ· η_{X} = s, for every s : X ⟶ T Y, X, Y finitely presentable.

(c) { \atop (t̂· s)} = t̂· ŝ, for every pair s : X ⟶ T Y and t : Y ⟶ T Z, where X, Y and Z are finitely presentable.

Therefore we often, instead of specifying a finitary monad, specify the corresponding finitary Kleisli triple.

We proceed now by “lifting” the above treatment of finitary monads to the parametrized case. Parametrized monads were first studied by Uustalu in [22]. In our subsequent work [6] we introduced the name base for the finitary case. We recall this concept and the concept of a parametrized endofunctor first.

2.3. Definition. By a base on 𝒜 we understand a finitary functor □ from 𝒜 to the category Mnd_{f} (𝒜) of finitary monads on 𝒜.

A base morphism is a natural transformation between bases.

2.4. Notation. We use bases □ : 𝒜 ⟶ Mnd_{f} (𝒜) in the uncurried form as functors in two variables: X □ A is the object that the monad X □ − assigns to A. Analogously for morphisms f : X ⟶ X′, g : A ⟶ A′, we write f □ g : X □ A ⟶ X′ □ A′. Every finitary monad X □ − has the unit u_{A}^{X} : A ⟶ X □ A and the multiplication m_{A}^{X} = X □ (X □ A) ⟶ X □ A.

A PRESENTATION OF BASES FOR PARAMETRIZED ITERATIVITY  687

2.5. Example. ([5])

(1) Coproduct yields a base

X □ A = X + A

Every finitary monad X + − has the unit u_{A}^{X} = inr : A ⟶ X + A and the multiplication m_{A}^{X} = ∇ + A.

(2) In the category of sets we have the base

X □ A = X^{∗} × A where (X^{∗}, η_{X}, μ_{X}) is the free monoid on X. The unit of X □ − is u_{A}^{X} = η_{X} × A : 1×A ⟶ X^{∗} ×A and the multiplication of X □− is m_{A}^{X} = μ_{X} ×A : X^{∗} ×X^{∗} ×A ⟶ X^{∗} × A.

(3) Every finitary endofunctor H : 𝒜 ⟶ 𝒜 defines the base

X □ A = HX + A with the unit of X □ − being u_{A}^{X} = inr : A ⟶ HX + A and the multiplication of X □ − being m_{A}^{X} = ∇ + A : HX + HX + A ⟶ HX + A.

(4) Finitary monads (M, η, μ) are bases independent of the parameter: X □ A = MA.

(5) More generally, for every finitary monad (M, η, μ) on 𝒜 and every finitary endofunctor

H : 𝒜 ⟶ 𝒜 we have a base

X □ A = M(HX + A)

with the unit of X □ − being u_{A}^{X} = η_{HX+A} · inr and the multiplication of X □ − being

M(HX + M(HX + A)) ⟶^{M[η_{HX+A}·inl ,id]} MM(HX + A) ⟶^{μ_{HX+A}} M(HX + A).

2.6. Notation. We denote by

Base(𝒜) = Fin[𝒜 , Mnd_{f} (𝒜)]

the category of bases on 𝒜. 2.7. Definition. A parametrized endofunctor on 𝒜 is a finitary functor

H : 𝒜 ⟶ Fin[𝒜 , 𝒜]

into the category Fin[𝒜 , 𝒜] of finitary endofunctors on 𝒜. We will often write the values of H in uncurried form as H(X, A) (rather than H(X)(A)).

The category

ParFin(𝒜)

of parametrized endofunctors is defined as the category Fin[𝒜 , Fin[𝒜 , 𝒜]].

To specify a parametrized endofunctor, it suffices to specify a functor of two finitely presentable variables, since the equivalences below hold:

ParFin(𝒜) ≃ [𝒜_{fp}, [𝒜_{fp}, 𝒜]] ≃ [𝒜_{fp} × 𝒜_{fp}, 𝒜].  (2.1)

Again we shall often write the same symbol for a parametrized endofunctor and its corresponding restrictions to 𝒜_{fp} in either or both of its arguments.

2.8. Notation. The strict monoidal structure on Fin[𝒜 , 𝒜] induces a strict monoidal structure on the category

ParFin(𝒜) = Fin[𝒜 , Fin[𝒜 , 𝒜]] in the “pointwise” manner. Namely, for parametrized endofunctors H, K we define the parametrized endofunctor K∘H by putting, (K∘H)(X) : 𝒜 ⟶ 𝒜 to be the composite K(X) · H(X), for every X. Written in the uncurried form:

(K ∘ H)(X, A) = K(X, H(X, A))

Thus the monoidal multiplication (K, H) ⟼ K ∘ H is finitary in each variable, and it is strictly associative. The two-sided unit is given by the family I(X) = Id : 𝒜 ⟶ 𝒜, or, when uncurried,

I(X, A) = A

constitutes the two-sided unit for ∘.

2.9. Lemma. The bases on 𝒜 are in bijective correspondence with the monoids in the monoidal category (ParFin(𝒜), ∘, I).

Proof. Write a base □ : 𝒜 ⟶ Mnd_{f} (𝒜) in its uncurried form, i.e., write

X □ A

for the value of □ at X, A. Denote the finitary monad given by every X □ − by

(X □ −, u^{X}, m^{X})

Apart from monad laws, the above data must satisfy the following compatibility conditions for every h : X ⟶ X′ and every f : A ⟶ A′:

\xymatrix{A \ar[r]^{u_{A}^{X}} \ar[d]_{f} & X □ A \ar[d]^{h□f} \\ A′ \ar[r]_{u_{B′}^{X′}} & X′ □ A′}  (2.2)

and

\xymatrix{X □ (X □ A) \ar[r]^{m_{A}^{X}} \ar[d]_{h□(h□f)} & X □ A \ar[d]^{h□f} \\ X′ □ (X′ □ A′) \ar[r]_{m_{A′}^{X′}} & X′ □ A′}  (2.3)

They express the naturality of u^{X} and m^{X} and the fact that for every morphism h : X ⟶ X′ we have a monad morphism h □ (−) : X □ (−) ⟶ X′ □ (−).

The morphisms u : I ⟶ □ and m : □ ∘ □ ⟶ □ in ParFin(𝒜) satisfy the axioms for a monoid, this follows from the unit law and the associativity of the monads X □ (−)

The correspondence between morphisms of bases and morphisms of monoids is verified analogously.

2.10. Notation. For a set M and an object A of 𝒜 we denote by

M • A = ∐_{m∈M} A

the M-fold copower of A and by

M ⋔ A = ∏_{m∈M} A

the M-fold power of A. Analogously, for a morphism g : A ⟶ B we denote by M • g : M • A ⟶ M • B the M-fold copower and by M ⋔ g : M ⋔ A ⟶ M ⋔ B the M-fold power of g.

For every set M there are bijections

𝒜 (X, M ⋔ A) ≅ Set(M, 𝒜 (X, A)) ≅ 𝒜 (M • X, A)  (2.4)

natural in X and A.

2.11. Remark.

(1) The equivalence (2.1) allows us to transfer the monoidal structure of Notation 2.8 from ParFin(𝒜) to [𝒜_{fp} × 𝒜_{fp}, 𝒜]. More precisely, the monoidal product K ∘ H is transferred to

(K ⊗ H)(X, A) = ∫ ^{Z:𝒜_{fp}} 𝒜 (Z, H(X, A)) • K(X, Z)  (2.5)

The two-sided unit I of the (now non-strict!) monoidal product ⊗ is I(X, A) = A.

(2) Due to the above equivalence and Lemma 2.9 we obtain an equivalence

Base(𝒜) ≃ Mon([𝒜_{fp} × 𝒜_{fp}, 𝒜])

in complete analogy to finitary monads.

In addition, by the above equivalences, both Base(𝒜) and ParFin(𝒜) are locally finitely presentable categories, hence complete and cocomplete.

(3) Observe that for any H, K, the functors K ⊗ − and − ⊗ H preserve filtered colimits. The former follows directly from (2.5) and the latter follows from the fact that − ⊗ H is a left adjoint. Indeed, by a standard argument, there is a natural bijection

\frac{K ⊗ H ⟶ L}{K ⟶ [[H, L]]}  (2.6)

in [𝒜_{fp} × 𝒜_{fp}, 𝒜], where

[[H, L]](X, A) = ∫_{Z:𝒜_{fp}} 𝒜 (A, H(X, Z)) ⋔ L(X, Z).

Recall the concept of an algebra for an endofunctor H as a pair (A, a) where a : HA ⟶ A is a morphism. Alg H is the category of algebras for H and homomorphisms (given by the obvious commutative squares). If H is finitary, then every object A of 𝒜 generates a free H-algebra given by the colimit of the ω-chain (W_{n}) with W_{0} = A and W_{n+1} = A + HW_{n}, see [2]. Analogously for parametrized endofunctors:

2.12. Proposition. The forgetful functor

U_{base} : Base(𝒜) ⟶ ParFin(𝒜)  (2.7)

has a left adjoint F_{base}. The free base □_{H} = F_{base}(H) on a parametrized endofunctor H is given by

X □_{H} A = free algebra on A for the endofunctor H(X, −).

Explicitly, X □_{H} A is a colimit of the following ω-chain:

\xymatrix{A \ar[r] & A + H(X, A) \ar[r] & A + H(X, A + H(X, A)) \ar[r] & ⋯}

Proof. For the purposes of the proof, it is more convenient to perceive □_{H} as a free monoid in ParFin(𝒜) with the monoidal structure ∘ of Notation 2.8.

The free monoid chain of [12, 13] translates to

W_{0} = I, W_{k+1} = I + H ∘ W_{k}

with the obvious connecting morphisms w_{k,k+1} : W_{k} ⟶ W_{k+1}. For fixed X and A, we therefore obtain

W_{0}(X, A) = I(X, A) = A,
W_{k+1}(X, A) = I(X, A) + (H ∘ W_{k})(X, A) = A + H(X, W_{k}(X, A)).

The colimit X □_{H} A of the above chain is obviously the free algebra on A for the functor H(X, −). The unit of the free algebra is u_{A}^{X} : X ⟶ X □_{H} A.

3. Monadicity of bases over parametrized signatures

Using [15] we prove in this section that bases are monadic over the category of parametrized signatures. Recall the concept of a signature in a locally finitely presentable category from the Introduction. The parametrized analogue is the following concept:

3.1. Definition. A parametrized signature Σ on 𝒜 is a collection

Σ = (Σ(i, p))_{i,p∈|𝒜_{fp}|}

of objects of 𝒜 indexed by pairs of finitely presentable objects.

3.2. Remark. In the case where 𝒜 = Set we can choose |Set_{fp}| as the set of natural numbers and consider the sets Σ(i, p) as consisting of operation symbols of arity i + p; for every σ ∈ Σ(i, p) the number i is called the iterativity of σ. This name stems from the fact that the first i arguments of operations specified by a signature Σ may be used in recursive specifications, which can be solved in iterative Σ-algebras (see [5, 6]). For the purposes of the present paper, “iterativity” is just a name.

3.3. Notation. A parametrized signature can be viewed as a functor Σ : |𝒜_{fp}|×|𝒜_{fp}| ⟶ 𝒜. We denote by

ParSig(𝒜) = [|𝒜_{fp}| × |𝒜_{fp}|, 𝒜]

the category of all parametrized signatures on 𝒜.

3.4. Remark. In the following remark and in the proof of Corollary 3.19 we will apply Paré’s “absolute coequalizer” version [20] of Beck’s monadicity theorem. According to this theorem a functor G : ℬ ⟶ 𝒞 is monadic if and only if (a) G has a left adjoint,

(b) G reflects isomorphisms, and (c) ℬ has coequalizers of those reflexive pairs whose image under G has an absolute coequalizer, and G preserves these coequalizers. Actually, in most of our applications ℬ will be cocomplete and G a left adjoint from which (c) clearly follows.

3.5. Remark. Denote by J : |𝒜_{fp}| ⟶ 𝒜_{fp} the inclusion functor. Composition with J × J : |𝒜_{fp}| × |𝒜_{fp}| ⟶ 𝒜_{fp} × 𝒜_{fp} yields a functor

U_{fun} : ParFin(𝒜) ⟶ ParSig(𝒜), H ⟼ ((i, p) ⟼ H(i, p))  (3.1)

that has both left and right adjoints, given by left and right Kan extensions along J × J. Moreover, since J × J is identity on objects, U_{fun} reflects isomorphisms. Since ParFin(𝒜) is cocomplete we conclude from Remark 3.4 that U_{fun} is monadic.

The left adjoint

F_{fun} : ParSig(𝒜) ⟶ ParFin(𝒜)  (3.2)

of U_{fun} is given by left Kan extension along J × J. To every parametrized signature Σ it assigns the corresponding polynomial parametrized endofunctor:

F_{fun}(Σ) = H_{Σ}(X, A) = ∐_{i,p∈|𝒜_{fp}|} (𝒜 (i, X) × 𝒜 (p, A)) • Σ(i, p)  (3.3)

On morphisms F_{fun} is defined analogously.

3.6. Notation. We denote by

U : Base(𝒜) ⟶ ParSig(𝒜)

the forgetful functor assigning to a base □ the parametrized signature Σ given by

Σ(i, p) = i □ p for all i, p finitely presentable.

That is, identifying bases with monoids in [𝒜_{fp}×𝒜_{fp}, 𝒜], the functor U is the composite of the functors U_{base} of (2.7) and U_{fun} of (3.1). And thus U has a left adjoint that we denote by F : ParSig(𝒜) ⟶ Base(𝒜). Summing up, we have the following picture of adjoint situations:

[figure: Base(𝒜); U_{base}; ⊥; F; ParFin(𝒜); F_{base}; U_{fun}; ⊥; ParSig(𝒜); F_{fun}; U]  (3.4)

3.7. Theorem. The functor U : Base(𝒜) ⟶ ParSig(𝒜) is monadic, i.e., bases are monadic over parametrized signatures.

Proof. The proof uses Theorem 2 of [15]. To verify its assumptions we use that

Base(𝒜) ≃ Mon([𝒜_{fp} × 𝒜_{fp}, 𝒜]), ParSig(𝒜) = [|𝒜_{fp}| × |𝒜_{fp}|, 𝒜],

and that the following conditions hold:

(1) The monoidal structure on [𝒜_{fp} × 𝒜_{fp}, 𝒜] is closed on the right. This is precisely what (2.6) says.

(2) The functor U_{base} : Mon([𝒜_{fp} × 𝒜_{fp}, 𝒜]) ⟶ [𝒜_{fp} × 𝒜_{fp}, 𝒜] has a left adjoint and the functor U_{fun} : [𝒜_{fp} × 𝒜_{fp}, 𝒜] ⟶ [|𝒜_{fp}| × |𝒜_{fp}|, 𝒜] is monadic. The former is given by Proposition 2.12 and the latter was shown in Remark 3.5.

(3) There is a functor ♢ : [𝒜_{fp} × 𝒜_{fp}, 𝒜] × [|𝒜_{fp}| × |𝒜_{fp}|, 𝒜] ⟶ [|𝒜_{fp}| × |𝒜_{fp}|, 𝒜] such that the square

[figure: [𝒜_{fp} × 𝒜_{fp}, 𝒜] × [𝒜_{fp} × 𝒜_{fp}, 𝒜]; ⊗; Id×U_{fun}; [𝒜_{fp} × 𝒜_{fp}, 𝒜]; U_{fun}; [𝒜_{fp} × 𝒜_{fp}, 𝒜] × [|𝒜_{fp}| × |𝒜_{fp}|, 𝒜]; ♢; [𝒜_{fp} × 𝒜_{fp}, 𝒜]]

commutes up to an isomorphism. Indeed, it suffices to define the parametrized signature H♢Σ by putting

(H♢Σ)(i, p) = H(i, Σ(i, p)).

3.8. Example. ([5]) We present free bases on the parametrized signature Σ that has just one binary operation, but of various iterativities.

(1) In the case of iterativity 2, i.e., Σ(2, 0) = 1 and Σ(i, p) = 0 else, the corresponding parametrized endofunctor H = F_{fun}(Σ) of Set is given by

H(X, A) = X × X

and the free base □_{Σ} = F_{base}(H) is, as shown in [5], given by

X □_{Σ} A = HX + A = X × X + A.

(2) In the case of iterativity 1, i.e., Σ(1, 1) = 1 and Σ(i, p) = 0 else, the corresponding parametrized endofunctor H = F_{fun}(Σ) is given by

H(X, A) = X × A

and the free base □_{Σ} is

X □_{Σ} A = X^{∗} × A

where X^{∗} denotes the free monoid on X.

(3) In the case of iterativity 0, i.e., Σ(0, 2) = 1 and Σ(i, p) = 0 else, we have H = F_{fun}(Σ)

given by

H(X, A) = A × A

and the free base □_{Σ} assigns to (X, A) a free binary algebra on A.

3.9. Remark.

(1) By Theorem 3.7, every base □ can be expressed as a coequalizer of the form

\xymatrix{□_{Γ} \ar[r] \ar[r] & □_{Σ} \ar[r] & □}

where □_{Γ} and □_{Σ} are bases, free on parametrized signatures Γ and Σ. We will use this coequalizer in giving an equational description of algebras for a base in Section 5.

(2) Every parametrized signature Σ defines derived signatures (non-parametrized, see Definition 1.1) depending on a choice X of an object of 𝒜: we define Σ^{(X)} to have as p-ary symbols those given by the copowers of Σ(i, p) indexed by all morphisms from i to X. Here i ranges through 𝒜_{fp}. Shortly:

Σ^{(X)}(p) = ∐_{i∈|𝒜_{fp}|} 𝒜 (i, X) • Σ(i, p) for all p ∈ |𝒜_{fp}|.  (3.5)

3.10. Proposition. The base □_{Σ}, free on a parametrized signature Σ, is given by

X □_{Σ} A = free Σ^{(X)}-algebra on A.

Proof. By Proposition 2.12, u_{A}^{X} : A ⟶ X □_{Σ}A is a free algebra on A for the endofunctor F_{fun}(Σ)(X, −) = H_{Σ}(X, −), see (3.3). Because we have the isomorphisms

H_{Σ}(X, −) = ∐_{i,p∈|𝒜_{fp}|} (𝒜 (i, X) × 𝒜 (p, −)) • Σ(i, p)
≅ ∐_{p∈|𝒜_{fp}|} 𝒜 (p, −) • ( ∐_{i∈|𝒜_{fp}|} 𝒜 (i, X) • Σ(i, p))
= ∐_{p∈|𝒜_{fp}|} 𝒜 (p, −) • Σ^{(X)}(p),

the functor H_{Σ}(X, −) is the ordinary polynomial functor H_{Σ^{(X)}} : 𝒜 ⟶ 𝒜 for the ordinary derived finitary signature (3.5). Thus, u_{A}^{X} : X ⟶ X □_{Σ} A exhibits X □_{Σ} A as a free Σ^{(X)}-algebra on A.

3.11. Example. Let 𝒜 = Set. The base □_{Σ} = F (Σ), free on a parametrized signature Σ, can be described by using the following (ordinary) signatures

Σ^{(i)}, i ∈ ℕ.

The p-ary operation symbols of Σ^{(i)} have the form

σ(x_{0}, …, x_{j−1}, −, …, −)

where, for any j ∈ ℕ, we choose σ in Σ(j, p) and we also choose a j-tuple (x_{0}, …, x_{j−1}) in i = {0, …, i − 1}.

We then have

i □_{Σ} p = all terms of Σ^{(i)} in p variables.

3.12. Notation. For every signature Σ (in the sense of Definition 1.1) we denote by Σ^{∗} the signature given by the free monad on Σ. Thus (−)^{∗} is the monad of the adjunction F′ ⊣ U′ : Mnd_{f} (𝒜) ⟶ Sig(𝒜) described in the Introduction.

3.13. Notation. The monad Σ ⟼ Σ^{∗} has the following parametrized version:

Σ^{@} = UF (Σ), the parametrized signature given by the free base on Σ

for the adjunction F ⊣ U : Base(𝒜) ⟶ ParSig(𝒜).

3.14. Example. Let Σ be a parametrized signature on Set. Then Σ^{@}(i, p) = (Σ^{(i)})^{∗} (p) is the set of all terms of the signature Σ^{(i)} of Example 3.11 in p variables.

3.15. Remark. The above formation i ⟼ Σ^{(i)} of signatures from a parametrized signature Σ extends to morphisms u : i ⟶ i′ of 𝒜_{fp} in the expected way: Σ^{(u)} : Σ^{(i)} ⟶ Σ^{(i′)} is given by components

Σ^{(u)}(p) = ∐_{j∈|𝒜_{fp}|} 𝒜 (j, u) • Σ(j, p), p in 𝒜_{fp}.

Thus every parametrized signature Σ defines a functor into the category of signatures of Definition 1.1:

Σ^{(−)} : 𝒜_{fp} ⟶ Sig(𝒜)

Such a functor is an example of an indexed signature that we define next. Observe that Σ^{@} in its curried form |𝒜_{fp}| ⟶ Sig(𝒜) is just the restriction (along J : |𝒜_{fp}| ⟶ 𝒜_{fp}) of the indexed signature (Σ^{(−)})^{∗}.

3.16. Definition. An indexed signature is a functor from 𝒜_{fp} to Sig(𝒜). The category of indexed signatures is thus the functor category

IdxSig(𝒜) = [𝒜_{fp}, Sig(𝒜)].

3.17. Example. Conversely, every indexed signature D : 𝒜_{fp} ⟶ Sig(𝒜) defines canonically a parametrized one, called U_{sig}(D): its symbols of iterativity i and parametricity p are precisely the p-ary symbols of D(i):

U_{sig}(D)(i, p) = D(i)(p)

This gives us a forgetful functor

U_{sig} : IdxSig(𝒜) ⟶ ParSig(𝒜)

Its left adjoint F_{sig} is defined by

F_{sig}(Σ) = Σ^{(−)}.

3.18. Remark. Every parametrized endofunctor

H : 𝒜_{fp} ⟶ [𝒜_{fp}, 𝒜]

defines an indexed signature i ⟼ H(i) · J. This defines a forgetful functor

U′_{fun} : ParFin(𝒜) ⟶ IdxSig(𝒜).

It has a left adjoint

F′_{fun} : IdxSig(𝒜) ⟶ ParFin(𝒜)

assigning to every indexed signature D : 𝒜_{fp} ⟶ [|𝒜_{fp}|, 𝒜] the parametrized endofunctor obtained by left Kan extension of uncurry(D) : 𝒜_{fp} × |𝒜_{fp}| ⟶ 𝒜 along id × J : 𝒜_{fp} × |𝒜_{fp}| ⟶ 𝒜_{fp} × 𝒜_{fp}.

3.19. Corollary. The monadic forgetful functor U : Base(𝒜) ⟶ ParSig(𝒜) has the following decomposition into three monadic functors

\xymatrix{Base(𝒜) \ar[r]^{U} \ar[d]_{U_{base}} & ParSig(𝒜) \\ ParFin(𝒜) \ar[r]_{U′_{fun}} \ar@{.>}[ur]^{U_{fun}} & IdxSig(𝒜) \ar[u]_{U_{sig}}}

where we have

U_{fun} = U_{sig} · U′_{fun}

(cf. (3.4)), and the corresponding left adjoint is

F_{fun} = F′_{fun} · F_{sig}.

Proof. That U = U_{base} · U′_{fun} · U_{sig} follows from the definition of U_{sig}, U′_{fun} and U_{base}. All three functors have left adjoints. The left adjoints of U_{sig} and U′_{fun} are given by left Kan extension along J × id : |𝒜_{fp}| × 𝒜_{fp} ⟶ |𝒜_{fp}| × 𝒜_{fp} and id × J : 𝒜_{fp} × |𝒜_{fp}| ⟶ 𝒜_{fp} × 𝒜_{fp}, respectively. The functors U_{sig} and U′_{fun} also have right adjoints given by right Kan extension. Since both J × id and id × J are bijective on objects, both U_{sig} and U′_{fun} reflect isomorphisms. It follows that both functors are monadic using Remark 3.4. The functor U_{base} has a left-adjoint by Proposition 2.12, and U_{base} reflects isomorphisms since U does. Finally, condition (c) from Remark 3.4 for U_{base} follows since the monadic functor U satisfies condition (c). Indeed, if c is a reflexive coequalizer that is mapped by U_{base} to an absolute coequalizer in ParFin(𝒜), then c is mapped by U_{fun} to an absolute coequalizer in ParSig(𝒜). Since U preserves the reflexive coequalizer c, so does U_{base}.

4. Algebras for a base and the calculus of bases

Every base, similarly to a monad, gives rise to the category of its algebras. These are defined as follows:

4.1. Definition. (See [5].) An algebra (A, a) for a base □ is given by its underlying object A and its structure map a : A □ A ⟶ A that makes it an Eilenberg-Moore algebra for the monad A □ −, i.e., the following two diagrams commute:

[figure: A; u_{A}^{A}; A □ A; a; A; A □ (A □ A); A□a; m_{A}^{A}; A □ A; a; A □ A; a; A]

A homomorphism from a base algebra (A, a) to a base algebra (B, b) is a morphism

A PRESENTATION OF BASES FOR PARAMETRIZED ITERATIVITY  697

f : A ⟶ B in 𝒜 making the following square commutative:

\xymatrix{A □ A \ar[r]^{f□f} \ar[d]_{a} & B □ B \ar[d]^{b} \\ A \ar[r]_{f} & B}

4.2. Notation.

1. We denote the category of all algebras for □ by Alg □ .

2. Analogously, given a parametrized endofunctor H, by an H-algebra we mean an

object A together with a structure map a : H(A, A) ⟶ A. We denote by

Alg H the category of H-algebras and homomorphisms (defined by an obvious square).

4.3. Example.

(1) A base algebra for X □ A = X + A is precisely an algebra with one unary operation: the algebra structure is given by an endomorphism of A.

(2) A base algebra for X □ A = X^{∗} × A is an algebra with one binary operation: given α : A×A ⟶ A, we obtain the corresponding base-algebra structure \overline{α} : A^{∗}×A ⟶ A by \overline{α}(a_{1} … a_{n}, a) = α(a_{1}, α(a_{2}, …, α(a_{n}, a)). And every base-algebra structure has the form \overline{α} for a unique α.

(3) Base algebras for X □ A = HX + A are precisely the algebras for the endofunctor H. That is, an algebra structure is given by a morphism α : HA ⟶ A. Thus, for example, the bases X^{∗} × A and X × X + A have the same algebras. Observe that the algebras for a base □ are not the actions of the corresponding monoid

□. Thus we cannot employ the closed structure of (2.6) to deal with the bijection

\frac{□ ⊗ H ⟶ H}{□ ⟶ [[H, H]]}

of monoid actions and monoid homomorphisms. Instead, we modify the notions of [13] to obtain bijections

\frac{H(B, B) ⟶ C}{H ⟶ ⟨⟨B, C⟩⟩}

where H is a parametrized endofunctor. We achieve the bijection in two stages: the first stage uses the bijection

\frac{H(B)(B) ⟶ C}{H(B) ⟶ ⟨B, C⟩}

where ⟨B, C⟩ is the construction from [12, 13], which we recall in Definition 4.4 below. Notice that above we wrote the parametrized functor in its curried form, hence H(B) is the finitary functor X ⟼ H(B, X). Finally, we use the ideas of right Kan extensions to achieve the bijection

\frac{H(B) ⟶ ⟨B, C⟩}{H ⟶ ⟨⟨B, C⟩⟩}

4.4. Definition. [See [13]]

(a) For objects B and C of 𝒜 we denote by

⟨B, C⟩ : 𝒜_{fp} ⟶ 𝒜 (pronounced “brackets B, C”)

the functor given pointwise by the formula

⟨B, C⟩(X) = 𝒜 (X, B) ⋔ C, X in 𝒜_{fp},  (4.1)

defined in the expected manner on morphisms. This assignment is contravariant in B and covariant in C: that is, we obtain a functor

⟨−, −⟩ : 𝒜^{op} × 𝒜 ⟶ [𝒜_{fp}, 𝒜]

defined on objects as expected: for f : B′ ⟶ B and g : C ⟶ C′, we define

⟨f, g⟩ : ⟨B, C⟩ ⟶ ⟨B′, C′⟩

to be the natural transformation with the X-component

⟨f, g⟩X = 𝒜 (X, f) ⋔ g.

(b) For a morphism f : B ⟶ C of 𝒜 we denote by

{f, f} : 𝒜_{fp} ⟶ 𝒜 (pronounced “braces f, f”)

the following pullback:

\xymatrix{\{f, f\} \ar[r]^{p_{B}} \ar[d]_{p_{C}} & ⟨B, B⟩ \ar[d]^{⟨B,f⟩} \\ ⟨C, C⟩ \ar[r]_{⟨f,C⟩} & ⟨B, C⟩}

in the category [𝒜_{fp}, 𝒜].

4.5. Remark. Technically speaking, to obtain ⟨B, C⟩ one first computes the right Kan extension Ran_{B} C : 𝒜 ⟶ 𝒜 of C : 1 ⟶ 𝒜 along B : 1 ⟶ 𝒜 and then restricts the result along the full embedding E : 𝒜_{fp} ⟶ 𝒜:

⟨B, C⟩ = Ran_{B} C · E.

The corresponding finitary endofunctor on 𝒜 is then given by forming the left Kan extension of ⟨B, C⟩ along E. Note that this is different from Ran_{B} C. Further note that Ran_{B} C(X) = 𝒜 (B, C) ⋔ X holds for all objects X, while Equation (4.1) holds only for finitely presentable objects X.

The following facts are verified using easy modifications of considerations in the proof of [12, Proposition 22.4] (see also [13] or [14, Theorem 3.2]).

4.6. Observation.

1. For every object B of 𝒜, the functor ⟨B, B⟩ is a finitary monad on 𝒜.

To see this, recall first that for every endofunctor H : 𝒜 ⟶ 𝒜 there is a bijection

[𝒜 , 𝒜](H, Ran_{B} C) ≅ 𝒜 (HB, C).

Therefore, if H is finitary we thus obtain

[𝒜_{fp}, 𝒜](H · E, ⟨B, C⟩) ≅ [𝒜 , 𝒜](H, Ran_{B} C) ≅ 𝒜 (HB, C),  (4.2)

where the first bijection is by the adjunction Lan_{E} ⊣ (−) · E and using that H ≅ Lan_{E}(H · E).

Thus, we have an adjunction ev_{B} ⊣ ⟨B, −⟩, where ev_{B} sends H : 𝒜_{fp} ⟶ 𝒜 to HB. By abstracting B, ev yields a monoidal action

ev : [𝒜_{fp}, 𝒜] × 𝒜 ⟶ 𝒜 ,

and from this one sees that, for every object B of 𝒜, ⟨B, B⟩ is a monoid in [𝒜_{fp}, 𝒜] (equivalently, a finitary monad on 𝒜) by general principles of monoidal actions.

2. Given an object B of 𝒜 and a finitary monad T, the above bijection (4.2) restricts to a bijection between monad morphisms b : T ⟶ ⟨B, B⟩ and Eilenberg-Moore algebras b^{♯} : T B ⟶ B.

4.7. Remark. By using an analogous argument as in Observation 4.6 one can show that for every morphism f : B ⟶ C of 𝒜 the functor {f, f} is a finitary monad on 𝒜. Moreover, given a finitary monad T there is a bijection between

(a) monad morphisms m : T ⟶ {f, f}, and

(b) homomorphisms of T -algebras carried by f between (p_{B}m)^{♯} : T B ⟶ B and (p_{C}m)^{♯} : T C ⟶ C.

This bijection is natural in T and B, C in 𝒜.

4.8. Definition. For objects B and C of 𝒜, define the parametrized endofunctor

⟨⟨B, C⟩⟩ : 𝒜_{fp} ⟶ [𝒜_{fp}, 𝒜] (pronounced “double brackets B, C”)

by

⟨⟨B, C⟩⟩ : X ⟼ 𝒜 (X, B) ⋔ ⟨B, C⟩, X in 𝒜_{fp},  (4.3)

where the power is taken in the (complete) category [𝒜_{fp}, 𝒜]. Its action on morphisms is as expected.

For arrows f : B′ ⟶ B and g : C ⟶ C′, define

⟨⟨f, g⟩⟩ : ⟨⟨B, C⟩⟩ ⟶ ⟨⟨B′, C′⟩⟩

to be the natural transformation with the X-component

⟨⟨f, g⟩⟩X = 𝒜 (X, f) ⋔ ⟨f, g⟩.

4.9. Remark. Let H : 𝒜 ⟶ Fin[𝒜 , 𝒜] be a parametrized endofunctor. Then there is a bijection between natural transformations from H to ⟨⟨B, C⟩⟩ and morphisms from H(B, B) to C, natural in B, C in 𝒜. In fact, the parametrized endofunctor ⟨⟨B, C⟩⟩ is, technically, a right Kan extension of ⟨B, C⟩ : 1 ⟶ Fin[𝒜 , 𝒜] along B : 1 ⟶ 𝒜 restricted to finitely presentable objects. Using this definition of ⟨⟨B, C⟩⟩, a similar argument as in Observation 4.6.1 establishes the bijections

ParFin(𝒜)(H, ⟨⟨B, C⟩⟩) ≅ Fin[𝒜 , 𝒜](HB, ⟨B, C⟩) ≅ 𝒜 (H(B, B), C).  (4.4)

We again use the uncurried form of ⟨⟨B, C⟩⟩ as a functor from 𝒜 × 𝒜 to 𝒜 (noting that this is different from Ran_{B}⟨B, C⟩). For finitely presentable objects X and A, the value of ⟨⟨B, C⟩⟩ can be computed as follows:

\begin{aligned}⟨⟨B, C⟩⟩(X, A) & = & (𝒜 (X, B) ⋔ ⟨B, C⟩)(A) \\ & = & 𝒜 (X, B) ⋔ (𝒜 (A, B) ⋔ C) \\ & ≅ & (𝒜 (X, B) × 𝒜 (A, B)) ⋔ C \\ & ≅ & 𝒜 (X + A, B) ⋔ C. \end{aligned}  (4.5)

4.10. Observation. The functor ⟨⟨B, B⟩⟩ is a base for every object B of 𝒜. In fact, objectwise we have ⟨⟨B, B⟩⟩X = 𝒜 (X, B) ⋔ ⟨B, B⟩, thus, ⟨⟨B, B⟩⟩ : 𝒜_{fp} ⟶ Mnd_{f} (𝒜) assigns to X the power of the monad ⟨B, B⟩ with exponent 𝒜 (X, B). Analogously for morphisms h : X ⟶ X′ we have that

⟨⟨B, B⟩⟩(h) = 𝒜 (h, B) ⋔ ⟨B, B⟩ : 𝒜 (X, B) ⋔ ⟨B, B⟩ ⟶ 𝒜 (X′, B) ⋔ ⟨B, B⟩

is a monad morphism, since it is a power of the identity monad morphism on ⟨B, B⟩.

4.11. Proposition. The bijection (4.4) restricts to a natural bijection between base morphisms τ : □ ⟶ ⟨⟨B, B⟩⟩ and base algebras τ^{♯} : B □ B ⟶ B, natural in B in 𝒜 and □ in Base(𝒜).

Proof. A base morphism τ : □ ⟶ ⟨⟨B, B⟩⟩ is a collection

τ_{X} : X □ (−) ⟶ ⟨⟨B, B⟩⟩(X)

of monad morphisms that is natural in X in 𝒜. It is not difficult to prove that the bijection (4.4) sends the collection (τ_{X}) to a single monad morphism

τ_{B} : B □ (−) ⟶ ⟨B, B⟩

which, by virtue of Remark 4.5, corresponds to an Eilenberg-Moore algebra

B □ B ⟶ B

for the monad B □ (−).

4.12. Definition. For every morphism f : B ⟶ C in 𝒜 we define the parametrized endofunctor

{{f, f}} : 𝒜_{fp} ⟶ [𝒜_{fp}, 𝒜] (pronounced “double braces f, f”)

by the pullback

\xymatrix{\{\{f, f\}\} \ar[r]^{p_{B}} \ar[d]_{p_{C}} & ⟨⟨B, B⟩⟩ \ar[d]^{⟨⟨B,f⟩⟩} \\ ⟨⟨C, C⟩⟩ \ar[r]_{⟨⟨f,C⟩⟩} & ⟨⟨B, C⟩⟩}  (4.6)

in the category ParFin(𝒜) of parametrized endofunctors of 𝒜.

4.13. Proposition. The functor {{f, f}} is a base for every morphism f : B ⟶ C

Proof. We show first that each {{f, f}}X is a finitary monad. It is easier to prove that this defines a finitary Kleisli triple (recall that notion from Remark 2.2).

Observe that the pullback defining {{f, f}} is formed pointwise. To define the unit

u_{A}^{X} : A ⟶ {{f, f}}(X, A)

use the universal property of pullbacks on the commutative square

\xymatrix{A \ar[r]^{α} \ar[d]_{β} & ⟨⟨B, B⟩⟩(X, A) \ar[d]^{⟨⟨B,f⟩⟩(X,A)} \\ ⟨⟨C, C⟩⟩(X, A) \ar[r]_{⟨⟨f,C⟩⟩(X,A)} & ⟨⟨B, C⟩⟩(X, A)}  (4.7)

where α : A ⟶ ⟨⟨B, B⟩⟩(X, A) is determined by the unit η_{A}^{B} : A ⟶ ⟨B, B⟩A of the monad ⟨B, B⟩ as follows:

\xymatrix{A \ar[r]^{α} \ar[dr]_{η_{A}^{B}} & ⟨⟨B, B⟩⟩(X, A) = 𝒜 (X, B) ⋔ ⟨B, B⟩A \ar[d]^{π_{h}} \\  & ⟨B, B⟩A}  (4.8)

and similarly for β

\xymatrix{A \ar[r]^{β} \ar[dr]_{η_{A}^{C}} & ⟨⟨C, C⟩⟩(X, A) = 𝒜 (X, C) ⋔ ⟨C, C⟩A \ar[d]^{π_{k}} \\  & ⟨C, C⟩A}  (4.9)

That the square (4.7) commutes follows from the fact that projections

π_{h} : 𝒜 (X, B) ⋔ ⟨B, C⟩A ⟶ ⟨B, C⟩A

are collectively monic and from the commutative diagram below:

[figure: (4.8); A; α; β; η_{A}^{C}; η_{A}^{B}; 𝒜 (X, B) ⋔ ⟨B, B⟩A; 𝒜 (X,B)⋔⟨B,f⟩A; π_{h}; ⟨B, B⟩A; ⟨B,f⟩A; (4.9); 𝒜 (X, C) ⋔ ⟨C, C⟩A; 𝒜 (X,f)⋔⟨f,C⟩A; π_{fh}; (∗); 𝒜 (X, B) ⋔ ⟨B, C⟩A; π_{h}; ⟨C, C⟩A; ⟨f,C⟩A; ⟨B, C⟩A]

(part (∗) commutes by the definition of 𝒜 (X, f) ⋔ ⟨f, C⟩A).

For every morphism

s : A ⟶ {{f, f}}(X, A′)

we define the extension

s̃: {{f, f}}(X, A) ⟶ {{f, f}}(X, A′)

using the universal property of pullbacks as follows:

Firstly, s : A ⟶ {{f, f}}(X, A′) determines s_{B} = p_{B} · s : A ⟶ ⟨⟨B, B⟩⟩(X, A′) (see (4.6)), hence we have an extension

ŝ_{B} : ⟨⟨B, B⟩⟩(X, A) ⟶ ⟨⟨B, B⟩⟩(X, A′)

w.r.t. the monad ⟨⟨B, B⟩⟩(X, −). Similarly, one obtains

ŝ_{C} : ⟨⟨C, C⟩⟩(X, A) ⟶ ⟨⟨C, C⟩⟩(X, A′).

The outside of the following diagram below is easily seen to commute:

\xymatrix{\{\{f, f\}\}(X, A) \ar[rr]^{p_{B}(X,A)} \ar[dd]_{p_{C}(X,A)} \ar@{.>}[dr]^{s̃} &  & ⟨⟨B, B⟩⟩(X, A) \ar[d]^{ŝ_{B}} \\  & \{\{f, f\}\}(X, A′) \ar[r]^{p_{B}(X,A′)} \ar[d]_{p_{C}(X,A′)} & ⟨⟨B, B⟩⟩(X, A′) \ar[d]^{⟨⟨B,f⟩⟩(X,A′)} \\ ⟨⟨C, C⟩⟩(X, A) \ar[r]_{ŝ_{C}} & ⟨⟨C, C⟩⟩(X, A′) \ar[r]_{⟨⟨f,C⟩⟩(X,A′)} & ⟨⟨B, C⟩⟩(X, A′)}

Thus, we can define s̃ as the unique mediating morphism. The axioms for a finitary Kleisli triple are easily verified by using the universal property of the pullback (4.6).

4.14. Proposition. For every morphism f : B ⟶ C in 𝒜 and every base □ there is a natural bijection between

(a) base morphisms a : □ ⟶ {{f, f}} and

(b) homomorphisms of base algebras carried by f between (p_{B}a)^{♯} : B □ B ⟶ B and (p_{C}a)^{♯} : C □ C ⟶ C (cf. Observation 4.6).

Proof. (1) Let us write ⟨B, C⟩_{•} for Ran_{B} C, i.e. we have

⟨B, C⟩_{•}X = 𝒜 (X, B) ⋔ C for all X in 𝒜.

The functor ⟨⟨B, C⟩⟩ : 𝒜_{fp} ⟶ [𝒜_{fp}, 𝒜] is a finitary version of the functor

⟨⟨B, C⟩⟩_{•} : 𝒜 ⟶ [𝒜 , 𝒜]

given by the right Kan extension of Ran_{B} C : 1 ⟶ [𝒜 , 𝒜] along B : 1 ⟶ 𝒜, i.e. we have

⟨⟨B, C⟩⟩_{•}X = 𝒜 (X, B) ⋔ ⟨B, C⟩_{•} for all X in 𝒜.

Now observe that to every functor H : 𝒜_{fp} ⟶ [𝒜_{fp}, 𝒜] we can assign the composite with Lan_{E} : [𝒜_{fp}, 𝒜] ⟶ [𝒜 , 𝒜] and take the left Kan extension along E : 𝒜_{fp} ⟶ 𝒜 to obtain a functor

H_{⋆} = Lan_{E}(Lan_{E}(−) · H) : 𝒜 ⟶ [𝒜 , 𝒜].

This defines a functor (−)_{⋆} : [𝒜_{fp}, [𝒜_{fp}, 𝒜]] ⟶ [𝒜 , [𝒜 , 𝒜]], which has a right-adjoint assigning to K : 𝒜 ⟶ [𝒜 , 𝒜] the functor

K^{⋆} : 𝒜_{fp} ⟶ [𝒜_{fp}, 𝒜] with K^{⋆}X = KEX · E : 𝒜_{fp} ⟶ 𝒜 .

It is easy to verify that our functor ⟨⟨B, C⟩⟩ from Definition 4.8 is precisely (⟨⟨B, C⟩⟩_{•})^{⋆}. So the adjunction (−)_{⋆} ⊣ (−)^{⋆} gives us for every base □ the natural isomorphism below (where ⟨⟨B, C⟩⟩ is considered as a parametrized endofunctor on the left):

ParFin(𝒜)(□, ⟨⟨B, C⟩⟩) ≅ [𝒜_{fp}, [𝒜_{fp}, 𝒜]](□^{⋆}, (⟨⟨B, C⟩⟩_{•})^{⋆}) ≅ [𝒜 , [𝒜 , 𝒜]](□, ⟨⟨B, C⟩⟩_{•}),

where the second isomorphism uses that (□^{⋆})_{⋆} ≅ □ due to finitarity.

(2) Observe that when a base □ is specified, then to give a base morphism a : □ ⟶ {{f, f}} is to give a commutative square in ParFin(𝒜) with b and c are morphisms in Base(𝒜):

\xymatrix{□ \ar[r]^{b} \ar[d]_{c} & ⟨⟨B, B⟩⟩ \ar[d]^{⟨⟨B,f⟩⟩} \\ ⟨⟨C, C⟩⟩ \ar[r]_{⟨⟨f,C⟩⟩} & ⟨⟨B, C⟩⟩}

(Hence, p_{B}a = b and p_{C}a = c.) By using the adjunction in part (1) and the fact that □ is finitary this is equivalent to giving a commutative square in [𝒜 , [𝒜 , 𝒜]] where ⟨⟨−, −⟩⟩ replaced by ⟨⟨−, −⟩⟩_{•} everywhere. And this is equivalent to giving a commutative diagram as follows

[figure: B□B; f□f; b_{B,B}; c_{B,B}; b^{♯}; C□C; c_{C,C}; c^{♯}; 𝒜 (B,C)⋔⟨C,C⟩_{•}B; 𝒜 (f,C)⋔⟨C,C⟩_{•}f; 𝒜 (B,f)⋔⟨f,C⟩_{•}B; π_{f}; 𝒜 (C,C)⋔⟨C,C⟩_{•}C; π_{id}; 𝒜 (B,B)⋔⟨B,B⟩_{•}B; 𝒜 (B,B)⋔⟨B,f⟩_{•}B; π_{id}; 𝒜 (B,B)⋔⟨B,C⟩_{•}B; π_{id}; ⟨C,C⟩_{•}B; ⟨f,C⟩_{•}B; ⟨C,C⟩_{•}f; ⟨C,C⟩_{•}C; π_{id}; ⟨f,C⟩_{•}C; ⟨B,B⟩_{•}B; ⟨B,f⟩_{•}B; π_{id}; ⟨B,C⟩_{•}B; ⟨B,C⟩_{•}f; π_{id}; ⟨B,C⟩_{•}C; π_{f}; B; f; C]

All inner parts commute either by definition or by naturality.

4.15. Remark. Recalling from the Introduction the concept of Σ-algebras and homomorphisms for non-parametrized signatures, we use an analogous concept here. More precisely: let Σ be a parametrized signature and denote by \overline{Σ} the corresponding nonparametrized signature with

\overline{Σ}(m) = ∐ Σ(i, p),

where the coproduct ranges over all pairs i, p of objects of 𝒜_{fp} whose coproduct is m. Then \overline{Σ}-algebras are called, by abuse of notation, simply Σ-algebras (and the corresponding category is denoted by Alg Σ). Explicitly, a Σ-algebra consists of an object A and a morphism

a : ∐_{i,p∈|𝒜_{fp}|} 𝒜 (i + p, A) • Σ(i, p) ⟶ A.

4.16. Observation.

1. Σ-algebras can alternatively be described as morphisms Σ ⟶ U(⟨⟨A, A⟩⟩) of parametrized signatures:

ParSig(𝒜)(Σ, U(⟨⟨A, A⟩⟩)) ≅ ∏_{i,p∈|𝒜_{fp}|} 𝒜 (Σ(i, p), 𝒜 (i + p, A) ⋔ A) by (4.5)
≅ ∏_{i,p∈|𝒜_{fp}|} 𝒜 (𝒜 (i + p, A) • Σ(i, p), A) by (2.4)
≅ 𝒜 ( ∐_{i,p∈|𝒜_{fp}|} 𝒜 (i + p, A) • Σ(i, p), A)

2. Similarly, every homomorphism f : (A, a) ⟶ (B, b) of Σ-algebras can be identified with a morphism of parametrized signatures from Σ to U({{f, f}}). (Use the fact that U preserves the pullback defining {{f, f}} and then perform analogous considerations as in the proof of Proposition 4.13.)

3. The adjunction F ⊣ U : Base(𝒜) ⟶ ParSig(𝒜) yields the bijection

Base(𝒜)(□_{Σ}, ⟨⟨A, A⟩⟩) ≅ ParSig(𝒜)(Σ, U(⟨⟨A, A⟩⟩)).

This bijection allows us to identify Σ-algebras A with base morphisms □_{Σ} ⟶ ⟨⟨A, A⟩⟩.

4.17. Notation. Let □ be a base and Σ a parametrized signature. For a morphism f : Σ ⟶ U(□) we denote by

f̌: □_{Σ} ⟶ □  (4.10)

its transpose under the monadic adjunction F ⊣ U of Theorem 3.7. In particular, for a Σ-algebra (A, a) we obtain ǎ : □_{Σ} ⟶ ⟨⟨A, A⟩⟩ by the above bijection.

4.18. Proposition. The categories Alg Σ and Alg □_{Σ} are isomorphic.

Proof. The correspondence of a : Σ ⟶ U(⟨⟨A, A⟩⟩) and ǎ in (4.10) gives us the desired bijection on objects. To obtain the (functorial) bijection on hom-sets replace ⟨⟨A, A⟩⟩ by {{f, f}} and observe that, by Proposition 4.14, f is a homomorphism of Σ-algebras if and only if it is a homomorphism of base algebras for □_{Σ}.

5. Equations and equational presentations

Every algebra (X, a) for a monad (M, i, m) on a general category 𝒳 has a presentation in the form of a coequalizer

\xymatrix{(MMX, m_{MX}) \ar[r]^{Ma} \ar[r]_{m_{X}} & (MX, m_{X}) \ar[r]^{a} & (X, a)}  (5.1)

see, e.g. [17]. Apply this to the monad (M, i, m) on the category 𝒳 = [|Set_{fp}|, Set] of signatures that assigns to a signature Σ the signature Σ^{∗} given by the free monad F′(Σ) on the signature Σ (see Notation 3.12), i.e. we have

MΣ = Σ^{∗}.  (5.2)

The above coequalizer can be used to prove that algebras for a finitary monad on Set are precisely the algebras for a certain signature that satisfy certain equations, see [17, Theorem 1.5.40] or [16].

Indeed, the coequalizer (5.1) is but a special case of the most general situation

\xymatrix{F′(Γ) \ar[r]^{λ̌} \ar[r]_{ρ̌} & F′(Σ) \ar[r]^{γ} & T}  (5.3)

where Γ and Σ are signatures and λ̌, ρ̌ denote the adjoint transposes of signature morphisms λ, ρ : Γ ⟶ Σ^{∗}. The universal property of coequalizers, together with Observation 4.6, then establish the following bijections for the above monad T (where the last line is explained further below):

algebras T A ⟶ A for T

monad morphisms T ⟶ ⟨A, A⟩

monad morphisms F′(Σ) ⟶ ⟨A, A⟩ coequalizing λ̌, ρ̌

Let us now explain that the last line equivalently expresses that A is a Σ-algebra satisfying the set of equations given by λ and ρ. First, the adjoint transpose under F′ ⊣ U′ of a monad morphism F′(Σ) ⟶ ⟨A, A⟩ is a signature morphism Σ ⟶ U(⟨A, A⟩). And this signature morphism is in turn equivalent to a Σ-algebra structure on A (analogously as in Observation 4.16 for parametrized signatures). Second, to understand how a pair of signature morphisms λ, ρ : Γ ⟶ Σ^{∗} encodes equations, recall that an equation t = s in n variables for a classical signature Σ in Set is a pair of elements of a free Σ-algebra Φ_{Σ}n on n generators. Thus, a collection Γ of equations for Σ can be viewed as another signature, where Γn is the set Γ ∩ (Φ_{Σ}n)^{2} of all equations of Γ using n variables. Since for Σ^{∗} from (5.2) we have Σ^{∗}n = Φ_{Σ}n, the collection Γ of equations yields two signature morphisms ρ, λ : Γ ⟶ Σ^{∗} (assigning to t = s in Γn the terms t and s, respectively). It is now not difficult to prove that the Σ-algebra A satisfies the equations in Γ (in the usual sense of general algebra) iff the corresponding monad morphism F′(Σ) ⟶ ⟨A, A⟩ coequalizes λ̌ and ρ̌.

Here is the parametric variant of the above:

5.1. Definition.

(1) An equation λ = ρ for a parametrized signature Σ is a parallel pair of morphisms in ParSig(𝒜) with codomain Σ^{@}:

\xymatrix{Γ \ar[r]_{λ} \ar[r]^{ρ} & Σ^{@}.}

We call λ and ρ the left-hand and right-hand sides of λ = ρ, respectively.

(2) A Σ-algebra a : A □_{Σ} A ⟶ A satisfies the equation λ = ρ if ǎ : □_{Σ} ⟶ ⟨⟨A, A⟩⟩ coequalizes λ̌, ρ̌ (see Notation 4.17):

\xymatrix{□_{Γ} \ar[r]_{λ̌} \ar[r]^{ρ̌} & □_{Σ} \ar[r]^{ǎ} & ⟨⟨A, A⟩⟩.}

5.2. Examples. Here bases in Set are considered.

(1) Consider the free base

X □_{Σ} A = X × X + A

on the parametrized signature Σ of one binary operation of iterativity 2, see Example 3.8(1). Its algebras are the sets with a binary operation. The commutativity law of that operation is formalized as follows. Let Γ be the parametrized signature with Γ(i, p) = i × i for all i, p. Let λ, ρ : Γ ⟶ Σ^{@} be given by λ(x, y) = (x, y) and ρ(x, y) = (y, x). Then it is easy to see that a base algebra is commutative iff it satisfies λ = ρ.

In contrast, associativity is not an equation in the sense of Definition 5.1. We demonstrate this in Example 6.8.

(2) For the base

□_{Σ} = X^{∗} × A

of one binary operation of iterativity 1, see Example 3.8(2), commutativity is not an equation in the sense of Definition 5.1, see Example 6.13.

5.3. Notation. For every equation

\xymatrix{Γ \ar[r]_{λ} \ar[r]^{ρ} & Σ^{@}}

we denote by Alg (Σ, λ = ρ) the full subcategory of Alg Σ consisting of all Σ-algebras satisfying it.

5.4. Theorem. The category Alg (Σ, λ = ρ) is isomorphic to Alg □ for the base □ obtained as a coequalizer

\xymatrix{□_{Γ} \ar[r]_{λ̌} \ar[r]^{ρ̌} & □_{Σ} \ar[r]^{γ} & □}

in the category Base(𝒜).

708  JIŘÍ ADÁMEK, STEFAN MILIUS AND JIŘÍ VELEBIL

Proof. We define a functor

Φ : Alg □ ⟶ Alg (Σ, λ = ρ)

using composition with γ : □_{Σ} ⟶ □ as follows:

Consider the following diagram

\xymatrix{□_{Γ} \ar[r]_{λ̌} \ar[r]^{ρ̌} & □_{Σ} \ar[r]^{γ} \ar[dr] & □ \ar[d] \\  &  & ⟨⟨A, A⟩⟩}

in Base(𝒜) from which it immediately follows, due to Propositions 4.11 and 4.13, that we have natural bijections

base algebras A □ A ⟶ A base morphisms □ ⟶ ⟨⟨A, A⟩⟩ base morphisms □_{Σ} ⟶ ⟨⟨A, A⟩⟩ coequalizing λ̌, ρ̌ Σ-algebras satisfying λ = ρ

This defines Φ on objects.

To prove the (functorial) bijective correspondence for morphisms, take □-algebras (B, b) and (C, c) and a morphism f : B ⟶ C and consider the diagram

\xymatrix{□_{Γ} \ar[r]_{λ̌} \ar[r]^{ρ̌} & □_{Σ} \ar[r]^{γ} \ar[dr] & □ \ar[d] \\  &  & \{\{f, f\}\}}

from which it follows that we have by applying natural bijections f a homomorphism of □-algebras a base morphism □ ⟶ {{f, f}} a base morphism □_{Σ} ⟶ {{f, f}} coequalizing λ̌, ρ̌ f a homomorphism of Σ-algebras satisfying λ = ρ

Thus, we define that Φ is the identity on hom sets.

It is easy to verify that this is an isomorphism of categories.

We analyse in detail now what it means for an algebra A for a parametrized signature Σ to satisfy an equation

\xymatrix{Γ \ar[r]_{λ} \ar[r]^{ρ} & Σ^{@} = UF (Σ).}

By using the decomposition U = U_{sig} · U′_{fun} · U_{base} and F_{base} · F′_{fun} · F_{sig} of F ⊣ U of Corollary 3.19, the above pair corresponds uniquely to the pair

\xymatrix{F_{sig}(Γ) \ar[r]_{λ̂} \ar[r]^{ρ̂} & U′_{fun}U_{base}F (Σ)}

in IdxSig(𝒜), i.e., to the family of pairs

\xymatrix{Γ^{(i)} \ar[r]_{λ̂_{i}} \ar[r]^{ρ̂_{i}} & (Σ^{(i)})^{∗}}  (5.4)

of morphisms in Sig(𝒜) natural in i ranging over 𝒜_{fp}.

5.5. Definition. Given an equation λ = ρ the above pair (5.4) is called the i-th derived equation of λ = ρ.

5.6. Proposition. A diagram

\xymatrix{□_{Γ} \ar[r]_{λ̌} \ar[r]^{ρ̌} & □_{Σ} \ar[r]^{γ} & □}  (5.5)

is a coequaliser in Base(𝒜) iff every u_{p}^{i} : p ⟶ i □ p is a free Σ^{(i)}-algebra on p satisfying the i-th derived equation of λ = ρ.

Proof. The above diagram (5.5) is a coequaliser in Base(𝒜) iff the following diagram

\xymatrix{i □_{Γ} (−) \ar[r]_{λ̌(i,−)} \ar[r]^{ρ̌(i,−)} & i □_{Σ} (−) \ar[r]^{γ(i,−)} & i □ (−)}  (5.6)

is a coequaliser in Mnd_{f} (𝒜) for every i. By Proposition 3.10, i □_{Γ} (−) is the free monad F′(Γ^{(i)}) and i □_{Σ} (−) is the free monad F′(Σ^{(i)}). Hence the coequaliser (5.6) has the form

\xymatrix{F′(Γ^{(i)}) \ar[r]_{λ̌(i,−)} \ar[r]^{ρ̌(i,−)} & F′(Σ^{(i)}) \ar[r]^{γ(i,−)} & i □ (−)}  (5.7)

Thus, by the results of [13], i □ (−) is the monad of Σ^{(i)}-algebras satisfying the equation

\xymatrix{Γ^{(i)} \ar[r]_{(λ̌(i,−))^{♭}} \ar[r]^{(ρ̌(i,−))^{♭}} & U′F′(Σ^{(i)})}

in Sig(𝒜), where (−)^{♭} denotes the transpose under F′ ⊣ U′ : Mnd_{f} (𝒜) ⟶ Sig(𝒜). Since U′F′(Σ^{(i)}) = (Σ^{(i)})^{∗} by Notation 3.12, it remains to prove that

(λ̌(i, −))^{♭} = λ̂_{i} and (ρ̌(i, −))^{♭} = ρ̂_{i}.

But this follows from the fact that the composite U′_{fun} · U_{base} : Base(𝒜) ⟶ IdxSig(𝒜) is the functor [𝒜_{fp}, U′] : [𝒜_{fp}, Mnd_{f} (𝒜)] ⟶ [𝒜_{fp}, Sig(𝒜)] that postcomposes with U′ : Mnd_{f} (𝒜) ⟶ Sig(𝒜). This completes the proof.

5.7. Remark. The coequaliser in Base(𝒜) of Proposition 5.6 presents a base □ by “operations and equations”. Every base □ can be presented in this way. This follows from the presentation of □ by the coequalizer in (5.1):

\xymatrix{(Σ^{@@}, μ_{Σ^{@}}) \ar[r]_{μ_{Σ}} \ar[r]^{α^{@}} & (Σ^{@}, μ_{Σ}) \ar[r]^{α} & (Σ, α),}

where (Σ, α) is the (−)^{@}-algebra corresponding to □. The corresponding equation is then α^{@} · η_{Σ^{@}} = id, i.e, the following parallel pair in ParSig(𝒜):

\xymatrix{Σ^{@} \ar[r]_{id} \ar[r]^{α^{@}·η_{Σ^{@}}} & Σ^{@}.}

For the concrete examples presented in the next section we need the following view of base algebras as “natural” collections of Eilenberg-Moore algebras for the monads i □ (−) where i ranges over |𝒜_{fp}|:

5.8. Notation. Let a : A □ A ⟶ A be a base algebra. For every i ∈ |𝒜_{fp}| and every morphism h : i ⟶ A we denote by

A^{(h)}

the Eilenberg-Moore algebra for i □ (−) given by the morphism

a_{h} = (\xymatrix{i □ A \ar[r]^{h□A} & A □ A \ar[r]^{a} & A}).

5.9. Remark. Observe that for all m : i ⟶ j in 𝒜_{fp} the following triangle commutes:

\xymatrix{i □ A \ar[dr]^{a_{h·m}} \ar[d]_{m□A} \\ j □ A \ar[r]_{a_{h}} & A.}  (5.8)

5.10. Definition. Let □ be a base. By a natural family of algebras on a given object A of 𝒜 we mean a family of Eilenberg-Moore algebras

a_{h} : i □ A ⟶ A

indexed by all morphisms h : i ⟶ A with i ∈ |𝒜_{fp}| and such that the triangles (5.8) commute.

5.11. Lemma. There is a bijective correspondence between base algebras on A and natural families of Eilenberg-Moore algebras on A.

Proof. The passage from a base algebra to the natural family of Notation 5.8 has the following inverse: write A as the colimit of the canonical diagram of all morphisms h : i ⟶ A, i ∈ |𝒜_{fp}|. Since □ is finitary, A □ A is a filtered colimit of all objects of the form i □ A, i ∈ |𝒜_{fp}|, with colimit injections h □ A : i □ A ⟶ A □ A. The morphisms a_{h} : i □ A ⟶ A form a compatible cocone. Let a : A □ A ⟶ A be the unique morphism with

a · (h □ A) = a_{h}.

It is easy to verify that (1) a : A □ A ⟶ A is a base algebra and (2) by applying the construction in Notation 5.8 to it, we obtain the original natural family.

Now note that by the Lemma 5.11 to give Σ-algebra structure a : A □_{Σ} A ⟶ A is equivalent to giving a natural family of Σ^{(i)}-algebra structures on A, i.e. a natural family of Eilenberg-Moore algebra structures a_{h} : i □_{Σ} A ⟶ A indexed by h : i ⟶ A.

5.12. Corollary. A Σ-algebra A satisfies the equation λ = ρ iff for every morphism h : i ⟶ A, i ∈ |𝒜_{fp}|, the Σ^{(i)}-algebra (A^{(h)}) of Notation 5.8 satisfies the i-th derived equation of λ = ρ.

Proof. Indeed, consider the coequalizer in (5.5). A Σ-algebra A satisfying λ = ρ is equivalently a base algebra a : A □ A ⟶ A, which in turn is equivalent to giving the natural family of Eilenberg-Moore algebras a·(h□A) : i□A ⟶ A where h ranges over all morphisms h : i ⟶ A. And this means, equivalently, that the Σ^{(i)}-algebras A^{(h)} satisfy the i-th derived equation of λ = ρ.

6. Presentation of bases over Set

In this section we study in more detail a presentation of bases over Set by means of “operations and equations”. That is, we explicate Proposition 5.6 for the case 𝒜 = Set.

6.1. Definition. Let Σ be a parametrized signature over Set. A pair (l, r) of elements of Σ^{@}(i, p) (for i, p in ℕ) is called a Σ-equation; we denote it by l = r. The equation is called n-ary if n = i + p.

How does this relate to the equations λ, ρ : Γ ⟶ Σ^{@} of Definition 5.1? For any equation λ = ρ we can substitute the following set E of Σ-equations:

E = { l = r | l = λ(x) and r = ρ(x) for some i, p ∈ Set_{fp} and x ∈ Γ(i, p) }.  (6.1)

This is the idea behind the following concept of a Σ-algebra satisfying l = r. Recall that

Σ^{@}(i, p) = free Σ^{(i)}-algebra on p generators.

Recall also that

Σ^{(i)}p = ∐_{j} Set_{fp}(j, i) • Σ(j, p).

6.2. Remark.

1. Recall from Example 3.14 that Σ^{@}(i, p) = (Σ^{(i)})^{∗} (p). Thus, every Σ-equation l = r in Σ^{@}(i, p) is also an equation w.r.t. the ordinary signature Σ^{(i)}.

It is easy to see that a Σ-algebra A satisfies the Σ-equation l = r if and only if for each h : i ⟶ A, the Σ^{(i)}-algebra A^{(h)} of Notation 5.8 satisfies this equation (considered as a Σ^{(i)}-equation) in the ordinary sense of general algebra.

2. Given a morphism u : i ⟶ j in Set_{fp}, the signature morphism (Σ^{(u)})^{∗} : (Σ^{(i)})^{∗} ⟶ (Σ^{(j)})^{∗} obtained from Σ^{(u)} in Remark 3.15 has components that we denote by

(Σ^{(u)})^{∗} (p) : (Σ^{(i)})^{∗} (p) ⟶ (Σ^{(j)})^{∗}(p).

3. Let λ = ρ be an equation. Then for every i in Set_{fp} the i-th derived equation λ̂_{i}, ρ̂_{i} : Γ^{(i)} ⟶ (Σ^{(i)})^{∗} yields the following set

E_{i} = {λ̂_{i}(p)(x) = ρ̂_{i}(p)(x) | p ∈ Set_{fp}, x ∈ Γ^{(i)}(p)}

of Σ^{(i)}-equations. Note that λ̂_{i} : Γ^{(i)} ⟶ (Σ^{(i)})^{∗} = Σ^{@}(i, −) acts as follows: we have Γ^{(i)}p = ∐_{j} Set_{fp}(j, i) • Γ(j, p), and the p-component of λ̂_{i} is the unique morphism induced by the family of all

\xymatrix{Γ(j, p) \ar[r]^{λ_{j,p}} & (Σ^{(j)})^{∗} (p) \ar[r]^{(Σ^{(u)})^{∗}(p)} & (Σ^{(i)})^{∗} (p)},

indexed by all maps u : j ⟶ i. The natural transformation ρ̂_{i} is obtained similarly from ρ.

4. It follows that for the set E of Σ-equations of (6.1) we have E ⊆ ⋃ E_{i}. Indeed, for u = id : i ⟶ i, λ̂_{i}(p) is equal to λ_{i,p}.

6.3. Remark. Let A be a Σ-algebra. We have seen in Notation 5.8 that every i-tuple h : i ⟶ A induces the Σ^{(i)}-algebra A^{(h)}. Explicitly, for 𝒜 = Set, any operation symbol σ(x_{0}, …, x_{i−1}, −, …, −) with σ ∈ Σ(i, p) defines the p-ary operation

σ_{A^{(h)}}(h(x_{0}), …, h(x_{i−1}), −, …, −) : A^{p} ⟶ A.

6.4. Notation. Let A be a Σ-algebra. Given an element s ∈ Σ^{@}(i, p) and an i-tuple h : i ⟶ A, we denote by

h^{♯}(s) : A^{p} ⟶ A

the p-ary polynomial of the Σ^{(i)}-algebra A^{(h)} induced by the Σ^{(i)}-term s. Explicitly, h^{♯}(s) sends a p-tuple k : p ⟶ A to the unique Σ^{(i)}-homomorphism k̂ from Σ^{@}(i, p) to A^{(h)} extending k, evaluated at s. (Recall that Σ^{@}(i, p) is the free Σ^{(i)}-algebra on p by Proposition 3.10.)

6.5. Definition. A Σ-algebra A satisfies a Σ-equation l = r in Σ^{@}(i, p) provided that

h^{♯}(l) = h^{♯}(r) for every i-tuple h : i ⟶ A.

Recall from Remark 6.2.1 that Σ^{@}(i, p) = (Σ^{(i)})^{∗} (p);

6.6. Lemma. If a Σ-algebra satisfies a Σ-equation l = r in Σ^{@}(i, p), then for every function u : i ⟶ i′ it also satisfies l^{(u)} = r^{(u)} in Σ^{@}(i′, p), where l^{(u)} = (Σ^{(u)})^{∗} (p)(l) and r^{(u)} = (Σ^{(u)})^{∗} (p)(r).

Proof. Given a Σ-algebra A satisfying l = r and a function h : i′ ⟶ A, it is our task to prove

h^{♯}(l^{(u)}) = h^{♯}(r^{(u)})

in the Σ^{(i′)}-algebra A^{(h)}. That is, given a p-tuple k : p ⟶ A and the Σ^{(i′)}-homomorphism k̂ : Σ^{@}(i′, p) ⟶ A^{(h)}, we are to prove that

k̂(l^{(u)}) = k̂(r^{(u)}).

Consider the Σ^{(i)}-algebra A^{(h·u)} given by the composite h · u : i ⟶ A, and let k̃ : Σ^{@}(i, p) ⟶ A^{(h·u)} be the Σ^{(i)}-homomorphism extending k above. We know that k̃(l) = k̃(r). Thus, the desired equality follows from the following ones:

k̂(t^{(u)}) = k̃(t) for all t in Σ^{@}(i, p),

which we now prove by induction on the complexity of the term t.

If t is one of the p variables, then k̃(t) = k(t) and, since t^{(u)} = t, also k̂(t^{(u)}) = k(t). In the induction step we assume that t is, for some q-ary operation symbol of Σ^{(i)},

given by a q-tuple t_{0}, …, t_{q−1} of terms for which the desired equality holds:

k̂(t_{0}^{(u)}) = k̃(t_{0}), …, k̂(t_{q−1}^{(u)}) = k̃(t_{q−1}).

An operation symbol in Σ^{(i)} has the form σ(x_{0}, …, x_{j−1}, −, …, −) for some σ in Σ(j, q) and some j-tuple (x_{0}, …, x_{j−1}) in i. Thus we perform the induction step on the term

t = σ(x_{0}, …, x_{j−1}, t_{0}, …, t_{q−1}).

The left-hand side of the desired equation works with t^{(u)} which is the term

t^{(u)} = σ(u(x_{0}), …, u(x_{j−1}), t_{0}^{(u)}, …, t_{q−1}^{(u)}).

(We leave the straightforward induction verifying this to the reader.) Since k̂ is a Σ^{(i′)}-homomorphism and the operation σ(u(x_{0}), …, u(x_{j−1}), −, …, −) is interpreted as σ(hu(x_{0}), …, hu(x_{j−1}), −, …, −) in A^{(h)}, we get

k̂(t^{(u)}) = σ(hu(x_{0}), …, hu(x_{j−1}), k̂(t_{0}^{(u)}), …, k̂(t_{q−1}^{(u)}))
= σ(hu(x_{0}), …, hu(x_{j−1}), k̃(t_{0}), …, k̃(t_{q−1})).x

Since k̃ is a Σ^{(i)}-homomorphism and the operation σ(x_{0}, …, x_{j−1}, −, …, −) is interpreted as

σ(hu(x_{0}), …, hu(x_{j−1}), −, …, −)

in A^{(h·u)}, we have

k̃(t) = σ(hu(x_{0}), …, hu(x_{j−1}), k̃(t_{0}), …, k̃(t_{q−1})).

This completes the proof.

The above immediately implies that satisfaction of any equation

\xymatrix{Γ \ar[r]_{λ} \ar[r]^{ρ} & Σ^{@}}

in the sense of Definition 5.1 is the same as satisfaction of the corresponding set of Σequations:

6.7. Corollary. A Σ-algebra satisfies an equation λ = ρ iff it satisfies the set E of Σ-equations of (6.1).

Proof. Suppose that a Σ-algebra A satisfies the equation λ = ρ. By Corollary 5.12, the Σ^{(i)}-algebra A^{(h)} satisfies the i-th derived equation of λ = ρ. Equivalently, each A^{(h)} satisfies the Σ^{(i)}-equations from the set E_{i}. Thus by Remark 6.2(4), A satisfies the Σ-equations in the set E.

Conversely, if A satisfies the Σ-equations in E, then it satisfies the Σ-equations in every set E_{i}; this follows from Lemma 6.6 recalling the definition of λ̂_{i} and ρ̂_{i} from Remark 6.2(3). Equivalently, each A^{(h)} satisfies the Σ^{(i)}-equations in E_{i} by Remark 6.2(1).

6.8. Example. One binary operation of iterativity 2:

Σ(2, 0) = {σ}, Σ(i, p) = ∅ otherwise.

A Σ-algebra is a set with a binary operation. We know from Example 3.11 that Σ^{(i)} is the signature of nullary operations σ(x_{0}, x_{1}) indexed by i × i. Thus

Σ^{@}(i, p) = i × i + p

(a) Choose i = 2 and consider the Σ-equation

(0, 1) = (1, 0)

It is satisfied by an algebra A iff for every pair h : i ⟶ A we have σ(h(x_{0}), h(x_{1})) = σ(h(x_{1}), h(x_{0})). This is the commutativity of the operation.

(b) Associativity cannot be expressed as a Σ-equation. Indeed, given a Σ-equation l = r in Σ^{@}(i, p) with l ≠ r, if l and r both lie in the right-hand summand of i × i + p, then the equation l = r holds for trivial algebras (of at most one element) only. If l and r both lie in the left-hand summand of i × i + p, they present one of the following laws for Σ:

(b1) σ(x, y) = σ(y, x) (commutativity of σ),

(b2) σ(x, x) = σ(y, y) (diagonal is merged),

(b3) σ(x, y) = σ(x′, y) (σ depends on the right-hand variable only); note that this is equivalent to σ(x, y) = σ(y, y),

(b4) σ(x, y) = σ(x, y′) (σ depends on the left-hand variable only); note that this is equivalent to σ(x, y) = σ(x, x),

or

(b5) σ(x, y) = σ(x′, y′) (σ is constant).

And the case of l and r lying in different summands of i × i + p yields two cases σ(x, y) = z and σ(x, x) = y both of which only hold in the trivial algebras.

6.9. Notation. Let E be a set of Σ-equations. Define a parametrized signature Γ_{E} as follows:

Γ_{E}(i, p) = E ∩ (Σ^{@}(i, p) × Σ^{@}(i, p)) for all i, p in ℕ.

We have obvious projections

λ, ρ : Γ_{E} ⟶ Σ^{@}

in ParSig(Set): they assign to l = r in E the elements l and r, respectively.

6.10. Definition. A base □ over Set is said to have a presentation by Σ-equations for some parametrized signature Σ if there exists a coequaliser in Base(Set) of the form

\xymatrix{□_{Γ_{E}} \ar[r]_{λ̌} \ar[r]^{ρ̌} & □_{Σ} \ar[r]^{γ} & □}

for some set E of Σ-equations.

6.11. Remark. For every i let

E^{i} = {l^{(u)} = r^{(u)} | j ∈ ℕ, (l, r) ∈ E_{j} and u : j ⟶ i arbitrary }

Then i □ p is the free Σ^{(i)}-algebra on p generators modulo the equations E^{i}.

6.12. Example.

(1) The base

i □ p = 𝒫_{2}i + p

where 𝒫_{2} is the functor assigning to every set all unordered pairs in it, has a presentation by Σ of Example 6.8 and the single equation (0, 1) = (1, 0) in Σ^{@}(2, 0).

Indeed, 𝒫_{2}i+p is the free algebra on p generators for the signature of nullary operation symbols σ(x_{0}, x_{1}) where (x_{0}, x_{1}) range through 𝒫_{2}i. Thus Example 6.8 yields the result.

(2) The base

i □ p = (i × i)/∼ + p

where ∼ merges the diagonal of i × i to a single element has a presentation by Σ of Example 6.8 and the single Σ-equation (0, 0) = (1, 1) in Σ^{@}(2, 0) (this is case (b2) in Example 6.8).

(3) The two equations

(1, 0) = (0, 1) and (0, 0) = (1, 1)

together present the base

i □ p = (i × i)/≈ + p

where ≈ merges both (x, y) with (y, x) and all (x, x).

6.13. Example. One binary operation of iterativity 1:

Σ(1, 1) = {σ}, Σ(i, p) = ∅ otherwise.

We know from Example 3.11 that Σ^{(i)} is the signature of i unary operations σ(x, −) for x = 0, …, i − 1. Thus

Σ^{@}(i, p) = i^{∗} × p.

For i = 2 and p = 1 consider the Σ-equation

(01, 0) = (10, 0).

This is satisfied by precisely those Σ-algebras that fulfil the following weakening of the commutative law:

σ(x, σ(y, z)) = σ(y, σ(x, z)).

That is, the derived unary operations σ(x, −) commute with each other. Let ℬ be the bag functor, assigning to every set X the set ℬX of bags (i.e., finite multisets in X), which is the free commutative monoid on X. The free binary algebra on p generators modulo the above weakened commutative law is ℬi × p. Thus, we obtained a presentation of the base

i □ p = ℬi × p.

6.14. Example. Finally, consider a single binary operation of iterativity 0:

Σ(0, 2) = {σ}, Σ(i, p) = ∅ otherwise.

Thus Σ^{(i)} = {σ} for all i and Σ^{@}(i, p) is the free binary algebra on p generators. For every variety 𝒱 of algebras on a single binary operation we obtain a presentation of the following base

i □ p = free algebra of 𝒱 on p generators.

6.15. Corollary. Every base over Set has a presentation by a parametrized signature Σ and Σ-equations.

Proof. This follows from Theorem 5.4 and Corollary 6.7.

References

[1] P. Aczel, J. Adámek, S. Milius and J. Velebil, Infinite Trees and Completely Iterative Theories: A Coalgebraic View, Theoret. Comput. Sci., 300 (2003), 1–45.

[2] J. Adámek, Free algebras and automata realizations in the language of categories, Comment. Math. Univ. Carolin. 15 (1974), 589–602.

[3] J. Adámek, S. Milius and J. Velebil, Some remarks on finitary and iterative monads, Appl. Categ. Structures 11 (2003), 521–541.

[4] J. Adámek, S. Milius and J. Velebil, Iterative algebras at work, Math. Structures in Comput. Sci. 16 (2006), 1085–1131.

[5] J. Adámek, S. Milius and J. Velebil, Algebras with parametrized iterativity, Theoret. Comput. Sci. 388 (2007) 130–151.

[6] J. Adámek, S. Milius and J. Velebil, Bases for parametrized iterativity, Inform. and Comput. 206 (2008), 966–1002.

[7] J. Adámek, S. Milius and J. Velebil, Base modules for parametrized iterativity, Theoret. Comput. Sci. 523 (2014), 56–85.

[8] J. Adámek and J. Rosický, Locally presentable and accessible categories, Cambridge University Press, 1994.

[9] M. Barr, Coequalizers and free triples, Math. Z. 116 (1970), 343–375.

[10] C. C. Elgot, S. L. Bloom and R. Tindell, On the algebraic structure of rooted trees, J. Comput. System Sci. 16 (1978), 362–399.

[11] P. Gabriel and F. Ulmer, Lokal präsentierbare Kategorien, Lecture N. Math. 221, Springer-Verlag, Berlin 1971.

[12] G. M. Kelly, A unified treatment of transfinite constructions for free algebras, free monoids, colimits, associated sheaves, and so on, Bull. Austral. Math. Soc. 22 (1980), 1–8i3.

[13] G. M. Kelly and A. J. Power, Adjunctions whose counits are coequalizers and presentations of enriched monads, J. Pure Appl. Algebra 89 (1993), 163–179.

[14] A. Kock, On Double Dualization Monads, Math. Scan. 27 (1970), 151–165.

[15] S. Lack, On the monadicity of finitary monads, J. Pure Appl. Algebra 140 (1999), 65–73.

[16] F. E. J. Linton, An outline of functorial semantics, Lecture Notes Math. 80, Springer 1969, 7–52.

[17] E. G. Manes, Algebraic Theories, Springer-Verlag, Berlin, Heidelberg, New York, 1976.

[18] L. S. Moss, Parametric corecursion, Theoret. Comput. Sci. 260 (2001), 139–163.

[19] E. Nelson, Iterative algebras, Theoret. Comput. Sci. 25 (1983), 67–94.

[20] R. Paré, On absolute colimits, J. Algebra, 19 (1971), 80–95.

[21] J. Tiuryn, Unique fixed points vs. least fixed points, Theoret. Comput. Sci. 12 (1980), 229–254.

[22] T. Uustalu, Generalizing substitution, Theor. Inform. Appl. 37.4 (2003), 315–336.

Department of Mathematics, Faculty of Electrical Engineering, Czech Technical University in Prague, Czech Republic

Lehrstuhl für Informatik 8 (Theoretische Informatik), Friedrich-Alexander-Universität Erlangen-Nürnberg, Germany

Department of Mathematics, Faculty of Electrical Engineering, Czech Technical University in Prague, Czech Republic

Email: j.adamek@tu-braunschweig.de
     mail@stefan-milius.eu
     velebil@math.feld.cvut.cz
This article may be accessed at http://www.tac.mta.ca/tac/

THEORY AND APPLICATIONS OF CATEGORIES (ISSN 1201-561X) will disseminate articles that significantly advance the study of categorical algebra or methods, or that make significant new contributions to mathematical science using categorical methods. The scope of the journal includes: all areas of pure category theory, including higher dimensional categories; applications of category theory to algebra, geometry and topology and other areas of mathematics; applications of category theory to computer science, physics and other mathematical sciences; contributions to scientific knowledge that make use of categorical methods. Articles appearing in the journal have been carefully and critically refereed under the responsibility of members of the Editorial Board. Only papers judged to be both significant and excellent are accepted for publication. Full text of the journal is freely available from the journal’s server at http://www.tac.mta.ca/tac/. It is archived electronically and in printed paper format.

Subscription information Individual subscribers receive abstracts of articles by e-mail as they are published. To subscribe, send e-mail to tac@mta.ca including a full name and postal address. For institutional subscription, send enquiries to the Managing Editor, Robert Rosebrugh, rrosebrugh@mta.ca.

Information for authors The typesetting language of the journal is TEX, and L^{A}TEX2e is required. Articles in PDF format may be submitted by e-mail directly to a Transmitting Editor. Please obtain detailed information on submission format and style files at http://www.tac.mta.ca/tac/.

Managing editor. Robert Rosebrugh, Mount Allison University: rrosebrugh@mta.ca

TEXnical editor. Michael Barr, McGill University: barr@math.mcgill.ca

Assistant TEX editor. Gavin Seal, Ecole Polytechnique Fédérale de Lausanne:

gavin seal@fastmail.fm

Transmitting editors.

Clemens Berger, Université de Nice-Sophia Antipolis: cberger@math.unice.fr Richard Blute, Université d’ Ottawa: rblute@uottawa.ca Lawrence Breen, Université de Paris 13: breen@math.univ-paris13.fr Ronald Brown, University of North Wales: ronnie.profbrown(at)btinternet.com Valeria de Paiva: Nuance Communications Inc: valeria.depaiva@gmail.com Ezra Getzler, Northwestern University: getzler(at)northwestern(dot)edu Kathryn Hess, Ecole Polytechnique Fédérale de Lausanne: kathryn.hess@epfl.ch Martin Hyland, University of Cambridge: M.Hyland@dpmms.cam.ac.uk Anders Kock, University of Aarhus: kock@imf.au.dk Stephen Lack, Macquarie University: steve.lack@mq.edu.au F. William Lawvere, State University of New York at Buffalo: wlawvere@buffalo.edu Tom Leinster, University of Edinburgh: Tom.Leinster@ed.ac.uk Ieke Moerdijk, Utrecht University: i.moerdijk@uu.nl Susan Niefield, Union College: niefiels@union.edu Robert Paré, Dalhousie University: pare@mathstat.dal.ca Jiri Rosicky, Masaryk University: rosicky@math.muni.cz Giuseppe Rosolini, Università di Genova: rosolini@disi.unige.it Alex Simpson, University of Ljubljana: Alex.Simpson@fmf.uni-lj.si James Stasheff, University of North Carolina: jds@math.upenn.edu Ross Street, Macquarie University: ross.street@mq.edu.au Walter Tholen, York University: tholen@mathstat.yorku.ca Myles Tierney, Université du Québec à Montréal : tierney.myles4@gmail.com R. J. Wood, Dalhousie University: rjwood@mathstat.dal.ca