[INCLUDE TH/speedbar.blogme]
[SETFAVICON dednat4/dednat4-icon.png]
[lua: LR = R ]
[# 
(defun c () (interactive) (find-blogme3-sh0-if "2007dnc-bcc"))
;;    http://angg.twu.net/2007dnc-bcc.html
;; file:///home/edrx/TH/L/2007dnc-bcc.html
#]
[lua:
  -- (eev-math-glyphs-edrx)
  eev_math_glyphs_edrx()
]

[htmlize [J Downcasing the Beck-Chevalley Condition]

[WITHINDEX
[#
 # «.intro:bcc»			(to "intro:bcc")
 # «.downcasing-BCC»		(to "downcasing-BCC")
 # «.notation-for-subobjects»	(to "notation-for-subobjects")
 # «.long-names-for-vars»	(to "long-names-for-vars")
 # «.downcasing-subobject-maps»	(to "downcasing-subobject-maps")
 # «.downcasing-propositions»	(to "downcasing-propositions")
 # «.BCC-categorical-details»	(to "BCC-categorical-details")
 #]
[RULE ----------------------------------------]

[tsec «intro:bcc»  (to ".intro:bcc")
[++N]. Intro: BCC
=================
]

[tsec «downcasing-BCC»  (to ".downcasing-BCC")
[++N]. Downcasing Beck-Chevalley
================================
]

[tsec «notation-for-subobjects»  (to ".notation-for-subobjects")
[++N]. 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).
]

[tsec «long-names-for-vars»  (to ".long-names-for-vars")
[++N]. 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
]

[tsec «downcasing-subobject-maps»  (to ".downcasing-subobject-maps")
[++N]. 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).

]
[tsec «downcasing-propositions»  (to ".downcasing-propositions")
[++N]. 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

]
[tsec «BCC-categorical-details»  (to ".BCC-categorical-details")
[++N]. 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.
]

]

]
[#
 # Local Variables:
 # coding: raw-text-unix
 # modes: (fundamental-mode blogme-mode)
 # End:
#]