OK, I’ve been poking at this for a while and I think that in fact the type-1 condition does follow from the type-5 one in a cartesian bicategory. The proof is sketched, using mobile-phone pictures of string diagrams, here. (Apologies for the kludginess – time permitting, I will see about trying to formalise the proof using Globular.) A second opinion would be invaluable, so if anyone wants to try to reconstruct the whole proof then you would be doing me a favour by asking as many questions as necessary.
Briefly, though, it should follow from this that the type-1 condition holds in the situation of my previous comment, namely
]]>a cartesian monoidal bifibration satisfying Frobenius reciprocity and Beck–Chevalley conditions for squares of type 2, as well as for the squares expressing the coassociativity of diagonals (let’s call these type 5) and preservation of the condition under taking products with an object.
Something interesting re Zhen’s #22 and #24:
Suppose we’re working in a cartesian monoidal bifibration satisfying Frobenius reciprocity and Beck–Chevalley conditions for squares of type 2, as well as for the squares expressing the coassociativity of diagonals (let’s call these type 5) and preservation of the condition under taking products with an object. Then we can turn this fibration into a cartesian bicategory using the construction in Mike’s paper here, which will satisfy the ‘Frobenius law’ of Carboni and Walters (see e.g.~here).
Then the expression translates to (something isomorphic to) the composite of P with, or pullback of P along, the dual of as defined in ibid., proposition 3.8. That this is canonically isomorphic to should then follow from the fact that (theorem 3.11). So Zhen’s result would seem to hold even in a non-ordered fibration of the kind we’ve been considering, as long as the type-5 BCC holds too.
I wrote about this translation between fibrations and equipments in my thesis, and in particular tried to figure out if the type-1 BCC followed from the type-5 one in a cartesian bicategory. Using duality one can get a morphism of the right type, but despite filling several whiteboards with a mess of string diagrams I couldn’t find any reason why it should be the inverse of the Beck–Chevalley morphism. So I’m not so confident about #26 in a non-ordered fibration; but who knows, maybe I missed something the first time around, so I’ll keep looking.
]]>Out of curiosity, I’ve been poking around in the presheaf fibration over groupoids looking for counterexamples to or reasons to believe in the type-(1) BC conditions. Here are the inconclusive results. (I apologise if this is not interesting.)
Let’s stick with finite groups (not my usual stomping ground, so please be patient). If is a homomorphism and is a (right) -set then the pushforward is , which works out to be the usual induced representation, given by the set of orbits of the action of on where . Notice that this action will be free if either is injective or the action of on is free. We can count orbits using Burnside’s lemma, and in particular if acts freely on then the number of orbits is .
Both and the diagonal are split monomorphisms, so the induced actions of on and on are free, and therefore the number of orbits is
So it’s still possible that this BC condition holds. (Note that pulling back along doesn’t change the number of orbits.)
For the other type-(1) BC condition, let be a right -set. For we have an action of on given by . A fixed point is one where and , so the set is if and empty otherwise. Therefore the number of orbits is
For we can ignore the as before, so we have an action of on where . (You can see where this is going.) A fixed point has , and , so the set of them is if and and empty otherwise. So in fact we get the same formula as before for the number of orbits, after cancelling a factor of .
In short, no news is good news: if I haven’t made any mistakes then it at least can’t be ruled out that either type-(1) BC condition holds in the non-preordered hyperdoctrine of actions of finite groups.
]]>Very interesting!
]]>Lawvere shows that Frobenius reciprocity implies
and then uses the type-(1) BCC to show
How do you derive
from Frobenius alone?
]]>I think there is a mistake in the derivation for type-(1) squares, where in the last step you have
It’s not generally true that , because is contravariant.
I’m glad this has come up, because I had been looking at Seely’s paper again recently. In section 3 he seems to require only one of the two possible BC conditions for each pullback square, i.e.~the one involving pushforwards of the vertical morphisms, but then later towards the end of section 4 he shows that both conditions hold in syntactic hyperdoctrines for pullbacks of type (1) above (type (a) in the paper), and he seems to use the opposite condition to that suggested in section 3 in lemma 2 of section 8. This latter ‘opposite’ condition is the one Lawvere talks about in Equality in hyperdoctrines, and (together with Frobenius reciprocity) it’s responsible for the sensible interpretation of . I can’t work out whether Seely even uses the former condition anywhere. Does anyone know whether either follows from the other, in the presence of Frobenius reciprocity?
As it happens, the naturality squares for the symmetry maps always satisfy both possible conditions, and for each type of pullback except type (a) you can ‘flip it over’ to generate the other BC condition by pasting with symmetry-naturality squares, so type-(a) pullbacks are the only case where requiring only one BC condition might make a difference.
]]>– and hence – splits, and thus is full and faithful.
I don’t think this is necessarily true unless the ‘pseudo-section’ of is also its left adjoint. For example, take the unique functor from the free parallel pair to the terminal category. It has a section, because is inhabited, but it is not faithful.
I think a counterexample to this BC condition is the presheaf fibration over Cat (considered as a 1-category). Here takes a presheaf to the presheaf on A. For a transformation , i.e.~a natural family , there doesn’t seem to be any good reason why it should come from a unique transformation . You can cook up counterexamples if you take A to be the arrow category , for example, so that P is a commuting square in Set and is the morphism both of its sides are equal to. A transformation like looks like this:
and to lift it to a transformation is to give functions and so that everything commutes. But using the initial, terminal and 2-element sets I think you can find examples where there is no such extension or more than one for given .
I still have to read your argument for type-1 squares closely, but maybe lemma 3 in section 8 of Seely’s paper is relevant (annoyingly, he says the proof is ‘trivial’ :| ).
]]>Jonas said:
one can ask how many of Todd’s “productive pullbacks” one should demand the BC condition for – to assure a sound interpretation of logic they are not all needed I think, but they may give additional desirable properties.
Seely talks about this in sections 3 and 8 of Hyperdoctrines, natural deduction and the Beck condition (PDF).
]]>Part of me would like to codify it all top down from the standpoint of nonabelian cohomology, and then point to these other things as special cases.
This is decidedly not my area, but there has been some work on descent, torsors, cohomology etc. done at a fairly high level of abstraction, which seems as though it should be relevant; you may well know about it already, but if not here are a couple of references:
Street. Characterization of bicategories of stacks, LNM 962, 1982.
Janelidze, Schumacher, Street. Galois theory in variable categories, Applied Categorical Structures 1, 1993.
The introductions and bibliographies of these have some good references to other work too.
]]>I’ve given it a mention, beside the link to your page comprehensive factorization (michaelshulman). (Note to self: read and understand that page!)
]]>Right, I’ve moved everything to axiom of separation and added a section on the comprehensive factorization, as well as a redirect from the page comprehension. I’ve blanked the latter, but now I’m not sure whether that’s the right thing to do in this situation.
]]>I was planning to add something on the comprehensive factorization to comprehension when I got the chance, so I’ll do that this evening, and move the whole lot to axiom of separation at the same time.
There’s nothing complicated about the factorization system, really: a fibration with full comprehension gives a subfibration of the codomain fibration, and if the resulting ’subtype inclusions’ are closed under composition, then that gives you a factorization system on the base category (this is in Carboni et. al., On localization and stabilization for factorization systems). The factorization of a morphism is the commuting triangle given by the unit of the reflection. For the subobject fibration of a regular category this is the usual epi-mono factorization, whereas for the presheaf fibration over Cat it gives the factorization of an arbitrary functor into a final functor followed by a discrete fibration.
]]>Thanks, Mike! Those are good questions:
Yes, neither gives what we want, which is colax transformations with tight components. A monad 2-cell gives a pseudonatural transformation whose components must be tight; a Kleisli 2-cell relaxes the latter condition, but doesn’t allow the transformation to be colax. I have an idea for how to get around this, but it will take more working out. (Loosely: a monad morphism in this context is a pseudo algebra for a certain pseudo monad, and the kind of 2-cell we want is a lax morphism between these algebras. Fitting all of these into a tricategory is the tricky part, but I’m hoping there will be enough lax morphism classifiers to simplify things.)
Yes, I would certainly expect so. I remember reading your paper with keen interest when it came out, and thinking it could be highly relevant to my work, but in the end I didn’t have the time to expand my stuff enough to connect it with yours. Of course, one issue is that what I’ve done only works in the presence of finite products, whereas I think I remember a conversation you, Todd and me had a while back where you said that you used allegories precisely because some of the sites you were dealing with didn’t have products. Again, I have an idea about how to generalize, but this one’s still rather vague.
Urs: the Wirthmüller stuff is interesting, although I can’t pretend to understand the context. But I would like to find out how much of this stuff works for monoidal fibrations that aren’t cartesian.
Tim: thanks! The viva hasn’t been scheduled yet; still waiting to hear back from the external examiners. I’m dreading it and looking forward to it in equal measure!
]]>I’ve rounded off my thesis outline (finnlawler), if anyone else would like to have a look. In particular, I’d be interested to hear if anyone has seen the first result under Tabulation and comprehension before, in this generality; I mean the equivalence for a predicate P over X in the bifibration E, where is the extension of P.
]]>Yes, good point. I have rephrased things slightly.
]]>Thanks, David! I should add that comments and questions are more than welcome.
]]>Looks fine. I’ve done some minor tidying-up, and added the example of the category of elements of a presheaf.
]]>New page at comprehension, describing Lawvere’s version of the comprehension schema in a hyperdoctrine, and also Jacobs’s variant.
]]>I finally submitted my thesis a couple of months ago, so I’ve put a brief not-yet-entirely-complete outline at thesis outline (finnlawler), for anyone who’s interested.
]]>I don’t mean to highjack the thread, but I’d like to reply to what Todd wrote about the two kinds of realizability constructions:
I would really like to have a unified understanding of these two paths, and have this reflected in the nLab.
So would I, and I’m writing my thesis on one aspect of that understanding, namely that you can organise predicates into either fibrations (like the effective tripos) or bicategories of relations (like Rel of the category of assemblies), and that with enough structure the 2-categories of these are equivalent. There is a(n unfinished) sketch of some of this on my personal web here. (Do ask if you’d like to know more; I intend to flesh this out when I get time.)
Here’s what I’m not doing (this is all due to Pieter Hofstra): say you start with a pca , e.g. the naturals with Kleene application. You can form an indexed poset that I’ll call (even though the ordering is not the pointwise one but the ’realizability’ one). The category of elements of this is the category of partitioned assemblies over . For any pca , the sets and of subsets and non-empty subsets of are again pcas and give indexed posets in the same way; the category of elements of is the category of assemblies over , while is the realizability tripos over .
This last is a regular fibration, so corresponds to (what I call) a framed bicategory of relations, and the (underlying bicategory of the) coreflexive splitting of the latter is Rel of the category of assemblies over . From that point on, the two paths coincide. (I’d very much like to understand the earlier parts of the two processes better, but then I’d also like to finish my thesis sometime this decade…)
]]>Right, there’s nothing new or tricky going on here. The distributive law is between ordinary monads on an ordinary category, that just happens to be a hom-category of a 2-category, and all of the conditions follow from the naturality of the associativity isomorphism of that 2-category.
]]>A distributive law doesn’t relate the units of the two monads — there are two triangle axioms, each asserting that the distributive law commutes with two different whiskerings of the same unit, so etc.
]]>Added to module over a monad an observation about bimodules as algebras over a composite monad.
]]>