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: theory: category theory

Topic: "homset" hyperdoctrine

Tom Hirschowitz (Aug 06 2024 at 13:02):

In conversations with @Ambroise, @Paul-André Melliès, Nick Behr, and others, we encountered the following hyperdoctrine construction. It seems to at least have some value for explaining work by Barbara König and others on conditional reactive systems, and we'd be interested if anyone knows about it, or is able to shed some relevant light on it.

Given a category $𝐂$ and an object $X ∈ 𝐂$, one can form a (covariant) posetal hyperdoctrine $P$ on it by taking:

• the fibre $P(C)$ over any $C ∈ 𝐂$ to be $𝒫(𝐂(C,X))$, i.e., predicates on the homset $𝐂(C,X)$, and
• the action $P(f)\colon P(C) → P(D)$ of any $f\colon C → D$ to be given by inverse image, i.e., $P(f) = 𝐂(f,X)^{-1}$; otherwise said, for any $φ ⊆ 𝐂(C,X)$, $P(f)(φ)$ is the set of all $g\colon D → X$ such that $gf ∈ φ.$

The Heyting algebra structure on each fibre is given by the powerset structure, and the left adjoint to reindexing is given by image, i.e., $∐_f (φ) = 𝐂(f,X)(φ)$.

The right adjoint is a bit more tedious: $∏_f(φ) = \{ h\colon C → X \mathrel{|} ∀ g\colon D → X, gf = h ⟹ g ∈ φ \}$.

If my calculations are correct, this easily satisfies Beck-Chevalley for all pushout squares (since we're considering a covariant hyperdoctrine, this is the normal situation).

Any comments?

Vincent Moreau (Aug 06 2024 at 16:30):

Hi Tom, if we see part of the structure in a bifibered way, then I have the impression that what you are describing is the pullback

$$\begin{CD} \bullet^\mathrm{op} @>>> \mathbf{SubSet}\\ @VVV @VVV\\ \mathbf{C}^\mathrm{op} @>>\mathbf{C}(-, X)> \mathbf{Set} \end{CD}$$

Indeed, an object of the pullback is a pair $(C, \varphi)$ of an object $C$ of $\mathbf{C}$ together with a subset $\varphi \subseteq \mathbf{C}(C, X)$ and a morphism $(C, \varphi) \to (D, \psi)$ is a morphism $f : C \to D$ in $\mathbf{C}$ such that for all $g \in \psi \subseteq \mathbf{C}(D, X)$, we have $g \circ f \in \varphi \subseteq \mathbf{C}(C, X)$.

Vincent Moreau (Aug 06 2024 at 16:37):

Pulling back a bifibration gives you another bifibration. If you see a (cloven) bifibration as a pseudofunctor into $\mathbf{Adj}$, the categories whose objects are categories and whose morphisms are adjunctions, then this pullback operation is just precomposition.

Tom Hirschowitz (Aug 06 2024 at 20:52):

Indeed, thanks @Vincent Moreau!