* Category of Heyting Algebras @ 2003-02-11 21:48 Galchin Vasili 2003-02-12 17:03 ` Prof. Peter Johnstone 2003-02-12 17:20 ` Robert McGrail 0 siblings, 2 replies; 5+ messages in thread From: Galchin Vasili @ 2003-02-11 21:48 UTC (permalink / raw) To: categories Hello, I have some questions about the category whose objects are Heyting algebras and whose arrows are Heyting algebra homomorphims. 1) Does this category possess a subobject classifier? 2) Is this category a CCC? 3) Is this category a topos? It would really be neat if 3) was true because of all kinds of self-reference or infinite regression, e.g. it's Omega would be an internal Heyting algebra, but my guess is "no" to all three. Regards, Bill Halchin ^ permalink raw reply [flat|nested] 5+ messages in thread
* Re: Category of Heyting Algebras 2003-02-11 21:48 Category of Heyting Algebras Galchin Vasili @ 2003-02-12 17:03 ` Prof. Peter Johnstone 2003-02-14 3:32 ` Robin Cockett 2003-02-12 17:20 ` Robert McGrail 1 sibling, 1 reply; 5+ messages in thread From: Prof. Peter Johnstone @ 2003-02-12 17:03 UTC (permalink / raw) To: categories On Tue, 11 Feb 2003, Galchin Vasili wrote: > > Hello, > > I have some questions about the category whose objects are Heyting > algebras and whose arrows are Heyting algebra homomorphims. > > 1) Does this category possess a subobject classifier? > > 2) Is this category a CCC? > > 3) Is this category a topos? > The category of Heyting algebras has no hope of being cartesian closed because its initial object (the free HA on one generator) is not strict initial. It doesn't have a subobject classifier either, because the theory of Heyting algebras doesn't have enough unary operations to satisfy the conditions of Theorem 1.3 in my paper "Collapsed Toposes and Cartesian Closed Varieties" (J. Algebra 129, 1990). On the other hand, the terminal object in the category of Heyting algebras is strict, which suggests that the dual of the category might come rather closer to being a topos (although, by an observation which I posted a couple of months ago, it can't have a subobject classifier). Indeed, the dual of (finitely-presented Heyting algebras) is remarkably well-behaved, as shown by Silvio Ghilardi and Marek Zawadowski ("A Sheaf Representation and Duality for Finitely Presented Heyting Algebras", J.Symbolic Logic 60, 1995): they identified a particular topos in which it embeds (non-fully, but conservatively) as a subcategory closed under finite limits, images and universal quantification. Peter Johnstone ^ permalink raw reply [flat|nested] 5+ messages in thread
* Re: Category of Heyting Algebras 2003-02-12 17:03 ` Prof. Peter Johnstone @ 2003-02-14 3:32 ` Robin Cockett 0 siblings, 0 replies; 5+ messages in thread From: Robin Cockett @ 2003-02-14 3:32 UTC (permalink / raw) To: categories Further to Peter's remark that the opposite of the category finitely presented Heyting algebras is rather nice ... one particular sense in which it is nice is that it is a lextensive category! So -- to seemingly contradict Peter :-) -- it does have a partial map classifier (but of course not for all monics)! The fact that it is a lextensive category can be obtained, by checking some Heyting algebra identities, from "Conditional Control is not quite Categorical Control" IV Higher Order Workshop, Banff 1990, Workshops in Computing (Springer-Verlag) 190-217 (1991) where the general question of when the opposite of an algebraic theory is extensive is answered. Any extensive category can be fully and faithfully embedded in a topos so as to preserve sums and limits ... so the ability to embed the opposite of Heyting algebra "nicely" into a topos can also be read from these results. -robin P.S.Whether this embedding has the other logical properties mentioned is, of course, another question ... On 12 Feb, Prof. Peter Johnstone wrote: > On Tue, 11 Feb 2003, Galchin Vasili wrote: > >> I have some questions about the category whose objects are Heyting >> algebras and whose arrows are Heyting algebra homomorphims. >> > > The category of Heyting algebras has no hope of being cartesian closed > because its initial object (the free HA on one generator) is not > strict initial. It doesn't have a subobject classifier either, because > the theory of Heyting algebras doesn't have enough unary operations > to satisfy the conditions of Theorem 1.3 in my paper "Collapsed > Toposes and Cartesian Closed Varieties" (J. Algebra 129, 1990). > > On the other hand, the terminal object in the category of Heyting > algebras is strict, which suggests that the dual of the category > might come rather closer to being a topos (although, by an observation > which I posted a couple of months ago, it can't have a subobject > classifier). Indeed, the dual of (finitely-presented Heyting > algebras) is remarkably well-behaved, as shown by Silvio Ghilardi > and Marek Zawadowski ("A Sheaf Representation and Duality for > Finitely Presented Heyting Algebras", J.Symbolic Logic 60, 1995): > they identified a particular topos in which it embeds (non-fully, > but conservatively) as a subcategory closed under finite limits, > images and universal quantification. > > Peter Johnstone > > > > ^ permalink raw reply [flat|nested] 5+ messages in thread
* Re: Category of Heyting Algebras 2003-02-11 21:48 Category of Heyting Algebras Galchin Vasili 2003-02-12 17:03 ` Prof. Peter Johnstone @ 2003-02-12 17:20 ` Robert McGrail 2003-02-12 19:31 ` Toby Bartels 1 sibling, 1 reply; 5+ messages in thread From: Robert McGrail @ 2003-02-12 17:20 UTC (permalink / raw) To: categories On Tuesday 11 February 2003 16:48, you wrote: > Hello, > > I have some questions about the category whose objects are Heyting > algebras and whose arrows are Heyting algebra homomorphims. > > 1) Does this category possess a subobject classifier? > > 2) Is this category a CCC? Unless my definition of Heyting algebra is a bit off, I am sure that this (and hence 3) is false. I assume that in a Heyting algebra T does not equal F. This follows the intuitive introduction of Heyting algebras by Moerdijk/MacLane as capturing the algebraic structure of topologies. If that is not the case then disregard the rest of my message. Anyway, under these assumptions, the trivial HA {T,F} is both initial and final. Hence 0 = 1 (= means is iso to). Any CCC with 0 = 1 is trivial. I will leave the diagram chase to you but it can be summarized as follows. Let A be any HA. Then A = A^1 = A^0 = 1. Hope this helps, Bob McGrail > > 3) Is this category a topos? > > It would really be neat if 3) was true because of all kinds of > self-reference or infinite regression, e.g. it's Omega would be an > internal Heyting algebra, but my guess is "no" to all three. > > Regards, Bill Halchin ^ permalink raw reply [flat|nested] 5+ messages in thread
* Re: Category of Heyting Algebras 2003-02-12 17:20 ` Robert McGrail @ 2003-02-12 19:31 ` Toby Bartels 0 siblings, 0 replies; 5+ messages in thread From: Toby Bartels @ 2003-02-12 19:31 UTC (permalink / raw) To: categories Robert McGrail wrote: >I assume that in a Heyting algebra T does not equal F. >This follows the intuitive introduction of Heyting algebras by >Moerdijk/MacLane as capturing the algebraic structure of topologies. Probably there are people that put this in the definition -- the same people that require 0 != 1 in any ring, or that a topological space not be empty, or (for that matter) that a CCC not be trivial. But if you're not one of those people, then the Heyting algebra {*} captures the algebraic structure of the (unique topology on the) empty space. >Anyway, under these assumptions, the trivial HA {T,F} is both initial and >final. So with my definition, {T,F} is initial but {*} is final. But even with yours, I don't believe that {T,F} becomes final. There are 2 homomorphisms to it from the power set of {T,F} (as a Boolean algebra, which is a special kind of Heyting algebra). I don't think that your category has a final object (any more than the category of nontrivial rings does, nor the category of nonempty spaces has an initial object). -- Toby ^ permalink raw reply [flat|nested] 5+ messages in thread
end of thread, other threads:[~2003-02-14 3:32 UTC | newest] Thread overview: 5+ messages (download: mbox.gz / follow: Atom feed) -- links below jump to the message on this page -- 2003-02-11 21:48 Category of Heyting Algebras Galchin Vasili 2003-02-12 17:03 ` Prof. Peter Johnstone 2003-02-14 3:32 ` Robin Cockett 2003-02-12 17:20 ` Robert McGrail 2003-02-12 19:31 ` Toby Bartels
This is a public inbox, see mirroring instructions for how to clone and mirror all data and code used for this inbox; as well as URLs for NNTP newsgroup(s).