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.
Made a start – hyperdoctrine.
just for the record, there is an entry titled first-order hyperdoctrine
I have added preliminary links between the two entries. But I guess they should be merged or otherwise harmononized?
I did link to that page from the ’classical’ in “Given any theory (several sorted, intuitionistic or classical) …”. But maybe it should be more apparent. Some commentary on whether the impression is correct that hyperdoctrines disappeared from view somewhat would be welcome.
I did link to that page
Oh, sorry. I didn’t see that.
I would be inclined to merge them.
Yes, they may as well be merged. Who knows about such things? I couldn’t even say how are the Beck-Chevalley and Frobenius conditions are related. Hmm, there’s a MO answer by Todd on this relation which he suggests might be incorporated into the nLab. And I dare say something from this thread could help give some more detail to the Beck-Chevalley condition.
Another example to be included is again described by Todd here $P: Grpd^{co op} \to CAT$.
David said:
I couldn’t even say how are the Beck-Chevalley and Frobenius conditions are related.
I’m not sure they are, if by Frobenius condition you mean Frobenius reciprocity. There is another usage of the name of Frobenius, as in e.g. Walters and Wood’s paper Frobenius objects in cartesian bicategories, where an object $A$ is Frobenius if the Beck-Chevalley condition is satisfied for a certain ’product-absolute’ pullback square involving the diagonal $\Delta \colon A \to A \times A$. I think the latter is what Todd’s MO answer refers to, but I for one don’t see a connection with Lawvere’s Frobenius condition. I’d love to be wrong about that, though.
Todd puts the question here. Also at the MO answer
…it is often the case (for example in certain simple type-theoretic contexts) where verification of the Beck-Chevalley condition boils down to Frobenius reciprocity.
Also, see this paper for a situation where
…one readily sees that the Frobenius Reciprocity Law is a particular case of the Beck-Chevalley Property.
How should what is described at Ubiquity of the push-pull formula be characterized?
What Todd calls Frobenius reciprocity is indeed a special case of Beck–Chevalley, but if you look at Equality in hyperdoctrines you’ll see that what Lawvere calls Frobenius reciprocity is what is described at the nLab page, and I can’t see that either has anything to do with the other.
In the paper you cite by Clementino, Giuli and Tholen, their derivation of (Lawvere’s) Frobenius condition from Beck–Chevalley is, I think, specific to subobject fibrations, because it involves taking an arrow (in a pullback square in) the base category to be a subobject, i.e. an object in a fibre of the hyperdoctrine; but that obviously doesn’t make sense in an arbitrary hyperdoctrine.
What Andrea Ferretti calls the push-pull formula in that MO question looks to be exactly Lawvere’s Frobenius condition (for monoidal bifibrations).
I think the Clementino-Giuli-Tholen observation will work whenever you have a hyperdoctrine equipped with a surjective map from the codomain fibration which preserves pullbacks, pushforwards, and fiberwise products. I’m not sure whether that’s noticeably more general than the context they’re actually in (fibrations of subobjects relative to a factorization system).
Re 12, so there’s Frobenius Reciprocity as described by Todd (FR1) which is a consequence of Beck-C. Then there’s Lawvere’s FR2 which bears no relation to it, but FR2 is a consequence of Beck-C in some situations.
I’m confused.
Re 12, so there’s Frobenius Reciprocity as described by Todd (FR1) which is a consequence of Beck-C. Then there’s Lawvere’s FR2 which bears no relation to it, but FR2 is a consequence of Beck-C in some situations.
Yes, that’s how it looks to me. The categories list might know more.
I’m confused.
I’m more or less permanently confused, so I can’t empathise, having forgotten what clarity feels like.
Possibly I was misremembering or misusing some terms here, but let me try to guess what I was thinking. What follows will be a bit didactic, mainly just to jog my own memory.
There is a Frobenius condition which occurs in, for example, Frobenius monoids or algebras, involving an equation relating a comultiplication $\delta$ and a multiplication $\delta^*$. It’s a pair of equations, one of which is
$\delta \delta^* = (\delta^* \otimes 1)(1 \otimes \delta^*)$More generally, there are Frobenius monads that arise from ambimorphic adjunctions $F \dashv G$ and $G \dashv F$; the $\delta$ would be the comultiplication of the comonad $G F$ arising from $G \dashv F$, and the $\delta^*$ would be the multiplication of the monad $G F$ arising from $F \dashv G$.
There are categorified instances of this Frobenius condition which arise in bicategories of relations and in certain cartesian bicategories, as emphasized often by Walters. Here we have a canonical arrow
$\delta \delta^* \to (\delta^* \otimes 1)(1 \otimes \delta^*)$where we have an adjunction $\delta \dashv \delta^*$ in a bicategory, and this arrow is mated to an coassociativity isomorphism for $\delta$. (A typical example is in the bicategory of sets and relations, where $\delta$ is the functional relation given by a diagonal.) The Frobenius condition would assert that this (and a similar arrow) are isomorphisms; this can be exploited to show that bicategories of relations are compact closed and that each object $c$ is dual to itself, using a unit
$1 \stackrel{\varepsilon^*}{\to} c \stackrel{\delta}{\to} c \otimes c$and a counit
$c \otimes c \stackrel{\delta^*}{\to} c \stackrel{\varepsilon}{\to} 1$As indicated in the MO answer mentioned above, this Frobenius condition holds for the bicategory of groupoids and profunctors between them, but does not hold for categories and profunctors. I think I managed to convince myself a few months ago that a form of it also holds for the tricategory of spans between groupoids.
Then, we have what I think many people call Frobenius reciprocity, although it is called by other names too (e.g., ’projection formula’), and seems to occur all over mathematics. It has to do, more or less, with pullback functors $f^*$ preserving internal homs (although it holds in other contexts too). Here we are dealing with an adjunction $f_! \dashv f^*$ or with an adjunction $f^* \dashv f_*$, and the condition is basically an equation of the form
$f_! S \otimes T = f_!(S \otimes f^* T)$where $S: W \to X$ and $T: W \to Y$ are “arrows” (relations, correspondences, etc.), where $\otimes$ refers to a local tensor living in local hom-categories like $\hom(W, Y)$, and $f_!: X \to Y$. This is well-known for bicategories of relations, and in the context of allegories is in fact generalized to Freyd’s modular law:
$R S \wedge T = R(S \wedge R^{op}T)$People around here have sometimes remarked that Freyd’s modular law is hard to really grok as a piece of categorical algebra (even though it has resonances elsewhere, as I tried to indicate once at the Café in the context of lattices of commuting equivalence relations). Walters makes this point too and shows how it follows in bicategories of relations from the other Frobenius condition, here.
I think there’s probably more to say here on the connections between the two Frobenius conditions. I have to leave in a few minutes, but I hope to come back to this when I have some more time.
Thanks Todd! The modular law made a whole lot more sense to me once I realized that it’s just a version of the (second) Frobenius condition. I didn’t realize the connection to the other Frobenius condition, though; I look forward to hearing what more you have to say!
Yes, thanks Todd. The mist is departing a little. I’m sure the nLab pages could use what you’ve written.
I tried labbifying the argument I gave at Frobenius reciprocity. There may be more to add, but I’m having trouble thinking of exactly what.
Okay, I think I now have something new to add now, and in some sense it’s actually pretty cool.
First, I’ve done some cleaning up in Frobenius reciprocity, in the section where I showed that Frobenius reciprocity holds in a bicategory of relations. (Recall that a bicategory of relations, in the sense of Walters or Carboni-Walters, is a locally posetal cartesian bicategory in which the so-called Frobenius laws hold. These are the laws similar to the key axioms of a Frobenius algebra, and which famously hold in the symmetric monoidal category of 2-cobordisms.)
What I labbified over a month ago (see comment 19) could be summarized as follows:
(I actually don’t think we need the ’locally posetal’ clause, but I’ll let that stand for the moment.) That’s the old news.
The new news is that I think we can also say
(Again, I doubt ’locally posetal’ plays much of a role.) I’ll sketch the proof here in old-fashioned notation, although it’s best comprehended with the aid of string diagrams, which I really don’t know how to display graphically – I’m no good at computer graphics stuff. At some point I’ll try to write up the proof at Frobenius reciprocity, but I want to run through it here first.
Recall what ’Frobenius reciprocity’ means in this context. Given a cartesian bicategory $\mathbf{B}$, there is for each object $c$ a corresponding hyperdoctrine
$\hom_{\mathbf{B}}(i-, c): Map(\mathbf{B})^{op} \to Cat$where $i: Map(\mathbf{B}) \hookrightarrow \mathbf{B}$ is the inclusion. The idea is that each map $f: a \to b$ induces a substitution map $f^\ast: \hom(b, c) \to \hom(a, c)$ on “relations” by pulling back along $f$. If $f^\dagger$ denotes the right adjoint of the map $f$ in $\mathbf{B}$, then the corresponding existential quantification is defined by $\exists_f = \hom(f^\dagger, c): \hom(a, c) \to \hom(b, c)$.
Frobenius reciprocity says that for each $c$, the canonical map
$\exists_f(q \wedge f^\ast r) \to (\exists_f q) \wedge r$is an isomorphism, for every map $f: a \to b$ and any “relations” $q: a \to c$, $r: b \to c$. (To repeat: I don’t think ’locally posetal’ is all that relevant, so that the conjunction $\wedge$ here probably can and should be replaced by a local cartesian product in a general cartesian bicategory. I’ll continue with this notation anyway.) In our case, this is the same as saying that the canonical map
$(q \wedge r f)f^\dagger \to (q f^\dagger) \wedge r$is an isomorphism.
Now let $x$ be any object, and consider the special case where $f = \delta = \delta_x: x \to x \otimes x$, where
$q = \varepsilon^\dagger \otimes 1_x: x \to x \otimes x$(i.e., $q = \varepsilon_{x}^\dagger \otimes 1_x$), and where
$r = \varepsilon \otimes 1_x \otimes \varepsilon^\dagger: x \otimes x \to x \otimes x$(i.e., $r = \varepsilon_{x} \otimes 1_x \otimes \varepsilon_{x}^\dagger$).
Claim 1: $(q \wedge r f)f^\dagger \cong \sigma \delta \delta^\dagger$, where $\sigma: x \otimes x \to x \otimes x$ is the symmetry.
Claim 2: $(q f^\dagger) \wedge r \cong \sigma (\delta^\dagger \otimes 1_x)(1_x \otimes \delta)$.
Putting these two claims together with the Frobenius reciprocity isomorphism, we derive an isomorphism
$\sigma \delta \delta^\dagger \cong \sigma (\delta^\dagger \otimes 1_x)(1_x \otimes \delta)$or, since $\sigma$ is an isomorphism,
$\delta \delta^\dagger \cong (\delta^\dagger \otimes 1_x)(1_x \otimes \delta)$which is the Frobenius law.
The full details of these claims are a little involved, and possibly boring, but easy via string diagrams. One needs a few ancillary results: first that
$q \wedge r \delta = \delta_{x \otimes x}^\dagger (q \otimes r \delta) \delta_x$Second, that $r \delta = (\varepsilon \otimes 1_x \otimes \varepsilon^\dagger)\delta = 1_x \otimes \varepsilon^\dagger$. This gives
$q \otimes r \delta = (x \otimes x \stackrel{\varepsilon^\dagger \otimes 1_x \otimes 1_x \otimes \varepsilon^\dagger}{\to} (x \otimes x) \otimes (x \otimes x)).$Third, that $\delta_{x \otimes x}^\dagger = (x \otimes x \otimes x \otimes x \stackrel{1_x \otimes \sigma \otimes 1_x}{\to} x \otimes x \otimes x \otimes x \stackrel{\delta^\dagger \otimes \delta^\dagger}{\to} x \otimes x)$. Hence $\delta_{x \otimes x}^\dagger (q \otimes r \delta)$ becomes
$x \otimes x \stackrel{\varepsilon^\dagger \otimes 1_x \otimes 1_x \otimes \varepsilon^\dagger}{\to} x \otimes x \otimes x \otimes x \stackrel{1 \otimes \sigma \otimes 1}{\to} x \otimes x \otimes x \otimes x \stackrel{\delta^\dagger \otimes \delta^\dagger}{\to} x \otimes x$which can be rearranged to
$x \otimes x \stackrel{\sigma}{\to} x \otimes x \stackrel{\varepsilon^\dagger \otimes 1 \otimes 1 \otimes \varepsilon^\dagger}{\to} x \otimes x \otimes x \otimes x \stackrel{\delta^\dagger \otimes \delta^\dagger}{\to} x \otimes x$which, up to isomorphism, collapses to just $\sigma: x \otimes x \to x \otimes x$. Therefore, we have $q \wedge r \delta \cong \sigma \delta$, so that
$(q \wedge r\delta)\delta^\dagger \cong \sigma \delta \delta^\dagger$which is Claim 1.
Whew.
I’m petering out now, but Claim 2 is proved in a wholly similar way.
Great stuff, Todd; very interesting! So it seems that Lawvere’s Frobenius reciprocity is indeed a consequence of the Beck–Chevalley condition for pullback squares. That’s a surprising result in itself.
This is great! I haven’t read the proof yet, though; I’d be much happier to see the string diagrams. Even scanned handwritten ones would be better than nothing.
In reply to Finn, I’m not sure it means that Lawvere’s Frobenius axiom is a consequence of the Beck-Chevalley condition. I think you need Lawvere’s Frobenius condition (in addition to Beck-Chevalley) in order to construct a bicategory of relations from a hyperdoctrine, which is the context that Todd’s working in.
I’ll see if I can scan something in, but even doing that tests my limits…
My memory (and this is from maybe more than 10 years ago) is that indeed both Frobenius reciprocity and Beck-Chevalley get used to obtain a cartesian bicategory from a hyperdoctrine. I’ll have to review what the deal is, and then I should write it up over at cartesian bicategory. (Actually, I have begun muttering stuff about hyperdoctrines over there already, but it’s somewhat preliminary. I do feel that these back and forth relationships between the Frobenius law and Frobenius reciprocity belong in the more general cartesian bicategory context, which would include Span.)
What about mailing photocopies to someone else who could scan them in? I’d be happy to do the scanning… (-:
Actually, I don’t think this correspondence even requires cartesianness; it should work in the more general context of monoidal fibrations and monoidal (framed?) bicategories. The construction of a monoidal bicategory from a monoidal fibration is in my paper “Framed bicategories and monoidal fibrations,” and I believe it specializes to the construction of a cartesian bicategory from a hyperdoctrine in the cartesian case. It uses both the Beck-Chevalley condition and Frobenius reciprocity (which I prefer, in that context, to call “$\otimes$ preserves indexed coproducts”). The other direction is more interesting and I’m not quite sure how it will go, but I think you’d need to use a framed bicategory as given rather than constructing the framing out of left adjoints the way you do in a cartesian bicategory.
I’d be happy to make (mock?) up some graphics from a hand-drawn version. Clearly mailing them to Mike to scan is quicker than mailing them to me :-)
I’ll mail them to both of you, a little later today. I might even be able to construct a .pdf of the thing.
David: thank you for the very kind offer! The biggest benefit to me would be to learn from what you did.
Mike #22: Oh, OK. I hadn’t realised that Frobenius was needed to pass from a monoidal fibration to a framed bicategory. Thanks for the clarification.
I have tried to brush-up the entry hyperdoctrine a little.
In particular I have tried to write a more informative Idea-section.
Would be glad if an expert found a minute to look over this. Despite its name, which suggests quite otherwise, the notion of hyperdoctrine is quite simple, and I hope we can get the entry to the point that it reflects this :-) (Why on earth was that name “hyperdoctrine” chosen?)
If you had to give the idea of hyperdoctrines in one short sentence, what would you do? How about
A hyperdoctrine is a collection of propositions in various contexts, together with a rule for how to change the context by substitution/introduction of variables and by applying quantifiers.
?
Isn’t it as simple as that?
Next, a hyper-cyber-multi-ultra-doctrine is… But let’s leave that for later ;-)
Lawvere defines a hyperdoctrine more generally to be a (pseudo)functor
$P: C^{op} \to Cat$(with adjoints on both sides, etc.), instead of restricting to just posets or lattices. And I agree with his decision.
Okay, sure, I’ll change the entry accordingly.
As far as I can see, this is the natural categorification of the logic, isn’t it? In view of (directed) homotopy type theory we’d allow ourselves to take values in more general higher categories, I suppose.
So I have made it now
A hyperdoctrine for a given notion of logic $L$ is a functor $P : T^{op} \to \mathbf{C}$ to some category or higher category $\mathbf{C}$ whose internal logic corresponds to $L$, such that…
But if you feel that this is not going in the right direction, please feel welcome to interfere.
I’m not sure what you mean by your second sentence in #30. But it seems to me that Lawvere is amplifying on his insight that quantifiers in ordinary logic are examples of adjoints, and he wants to emphasize here that adjoints, not ordinary logical quantifiers, are really the more basic foundational concept. (And I guess he would like to redefine “logic” in such a more general way, in terms of systems of adjoints between categories.)
Obviously the concept of hyperdoctrine is so plastic that you could generalize/specialize in all sorts of directions, such as the one you mention. But if I were to try to write something on “HTT for dummies”, my inclination would be to use Lawvere’s more vanilla definition at the outset ($P: C^{op} \to Cat$), and consider the example where $C$ is a model category, taking $P(c)$ to be the category of fibrations over $c$. (This is meant more as a pedagogical or expositional point.)
Re #31: looks good to me so far. Not sure if I want to “interfere” (or tinker) with that.
Lawvere is amplifying on his insight that quantifiers in ordinary logic are examples of adjoints, and he wants to emphasize here that adjoints, not ordinary logical quantifiers, are really the more basic foundational concept.
Okay, I see.
I’m not sure what you mean by your second sentence in #30.
Right, I didn’t say that well. What I am thinking is this:
Ordinary logic, interpreted in category theory, is the theory of monomorphisms. These form posets. That’s why a hyperdoctrine that expresses some ordinary theory will take values not in arbitrary categories, put in posets = $(0,1)$-categories.
This changes as we pass to the internal logic of higher categories. In the context of $(n,1)$-cartegories, logic is the theory $(n-2)$-truncated morphisms. These form $(n-1,1)$-categories, instead of just posets.
So when Lawvere generalizes from hyperdoctrines with values in $Lattice$ to general ones with values in $Cat$, he is essentially generalizing from 1-logic to 2-logic.
As far as I can see.
I follow that much better now – thanks for explaining. I don’t disagree with it in spirit (and I like the idea of keeping options open in the Idea section, as you have it now).
This is looking better. I rewrote the Idea section some more, to clarify that it is the objects of $\mathbf{C}$ whose internal logic is $L$, not $\mathbf{C}$ itself.
It is indeed looking better. Who are those quotations in the section on special cases attributed to? (They read a bit tentatively.)
I think the quotations are from Lawvere’s Equality in hyperdoctrines.
They read a bit tentatively.
Yes, these are remnants of the original form of the entry by, I think, David Corfield, which was all tentative by design. I think David was hoping one of us would pick up this thread and flesh out the entry. Which is what we are doing now.
That’s exactly what I was doing.
Now people are looking at hyperdoctrine, was I right in the modal logic post to think there could be a modal hyperdoctrine? Was Neel onto something here?
Then there’s the question of the relationship between the hyperdoctrine approach and the syntactic category approach. Is there a good way to pass between them?
Promted by discussion in another thread I have expanded the Idea-section at hyperdoctrine to now start as follows:
The notion of a hyperdoctrine is essentially an axiomatization of the collection of slices of a locally cartesian closed category (or something similar): a category $T$ together with a functorial assignment of “slice-like”-categories to each of its objects, satisfying some conditions.
In its use in mathematical logic a hyperdoctrine is thought of (under categorical semantics of logic/type theory) as a collection of contexts together with the operations of context extension/substitution and quantification on the categories of propositions or types in each context. Therefore specifying the structure of a hyperdoctrine over a given category is a way of equipping that with a given kind of logic.
1 to 41 of 41