Not signed in

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

• Username
• Password
• Remember me

• Sign in using OpenID
• Remember me

• Forgot your password?
• Apply for membership

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex-geometry computable-mathematics computer-science constructive cosmology definitions deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration 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 k-theory kan lie-theory limit limits linear linear-algebra locale localization logic mathematics measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology newpage nlab nonassociative noncommutative noncommutative-geometry number-theory object 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 string string-theory subobject superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory type type-theory universal variational-calculus

1. • CommentRowNumber1.
   • CommentAuthorUrs
   • CommentTimeMar 27th 2012
   • PermaLink
   Author: Urs
   Format: MarkdownItexat _[[Beck-Chevalley condition]]_ I have added an Examples-section _[Pullbacks of opfibrations](http://ncatlab.org/nlab/show/Beck-Chevalley+condition#PullbacksOfOpfibrations)_ with statement and proof that the diagram of presheaves induced by a pullback of a small obfibration satisfies Beck-Chevalley.

   at Beck-Chevalley condition I have added an Examples-section Pullbacks of opfibrations with statement and proof that the diagram of presheaves induced by a pullback of a small obfibration satisfies Beck-Chevalley.

2. • CommentRowNumber2.
   • CommentAuthorUrs
   • CommentTimeMay 15th 2012
   • PermaLink
   Author: Urs
   Format: MarkdownItexAdded to _[[Beck-Chevalley condition]]_ a remark on its interpretation _[In logic / type theory](http://ncatlab.org/nlab/show/Beck-Chevalley+condition#InTypeTheory)_. (This can be said more nicely and in more detail, but that's what I have for the moment.)

   Added to Beck-Chevalley condition a remark on its interpretation In logic / type theory.

   (This can be said more nicely and in more detail, but that’s what I have for the moment.)

3. • CommentRowNumber3.
   • CommentAuthorUrs
   • CommentTimeDec 7th 2013
   • (edited Dec 7th 2013)
   • PermaLink
   Author: Urs
   Format: MarkdownItexI have added the Beck-Chevalley-setup as an example to _[[mate]]_, just to have the cross-link. Here is a **Question**: Suppose we have a composite diagram of [[Wirthmüller contexts]] of the form $$ \array{ &&&& \mathcal{C} \\ && & {}^{\mathllap{p}_1}\swarrow && \searrow^{\mathrlap{p_2}} \\ && \mathcal{A} && && \mathcal{B} \\ & {}^{\mathllap{i_1}}\swarrow && \searrow^{\mathrlap{i_2}} && {}^{\mathllap{i_3}}\swarrow && \searrow^{\mathrlap{i_4}} \\ \mathcal{X} && && \mathcal{Y} && && \mathcal{Z} } $$ Then we get functors $$ \mathcal{X} \stackrel{F_1 \coloneqq (i_1)_!(i_2)^\ast}{\leftarrow} \mathcal{Y} \stackrel{F_2 \coloneqq (i_3)_!(i_4)^\ast}{\leftarrow} \mathcal{Z} $$ and the mate construction for the top square in the above diagram gives a composition transformation (at least if the BC condition holds) $$ F_1 \circ F_2 \Rightarrow F_3 $$ where $$ F_3 \coloneqq (i_1 p_1)_! (i_4 p_2)^\ast \,. $$ Further describing this kind of situation for longer sequences of spans of Wirthmüller contexts, which I will refrain from here in this comment, yields a "monad-oid" and its Kleisli composition, as discussed in [another thread](http://nforum.mathforge.org/discussion/5540/kleisli-category-for-a-monadoid/?Focus=43849#Comment_43849). Does this have an established name for the above kind of situation?

   I have added the Beck-Chevalley-setup as an example to mate, just to have the cross-link.

   Here is a Question:

   Suppose we have a composite diagram of Wirthmüller contexts of the form

   $$\array{ &&&& \mathcal{C} \\ && & {}^{\mathllap{p}_1}\swarrow && \searrow^{\mathrlap{p_2}} \\ && \mathcal{A} && && \mathcal{B} \\ & {}^{\mathllap{i_1}}\swarrow && \searrow^{\mathrlap{i_2}} && {}^{\mathllap{i_3}}\swarrow && \searrow^{\mathrlap{i_4}} \\ \mathcal{X} && && \mathcal{Y} && && \mathcal{Z} }$$

   Then we get functors

   $$\mathcal{X} \stackrel{F_1 \coloneqq (i_1)_!(i_2)^\ast}{\leftarrow} \mathcal{Y} \stackrel{F_2 \coloneqq (i_3)_!(i_4)^\ast}{\leftarrow} \mathcal{Z}$$

   and the mate construction for the top square in the above diagram gives a composition transformation (at least if the BC condition holds)

   $$F_1 \circ F_2 \Rightarrow F_3$$

   where

   $$F_3 \coloneqq (i_1 p_1)_! (i_4 p_2)^\ast \,.$$

   Further describing this kind of situation for longer sequences of spans of Wirthmüller contexts, which I will refrain from here in this comment, yields a “monad-oid” and its Kleisli composition, as discussed in another thread.

   Does this have an established name for the above kind of situation?

4. • CommentRowNumber4.
   • CommentAuthorMike Shulman
   • CommentTimeDec 8th 2013
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexTo check that I'm understanding: is it right that the canonical transformation is actually $F_3 \Rightarrow F_1 \circ F_2$, and the BC condition makes it invertible (and hence in particular can go the other direction)?

   To check that I’m understanding: is it right that the canonical transformation is actually $F_3 \Rightarrow F_1 \circ F_2$, and the BC condition makes it invertible (and hence in particular can go the other direction)?

5. • CommentRowNumber5.
   • CommentAuthorUrs
   • CommentTimeDec 8th 2013
   • PermaLink
   Author: Urs
   Format: MarkdownItexYes.

   Yes.

6. • CommentRowNumber6.
   • CommentAuthorUrs
   • CommentTimeSep 1st 2016
   • PermaLink
   Author: Urs
   Format: MarkdownItexI have added a _[[Beck-Chevalley condition]]_ in the section _[Examples -- For categories of presheaves](https://ncatlab.org/nlab/show/Beck-Chevalley+condition#PullbacksOfOpfibrations)_ a pointer to Joyal's document on quasicategories, for the corresponding statement. What would be a quick example to show that the condition that the original square in this case be not just a pullback, but a pullback of opfibrations is a necessary condition? Then I did a little reorganization of the entry: There used to be a subsection "Bibrations" under the section "Examples". This subsection had its own sub-sub-section "Examples". So I fixed that: I moved the paragraphs on BC for bifibrations to the Definition-section (maybe some haronization is now in order there), and merged its list of Examples into the general list of examples.

   I have added a Beck-Chevalley condition in the section Examples – For categories of presheaves a pointer to Joyal’s document on quasicategories, for the corresponding statement.

   What would be a quick example to show that the condition that the original square in this case be not just a pullback, but a pullback of opfibrations is a necessary condition?

   Then I did a little reorganization of the entry: There used to be a subsection “Bibrations” under the section “Examples”. This subsection had its own sub-sub-section “Examples”.

   So I fixed that: I moved the paragraphs on BC for bifibrations to the Definition-section (maybe some haronization is now in order there), and merged its list of Examples into the general list of examples.

7. • CommentRowNumber7.
   • CommentAuthorMike Shulman
   • CommentTimeSep 1st 2016
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItex> What would be a quick example to show that the condition that the original square in this case be not just a pullback, but a pullback of opfibrations is a necessary condition? $C=$ the [[interval category]] $(0\to 1)$, $D=C'=$ the terminal category, $\phi=0$, $\alpha=1$, so that $D'=\emptyset$, but $\alpha^*\phi_!$ is the identity functor.

   What would be a quick example to show that the condition that the original square in this case be not just a pullback, but a pullback of opfibrations is a necessary condition?

   $C=$ the interval category $(0\to 1)$, $D=C'=$ the terminal category, $\phi=0$, $\alpha=1$, so that $D'=\emptyset$, but $\alpha^*\phi_!$ is the identity functor.

8. • CommentRowNumber8.
   • CommentAuthorUrs
   • CommentTimeSep 1st 2016
   • PermaLink
   Author: Urs
   Format: MarkdownItexThanks! I have added that to the entry.

   Thanks! I have added that to the entry.

9. • CommentRowNumber9.
   • CommentAuthorDavid_Corfield
   • CommentTimeAug 6th 2017
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexI added Mackey's restriction formula as an example. Presumably that's something that could be readily shown in HoTT. Has there been any further work in HoTT concerning groups actions, etc.? Something seemed to have started a while ago, recall the [regular action thread](https://nforum.ncatlab.org/discussion/7095/regular-action/). By the way, why does Beck-Chevalley not appear in the HoTT book?

   I added Mackey’s restriction formula as an example.

   Presumably that’s something that could be readily shown in HoTT. Has there been any further work in HoTT concerning groups actions, etc.? Something seemed to have started a while ago, recall the regular action thread.

   By the way, why does Beck-Chevalley not appear in the HoTT book?

10. • CommentRowNumber10.
    • CommentAuthorMike Shulman
    • CommentTimeAug 6th 2017
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItex> Presumably that’s something that could be readily shown in HoTT. Probably, although you'd first need to define some group theory, including colimits of diagrams of abelian groups. > Has there been any further work in HoTT concerning groups actions, etc.? I don't know of any. > By the way, why does Beck-Chevalley not appear in the HoTT book? Where would it go?

    Presumably that’s something that could be readily shown in HoTT.

    Probably, although you’d first need to define some group theory, including colimits of diagrams of abelian groups.

    Has there been any further work in HoTT concerning groups actions, etc.?

    I don’t know of any.

    By the way, why does Beck-Chevalley not appear in the HoTT book?

    Where would it go?

11. • CommentRowNumber11.
    • CommentAuthorDavid_Corfield
    • CommentTimeAug 7th 2017
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItexI guess I thought commutativity of substitution and dependent sum at least would show up somewhere.

    I guess I thought commutativity of substitution and dependent sum at least would show up somewhere.

12. • CommentRowNumber12.
    • CommentAuthorMike Shulman
    • CommentTimeAug 7th 2017
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexThe nice thing about type theory is that commutativity of everything with substitution is built into the notation, so you don't even need to mention it. Of course it has to be mentioned when constructing categorical semantics, but the HoTT book is always working internally to type theory.

    The nice thing about type theory is that commutativity of everything with substitution is built into the notation, so you don’t even need to mention it. Of course it has to be mentioned when constructing categorical semantics, but the HoTT book is always working internally to type theory.

13. • CommentRowNumber13.
    • CommentAuthorDavid_Corfield
    • CommentTimeAug 7th 2017
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItexAh yes, of course. Thanks.

    Ah yes, of course. Thanks.