Notes on other downcasings

These are notes on downcasings that I have not completed yet. They are for personal use; they contain errors.

• 1. (Right) Kan extensions
• 2. Enriched categories
• 3. Polynomials
• 4. Geometric morphisms
• 5. Geometric morphisms: simple examples
• 6. Germs and sections
• 7. Geometric morphisms: examples with sheaves
• 8. Filterpowers

1. (Right) Kan extensions
=========================
A downcasing for the notation in CWM (sec X.3, p.232):

          C
 	  ^ \\		         m^K ==========> m^KS
 	  |  \\      		  /\ \\            -
 	  |   \\ S   S		  ||  \\           | σ
 	  |  R \\    vσ		  ||   \\          v
 	K |     \\   R		  ||    \======> m^KR
 	  |     :\\		  ||               -
 	  |    ε: \\		  ||               | ε
 	  |     v  vv		  ||               v
 	  M -------> A 		  m ============> m^T



               A^K
        A^M <------ A^C

         SK <-------| S          (m=>m^KS) <====== (m^K=>m^KS)
       | |            |   	     -                  -
       | | σK  <--|   | σ 	     |       <--|       |
       | v            v   	     v                  v
  ε·σK | RK <-------| R   	 (m=>m^KR) <====== (m^K=>m^KR)
       | |		      	     -
       | | ε	      		     | (univ)
       v v		      	     v
         T                	 (m=>m^T)


   Nat(SK,T) <--- Nat(S,Ran_K T)
        ε·σK <--| σ

2. Enriched categories
======================
Definition (from SLNM 752):
a category \catC is enriched over \catV
(motivations: FinVec is enriched over itself;
  any small category is enriched over Set)
when its hom-sets have more structure:
for any objects A,B,C of \catC,

     Hom(A,B) × Hom(B,C)    -> Hom(A,C)
   \catV(A,B) ⊗ \catV(B,C)  -> \catV(A,C)
  FinVec(A,B) ⊗ FinVec(B,C) -> FinVec(A,C)

3. Polynomials
==============

4. Geometric morphisms
======================
A geometric morphism, f,
        f
  \tF ------> \tE

is an adjunction:

        f^*         <- "inverse image"
  \tF <------ \tE      (left exact, i.e.
        _|_	        preserves finite limits)
      ------>
        f_*         <- "direct image"

If f^* has a left adjoint -
which is a bit stronger than
preserving finite limits -

        f_!
      ------>
        _|_
  \tF <------ \tE
        f^*

then f is said to be _essential_.

5. Geometric morphisms: simple examples
=======================================

Set -> Set^2:

   A |---> (A,0)       a ======> a;⊥    .
   |         |         -          -
   |  <-->   |	       |   <-->   |
   v         v	       v          v
   B <---| (B,B')      b <====== b;c
   |         |         -          -
   |  <-->   |         |   <-->   |
   v         v         v          v
   D |---> (D,1)       d ======> d;*

  {1} ---> {1,2}



Set^N -> Set:

  (A_i)_{i∈N} |--> Σi:N.A_i      i;a_i ====> i,a_i
       |              |            -           -
       |     <-->     |            |    <->    |
       v              v            v           v
   (B)_{i∈N} <------| B           i;b <======= b
       |              |            -           -
       |     <-->     |            |    <->    |
       v              v            v           v
  (C_i)_{i∈N} |--> Πi:N.C_i      i;c_i ===> i|->c_i

       N -----------> 1

6. Germs and sections
=====================
(Johnstone, sec. 0.24):

  / L(P)\                             /x,a_{⊥_x}\
  |  |  |     L	  		      |    -    |
  | π|  | <------| (U^op|->P(U))      |    |    | <====== (u^op=>a_U)
  |  v  |                |	      |    v    | 	   -
  \  X  /      		 |	      \    x    / 	   |
     |	       		 |	           -		   |
     |	      <--->    	 |	           |       <--->   |
     v	       	   	 |	           v	    	   |
  /  E  \      	   	 |	         / e \	    	   |
  |  |  |      	   	 v	         | - |	    	   v
  | p|  | |----> (U^op|->Γ(E,p)(U))      | | | ========> (u^op=>u|->e)
  |  v  |    Γ 			         | v |
  \  X  /			         \ x /
               L
  esp/(X,T) <------ Set^{T^op}
              _|_
            ------>
               Γ                      .

(Johnstone, sec. 0.25):
                                           shv
  (U^op|->ΓLA(U)) <--| (U^op|->A(U))   (u^op=>u|->x,a_{⊥_x}) <=== (u^op=>a_U)
          |                   |                  -                     -
          |       <-->        |                  |         <-->        |
          v                   v                  v                     v
   (U^op|->B(U)) |---> (U^op|->B(U))        (u^op=>b_U) ========> (u^op=>b_U)
                                                shv
                  ΓL
             <----------
      Shv(X)     _|_     Set^{T^op}
             ---------->
                incl

(Johnstone, sec. 0.26):

  (T^op|->Γ(f^*(L(E)),f^*π)(T)) <--> (U^op|->E(U))

7. Geometric morphisms: examples with sheaves
=============================================

  Shv(X) ----> Shv(Y)

       X ----> Y



             sheafification
  Shv(\C,J) <--------------- Set^{\C^op}
             --------------->
                inclusion

8. Filterpowers
===============
(As in Johnstone's "Topos Theory". pp.319-322)

  n;*_{n∈U}
     /
     |
     v
    n;* ============> * |-> (n|->Ï)|_big |-----------> ⊤            .
       /                 /       /                     /
        \       |-->      \      |                     |
         v                 v     v                     v
         n;Ï[n∈U] =========> (n|->Ï) |-------> Ï[n|->Ï) is big]

    U
    v
    |
    v       L
  1_\tE |------> 1_\tF                    1_\tF
       \              \                     v
      u \     |-->     \ L(u)               | t
         v              v                   v
          Ω_\tE |-----> L(Ω_\tE) -------> Ω_\tF
                   L               \Phi