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 definitions 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 k-theory lie-theory 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 nlab 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 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: Beck-Chevalley condition

Bottom of Page

1 to 38 of 38

  1.  
    • CommentRowNumber1.
    • CommentAuthorUrs
    • CommentTimeMar 27th 2012

    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.

    • CommentRowNumber2.
    • CommentAuthorUrs
    • CommentTimeMay 15th 2012

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

    • CommentRowNumber3.
    • CommentAuthorUrs
    • CommentTimeDec 7th 2013
    • (edited Dec 7th 2013)

    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

    𝒞 p 1↙ ↘ p 2 𝒜 ℬ i 1↙ ↘ i 2 i 3↙ ↘ i 4 𝒳 𝒴 𝒵 \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

    𝒳←F 1≔(i 1) !(i 2) *𝒴←F 2≔(i 3) !(i 4) *𝒵 \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∘F 2⇒F 3 F_1 \circ F_2 \Rightarrow F_3

    where

    F 3≔(i 1p 1) !(i 4p 2) *. 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?

    • CommentRowNumber4.
    • CommentAuthorMike Shulman
    • CommentTimeDec 8th 2013

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

    • CommentRowNumber5.
    • CommentAuthorUrs
    • CommentTimeDec 8th 2013

    Yes.

    • CommentRowNumber6.
    • CommentAuthorUrs
    • CommentTimeSep 1st 2016

    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.

    • CommentRowNumber7.
    • CommentAuthorMike Shulman
    • CommentTimeSep 1st 2016

    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=C= the interval category (0→1)(0\to 1), D=C′=D=C'= the terminal category, ϕ=0\phi=0, α=1\alpha=1, so that D′=∅D'=\emptyset, but α *ϕ !\alpha^*\phi_! is the identity functor.

    • CommentRowNumber8.
    • CommentAuthorUrs
    • CommentTimeSep 1st 2016

    Thanks! I have added that to the entry.

    • CommentRowNumber9.
    • CommentAuthorDavid_Corfield
    • CommentTimeAug 6th 2017

    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?

    • CommentRowNumber10.
    • CommentAuthorMike Shulman
    • CommentTimeAug 6th 2017

    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?

    • CommentRowNumber11.
    • CommentAuthorDavid_Corfield
    • CommentTimeAug 7th 2017

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

    • CommentRowNumber12.
    • CommentAuthorMike Shulman
    • CommentTimeAug 7th 2017

    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.

    • CommentRowNumber13.
    • CommentAuthorDavid_Corfield
    • CommentTimeAug 7th 2017

    Ah yes, of course. Thanks.

    • CommentRowNumber14.
    • CommentAuthorUrs
    • CommentTimeAug 7th 2022

    The list of references in Beck-Chevalley condition is unsatisfactory. Is there some textbook or similar which reviews/discusses the issue in some generality for a general audience?

    Searching, I have found

    which I have added now to the list. But this is not what I am looking for (it’s too specialized).

    diff, v28, current

    • CommentRowNumber15.
    • CommentAuthorUrs
    • CommentTimeAug 7th 2022

    This is better:

    diff, v28, current

    • CommentRowNumber16.
    • CommentAuthorUrs
    • CommentTimeAug 7th 2022

    added pointer also to

    • Duško Pavlović, Section 1 of: Categorical interpolation: Descent and the Beck-Chevalley condition without direct images, in: Category Theory, Lecture Notes in Mathematics 1488 (1991) [doi:10.1007/BFb0084229, pdf]

    together with this quote:

    The Beck-Chevalley condition has arisen in the theory of descent - as developed from Grothendieck 1959. Jon Beck and Claude Chevalley studied it independently from each another. […] It is conspicuous that neither of them ever published anything on it. [Pavlović 1991, §14]

    diff, v28, current

    • CommentRowNumber17.
    • CommentAuthorUrs
    • CommentTimeAug 7th 2022

    added pointer also to:

    diff, v29, current

    • CommentRowNumber18.
    • CommentAuthorUrs
    • CommentTimeAug 7th 2022
    • (edited Aug 7th 2022)

    finally for discussion in the generality of ∞\infty-categories:

    diff, v30, current

    • CommentRowNumber19.
    • CommentAuthorvarkor
    • CommentTimeSep 22nd 2022

    Added reference to exact square. More generally, it might be preferable to give this condition a more descriptive name, especially when the contribution of Beck to the definition of this condition is disputed (for instance, see the discussion on the categories mailing list in November 2007).

    diff, v32, current

    • CommentRowNumber20.
    • CommentAuthorDmitri Pavlov
    • CommentTimeJan 22nd 2023

    Transferred the content of an answer by Fosco Loregian.

    diff, v35, current

    • CommentRowNumber21.
    • CommentAuthorUrs
    • CommentTimeJan 22nd 2023

    Thanks for the alert that this motivation was missing on the page. I feel like we may have this elsewhere on the nLab, but would have to check (not right now though, am just on my phone in between other thing). There is some more along these lines in “Quantization via Linear Homotopy Types”, but may not expository enough for what we’d want here.

    In any case, I have rewritten the text you dropped, for better clarity. The simple point is that Beck-Chevalley is the condition to make pull-push base change through correspondences functorial under composition of correspondences by fiber product of adjacent legs.

    I would also like to redo the diagrams (pity to use xymatrix and then still show composition from top-right to bottom-left instead of just left to right as usual) but maybe later.

    diff, v36, current

    • CommentRowNumber22.
    • CommentAuthorUrs
    • CommentTimeJan 22nd 2023

    okay, I have now fixed the orientation of the diagrams (here)

    and added also brief mentioning of the other main motivation for Beck-Chevalley as expressing substitution of free variables commuting with quantification over bound variables (here)

    diff, v36, current

    • CommentRowNumber23.
    • CommentAuthorUrs
    • CommentTimeApr 25th 2023

    added pointer to:

    diff, v41, current

    • CommentRowNumber24.
    • CommentAuthorUrs
    • CommentTimeApr 25th 2023

    added pointer to:

    • Robert A. G. Seely, Hyperdoctrines, Natural Deduction and the Beck Condition, Zeitschr. f. math Logik und Grundlagen d. Math. 29 (1983) 505-542 [pdf]

    and

    diff, v41, current

    • CommentRowNumber25.
    • CommentAuthorUrs
    • CommentTimeApr 26th 2023

    added these pointers:

    diff, v42, current

    • CommentRowNumber26.
    • CommentAuthorUrs
    • CommentTimeApr 29th 2023
    • (edited Apr 29th 2023)

    I’d like the entry to state the following fact, if it is true:

    For

    • VV some cosmos for enrichment,

    • S⊂VCatS \subset VCat some sub-1-category of small strict VV-categories

    • C\mathbf{C} a (co)complete closed monoidal VV-category

    then the indexed monoidal VV-category of C\mathbf{C}-valued (co)presheaves on the 𝒳\mathcal{X}s

    (𝒳∈S)↦VFunc(𝒳,C) (\mathcal{X} \in S) \mapsto V Func( \mathcal{X} ,\, \mathbf{C} )

    satisfies Beck-Chevalley.

    In looking through the literature for who might have said this, I find Mike’s Theorem p. 9.3 here, whose proof seems like it claims a general statement of which this is a special case, if I am unwinding the notation correctly.(?)

    • CommentRowNumber27.
    • CommentAuthorUrs
    • CommentTimeMay 1st 2023
    • CommentRowNumber28.
    • CommentAuthorUrs
    • CommentTimeMay 2nd 2023

    added pointer to:

    diff, v44, current

    • CommentRowNumber29.
    • CommentAuthorUrs
    • CommentTimeMay 3rd 2023

    I have spelled out more details in the Examples-section (here) on BC for pull-push of general functor categories through pullback diagrams of opfibrations.

    diff, v45, current

    • CommentRowNumber30.
    • CommentAuthorUrs
    • CommentTimeMay 3rd 2023
    • (edited May 3rd 2023)

    To that same section I have added a remark (here) that the opfibrancy condition is to ensure that the pullback presents a 2-pullback/homotopy-pullback.

    diff, v45, current

    • CommentRowNumber31.
    • CommentAuthorUrs
    • CommentTimeMay 3rd 2023

    made fully explicit (here) the elementary example of Beck-Chevalley for images/preimages of sets — because it’s fun and because it gives already half of the proof of Beck-Chevalley for presheaf categories.

    diff, v47, current

    • CommentRowNumber32.
    • CommentAuthorUrs
    • CommentTimeMay 3rd 2023

    spelled out (here) a simple special case of Beck-Chevalley for enriched functor categories

    diff, v49, current

    • CommentRowNumber33.
    • CommentAuthorUrs
    • CommentTimeMay 19th 2023

    In the (stub) section “Motivation – From logic and type theory” (here) I added more explicit pointers to the references, including page and section number .

    diff, v51, current

    • CommentRowNumber34.
    • CommentAuthorUrs
    • CommentTimeMay 19th 2023

    added pointer to:

    diff, v51, current

    • CommentRowNumber35.
    • CommentAuthorUrs
    • CommentTimeMay 19th 2023

    and pointer to:

    diff, v51, current

  36. fixed the links to my como paper and maps II. (sorry, royal holloway kept my page for years after i left but recently they removed them and these links died. i will try to fix them.)

    dusko

    diff, v53, current

    • CommentRowNumber37.
    • CommentAuthorUrs
    • CommentTimeNov 8th 2023

    made more explicit (here) the first step in the proof of Beck-Chevalley for functor categories.

    diff, v58, current

  38. Make duality of Beck-Chevalley squares explicit, and make BCForPresheavesOnPullbacksOfOpfibrations precise.

    diff, v60, current

1 to 38 of 38

  1.