(1-) Category Theory
# pos
Unlike a set, A category has objects and morphisms.
Category pos has unique forall x y, x $ \to $ y is unique.
e.g.
pos = { {1, 2, 3}, { $ 1 _ 1 $ , $ 1 _ 2 $ , $ 1 _ 3 $ , 1 $ \to $ 2, 2 $ \to $ 3, 1 $ \to $ 3, }}.
A category C is a family of End, Hom sets.
- Obj
- end
- hom
- dom
- cod
- id
- com
- assoc
- unitr
- unitl
C := {Obj, Hom, Dom, Cod, Id, Com, Assoc, UnitL, UnitR}
- Obj : {1, 2, 3}
- Hom : Obj Obj -> C
- Hom : x y |-> Hom(x,y)
- Dom : Hom(x,y) -> Obj
- Dom : f |-> x
- Cod : Hom(x,y) -> Obj
- Cod : f |-> y
- Id : Obj -> Σ Hom(x,x)
- Id : x |-> 1 _ x
- Com : Hom(y,z) Hom(x,y) -> Hom(x,z)
- Com : g f |-> g.f
- Assoc : Com Hom(y,z) (Com Hom(x,y) Hom(w,x)) -> Com (Com Hom(y,z) Hom(x,y)) Hom(w,x)
- UnitR : Hom(x,y) ({Id x}) -> Hom(x,y)
- UnitL : ({Id y}) Hom(x,y) -> Hom(x,y)
...
- Mor = Σ Hom + Σ End
- Mor : { $ 1 _ 1 $ , $ 1 _ 2 $ , $ 1 _ 3 $ , 1 $ \to $ 2, 2 $ \to $ 3, 1 $ \to $ 3, }
- id : Obj $ \to $ Mor
- id : $ x \ \mapsto \ 1 _ x $
- com : Hom $ \times $ Hom $ \to $ Hom
- com : $ ( x, \ y ) \ \mapsto \ y \circ x $
- assoc : com Hom (com Hom) $ \to $ com (com Mor Mor)
- unitr : Hom $ \times $ $ { 1 _ x } $ $ \to $ Hom
- unitl : $ { 1 _ x } $ $ \times $ Hom $ \to $ Hom
We can omit Objects since Obj is isomorphic to { $ 1 _ 1 $ , $ 1 _ 2 $ , $ 1 _ 3 $ }.
In category theory, what we have to think is morphisms .
Note that
- morphism ' $ \le $ ' compose a category,
- morphism ' $ \lt $ ' does not compose a category, but a graph.
## The formal Definition
Category is composed of 6 definitions.
~~~
- Objects := { X, Y, Z, W }
- Morphisms := { f:X->Y, g:Y->Z, ... }
- Composition := { g.f:X->Z, h.g:Y->Z, ... }
- Identity := { id_x:X->X, ... }
- Associativity Laws := { h.(g.f) = (h.g).f }
- Unit Laws := { f.id_x = f, id_y.g = g , ... }
~~~
# Mike Shulman's Categoriacl Logic
## Unary Type Theory
$$\frac{A}{B}$$
# Categories and Sheaves
-
# Mac Lane
## Glossaries
* copower $X \bullet b$ $\iff$ constant coproduct $\bigsqcup_{x \in X} b$
* connected category $\mathscr C$ $\iff$ $\forall c, d \in \mathscr C ,$ there is a sequence of arrows s.t.
$$ c \to \bullet \leftarrow \bullet \rightarrow \bullet \leftarrow ... \leftarrow \bullet \rightarrow \bullet \leftarrow d $$
* wedge
* bifunctor
* dinatural transformation
* final functor $F : \mathscr I \to \mathscr J$ $\iff$ $\forall j \in \mathscr J$, $j \downarrow F$ is connected.
* $\mathbb Z \to \mathbb R$ is final
* $\triangle \to Top$ is final
* $\triangle \to \hat \triangle$ is final
* initial functor $F : \mathscr I \to \mathscr J$ $\iff$ $F^{op} : \mathscr I^{op} \to \mathscr J^{op}$ is final.
* i.e. $\iff$ $\forall j \in \mathscr J$, $F \downarrow j$ is connected.
* $\mathbb Z \to \mathbb R$ is initial
* $\triangle \to Top$ is initial
* $\triangle \to \hat \triangle$ is initial
* comma $d \downarrow F$ $\iff$ slice category $d / F(\mathscr C)$
* comma $F \downarrow d$ $\iff$ slice category $F(\mathscr C) / d$
* end of a functor $S : \mathscr C \times \mathscr C^{op} \to \mathscr D$
* $\iff$ a universal binatural transformation $\xi_c : e (=: \int_c S(c,c)) \to S(c,c)$
* $Nat(U,V) \equiv \int_c Hom(U c, V c)$
* coend := tensor
* $\iff$ a universal binatural transformation $S(c,c) \to d ( =: \int^c S(c,c))$
* This is tensor product
* indeed $M \otimes_R N$ $\equiv$ $\int^R M \otimes N$
* for a monoidal category with tensor multiplication $B$, and for $S : P \to B$ , $T : P^{op} \to B$,
$$ T \square_P S \equiv \int^P (T p)\square(S p) $$
## Kan Extension
* dense functor $K:M \to C$ $\iff$ $Colim((K \downarrow c) \to M \to C) = c$
* $\mathscr {\hat Y}$ is dense
* codense functor $K:M \to C$ $\iff$ $Lim((c \downarrow K) \to M \to C) = c$
* $\mathscr {\check Y}$ is codense
* $Lan_{\mathscr Y} F \dashv Lan_F \mathscr Y$
* e.g. $realization \dashv nerve$ (where $F: \triangle \to Top$ )
* This adjunction can be constructed since $\mathscr {\hat Y}$ is dense.