Downcasing the Beck-Chevalley ConditionQuick index:
1. Intro: BCC ============= 2. Downcasing Beck-Chevalley ============================ 3. A notation for subobjects ============================ Set^>->, or Sub(Set), is the category of subobjects of Set. Our favorite objects in Set^>-> are the ``canonical inclusions'', or ``propositions'': {a:A|P(a)} >-> A Let's write them with a double bar: {a:A||P(a)} := {a:A|P(a)} >-> A A morphism {a:A||P(a)} -> {a:A||Q(a)} is a commutative square: {a:A|P(a)} -> {a:A|Q(a)} v v | | v v A ----------> A we're not saying what are the horizontal morphisms in this square - this means: ``they're the obvious ones'' - the identity below, and the only possible inclusion above. The existence of a morphism {a:A||P(a)} -> {a:A||Q(a)} corresponds to: ∀a:A.P(a)⊃Q(a) or, in ``sequents'', or ``judgments'' (as in type theory), to: a:A;P(a)|-Q(a). 4. Long names for variables =========================== This notation for a subobject of A×B, {(a,b):A×B||R(a,b)} makes sense; let's allow long names for variables - then ``a,b'' is a good name (indeed, the default one!) for a variable ranging over A×B. We have an obvious morphism A×B->A - the projection. We will downcase it to: a,b |---> a and let's use ``a|P(a)'' as the name for a variable ranging over {a:A|P(a)}... now we can downcase the diagram for {a:A||P(a)} -> {a:A||Q(a)} as: {a:A|P(a)} -> {a:A|Q(a)} a|P(a) |--> a|Q(a) v v / / | | | | v v v v A ----------> A a |--------> a 5. Downcasing maps between subobjects ===================================== Sub^>-> = Sub(Set) is a fibration. The projection functor takes subobjects to their codomains. {a,b:A×B|R(a,b)} -> {a:A|Q(a)} a|P(a) |--> a|Q(a) v v - - | | | | v v v v A -------------> A a |-------> a and we can also downcase the *morphism* {a:A||P(a)} -> {a:A||Q(a)} all at once to: a||P(a) |--> a||Q(a) Note (and this is a wicked trick!) that /sometimes/ a downcased morphism x|->y will correspond to a map of points - sometimes not (details, examples). 6. Downcasing propositions ========================== A proposition P(b,c) over variables b,c is a subobject in a fibration, over B×C. Here's how (expansions): P(b,c) b,c||P(b,c) {b,c||P(b,c)} {(b,c)∈B×C||P(b,c)} b,c b,c B×C B×C P(b,c) b,c||P(b,c) {b,c||P(b,c)} {(b,c)∈B×C||P(b,c)} || || - - || || | | \/ \/ v v b,c b,c B×C B×C /b,c|P(b,c)\ /{b,c|P(b,c)}\ /{(b,c)∈B×C||P(b,c)}\ | / | | v | | v | | | | | | | | | | | v | | v | | v | \ b,c / \ B×C / \ B×C / || - - || | | \/ v v b,c B×C B×C 7. BCC: the categorical details =============================== g'*P |------------------> ∃f'g'*P | ^ | | \ |---> | v \ v g'*f*∃fP <\-> f'*g*∃fP <-----| g*∃fP /\ - ^ \ P |--------------------> ∃fP \ | \ - \ | <---| \ | id - v -v f*∃fP <------------------| ∃fP Ax_{B}C -----------------> B \ __| f' \ g' \ \ g v v A ---------------------> C f For any pullback square like the one in the diagram, for any object P over A, the morphism ∃f'g'*P -> g*∃fP constructed as the diagram indicates is an iso. |