Functorial semantics and HSP type theorems
type: Item
instance of: scholarly article
title: Functorial semantics and HSP type theorems
zbMATH Open document ID: 0794.18004
DOI: 10.1007/BF01236519
author: Michael Barr
published in: Algebra Universalis
publication date: 1994-08-22T00:00:00Z
review text: A full subcategory \({\mathcal C}_ 0\) of the category \({\mathcal C}\) of models of a Kleisli category \({\mathcal K}\) with respect to a given factorisation system \({\mathcal E}/{\mathcal M}\) of a complete base category \({\mathcal B}\) is called HSP subcategory if \({\mathcal C}_ 0\) is closed under certain epimorphisms, under \({\mathcal M}\)-monics, and under products. The aim of the present paper is to give a characterization of such HSP subcategories. Unlike to Birkhoff's theory the result introduced here depends on how one defines HSP (what kind of subobjects are allowed, idea of satisfying a certain Horn clause). The author proves after some preliminaries about factorization systems, \({\mathcal B}\)-based sketches, and models some necessary conditions for the existence of a left adjoint to a certain functor \(U\colon Mod({\mathcal K})\to {\mathcal B}\), where \({\mathcal K}\) is at least a \({\mathcal B}\)-based sketch. The next result is that the Kleisli category \({\mathcal K}\) of a triple \({\mathfrak T}\) on \({\mathcal B}\) is isomorphic to the full image of the left adjoint \(F^{\mathfrak T}\colon {\mathcal B}\to {\mathcal B}^{\mathfrak T}\) to \(U^{\mathfrak T}\colon {\mathcal B}^{\mathfrak T}\to {\mathcal B}\) arising from \(U\) in a natural manner. Furthermore, the corresponding Eilenberg-Moore category is isomorphic to the category of models of \({\mathcal K}\). Using results of Linton the author shows that the underlying functor \(U\colon {\mathcal C}\to {\mathcal B}\) is tripleable and the triple is \({\mathfrak T}\), whenever \({\mathfrak T}\) is a triple on \({\mathcal B}\) with Kleisli category \({\mathcal K}\) and \({\mathcal C}\) as category of models of the resultant theory- type sketch. An HSP subcategory of \({\mathcal C}\) is tripleable if \(U\colon {\mathcal C}\to {\mathcal B}\) is tripleable. So one obtains the main HSP theorem: Let \(F\colon {\mathcal B}\to {\mathcal K}\) be the free functor into a Kleisli category with respect t…
Mathematics Subject Classification ID: 18C10
Mathematics Subject Classification ID: 18C20
Mathematics Subject Classification ID: 03C05
Mathematics Subject Classification ID: 18C15
Mathematics Subject Classification ID: 18A20
Mathematics Subject Classification ID: 03G30
zbMATH DE Number: 549248
zbMATH Keywords: functorial semantics
zbMATH Keywords: adjointness
zbMATH Keywords: Kleisli category
zbMATH Keywords: factorisation system
zbMATH Keywords: sketches
zbMATH Keywords: models
zbMATH Keywords: triple
zbMATH Keywords: Horn clauses
zbMATH Keywords: HSP theorem
reviewed by: Hans-Jürgen Vogel
MaRDI profile type: Publication
cites work: Accessible categories and models of linear logic
cites work: Q3961629
cites work: Every Standard Construction is Induced by a Pair of Adjoint Functors
cites work: Q3961632
cites work: Q5570958
cites work: A theorem on Barr-exact categories, with an infinitary generalization
description: scientific article; zbMATH DE number 549248