Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
The observation that the preorder $sub(x)$ of subobjects of some object $x$ in an elementary topos happens to be a Heyting algebra is the starting point of categorical semantics.
The dual situation where the preorder $sup(x)$ consisting of epimorphisms out of the object is considered (which should give an Esakia space in an elementary topos, I guess), I have never seen mentioned in context of categorical logic. Is this really dual to the $sub(x)$-case in that we obtain a supobject classifier (respectively: an object co-classifier if we are in $(\infty,1)$-categories) satisfying dual statements etc. ?
What are the reasons for this not being mentioned? Maybe I just have to look under a different keyword to find some material.
It is not possible to have a “supobject” classifier $\mho$ in an elementary topos: the universal epimorphism would be an arrow $\mho \to 0$, but the initial object of a cartesian closed category is strict, so $\mho \cong 0$.
Is this idea becoming more interesting if we consider it in an ”elementary cotopos” (finite colimits, cocartesian co-closed, and ”sup object classifier”)?
Epimorphisms out of an object are quotient objects, not superobjects. A superobject (following the term ‘superset’) would be a monomorphism out of the object.
I wouldn’t expect quotients objects of an object in a topos to form an Esakia space; Esakia duality says that Heyting algebras and Esakia spaces are essentially the same thing, except that the morphisms go in opposite directions. The quotient objects (of a fixed object in a topos) will still form a lattice, albeit not a Heyting algebra but some other kind of lattice.
If you dualise everything and look at quotient objects in a ‘cotopos’, then this is really just the same as looking at subobjects in the opposite category (which is a topos), so we’re back to Heyting algebras.
1 to 4 of 4