On the Morphisms and Transformations of Tsuyoshi Fujiwara (as a concretion of a bidimensional many-sorted general algebra and its application to the equivalence between many-sorted clones and algebraic theories)

TL;DR

This paper extends Fujiwara's morphism theory to many-sorted algebras, establishing a 2-category framework that demonstrates equivalences between different algebraic specifications and introduces a new concept of 2-institution.

Contribution

It introduces polyderivors for many-sorted signatures, constructs a 2-category of specifications, and proves equivalences between algebraic theories and specifications, generalizing previous concepts.

Findings

Established a category of polyderivors isomorphic to a Kleisli category.

Proved the equivalence of Hall and Bénabou specifications and their algebra categories.

Introduced the concept of 2-institution as a strict generalization of institutions.

Abstract

For single-sorted algebras, Fujiwara defined, through the concept of family of basic mapping-formulas, a notion of morphism which generalizes the ordinary notion of homomorphism between algebras and an equivalence relation, the conjugation, on the families of basic mapping-formulas, which corresponds to the relation of inner isomorphism for algebras. In this paper we extend the theory of Fujiwara about morphisms to the many-sorted algebras, by defining the concept of polyderivor between many-sorted signatures, which assigns to basic sorts, words and to formal operations, families of derived terms, and under which the standard signature morphisms, the basic mapping-formulas of Fujiwara, and the derivors of Goguen-Thatcher-Wagner are subsumed. Then, by means of the homomorphisms between B\'enabou algebras, which are the algebraic counterpart of the finitary many-sorted algebraic theories of B\'enabou, we define the composition of polyderivors from which we get a corresponding category, isomorphic to the category of Kleisli for a monad on the standard category of many-sorted signatures. Next, by defining the notion of transformation between polyderivors, we endow the category of many-sorted signatures and polyderivors with a structure of 2-category. From this we get a derived 2-category of many-sorted specifications in which we prove the equivalence of the many-sorted specifications of Hall and B\'enabou, and deduce the equivalence of the categories of Hall and B\'enabou algebras. Besides, by defining corresponding categories of generalized many-sorted terms, we prove that the realization of these terms in the many-sorted algebras is invariant under polyderivors and compatible with the transformations between polyderivors, and from this we get an example, among others, of the new concept of 2-institution, itself an strict generalization of that of institution by Goguen and Burstall.