Downcasing the Beck-Chevalley Condition

• 1. Intro: BCC
• 2. Downcasing Beck-Chevalley
• 3. A notation for subobjects
• 4. Long names for variables
• 5. Downcasing maps between subobjects
• 6. Downcasing propositions
• 7. BCC: the categorical details

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.