\[ \require{mathtools} \let\DeclarePairedDelimiter\DeclarePairedDelimiters % MathJax typo %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % symbol %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % sets \newcommand{\N}{\mathbb{N}} % natural numbers \newcommand{\Z}{\mathbb{Z}} % integers \newcommand{\Q}{\mathbb{Q}} % rational numbers \newcommand{\R}{\mathbb{R}} % real numbers \newcommand{\C}{\mathbb{C}} % complex numbers % category \newcommand{\catf}[1]{{\mathbf{#1}}} \newcommand{\cA}{\catf{A}} \newcommand{\cB}{\catf{B}} \newcommand{\cC}{\catf{C}} \newcommand{\cD}{\catf{D}} \newcommand{\cE}{\catf{E}} \newcommand{\cF}{\catf{F}} \newcommand{\cG}{\catf{G}} \newcommand{\cH}{\catf{H}} \newcommand{\cI}{\catf{I}} \newcommand{\cJ}{\catf{J}} \newcommand{\cK}{\catf{K}} \newcommand{\cL}{\catf{L}} \newcommand{\cM}{\catf{M}} \newcommand{\cN}{\catf{N}} \newcommand{\cO}{\catf{O}} \newcommand{\cP}{\catf{P}} \newcommand{\cQ}{\catf{Q}} \newcommand{\cR}{\catf{R}} \newcommand{\cS}{\catf{S}} \newcommand{\cT}{\catf{T}} \newcommand{\cU}{\catf{U}} \newcommand{\cV}{\catf{V}} \newcommand{\cW}{\catf{W}} \newcommand{\cX}{\catf{X}} \newcommand{\cY}{\catf{Y}} \newcommand{\cZ}{\catf{Z}} \newcommand{\cZero}{\catf{0}} \newcommand{\cOne}{\catf{1}} \newcommand{\cTwo}{\catf{2}} \newcommand{\cArr}{\catf{Arr}} % arrow \newcommand{\cPSh}{\catf{PSh}} % presheaf \newcommand{\cCone}{\catf{Cone}} % cone \newcommand{\cCocone}{\catf{Cocone}} % cocone \newcommand{\cFin}{\catf{Fin}} % finite prefix \newcommand{\cSet}{\catf{Set}} % functions \newcommand{\cRel}{\catf{Rel}} % relations \newcommand{\cPos}{\catf{Pos}} % posets \newcommand{\cMon}{\catf{Mon}} % monoids \newcommand{\cCMon}{\catf{CMon}} % commutative monoids \newcommand{\cGrp}{\catf{Grp}} % groups \newcommand{\cAb}{\catf{Ab}} % abelian groups \newcommand{\cCat}{\catf{Cat}} % categories \newcommand{\cGrpd}{\catf{Grpd}} % groupoids \newcommand{\cVect}{\catf{Vect}} % vector spaces \newcommand{\cMat}{\catf{Mat}} % matrices \newcommand{\cTop}{\catf{Top}} % topological spaces and continuous maps \newcommand{\cMet}{\catf{Met}} % metric spaces and metric maps \newcommand{\cMeas}{\catf{Meas}} % measurable spaces and measurable functions \newcommand{\cStoch}{\catf{Stoch}} % measurable spaces and stochastic maps \newcommand{\cProb}{\catf{Prob}} % probability measures and measure-preserving functions %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % supscript %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \newcommand{\op}{^\mathrm{op}} \newcommand{\inv}{^{-1}} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % function %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \DeclareMathOperator{\lcm}{lcm} \DeclareMathOperator{\logsumexp}{log-sum-exp} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % arrow %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % morphism \newcommand{\xto}{\xrightarrow} % -> \newcommand{\xot}{\xleftarrow} % <- \newcommand{\toot}{\rightleftarrows} % <=> \newcommand{\xtoot}[2]{\xrightleftharpoons[#2]{#1}} \newcommand{\iso}{\cong} % ~= \newcommand{\klto}{\rightsquigarrow} % ~> \newcommand{\mono}{\rightarrowtail} % >-> \newcommand{\epi}{\twoheadrightarrow} % ->> \newcommand{\ihom}{\multimap} % -o % category \newcommand{\incl}{\hookrightarrow} \newcommand{\adjto}[2]{\overset{{}\xto[]{#1}{}}{\underset{{}\xot[#2]{}{}}{\bot}}} % functor \newcommand{\nat}{\Rightarrow} % => \newcommand{\xnat}{\xRightarrow} % => \newcommand{\comma}{\downarrow} \newcommand{\adj}{\dashv} % -| %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % delimiter %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \DeclarePairedDelimiter{\parens}{(}{)} % parentheses ( ) \DeclarePairedDelimiter{\bracks}{[}{]} % brackets [ ] \DeclarePairedDelimiter{\braces}{\{}{\}} % braces { } \DeclarePairedDelimiter{\angles}{\langle}{\rangle} % angles \DeclarePairedDelimiter{\floor}{\lfloor}{\rfloor} \DeclarePairedDelimiter{\ceil}{\lceil}{\rceil} \newcommand{\set}{\braces} \newcommand{\singleton}{{\set{*}}} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % operator %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \newcommand{\compL}{\mathbin{\circ}} \newcommand{\compR}{\mathbin{;}} \newcommand{\Kl}{\mathrm{Kl}} \DeclareMathOperator{\Obj}{Obj} \DeclareMathOperator{\Hom}{Hom} \DeclareMathOperator{\Sub}{Sub} \DeclareMathOperator{\Eq}{Eq} \DeclareMathOperator{\Coeq}{Coeq} \DeclareMathOperator{\Pull}{Pull} \DeclareMathOperator{\Push}{Push} \DeclareMathOperator{\Lan}{Lan} \DeclareMathOperator{\Ran}{Ran} \DeclareMathOperator{\Lift}{Lift} \DeclareMathOperator{\Rift}{Rift} \DeclareMathOperator{\id}{id} \DeclareMathOperator{\colim}{colim} % exponential \DeclareMathOperator{\partf}{partial} \DeclareMathOperator{\curry}{curry} % natural number \DeclareMathOperator{\zero}{zero} \DeclareMathOperator{\successor}{succ} % list \DeclareMathOperator{\nil}{nil} \DeclareMathOperator{\cons}{cons} \newcommand{\concat}{\mathbin{{+}\mspace{-8mu}{+}}} % fold \DeclareMathOperator{\fold}{fold} \DeclareMathOperator{\map}{map} \DeclareMathOperator{\filter}{filter} % bool \DeclareMathOperator{\cond}{cond} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % order %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \newcommand{\meet}{\wedge} \newcommand{\join}{\vee} \newcommand{\bigmeet}{\bigwedge} \newcommand{\bigjoin}{\bigvee} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % logic %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \newcommand{\lT}{\top} \newcommand{\lF}{\bot} % logical connective \newcommand{\binop}[1]{\mathbin{#1}} % conjunction AND \newcommand{\lcon}{\binop{\wedge}} % not conjunction NAND \newcommand{\lncon}{\binop{\uparrow}} % disjunction OR \newcommand{\ldis}{\binop{\vee}} % not disjunction NOR \newcommand{\lndis}{\binop{\downarrow}} % implication \newcommand{\limp}{\binop{\rightarrow}} % not implication \newcommand{\lnimp}{\binop{\nrightarrow}} % converse implication \newcommand{\lcim}{\binop{\leftarrow}} % not converse implication \newcommand{\lncim}{\binop{\nleftarrow}} % equivalence XNOR \newcommand{\leqv}{\binop{\leftrightarrow}} % not equivalence XOR \newcommand{\lneqv}{\binop{\nleftrightarrow}} \newcommand{\lproves}{\binop{\vdash}} % |- \newcommand{\lmodels}{\binop{\vDash}} % |= \newcommand{\lnproves}{\binop{\nvdash}} % |/- \newcommand{\lnmodels}{\binop{\nvDash}} % |/= \newcommand{\truth}{{\set{\lT, \lF}}} \newcommand{\quant}{{[0, \infty]}} \newcommand{\inter}{{[0, 1]}} \newcommand{\qnot}{\mathord{\sim}} \newcommand{\qcon}{\binop{\otimes}} \newcommand{\qdis}{\binop{\oplus}} \newcommand{\qimp}{\binop{\multimap}} \DeclareMathOperator*{\qforall}{\triangledown} \DeclareMathOperator*{\qexists}{\vartriangle} \]
Universal construction defines objects in terms of their relations with other objects.
1 Terminal object & initial object
- A terminal object is an object \(1\) that for every object \(A\) there exists a unique morphism \(e_A: A \to 1\) to it.
- An initial object is an object \(0\) that for every object \(B\) there exists a unique morphism \(i_B: 0 \to B\) from it.
\[\begin{aligned} \begin{array}{rlcll} \text{terminal object:} & 1 & \equiv & \forall A. & \exists! e_A: A \to 1. \\ \text{initial object:} & 0 & \equiv & \forall B. & \exists! i_A: 0 \to B. \end{array} \end{aligned}\]
- A weakly terminal object is an object that for every object there exists at least one morphism to it.
- A weakly initial object is an object that for every object there exists at least one morphism from it.
- A subterminal object is an object that for every object there exists at most one morphism to it.
- A subinitial object is an object that for every object there exists at most one morphism from it.
- A strictly terminal object is a terminal object \(1\) that every morphism from it is a isomorphism.
- A strictly initial object is an initial object \(0\) that every morphism to it is a isomorphism.
- A zero object \(0\) is both a terminal object and an initial object.
- A zero morphism \(0_{A, B}: A \to 0 \to B\) is the unique morphism that factors through the zero object \(0\).
- A pointed category is a category with a zero object.
- A generalized element of \(A\) is a morphism \(a: X \to A\).
- A global element of \(A\) is a morphism \(a: 1 \to A\).
2 Universal morphism
\[\begin{aligned} \begin{array}{ccccc} F: & \cC & \toot & \cD & :G \\ & A && B & \\ & f && g & \end{array} \end{aligned}\]
- A universal morphism from \(F\) to \(B\) is a terminal object \((T, FT \xto{\epsilon} B)\) in the comma category \((F: \cC \to \cD) \comma (B: \cOne \to \cD)\).
- A universal morphism from \(A\) to \(G\) is an initial object \((I, A \xto{\eta} GI)\) in the comma category \((A: \cOne \to \cC) \comma (G: \cD \to \cC)\).
\[\begin{aligned} \begin{array}{rlclll} \text{universal morphism from $F$ to $B$:} & (T, FT \xto{\epsilon} B) & \equiv & \forall g: FA \to B. & \exists! \hat{g}: A \to T. & g = \epsilon \compL F\hat{g}. \\ \text{universal morphism from $A$ to $G$:} & (I, A \xto{\eta} GI) & \equiv & \forall f: A \to GB. & \exists! \hat{f}: I \to B. & f = G\hat{f} \compL \eta. \end{array} \end{aligned}\]
3 Adjunction
3.1 Adjoint functor
- A right adjoint functor of \(F\) is a universal morphism \((G, \epsilon: FG \nat \id_\cD)\) from \(F^\cD: \cC^\cD \to \cD^\cD\) to \(\id_\cD\).
- A left adjoint functor of \(G\) is a universal morphism \((F, \eta: \id_\cC \nat GF)\) from \(\id_\cC\) to \(G^\cC: \cD^\cC \to \cC^\cC\).
- For each \(\cD\)-object \(B\), there exists a universal morphism \((GB, \epsilon_B: FGB \to B)\) from \(F\) to \(B\).
- For each \(\cC\)-object \(A\), there exists a universal morphism \((FA, \eta_A: A \to GFA)\) from \(A\) to \(G\).
\[G(B \xto{g} B') := \widehat{g \compL \epsilon_B}\]
\[F(A \xto{f} A') := \widehat{\eta_A' \compL f}\]
3.2 Hom-set isomorphism
\[\alpha: \Hom_\cD(FA, B) \iso \Hom_\cC(A, GB) :\alpha\inv\]
\[\begin{aligned} \begin{array}{cccc} \alpha\inv_{GB, B}: & \Hom_\cC(GB, GB) & \iso & \Hom_\cD(FGB, B) \\ & \id_{GB} & \mapsto & \epsilon_B \\ \alpha_{A, FA}: & \Hom_\cD(FA, FA) & \iso & \Hom_\cC(A, GFA) \\ & \id_{FA} & \mapsto & \eta_A \end{array} \end{aligned}\]
3.3 Counit-unit adjunction
\[\begin{aligned} \begin{array}{rll} \text{isomorphism:} & \id_\cC = GF & FG = \id_\cD \\ \text{equivalence:} & \id_\cC \iso GF & FG \iso \id_\cD \\ \text{adjunction:} & \id_\cC \nat GF & FG \nat \id_\cD \end{array} \end{aligned}\]
\[\cC \adjto{F}{G} \cD\]
An adjunction \(F \adj G\) consists of a pair of adjoint functors \(F: \cC \toot \cD: G\) with
- counit \(\epsilon: FG \nat \id_\cD\)
- unit \(\eta: \id_\cC \nat GF\)
such that
- \((\epsilon F) \compL (F \eta) = \id_F\)
- \((G \epsilon) \compL (\eta G) = \id_G\)
3.4 Galois connection
\[F: (A, \leq_A) \adj (B, \leq_B) :G\]
\[\begin{aligned} Fa := \min \set{b \in B \mid a \leq_A Gb} \\ Gb := \max \set{a \in A \mid Fa \leq_B b} \end{aligned}\]
3.4.1 Multiplication and division
\[(\R, \leq) \adjto{- / c}{- \times c} (\R, \leq)\]
\[a / c \leq b \equiv a \leq b \times c\]
- \(\eta_a: a \leq a / c * c = \id_a\)
- \(\epsilon_a: a * c / c \leq a = \id_a\)
3.4.2 Union and intersection
\[(PA, \subseteq) \adjto{- \cap X}{\overline{X} \cup -} (PA, \subseteq)\]
\[Z \cap X \subseteq Y \equiv Z \subseteq \overline{X} \cup Y\]
- \(\eta_A: A \subseteq \overline{X} \cup (A \cap X)\)
- \(\epsilon_A: (\overline{X} \cup A) \cap X \subseteq A\)
3.4.3 Floor and ceiling
\[(\R, \leq) \adjto{\ceil{-}}{} (\Z, \leq) \adjto{}{\floor{-}} (\R, \leq)\]
\[\ceil{x} \leq_\Z n \equiv x \leq_\R n\]
\[n \leq_\R x \equiv n \leq_\Z \floor{x}\]
- \(\eta_x: x \leq_\R \ceil{x}\)
- \(\epsilon_n: \ceil{n} \leq_\Z n = \id_n\)
- \(\eta_n: n \leq_\Z \floor{n} = \id_n\)
- \(\epsilon_x: \floor{x} \leq_\R x\)
3.4.4 Maximum and minimum
\[\cOne \adjto{\min A}{} (A, \leq) \adjto{}{\max A} \cOne\]
- \(\eta_* = \id_*\)
- \(\epsilon_a: \min A \leq a\)
- \(\eta_a: a \leq \max A\)
- \(\epsilon_* = \id_*\)
\[(PA, \subseteq) \adjto{\max}{A_{\leq -}} (A, \leq) \adjto{A_{\geq -}}{\min} (PA, \supseteq)\]
\[\max A \leq b \equiv A \subseteq A_{\leq b}\]
\[A_{\geq a} \supseteq B \equiv a \leq \min B\]
- \(\eta_A: A \subseteq A_{\leq \max A}\)
- \(\epsilon_b: \max A_{\leq b} \leq b = \id_b\)
- \(\eta_a: a \leq \min A_{\geq a} = \id_a\)
- \(\epsilon_B: A_{\geq \min B} \supseteq B\)
\[(PA, \subseteq) \adjto{\min}{A_{\geq -}} (A, \geq) \adjto{A_{\leq -}}{\max} (PA, \supseteq)\]
\[\min A \geq b \equiv A \subseteq A_{\geq b}\]
\[A_{\leq a} \supseteq B \equiv a \geq \max B\]
- \(\eta_A: A \subseteq A_{\geq \min A}\)
- \(\epsilon_b: \min A_{\geq b} \geq b = \id_b\)
- \(\eta_a: a \geq \max A_{\leq a} = \id_a\)
- \(\epsilon_B: A_{\leq \max B} \supseteq B\)
3.5 Free-forgetful adjunction
\[\cC \adjto{F\text{ree}}{U\text{nderlying}} \cD\]
4 Kan
- \(F: \cA \to \cC\)
- \(G: \cA \to \cB\)
- \(H: \cB \to \cC\)
- \(\cC^G: \cC^\cB \to \cC^\cA\) precomposition
- \(H^\cA: \cB^\cA \to \cC^\cA\) postcomposition
- \(\Lan_G, \Ran_G: \cC^\cA \to \cC^\cB\) Kan extension
- \(\Lift_H, \Rift_H: \cC^\cA \to \cB^\cA\) Kan lift
4.1 Kan extension
- A right Kan extension of \(F\) through \(G\) is a universal morphism \((\Ran_G F: \cB \to \cC, \epsilon_F: \Ran_G F G \nat F)\) from \(\cC^G\) to \(F\).
- A left Kan extension of \(F\) through \(G\) is a universal morphism \((\Lan_G F: \cB \to \cC, \eta_F: F \nat \Lan_G F G)\) from \(F\) to \(\cC^G\).
\[\Lan_G \adj \cC^G \adj \Ran_G\]
4.2 Kan lift
- A right Kan lift of \(F\) through \(H\) is a universal morphism \((\Rift_H F: \cA \to \cB, \epsilon_F: H \Rift_H F \nat F)\) from \(H^\cA\) to \(F\).
- A left Kan lift of \(F\) through \(H\) is a universal morphism \((\Lift_H F: \cA \to \cB, \eta_F: F \nat H \Lift_H F)\) from \(F\) to \(H^\cA\).
\[\Lift_H \adj H^\cA \adj \Rift_H\]
5 Limit & colimit
A diagram of type \(\cI\) in a category \(\cC\) is a functor
\[\begin{aligned} D: \cI & \to \cC \\ i & \mapsto D_i \\ ij & \mapsto D_{ij} \end{aligned}\]
\(\cI\) is called the index category.
Given the diagonal functor \(\Delta: \cC \to \cC^\cI\) and a diagram \(D: \cI \to \cC\):
- A limit is a universal morphism \((\lim D, \epsilon_D: \Delta \lim D \nat D)\) from \(\Delta\) to \(D\).
- A colimit is a universal morphism \((\colim D, \eta_D: D \nat \Delta \colim D)\) from \(D\) to \(\Delta\).
\[\begin{aligned} \begin{array}{rlclll} \text{limit:} & \epsilon_D: \Delta \lim D \nat D & \equiv & \forall c: \Delta C \nat D. & \exists! \hat{c}: C \to \lim D. & c = \epsilon_D (\Delta \hat{c}). \\ \text{colimit:} & \eta_D: D \nat \Delta \colim D & \equiv & \forall c: D \nat \Delta C. & \exists! \hat{c}: \colim D \to C. & c = (\Delta \hat{c}) \eta_D. \end{array} \end{aligned}\]
\[\colim \adj \Delta \adj \lim\]
- A (finitely) (co)complete category has all (finite) (co)limits.
- A (finitely) bicomplete category is (finitely) complete and (finitely) cocomplete.
5.1 Cone & cocone
A cone \((C, c)\) over a diagram \(D: \cI \to \cC\) consists of
- a \(\cC\)-object \(C\)
- a collection of \(\cC\)-morphisms from \(C\) indexed by \(\cI\)-objects \(c_i: C \to D_i\)
such that for all \(\cI\)-morphisms \(ij: i \to j\), \(c_j = D_{ij} \compL c_i\).
A cone morphism \(f: (C, c) \to (C', c')\) is a \(\cC\)-morphism \(f: C \to C'\) that for all \(\cI\)-objects \(i\), \(c_i = c'_i \compL f\).
A cone category \(\cCone(D)\) consists of all cones over a diagram \(D\) and all cone morphisms.
A limit \(\lim D\) of a diagram \(D\) is a terminal object in \(\cCone(D)\).
- A limit is a cone: (a \(\cC\)-object \(\lim D\), a collection of \(\cC\)-morphisms \(\epsilon_i: \lim D \to D_i\))
- A limit is a terminal object: for all cones \((C, c)\), there exists a unique cone morphism \(f: (C, c) \to (\lim D, \epsilon)\) such that \(c_i = \epsilon_i \compL f\).
The concepts of cocone, cocone morphism, cocone category and colimit are defined dually.
- cone: \(c: \Delta C \nat D\), cocone: \(c: D \nat \Delta C\)
- cone/cocone morphism: \(\Delta f: \Delta C \nat \Delta C'\)
- cone category: \(\Delta \comma D\), cocone category: \(D \comma \Delta\)
- limit: \(\epsilon_D: \Delta \lim D \nat D\), colimit: \(\eta_D: D \nat \Delta \colim D\)
5.2 Preservation
For a diagram \(D: \cI \to \cC\) and a functor \(F: \cC \to \cD\),
- \(F\) preserves a limit \((\lim D, \epsilon_D)\) in \(\cC\) if \((F \lim D, F \epsilon_D)\) is a limit in \(\cD\)
- \(F\) preserves a colimit \((\colim D, \eta_D)\) in \(\cC\) if \((F \colim D, F \eta_D)\) is a colimit in \(\cD\)
A (finitely) (co)continuous functor preserves all (finite) (co)limits.
\(F\) is a left adjoint functor \(\equiv\) \(F\) preserves colimits. \(G\) is a right adjoint functor \(\equiv\) \(G\) preserves limits.
Limits commute with limits; colimits commute with colimits.
\(\Hom_\cC\) preserves limits.
\[\Hom_\cC(C, \lim D) \iso \lim \Hom_\cC(C, -) D\]
\[\Hom_\cC(\colim D, C) \iso \lim \Hom_\cC(-, C) D\]
\[\Hom_\cC(C, A \times B) \iso \Hom_\cC(C, A) \times \Hom_\cC(C, B)\]
\[\Hom_\cC(A + B, C) \iso \Hom_\cC(A, C) \times \Hom_\cC(B, C)\]
6 Examples
Tarski’s high school algebra (in a bicartesian closed category):
- \(A + B \iso B + A\)
- \((A + B) + C \iso A + (B + C)\)
- \(A \times 1 \iso A\)
- \(A \times B \iso B \times A\)
- \((A \times B) \times C \iso A \times (B \times C)\)
- \(A \times B + A \times C \iso A \times (B + C)\)
- \(1^A \iso 1\)
- \(A^1 \iso A\)
- \(A^{B + C} \iso A^B \times A^C\)
- \((A \times B)^C \iso A^C \times B^C\)
- \((A^B)^C \iso A^{B \times C}\)
6.1 Set
| terminal object | singleton \(\set{*}\) |
| initial object | empty set \(\varnothing\) |
| product | cartesian product \(A \times B\) |
| coproduct | disjoint union \(A + B\) |
| equalizer | \(\Eq(f, g: A \to B) = \set{a \in A \mid f(a) = g(a)}\) |
| coequalizer | \(\Coeq(f, g: A \to B) = B / \sim\) where \(b_1 \sim b_2\) if \(\exists a \in A. f(a) = b_1 \land g(a) = b_2\) |
| pullback | \(\Pull(f: A \to C, g: B \to C) = \set{(a, b) \in A \times B \mid f(a) = g(b)}\) |
| pushout | \(\Push(f: C \to A, g: C \to B) = (A + B) / \sim\) where \(a \sim b\) if \(\exists c \in C. f(c) = a \land g(c) = b\) |
| fiber | inverse image \(\Pull(f: A \to B, b: 1 \to B) = \set{a \in A \mid f(a) = b}\) |
| monomorphism | injective function |
| epimorphism | surjective function |
| subobject | subset |
| subobject classifier | indicator function |
| power object | power set |
| exponential object | the set of functions and function evaluation |
6.2 Cat
| terminal object | \(\cOne\) |
| initial object | \(\cZero\) |
| product | product category \(\cC \times \cD\) |
| exponential object | functor category \([\cC, \cD]\) |
6.3 Poset
\((A, \leq)\)
| terminal object | greatest element / top \(\top\) |
| initial object | least element / bottom \(\bot\) |
| product | greatest lower bound / meet \(a \meet b\) |
| coproduct | least upper bound / join \(a \join b\) |
| equalizer | \(\id_a: a \leq a\) |
| coequalizer | \(\id_b: b \leq b\) |
| pullback | \(p_1: a \meet b \leq a\), \(p_2: a \meet b \leq b\) |
| pushout | \(i_1: a \leq a \join b\), \(i_2: a \leq a \join b\) |
| exponential object | \(a \ihom b := \bigjoin\set{c \mid c \lcon a \leq b}\) (\(c \lcon a \leq b \equiv c \leq a \ihom b\)) |
- A meet-semilattice is a poset with all binary meets \(a \meet b\).
- A join-semilattice is a poset with all binary joins \(a \join b\).
- A lattice is a meet-semilattice and a join-semilattice.
- A bounded poset is a poset with a terminal object \(\top\) and/or an initial object \(\bot\).
- A bounded meet-semilattice is a finitely complete poset.
- A bounded join-semilattice is a finitely cocomplete poset.
- A bounded lattice is a finitely bicomplete poset.
- A Heyting algebra is a cartesian closed bounded lattice.
- A Boolean algebra is a Heyting algebra satisfying the law of excluded middle.
A Heyting algebra is finitely distributive because it is finitely bicartesian and closed.
- A inflattice is a complete poset.
- A suplattice is a cocomplete poset.
- A complete lattice is a bicomplete poset.
By the adjoint functor theorem for posets, all joins \(\equiv\) all meets, i.e., inflattice = suplattice = complete lattice.
A inflattice/suplattice homomorphism is a monotone preserving meets/joins.
A complete Heyting algebra is a cartesian closed complete lattice.
6.3.1 \((\N, \leq)\)
| terminal object | \(-\) | |
| initial object | \(0\) | \(0 \leq a\) |
| product | \(\min\) | \(c \leq a, c \leq b \equiv c \leq \min(a, b)\) |
| coproduct | \(\max\) | \(a \leq c, b \leq c \equiv \max(a, b) \leq c\) |
| exponential object | \(-\) |
6.3.2 \((\N, \mid)\)
| terminal object | \(0\) | \(a \mid 0\) |
| initial object | \(1\) | \(1 \mid a\) |
| product | \(\gcd\) | \(c \mid a, c \mid b \equiv c \mid \gcd(a, b)\) |
| copoduct | \(\lcm\) | \(a \mid c, b \mid c \equiv \lcm(a, b) \mid c\) |
| exponential object | \(-\) |
6.3.3 \((\set{\lfal, \ltru}, \lfal \lproves \ltru)\)
| terminal object | \(\ltru\) | |
| initial object | \(\lfal\) | |
| product | \(\lcon\) | \(C \lproves A, C \lproves B \equiv C \lproves A \lcon B\) |
| copoduct | \(\ldis\) | \(A \lproves C, B \lproves C \equiv A \ldis B \lproves C\) |
| exponential object | \(\limp\) | \(C \lcon A \lproves B \equiv C \lproves (A \limp B)\) |
6.3.4 \(([0, \infty], \geq)\)
| terminal object | \(0\) | \(a \geq 0\) |
| initial object | \(\infty\) | \(\infty \geq a\) |
| product | \(\max\) | \(c \geq a, c \geq b \equiv c \geq \max(a, b)\) |
| copoduct | \(\min\) | \(a \geq c, b \geq c \equiv \min(a, b) \geq c\) |
| exponential object | \(\begin{cases}0 & a \geq b \\ b & \text{otherwise}\end{cases}\) | \(\max(c, a) \geq b \equiv c \geq \begin{cases}0 & a \geq b \\ b & \text{otherwise}\end{cases}\) |
6.4 Met
metric spaces \((A, d_A: A \times A \to [0, \infty])\) and metric functions \(d_A(a, a') \geq d_B(f(a), f(a'))\).
| terminal object | singleton \((\set{*}, d)\) |
| initial object | empty set \((\varnothing, d)\) |
| product | product metric \(d_{A \times B}((a, b), (a', b')) := \max(d_A(a, a'), d_B(b, b'))\) |
| coproduct | disjoint metric \(d_{A + B}(a, a') := d_A(a, a')\), \(d_{A + B}(b, b') := d_B(b, b')\), \(d_{A + B}(a, b) = d_{A + B}(b, a) := \infty\) |