Not signed in (Sign In)

Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

  • Sign in using OpenID

Site Tag Cloud

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory internal-categories k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).

nLab > Latest Changes: First-order hyperdoctrines and triposes

Bottom of Page

1 to 35 of 35

  1.  
    • CommentRowNumber1.
    • CommentAuthorSridharRamesh
    • CommentTimeFeb 23rd 2010
    • (edited Feb 23rd 2010)

    Continuing from a very minor edit on localic topos, I've created articles on first-order hyperdoctrines and triposes; both need fleshing out, but the latter in particular I've only just barely started. I intend to add to it a more explicit description of the construction of a topos from a tripos, and discussion of some specific examples (those given by complete Heyting algebras and by realizability relative to a partial combinatory algebra). (Also, the definition has only been given for a special case at the moment).

    • CommentRowNumber2.
    • CommentAuthorSridharRamesh
    • CommentTimeFeb 23rd 2010

    (I've made a number of stub articles branching out from these, which will presumably get fleshed out in parallel with these)

    • CommentRowNumber3.
    • CommentAuthorDaniil
    • CommentTimeNov 2nd 2015

    Can someone elaborate on the restriction of the category of Heyting algebras to that particular subcategory? I haven’t seen it in the literature before.

    • CommentRowNumber4.
    • CommentAuthorZhen Lin
    • CommentTimeNov 2nd 2015

    We want to be able to interpret quantification, so we need both adjoints.

    • CommentRowNumber5.
    • CommentAuthorDaniil
    • CommentTimeNov 3rd 2015

    Ah, fair enough, I didn’t fully understand the wording. I thought that the “morphisms” in “subcategory of the category of Heyting algebras containing only those morphisms with left and right adjoints” refer to morphisms f : A -> B of Heyting algebras, whilst the morphisms that have adjoints are P(f) : P(Y) -> P(X).

    • CommentRowNumber6.
    • CommentAuthorJonasFrey
    • CommentTimeNov 3rd 2015

    It should be emphasized that the adjoints in HeytAlg AdjCyl\mathrm{HeytAlg}_\mathrm{AdjCyl} need not themselves be Heyting algebra morphisms, i.e. they are adjoints in the 2-category Ord\mathrm{Ord} of preorders, not in the 2-category HeytAlg\mathrm{HeytAlg} of Heyting algebras.

    And I have never seen the Beck-Chevalley condition for equality postulated for squares of the form

    A →δ A A×A δ A↓ ↓ 1 A×δ A A×A →δ A×1 A A×A×A.\array{ A & \stackrel{\delta_A}{\to} & A \times A \\ ^\mathllap{\delta_A} \downarrow & & \downarrow^\mathrlap{1_A \times \delta_A} \\ A \times A & \underset{\delta_A \times 1_A}{\to} & A \times A \times A }.

    Is that really sufficient?

    I think Jacobs requires it for squares of the form (Def. 3.4.1 in “Categorical logic and type theory”)

    A×B →A×f A×C δ A×B↓ ↓ δ A×C A×A×B →A×A×f A×A×C.\array{ A\times B & \stackrel{A\times f}{\to} & A \times C \\ ^\mathllap{\delta_A\times B} \downarrow & & \downarrow^\mathrlap{\delta_A \times C} \\ A \times A \times B& \underset{A\times A\times f}{\to} & A \times A \times C }.

    On the other hand, Pitts (Def.~2.1 in “Tripos theory in retrospect”) doesn’t require any Beck Chevalley condition for equality at all.

    • CommentRowNumber7.
    • CommentAuthorZhen Lin
    • CommentTimeNov 3rd 2015
    • (edited Nov 3rd 2015)

    I think it is reasonable to ask for the Beck–Chevalley condition as Jacobs does. This is connected with indiscernibility of identicals for predicates with parameters. (The Frobenius condition only gives us indiscernibility of identicals for predicates without parameters.)

    • CommentRowNumber8.
    • CommentAuthorTodd_Trimble
    • CommentTimeNov 3rd 2015

    Re #6: I think I checked before, but it certainly bears checking again, that when the base categories C TC_T is a free category-with-products generated by a given set of sorts, the BC condition for that special case implies the BC condition for all pullback squares that obtain in C TC_T.

    In some unfinished notes, I advocate the position that over a base category with finite products C TC_T, the BC condition ought to be enforced for all “productive pullback” diagrams in C TC_T, meaning pullbacks that are preserved by any product-preserving functor C T→DC_T \to D. The more general pulbacks mentioned by Jacobs are for example productive. (This notion of productive pullback could be seen as a special case of a more general notion of absolute limit, where we change doctrine from CatCat to categories with products.)

    • CommentRowNumber9.
    • CommentAuthorJonasFrey
    • CommentTimeNov 3rd 2015

    Hi Todd, that’s very interesting and I will have a closer look at your notes later.

    But you say you proved it for the case where the base category is freely generated by a set of sorts, and I think that’s not a requirement in the page first-order hyperdoctrine, or am I missing something?

    • CommentRowNumber10.
    • CommentAuthorTodd_Trimble
    • CommentTimeNov 3rd 2015

    No, you’re not missing anything; the page ought to be revised I think. Certainly to include Jacobs’s condition at the very least.

    • CommentRowNumber11.
    • CommentAuthorJonasFrey
    • CommentTimeNov 4th 2015

    I made some changes in first-order hyperdoctrine, but I’m not very happy with the result.

    I first removed the “Frobenius style” diagram, thinking that it was subsumed by the “Jacobs style” one, but now I’m not so sure anymore, so I put the “Frobenius style” diagram back in.

    So at the moment I’m not sure if the Frobenius style BC condition follows from the Jacobs style one, and if not, if we should include it in the definition additionally.

    More generally, 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.

    In the literature all authors seem to have their own variations.

    • CommentRowNumber12.
    • CommentAuthorZhen Lin
    • CommentTimeNov 4th 2015
    • (edited Nov 4th 2015)

    I think Todd’s condition is a special case of Jacobs’s condition. So the claim is

    (Δ A×id A) *∃ id A×Δ A⊤ A×A≅∃ Δ A⊤ A(\Delta_A \times \id_A)^* \exists_{id_A \times \Delta_A} \top_{A \times A} \cong \exists_{\Delta_A} \top_A

    but Jacobs’s condition implies

    ∃ id A×Δ A⊤ A×A≅d 0 *∃ Δ A⊤ A\exists_{id_A \times \Delta_A} \top_{A \times A} \cong d_0^* \exists_{\Delta_A} \top_A

    where d 0:A×A×A→A×Ad_0 : A \times A \times A \to A \times A is (x,y,z)↦(y,z)(x, y, z) \mapsto (y, z), hence,

    (Δ A×id A) *∃ id A×Δ A⊤ A×A≅(Δ A×id A) *d 0 *∃ Δ A⊤ A≅∃ Δ A⊤ A(\Delta_A \times \id_A)^* \exists_{id_A \times \Delta_A} \top_{A \times A} \cong (\Delta_A \times id_A)^* d_0^* \exists_{\Delta_A} \top_A \cong \exists_{\Delta_A} \top_A

    because d 0∘(Δ A×id A)=id A×Ad_0 \circ (\Delta_A \times id_A) = id_{A \times A}.

    • CommentRowNumber13.
    • CommentAuthorTodd_Trimble
    • CommentTimeNov 4th 2015

    (I wouldn’t call it ’my’ condition though. It’s one of those Frobenius conditions as explored here. If anything, I’m advocating BC conditions which are a priori more general.)

    • CommentRowNumber14.
    • CommentAuthorFinnLawler
    • CommentTimeNov 4th 2015

    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).

    • CommentRowNumber15.
    • CommentAuthorJonasFrey
    • CommentTimeNov 7th 2015
    • (edited Nov 7th 2015)

    Zhen Lin and Finn, thanks a lot for your replies. They were really helpful. Seely’s article is especially interesting, since it’s the only place where I have seen BC conditions discussed in this detail.

    However, after thinking about it for a while, I now suspect that two of Seely’s conditions are actually redundant, which leaves us with only one BC condition.

    Concretely, Seely considers BC for the four squares (a), (b), (c), (d) in Section 3 of his article. The same squares can be found on Todd’s page where they are numbered (1), (2), (3), (4) (above Definition 5).

    Seely observes correctly that BC for (4) is automatic since it’s a pullback of an isomorphism.

    However, I believe that BC for (3) is also automatic, and (1) follows from (2), so it seems we only have to postulate BC for (2).

    The arguments that (1) and (3) are as follows starting with (3), which is the following square.

    A → A ↓ ↓ δ A →δ A×A.\array{ A & {\to} & A \\ \downarrow & & \downarrow^\mathrlap{ \delta} \\ A & \underset{\delta}{\to} & A \times A }.

    BC for this square asserts that the counit of the adjunction ∃ δ⊣δ *\exists_\delta\dashv\delta^* is an isomorphism. But this is automatic since δ\delta – and hence δ *\delta^* – splits, and thus δ *\delta^* is full and faithful.

    Square (1) is of the form

    A →⟨id,f⟩ A×B f↓ ↓ f×B B →δ B×B,\array{ A & \stackrel{\langle id, f\rangle}{\to} & A \times B \\ ^\mathllap{f} \downarrow & & \downarrow^\mathrlap{f \times B} \\ B & \underset{\delta}{\to} & B\times B },

    and it is meant that ‘quantification happens vertically’ in the BC condition. To show that BC for squares of this form follows from BC for squares of the form (2) I adapt Zhen Lin’s proof from 12. The key point is that δ\delta and ⟨id,f⟩\langle \id,f\rangle are both split by the first projection, and the square has a left inverse

    A ←π 1 A×B f↓ ↓ f×B B ←π 1 B×B\array{ A & \stackrel{\pi_1}{\leftarrow} & A \times B \\ ^\mathllap{f} \downarrow & & \downarrow^\mathrlap{f \times B} \\ B & \underset{\pi_1}{\leftarrow} & B\times B }

    in the arrow category, which is a pullback and an instance of (2) (though interestingly it is not the square giving the ‘standard’ BC condition for quantification along projections, since quantification is happening vertically). BC for the fist square can be derived from BC for the second as follows.

    ∃ f⟨id,f⟩ *ψ≅δ *π 1 *∃ f⟨id,f⟩ *ψ≅δ *∃ f×Bπ 1 *⟨id,f⟩ *ψ≅δ *∃ f×Bψ \exists_f\langle id,f\rangle^*\psi \cong \delta^*\pi_1^*\exists_f\langle id,f\rangle^*\psi \cong \delta^*\exists_{f\times B}\pi_1^*\langle id,f\rangle^*\psi \cong \delta^*\exists_{f\times B}\psi

    Concluding, if I haven’t made a mistake I think we have to postulate BC only for squares of the form (2) on Todd’s page, which is as follows.

    A×C →f×C B×C A×g↓ ↓ B×g A×D →f×D B×D\array{ A\times C & \stackrel{f\times C}{\to} & B \times C \\ ^\mathllap{A\times g} \downarrow & & \downarrow^\mathrlap{B\times g} \\ A\times D & \underset{f\times D}{\to} & B\times D }

    In partiular the second square in 6 and the first square on the page are instances of this.

    • CommentRowNumber16.
    • CommentAuthorFinnLawler
    • CommentTimeNov 8th 2015

    δ\delta – and hence δ *\delta^* – splits, and thus δ *\delta^* is full and faithful.

    I don’t think this is necessarily true unless the ‘pseudo-section’ of δ *\delta^* is also its left adjoint. For example, take the unique functor from the free parallel pair P=•⇉•\mathbf{P} = \bullet \rightrightarrows \bullet to the terminal category. It has a section, because P\mathbf{P} 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 δ *\delta^* takes a presheaf P:(A×A) op→SetP \colon (A \times A)^{op} \to Set to the presheaf a↦P(a,a)a \mapsto P(a,a) on A. For a transformation α:δ *P⇒δ *P′\alpha \colon \delta^*P \Rightarrow \delta^*P', i.e.~a natural family α a:P(a,a)→P′(a,a)\alpha_a \colon P(a,a) \to P'(a,a), there doesn’t seem to be any good reason why it should come from a unique transformation P⇒P′P \Rightarrow P'. You can cook up counterexamples if you take A to be the arrow category 0→10 \to 1, for example, so that P is a commuting square in Set and δ *P\delta^* P is the morphism both of its sides are equal to. A transformation like α\alpha looks like this:

    P00 →α 0 P′00 ↓ ↓ P11 →α 1 P′11 \array{ P 0 0 & \stackrel{\alpha_0}{\to} & P' 0 0 \\ \downarrow & & \downarrow \\ P 1 1 & \stackrel{\alpha_1}{\to} & P' 1 1 }

    and to lift it to a transformation P⇒P′P \Rightarrow P' is to give functions P01→P′01P 0 1 \to P' 0 1 and P10→P′10P 1 0 \to P' 1 0 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 α\alpha.

    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’ :| ).

    • CommentRowNumber17.
    • CommentAuthorMike Shulman
    • CommentTimeNov 8th 2015

    The possible failure of BC for squares of type (3) is an important plot point in this paper.

    • CommentRowNumber18.
    • CommentAuthorZhen Lin
    • CommentTimeNov 8th 2015

    Since δ\delta is a split monomorphism, δ *\delta^* is essentially surjective on objects. In the poset case, that implies the unit is an isomorphism, i.e. ∃ δ\exists_\delta is fully faithful.

    • CommentRowNumber19.
    • CommentAuthorJonasFrey
    • CommentTimeNov 8th 2015

    Ooops, I got (3) totally wrong! Not only did I falsely assume that functors that have pseudo left inverses are full and faithful, i also mixed up left and right … (the exists part would have to be full and faithful, not the reindexing part).

    Thanks for your comments, Finn and Mike.

    Now I’m wondering if (3) is at least redundant in the posetal case …

    • CommentRowNumber20.
    • CommentAuthorFinnLawler
    • CommentTimeNov 9th 2015

    I think there is a mistake in the derivation for type-(1) squares, where in the last step you have

    δ *∃ f×Bπ 1 *⟨id,f⟩ *ψ≅δ *∃ f×Bψ.\delta^*\exists_{f\times B}\pi_1^*\langle id,f\rangle^*\psi \cong \delta^*\exists_{f\times B}\psi\,.

    It’s not generally true that π 1 *⟨id,f⟩ *≅1\pi_1^* \langle id, f \rangle^* \cong 1, 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 ∃ f\exists_f. 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 s:A×B→B×As \colon A \times B \to B \times A 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.

    • CommentRowNumber21.
    • CommentAuthorJonasFrey
    • CommentTimeNov 9th 2015
    • (edited Nov 9th 2015)

    You are right again Finn, I really wasn’t very careful when I wrote this.

    Concerning (3), I think I have a proof that it’s for free at least in the posetal case. This is because my wrong assumption that ‘split adjunctions are reflections’ is true for adjunctions between posets/preorders. Indeed, assume that f⊣g:B→Af\dashv g : B\to A and h:A→Bh:A \to B with gh≅id Agh\cong id_A. Then we have gfg≅ggfg \cong g, and multiplying by hh on the right we get gf≅idgf\cong\id, i.e. the adjunction is a coreflection and its unit an isomorphism. In the case of ∃ δ⊣δ *\exists_\delta\dashv\delta^* this shows that δ *∃ δ≅id\delta^*\exists_\delta\cong\id (since δ *\delta^* is split by π 1 *\pi_1^*), which is precisely the BC condition for square (3).

    On the other hand, (3) is not automatic for general hyperdoctrines, as can be seen by the fibration of group actions over groups (which satisfies (2) if I’m not mistaken). Presheaves over categories is also a counterexample, but it’s not a hyperdoctrine in the sense of Seely or the nlab since exponentiation is not stable under reindexing (exponential objects in presheaf categories are not computed pointwise).

    Regarding (1), my proof is clearly wrong, but I don’t have a counterexample, and I still hope that it follows from (2).

    I agree with your other remarks and don’t have an answer to your question.

    • CommentRowNumber22.
    • CommentAuthorZhen Lin
    • CommentTimeNov 9th 2015
    • (edited Nov 12th 2015)

    Observe that the Frobenius condition already implies

    ∃ fP≅∃ d 0(d 1 *P∧(f×id B) *∃ Δ⊤ B)\exists_f P \cong \exists_{d_0} (d_1^* P \wedge (f \times id_B)^* \exists_\Delta \top_B)

    where d 0:A×B→Bd_0 : A \times B \to B and d 1:A×B→Ad_1 : A \times B \to A are the respective projections. (I borrow the notion from simplicial objects.) In words, ∃ f\exists_f can be defined “naïvely” using existential quantification and equality; in symbols:

    (∃ fP)(b)≅∃(a:A.P(a)∧(f(a)=b))(\exists_f P)(b) \cong \exists (a : A . P (a) \wedge (f (a) = b))

    Thus, the Beck–Chevalley condition for product projections should be enough to prove everything we expect from existential logic.

    For instance, the Beck–Chevalley condition for pullback squares of type (1) translates to

    ∃(a:A.R(a,f(a))∧(f(a)=b′))≅∃(a:A,b:B.R(a,b)∧(f(a)=b′)∧(b=b′))\exists (a : A . R (a, f (a)) \wedge (f (a) = b')) \cong \exists (a : A , b : B . R (a, b) \wedge (f (a) = b') \wedge (b = b'))

    and this is surely derivable in existential logic, no?

    • CommentRowNumber23.
    • CommentAuthorFinnLawler
    • CommentTimeNov 9th 2015

    Lawvere shows that Frobenius reciprocity implies

    ∃ fP≅∃ d 0(d 1 *P∧(A,f) !⊤ A)\exists_f P \cong \exists_{d_0} (d_1^* P \wedge (A, f)_!\top_A)

    and then uses the type-(1) BCC to show

    (A,f) !⊤ A≅(A,f) !f *⊤ B≅(f×B) *d !⊤ A.(A,f)_! \top_A \cong (A, f)_! f^* \top_B \cong (f \times B)^* d_! \top_A\,.

    How do you derive

    ∃ fP≅∃ d 0(d 1 *P∧(f×id B) *∃ Δ⊤ B)\exists_f P \cong \exists_{d_0} (d_1^* P \wedge (f \times id_B)^* \exists_\Delta \top_B)

    from Frobenius alone?

    • CommentRowNumber24.
    • CommentAuthorZhen Lin
    • CommentTimeNov 9th 2015

    Let QQ be an arbitrary predicate on BB.

    1. Suppose ∃ d 0(d 1 *P∧(f×id B) *∃ Δ⊤ B)≤Q\exists_{d_0} (d_1^* P \wedge (f \times id_B)^* \exists_\Delta \top_B ) \le Q.
    2. Then d 1 *P∧(f×id B) *∃ Δ⊤ B≤d 0 *Qd_1^* P \wedge (f \times id_B)^* \exists_\Delta \top_B \le d_0^* Q.
    3. Then P∧⟨f,f⟩ *∃ Δ⊤ B≤f *QP \wedge \langle f, f \rangle^* \exists_\Delta \top_B \le f^* Q (by applying ⟨id A,f⟩ *\langle id_A, f \rangle^* to the previous inequality).
    4. Then P∧f *Δ *∃ Δ⊤ B≤f *QP \wedge f^* \Delta^* \exists_\Delta \top_B \le f^* Q.
    5. Then P≤f *QP \le f^* Q.

    Conversely:

    1. Suppose P≤f *QP \le f^* Q.
    2. Then d 1 *P≤d 1 *f *Qd_1^* P \le d_1^* f^* Q.
    3. Then d 1 *P∧(f×id B) *∃ Δ⊤ B≤d 1 *f *Q∧(f×id B) *∃ Δ⊤ Bd_1^* P \wedge (f \times id_B)^* \exists_\Delta \top_B \le d_1^* f^* Q \wedge (f \times id_B)^* \exists_\Delta \top_B.
    4. Then d 1 *P∧(f×id B) *∃ Δ⊤ B≤(f×id B) *(d 1 *Q∧∃ Δ⊤ B)d_1^* P \wedge (f \times id_B)^* \exists_\Delta \top_B \le (f \times id_B)^* (d_1^* Q \wedge \exists_\Delta \top_B).
    5. Then d 1 *P∧(f×id B) *∃ Δ⊤ B≤(f×id B) *(∃ Δ(⊤ B∧Δ *d 1 *Q))d_1^* P \wedge (f \times id_B)^* \exists_\Delta \top_B \le (f \times id_B)^* (\exists_\Delta (\top_B \wedge \Delta^* d_1^* Q)) (by Frobenius reciprocity).
    6. Then d 1 *P∧(f×id B) *∃ Δ⊤ B≤(f×id B) *(∃ ΔQ)d_1^* P \wedge (f \times id_B)^* \exists_\Delta \top_B \le (f \times id_B)^* (\exists_\Delta Q).
    7. Then d 1 *P∧(f×id B) *∃ Δ⊤ B≤(f×id B) *(∃ Δ(⊤ B∧Δ *d 0 *Q))d_1^* P \wedge (f \times id_B)^* \exists_\Delta \top_B \le (f \times id_B)^* (\exists_\Delta (\top_B \wedge \Delta^* d_0^* Q)).
    8. Then d 1 *P∧(f×id B) *∃ Δ⊤ B≤(f×id B) *(d 0 *Q∧∃ Δ⊤ B)d_1^* P \wedge (f \times id_B)^* \exists_\Delta \top_B \le (f \times id_B)^* (d_0^* Q \wedge \exists_\Delta \top_B) (by Frobenius reciprocity).
    9. Then d 1 *P∧(f×id B) *∃ Δ⊤ B≤(f×id B) *d 0 *Qd_1^* P \wedge (f \times id_B)^* \exists_\Delta \top_B \le (f \times id_B)^* d_0^* Q.
    10. Then d 1 *P∧(f×id B) *∃ Δ⊤ B≤d 0 *Qd_1^* P \wedge (f \times id_B)^* \exists_\Delta \top_B \le d_0^* Q.
    11. Then ∃ d 0(d 1 *P∧(f×id B) *∃ Δ⊤ B)≤Q\exists_{d_0} (d_1^* P \wedge (f \times id_B)^* \exists_\Delta \top_B ) \le Q.

    Thus ∃ d 0(d 1 *P∧(f×id B) *∃ Δ⊤ B)\exists_{d_0} (d_1^* P \wedge (f \times id_B)^* \exists_\Delta \top_B ) has the required universal property.

    • CommentRowNumber25.
    • CommentAuthorFinnLawler
    • CommentTimeNov 10th 2015

    Very interesting!

    • CommentRowNumber26.
    • CommentAuthorZhen Lin
    • CommentTimeNov 10th 2015
    • (edited Nov 16th 2015)

    Back to pullback squares of type (1) again. By the observation in #22,

    ∃ ⟨id A,f⟩⊤ A≅(f×id B) *∃ Δ⊤ B\exists_{\langle id_A, f \rangle} \top_A \cong (f \times id_B)^* \exists_\Delta \top_B

    which is actually an instance of a Beck–Chevalley condition because ⊤ A≅f *⊤ B\top_A \cong f^* \top_B. This suffices to prove:

    ∃ f⟨id Af⟩ *R≅Δ *∃ f×id BR\exists_f \langle id_A f \rangle^* R \cong \Delta^* \exists_{f \times id_B} R

    Indeed, since Δ:B→B×B\Delta : B \to B \times B is a split monomorphism, ∃ Δ\exists_\Delta is fully faithful, so it is enough to check that

    ∃ Δ∃ f⟨id Af⟩ *R≅∃ ΔΔ *∃ f×id BR\exists_\Delta \exists_f \langle id_A f \rangle^* R \cong \exists_\Delta \Delta^* \exists_{f \times id_B} R

    but

    ∃ Δ∃ f⟨id Af⟩ *R≅∃ f×id B∃ ⟨id A,f⟩⟨id A,f⟩ *R\exists_\Delta \exists_f \langle id_A f \rangle^* R \cong \exists_{f \times id_B} \exists_{\langle id_A, f \rangle} \langle id_A, f \rangle^* R

    and, by Frobenius reciprocity:

    ∃ f×id B∃ ⟨id A,f⟩⟨id A,f⟩ *R≅∃ f×id B(∃ ⟨id A,f⟩⊤ A∧R)\exists_{f \times id_B} \exists_{\langle id_A, f \rangle} \langle id_A, f \rangle^* R \cong \exists_{f \times id_B} (\exists_{\langle id_A, f \rangle} \top_A \wedge R)

    Then, using the observation above,

    ∃ f×id B(∃ ⟨id A,f⟩⊤ A∧R)≅∃ f×id B((f×id B) *∃ Δ⊤ B∧R)\exists_{f \times id_B} (\exists_{\langle id_A, f \rangle} \top_A \wedge R) \cong \exists_{f \times id_B} ((f \times id_B)^* \exists_\Delta \top_B \wedge R)

    and, by Frobenius reciprocity (twice),

    ∃ f×id B((f×id B) *∃ Δ⊤ B∧R)≅∃ Δ⊤ B∧∃ f×id BR≅∃ ΔΔ *∃ f×id BR\exists_{f \times id_B} ((f \times id_B)^* \exists_\Delta \top_B \wedge R) \cong \exists_\Delta \top_B \wedge \exists_{f \times id_B} R \cong \exists_\Delta \Delta^* \exists_{f \times id_B} R

    as required.

    Of course, the above is for the poset/preorder case, but I think it might even work for the general case – one just has to check that some diagrams commute.

    • CommentRowNumber27.
    • CommentAuthorFinnLawler
    • CommentTimeNov 11th 2015

    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 f:G→Hf \colon G \to H is a homomorphism and PP is a (right) GG-set then the pushforward f !Pf_!P is Lan f opP\mathrm{Lan}_{f^{op}} P, which works out to be the usual induced representation, given by the set of orbits of the action of GG on H×PH \times P where g⋅(h,p)=(f(g)h,p⋅g −1)g \cdot (h,p) = (f(g) h, p \cdot g^{-1}). Notice that this action will be free if either ff is injective or the action of GG on PP is free. We can count orbits using Burnside’s lemma, and in particular if HH acts freely on QQ then the number of orbits |Q/H|\left| Q / H \right| is |Q|/|H|\left| Q \right| / \left| H \right|.

    Both (1,f)(1,f) and the diagonal dd are split monomorphisms, so the induced actions of GG on G×HG \times H and HH on H×HH \times H are free, and therefore the number of orbits is

    |G×H||G|=|H|=|H×H||H|.\frac{\left| G \times H \right|}{\left|G\right|} = \left|H\right| = \frac{ \left| H \times H \right|}{\left| H \right|}\,.

    So it’s still possible that this BC condition holds. (Note that pulling d !Pd_! P back along (f×1)(f \times 1) doesn’t change the number of orbits.)

    For the other type-(1) BC condition, let PP be a right G×HG \times H-set. For f !(1,f) *Pf_!(1,f)^* P we have an action of GG on H×PH \times P given by g⋅(h,p)=(f(g)h,p⋅(g,f(g)) −1)g \cdot (h,p) = \big(f(g) h, p \cdot (g, f(g))^{-1}\big). A fixed point is one where f(g)=1f(g) = 1 and p⋅(g −1,1)=pp \cdot (g^{-1}, 1) = p, so the set (H×P) g(H \times P)^g is H×P (g,1)H \times P^{(g,1)} if f(g)=1f(g) = 1 and empty otherwise. Therefore the number of orbits is

    |H|∑ g∈kerf|P (g,1)||G|. \frac{\left| H \right| \sum_{g \in \ker f} \left| P^{(g,1)} \right|}{\left| G \right|}\,.

    For d *(f×1) !Pd^*(f \times 1)_! P we can ignore the d *d^* as before, so we have an action of G×HG \times H on H×H×PH \times H \times P where (g,h)⋅(h 0,h 1,p)=(f(g)h 0,hh 1,p⋅(g,h) −1)(g,h) \cdot (h_0, h_1, p) = (f(g) h_0, h h_1, p \cdot (g,h)^{-1}). (You can see where this is going.) A fixed point has f(g)=1f(g) = 1, h=1h = 1 and p⋅(g −1,1)=1p \cdot (g^{-1}, 1) = 1, so the set of them is H×H×P (g,1)H \times H \times P^{(g,1)} if f(g)=1f(g) = 1 and h=1h = 1 and empty otherwise. So in fact we get the same formula as before for the number of orbits, after cancelling a factor of |H|\left| H \right|.

    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.

    • CommentRowNumber28.
    • CommentAuthorMike Shulman
    • CommentTimeNov 12th 2015

    Type-(1) BC conditions hold for diagrams on groupoids, because those squares are actually always homotopy pullbacks as well as pullbacks.

    • CommentRowNumber29.
    • CommentAuthorJonasFrey
    • CommentTimeNov 16th 2015

    Coming back to this discussion, it seems that condition (1) follows from (2) in the posetal case, but the verdict is still out in the “proof-relevant” setting. Like Finn I tried to find a counterexample, but didn’t come up with anything.

    @Mike (28): That sounds very interesting. to make your argument formal (and get a proof that (1) holds in presheaves over groupoids), would one view the fibration of presheaves over groupoids as a subfibration of something like the codomain fibration of the infinity-topos of groupoids?

    @Zhen Lin (26): You say that “… I think it might even work for the general case – one just has to check that some diagrams commute.” I’m a bit sceptical about that because you use the argument that existential quantification along split monos is fully faithful, that led me to the false proof of BC for (3).

    And finally I’m still confused about orientation of squares. In 15, I claimed that ’it is meant that quantification happens vertically’ in the BC condition, since that’s what Seely does in condition (5’)(ii) on page 7 of his article, but in (20) Finn argues convincingly that the dual condition is the important one. In 26, Zhen Lin shows that condition (1) with vertical quantification follows from (2) in the posetal case. does the dual one follow as well? using my intuitions on internal logic I would think so, but i’ve been wrong before …

    • CommentRowNumber30.
    • CommentAuthorZhen Lin
    • CommentTimeNov 16th 2015
    • (edited Nov 16th 2015)

    Yes, in #26 I ended up talking about both of the possible Beck–Chevalley conditions on the same pullback square. I don’t really know what the significance of that is.

    As for ∃ Δ\exists_\Delta – yes, it may fail to be fully faithful, but it is always conservative, and that is the reason why we just have to check that some diagrams commute. But we can be lazy in the posetal case.

    • CommentRowNumber31.
    • CommentAuthorJonasFrey
    • CommentTimeNov 16th 2015

    Looking at Seely’s article, I came across this amusing passage (top of page 25, talking about presheaves over groupoids):

    … Its logic is perfectly well behaved as far as the equality-free part is concerned, but the logic of equality does show some curiosities. Clearly t=tt=t is quite different from ⊤\top, and so can be an important assumption in a derivation, for instance.

    In hindsight it looks very much like he’s talking about identity types …

    But unlike in what we call ’models of homotopy type theory’ today, the non-uniqueness of equality proofs manifests itself in a failure of BC for squares of type (3) here.

    • CommentRowNumber32.
    • CommentAuthorMike Shulman
    • CommentTimeNov 17th 2015

    @Jonas #29: it’s not necessary to do anything so high-powered. Squares of type (1) are homotopy pullbacks in the classical sense that the map from the pullback to the canonical homotopy pullback is an equivalence. Then just prove that canonical homotopy pullback squares satisfy BC, and that equivalences of groupoids induce equivalences of fiber categories.

    And #31: well, that BC does also fail in models of HoTT, for the same reasons. Although I guess in HoTT we don’t directly assert Σ\Sigma and Π\Pi along non-fibrations, is that what you mean?

    • CommentRowNumber33.
    • CommentAuthorJonasFrey
    • CommentTimeNov 17th 2015
    • (edited Nov 17th 2015)

    well, that BC does also fail in models of HoTT, for the same reasons. Although I guess in HoTT we don’t directly assert Σ\Sigma and Π\Pi along non-fibrations, is that what you mean?

    Ah yes, you’re right. I was confused by the fact that models of HoTT seem to postulate BC for all pullbacks, but that still excludes squares like (3) since the diagonals are not fibrations in non-trivial cases.

    • CommentRowNumber34.
    • CommentAuthorFinnLawler
    • CommentTimeNov 20th 2015

    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 ∃ d 0(d 1 *P∧(f×id B) *∃ Δ⊤ B)\exists_{d_0} (d_1^* P \wedge (f \times id_B)^* \exists_\Delta \top_B ) translates to (something isomorphic to) the composite of P with, or pullback of P along, the dual f ∘f^\circ of ff as defined in ibid., proposition 3.8. That this is canonically isomorphic to f !Pf_! P should then follow from the fact that f⊣f ∘f \dashv f^\circ (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.

    • CommentRowNumber35.
    • CommentAuthorFinnLawler
    • CommentTimeDec 8th 2015

    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.

1 to 35 of 35

  1.