Some questions about different notions of "theory"
1) Finitary monads correspond to Lawvere theories. Is there a name for those monads that correspond to toposes? 2) In topos theory is there any analogous result to Lawvere's theorem that the opposite of the category of free finitely generated gadgets is equivalent to the Lawvere theory of gadgets? Something like "the opposite of the category of fooable gadgets is equivalent to the topos of gadgets"? 3) nLab says a sketch is a small category T equipped with subsets (L,C) of its limit cones and colimit cocones. A model of a sketch is a Set-valued functor preserving the specified limits and colimits. Is preserving limits and colimits like a ring homomorphism? Preserving both limits and colimits sounds like it ought to involve profunctors, but maybe I'm level slipping. -- Mike Stay - metaweta@gmail.com http://www.cs.auckland.ac.nz/~mike http://reperiendi.wordpress.com [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
1) I'm not sure what Mike means by `those monads that correspond to toposes' since most toposes don't correspond to monads on anything. I did investigate those toposes which are monadic over Set, or a power of Set, in my papers `When is a variety a topos?', Algebra Universalis 21 (1985), 198--212, and `Collapsed toposes and cartesian closed varieties', J. Algebra 129 (1990), 446--480. 2) A possible answer to this question is that the (2-)category of finitely presented minimal toposes (and logical functors) is equivalent to the dual of the free topos (on no generators), where a topos is said to be minimal if it has no proper full logical subtoposes. This is a result of Peter Freyd, but I don't know whether he ever published it. Peter Johnstone On Nov 7 2017, Mike Stay wrote:
1) Finitary monads correspond to Lawvere theories. Is there a name for those monads that correspond to toposes?
2) In topos theory is there any analogous result to Lawvere's theorem that the opposite of the category of free finitely generated gadgets is equivalent to the Lawvere theory of gadgets? Something like "the opposite of the category of fooable gadgets is equivalent to the topos of gadgets"?
3) nLab says a sketch is a small category T equipped with subsets (L,C) of its limit cones and colimit cocones. A model of a sketch is a Set-valued functor preserving the specified limits and colimits. Is preserving limits and colimits like a ring homomorphism? Preserving both limits and colimits sounds like it ought to involve profunctors, but maybe I'm level slipping.
[For admin and other information see: http://www.mta.ca/~cat-dist/ ]
Is the following of any relevance? Dubuc, Eduardo J.; Kelly, G. M. (1983). "A presentation of topoi as algebraic relative to categories or graphs" <http://www.sciencedirect.com/science/article/pii/0021869383901977>. *J. Algebra*. *81* (2): 420–433. doi <https://en.wikipedia.org/wiki/Digital_object_identifier>: 10.1016/0021-8693(83)90197-7 <https://doi.org/10.1016%2F0021-8693%2883%2990197-7>. On Tue, Nov 7, 2017 at 6:57 PM, <ptj@maths.cam.ac.uk> wrote:
1) I'm not sure what Mike means by `those monads that correspond to toposes' since most toposes don't correspond to monads on anything. I did investigate those toposes which are monadic over Set, or a power of Set, in my papers `When is a variety a topos?', Algebra Universalis 21 (1985), 198--212, and `Collapsed toposes and cartesian closed varieties', J. Algebra 129 (1990), 446--480.
2) A possible answer to this question is that the (2-)category of finitely presented minimal toposes (and logical functors) is equivalent to the dual of the free topos (on no generators), where a topos is said to be minimal if it has no proper full logical subtoposes. This is a result of Peter Freyd, but I don't know whether he ever published it.
Peter Johnstone
On Nov 7 2017, Mike Stay wrote:
1) Finitary monads correspond to Lawvere theories. Is there a name
for those monads that correspond to toposes?
2) In topos theory is there any analogous result to Lawvere's theorem that the opposite of the category of free finitely generated gadgets is equivalent to the Lawvere theory of gadgets? Something like "the opposite of the category of fooable gadgets is equivalent to the topos of gadgets"?
3) nLab says a sketch is a small category T equipped with subsets (L,C) of its limit cones and colimit cocones. A model of a sketch is a Set-valued functor preserving the specified limits and colimits. Is preserving limits and colimits like a ring homomorphism? Preserving both limits and colimits sounds like it ought to involve profunctors, but maybe I'm level slipping.
[For admin and other information see: http://www.mta.ca/~cat-dist/ ]
In answer to Mike: "3) nLab says a sketch is a small category T equipped with subsets (L,C) of its limit cones and colimit cocones. A model of a sketch is a Set-valued functor preserving the specified limits and colimits. Is preserving limits and colimits like a ring homomorphism? Preserving both limits and colimits sounds like it ought to involve profunctors, but maybe I'm level slipping." Sketches were introduced by Charles Ehresmann in 1966 (and developed by us and our research students) in several papers, among which I'll cite: (i) The main Charles' paper "ESQUISSES ET TYPES DES STRUCTURES ALG??BRIQUES", Bul. Inst. Pol. Iasi, Tome XIV-1-2, 1968 (in French), reprinted in http://ehres.pagesperso-orange.fr/C.E.WORKS_fichiers/Ehresmann_C.-Oeuvres_IV... on p. 19-32 (with several Comments in English I added on p. 329-332); (ii) Our joint paper "Categories of sketched structures", Cahiers Top.GDC XIII-2, 1972 http://www.numdam.org/article/CTGDC_1972__13_2_104_0.pdf I have been surprised to see the definition given in nLab of a sketch as a category with some limit-cones and co-limit-cones. For us, a 'sketch' is a category S (or even a graph) with some distinguished cones and co-cones (but not necessarily (co-)limit-cones). And in the above citation we construct the 'prototype' of the sketch which is constructed by forcing the (co-)cones to become (co-)limit-cones. Indeed, our idea was that a sketch describes a 'smaller' presentation of a generalized algebraic structure (for instance of categories themselves), and from it we deduced its prototype and also its type (analogue of the theory for Lawvere algebraic structures). The 'realisation' (or 'model') of a sketch S in a category C is then a functor from S to C which transforms the distinguished (co-)cones into (co-)limit-cones. There is no need of profunctors here. Let us note that C is not required to admit all (co-)limits, just the images of the distinguished (co-)cones must become (co-)limit-cones. An initial 1959 example (at the basis of Charles' definition) was the notion of a 'differentiable category' which is a model of the sketch of categories into the category of differentiable maps (which admits limits but only specific co-limits). Sincerely Andree [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
On Thu, Nov 9, 2017 at 3:26 AM, Andrée Ehresmann <andree.ehresmann@u-picardie.fr> wrote:
I have been surprised to see the definition given in nLab of a sketch as a category with some limit-cones and co-limit-cones. For us, a 'sketch' is a category S (or even a graph) with some distinguished cones and co-cones (but not necessarily (co-)limit-cones).
Thanks for pointing this out. I think this is an error on the nLab page, or perhaps a sloppy phrasing that got misinterpreted by a later editor; I'll fix it. In the case when a sketch is a graph rather than a category, it has to come equipped also with some distinguished diagrams that are supposed to commute in its models, right? [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
How can we have a categorical definition of 'theory', when we do not have a categorical definition of 'sentence'? Institutions (Goguen) and Entailment Systems (Meseguer) do have a Sentence functor but their underlying category of signatures is abstract, so without sort (over a category?) and operators (potentially over another category?). Many-valuedness and its (algebraic) foundations is looking into these things. Just wondering if anybody is thinking along these lines. Uwe at least, I guess. Cheers, Patrik PS Why many-valuedness? Well, for one thing, everything in and around Google and Facebook is many-valued. On 2017-11-08 01:57, ptj@maths.cam.ac.uk wrote:
1) I'm not sure what Mike means by `those monads that correspond to toposes' since most toposes don't correspond to monads on anything. I did investigate those toposes which are monadic over Set, or a power of Set, in my papers `When is a variety a topos?', Algebra Universalis 21 (1985), 198--212, and `Collapsed toposes and cartesian closed varieties', J. Algebra 129 (1990), 446--480.
2) A possible answer to this question is that the (2-)category of finitely presented minimal toposes (and logical functors) is equivalent to the dual of the free topos (on no generators), where a topos is said to be minimal if it has no proper full logical subtoposes. This is a result of Peter Freyd, but I don't know whether he ever published it.
Peter Johnstone
On Nov 7 2017, Mike Stay wrote:
1) Finitary monads correspond to Lawvere theories. Is there a name for those monads that correspond to toposes?
2) In topos theory is there any analogous result to Lawvere's theorem that the opposite of the category of free finitely generated gadgets is equivalent to the Lawvere theory of gadgets? Something like "the opposite of the category of fooable gadgets is equivalent to the topos of gadgets"?
3) nLab says a sketch is a small category T equipped with subsets (L,C) of its limit cones and colimit cocones. A model of a sketch is a Set-valued functor preserving the specified limits and colimits. Is preserving limits and colimits like a ring homomorphism? Preserving both limits and colimits sounds like it ought to involve profunctors, but maybe I'm level slipping.
[For admin and other information see: http://www.mta.ca/~cat-dist/ ]
[For admin and other information see: http://www.mta.ca/~cat-dist/ ]
Dear Patrik, Categorical logic can interpret, but doesn't rigidly follow, the standard logical path of signature, formula and sentence to reach theory = signature + sentences. I guess that's the path you had in mind that underlies your question, and it is also the path that influenced Goguen and Meseguer. Even where categorical logic interprets that standard path, it can move away from the "Hilbert-style" idea that a sentence is a formula with no free variables. Look in Elephant part C (?) and you'll see that the sentences there are sequents in context. But categorical logic goes further than ordinary logic in its attempt to define 'theory'. Think of a category as loosely motivated by sets. The set constructions that logic most directly accesses - as formulae - are subsets of finite products (of carriers). It struggles to get to other constructions that category theory accesses quite naturally. Hence category theory can - and does - define 'theory' in ways that seem quite unnatural to a logician, either presented (for instance by sketches) or completed (as classifying categories, such as Lawvere theories). Regards, Steve. On 09/11/2017 07:13, peklund@cs.umu.se wrote:
How can we have a categorical definition of 'theory', when we do not have a categorical definition of 'sentence'?
Institutions (Goguen) and Entailment Systems (Meseguer) do have a Sentence functor but their underlying category of signatures is abstract, so without sort (over a category?) and operators (potentially over another category?).
Many-valuedness and its (algebraic) foundations is looking into these things.
Just wondering if anybody is thinking along these lines. Uwe at least, I guess.
Cheers,
Patrik
PS Why many-valuedness? Well, for one thing, everything in and around Google and Facebook is many-valued.
[For admin and other information see: http://www.mta.ca/~cat-dist/ ]
participants (7)
-
Andrée Ehresmann -
Keith Harbaugh -
Michael Shulman -
Mike Stay -
Patrik Eklund -
ptj@maths.cam.ac.uk -
Steve Vickers