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: deprecated: id my structure

Topic: logical category

Nico Beck (Aug 24 2023 at 13:50):

I have a condition on a category which has strong implications, so much so that I wonder if it is possible to classify categories with that property. I will call the property "very logical" since I lack a better word at the moment.

Definition. A category $\mathscr S$ with finite limits is very logical when there is a Grothendieck topology $W$ on $\mathscr S$ such that the subobject fibration of $\mathscr S$ is a stack with respect to that topology and any $W$-local sieve on an object $\Gamma$ can be represented by a subobject of $\Gamma$.

Explanation of the terminology: A sieve $S$ on $\Gamma$ is $W$-local when the following condition holds. Whenever $u:\Delta \to \Gamma$ is any map and there is a $W$-cover $v_i:\Theta_i\to \Delta$ of $\Delta$ such that each $uv_i$ is in $S$, then also $u$ is in $S$. A sieve $S$ on $\Gamma$ is represented by a subobject $m$ when the morphisms in $S$ are precisely the morphisms which factor through $m$.

Does somebody know what kind of categories are logical?

What I found out is:

• When a category is very logical then there is at most one topology $W$ wich satisfies the conditions listed in the definition, because the local sieves of that topology are determined by the subobjects in $\mathscr S$, and a sieve is a $W$-covering sieve in a site $(\mathscr S,W)$ if and only if the maximal sieve is the smallest $W$-local sieve which contains it
• Grothendieck topoi are very logical, and the unique topology $W$ which satisfies the conditions is the canonical one
• A very logical category must be a Heyting category (i.e. can interpret all the first-order logical connectives on its subobject fibration)
• A very logical category is regular and can interpret bracket types

(I hope I did not make a mistake with the above properties)

Patrick Nicodemus (Aug 25 2023 at 18:05):

Not exactly what you are looking for but I would point you to section 11.7 of Jacobs' Categorical Logic and Type Theory where he discusses relationships between interesting logical properties and the fibration being a stack. He is interested in the codomain fibration because it interprets dependent type theory rather than the subobject fibration.