Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.


Stream: learning: questions

Topic: A question about Heyting Algebras


view this post on Zulip Suraaj K S (Jun 18 2024 at 16:29):

We know that a Heyting algebra satisfies the distributive law. I think this is simply an instance of distributivity in a CCC with coproducts.

Moreover, a complete lattice is a Heyting algebra if it satisfies the infinite distributive law.
I was wondering if this was an instance of some other abstract cateogory theoretic notion?

view this post on Zulip Graham Manuell (Jun 18 2024 at 16:46):

The first is the fact that left adjoints preserve colimits. You can think of the second as a poset version of the adjoint functor theorem: a monotone map that preserves all joins has a right adjoint.

view this post on Zulip Todd Trimble (Jun 18 2024 at 17:03):

Moreover, a complete lattice is a Heyting algebra if it satisfies the infinite distributive law.

A complete lattice in which finite meets distribute over arbitrary sups is also known as a [[frame]].

This isn't quite what you were asking, but there is a strong pull to saying that the notion [[Grothendieck topos]] categorifies the notion of frame or of its dual notion, [[locale]]. The sharpest expression of the analogy is probably Street's characterization. A frame is a poset PP such that its 2\mathbf{2}-enriched Yoneda embedding P[Pop,2]P \to [P^{op}, \mathbf{2}] has a left exact (here, finite meet-preserving) left adjoint. Likewise, a Grothendieck topos is almost the same thing as a category EE such that its Set\mathsf{Set}-enriched Yoneda embedding has a left exact (here, finite limit-preserving) left adjoint. To remove the "almost" you just need a mild size condition on the class of morphisms, working here under the assumption of one universe (i.e. a set vs. small set distinction), and assuming EE is locally small so that we can speak of its Yoneda embedding.

See also Giraud's characterization, which is closely related.