From 1a358eae52fa52b56ff4471b3db06ad4c83482b6 Mon Sep 17 00:00:00 2001 From: zeramorphic <50671761+zeramorphic@users.noreply.github.com> Date: Fri, 24 Nov 2023 12:55:09 +0000 Subject: [PATCH] Lectures 22B --- iii/alggeom/06_divisors.tex | 57 +++++- iii/alggeom/07_sheaf_cohomology.tex | 32 ++++ iii/alggeom/main.tex | 2 + iii/cat/04_limits.tex | 2 +- .../07_additive_and_abelian_categories.tex | 163 ++++++++++++++++++ iii/mtncl/06_intuitionistic_logic.tex | 103 ++++++++++- 6 files changed, 351 insertions(+), 8 deletions(-) create mode 100644 iii/alggeom/07_sheaf_cohomology.tex diff --git a/iii/alggeom/06_divisors.tex b/iii/alggeom/06_divisors.tex index b6f2824..d692b8d 100644 --- a/iii/alggeom/06_divisors.tex +++ b/iii/alggeom/06_divisors.tex @@ -55,7 +55,7 @@ \subsection{Weil divisors} is finite. \end{proposition} \begin{proof} - Let \( f \in k(X)^\times \), and choose \( A \) such that \( U = \Spec A \) is an affine open, so \( FF(A) = k(X) \). + Let \( f \in k(X)^\times \), and choose \( A \) such that \( U = \Spec A \) is an affine open, so \( FF(A) = k(X) \). We can also require that \( f \in A \) by localising at the denominator, so \( f \) is \emph{regular} on \( U \). Then \( X \setminus U \) is closed and of codimension at least 1, so only finitely many prime Weil divisors \( Y \) of \( X \) are contained in \( X \setminus U \). On \( U \), as \( f \) is regular, \( \nu_Y(f) \geq 0 \) for all \( Y \). @@ -63,9 +63,9 @@ \subsection{Weil divisors} \end{proof} \begin{definition} A Weil divisor of the form \( \operatorname{div}(f) \) is called \emph{principal}. + In \( \operatorname{Div}(X) \), the set of principal divisors form a subgroup \( \operatorname{Prin}(X) \), and we define the \emph{Weil divisor class group} of \( X \) to be + \[ \operatorname{Cl}(X) = \faktor{\operatorname{Div}(X)}{\operatorname{Prin}(X)} \] \end{definition} -In \( \operatorname{Div}(X) \), the set of principal divisors form a subgroup \( \operatorname{Prin}(X) \), and we define the \emph{Weil divisor class group} of \( X \) to be -\[ \operatorname{Cl}(X) = \faktor{\operatorname{Div}(X)}{\operatorname{Prin}(X)} \] \begin{remark} \begin{enumerate} \item Let \( A \) be a Noetherian domain. @@ -114,8 +114,57 @@ \subsection{Cartier divisors} Consider the presheaf on \( X \) given by mapping \( U = \Spec A \) to \( S^{-1}A \) where \( S \) is the set of all elements that are not zero divisors. Sheafification yields the sheaf of rings \( \mathcal K_X \). Define \( \mathcal K_X^\star \subseteq \mathcal K_X \) to be the subsheaf of invertible elements; this is a sheaf of abelian groups under multiplication. +If \( X \) is integral, then \( \mathcal K_X \) is the constant sheaf, where the constant field is \( \mathcal O_{X,\eta_X} = FF(A) \) for any affine open \( \Spec A \). + Similarly, let \( \mathcal O_X^\star \subseteq \mathcal O_X \) be the subsheaf of invertible elements. Thus, every section of \( \faktor{\mathcal K_X^\star}{\mathcal O_X^\star} \) can be prescribed by \( \qty{(U_i, f_i)} \) where \( U_i \) is a cover of \( X \), \( f_i \) is a section of \( \mathcal K_X^\star(U_i) \), and that on \( U_i \cap U_j \), the ratio \( \faktor{f_i}{f_j} \) lies in \( \mathcal O_X^\star(U_i \cap U_j) \). \begin{definition} - A \emph{Cartier divisor} is a section of the sheaf \( \faktor{\mathcal K_X^\star}{\mathcal O_X^\star} \). + A \emph{Cartier divisor} is a global section of the sheaf \( \faktor{\mathcal K_X^\star}{\mathcal O_X^\star} \). +\end{definition} +We have a surjective sheaf homomorphism \( \mathcal K_X^\star \to \faktor{\mathcal K^X_\star}{\mathcal O_X^\star} \), but a global section of \( \faktor{\mathcal K^X_\star}{\mathcal O_X^\star} \) is not necessarily the image of a global section of \( \mathcal K_X^\star \). +\begin{definition} + The image of \( \Gamma(X, \mathcal K_X^\star) \) in \( \Gamma\qty(X, \faktor{\mathcal K_X^\star}{\mathcal O_X^\star}) \) is the set of \emph{principal} Cartier divisors. + The \emph{Cartier class group} is the quotient + \[ \faktor{\Gamma\qty(X, \faktor{\mathcal K_X^\star}{\mathcal O_X^\star})}{\Im \Gamma(X, \mathcal K_X^\star)} \] +\end{definition} +A section \( \mathcal D \in \Gamma\qty(X, \faktor{\mathcal K_X^\star}{\mathcal O_X^\star}) \) can be specified by \( \qty{(U_i, f_i)} \) where the \( \qty{U_i} \) form an open cover and \( f_i \in \mathcal K_X^\star(U_i) \), such that on \( U_i \cap U_j \), the quotient \( \frac{f_i}{f_j} \) lies in \( \mathcal O_X^\star(U_i \cap U_j) \). + +Let \( X \) be Noetherian, integral, separated, and regular in codimension 1. +Given a Cartier divisor \( \mathcal D \in \Gamma\qty(X, \faktor{\mathcal K_X^\star}{\mathcal O_X^\star}) \), we obtain a Weil divisor as follows. +If \( Y \subseteq X \) is a prime Weil divisor and its generic point is \( \eta_Y \), we represent \( \mathcal D \) by \( \qty{(U_i, f_i)} \) and set \( n_Y \) to be \( \nu_Y(f_i) \) for some \( U_i \) containing \( \eta_Y \). +Then we obtain the Weil divisor +\[ \sum_{Y \subseteq X} n_Y [Y] \] +This is well-defined: if \( \eta_Y \) is contained in both \( U_i \) and \( U_j \), the valuations of \( f_i \) and \( f_j \) differ by \( \nu_Y\qty(\frac{f_i}{f_j}) \), but \( \frac{f_i}{f_j} \) is a unit, so has valuation zero. +Similarly, one can show that this is independent of the choice of representative of \( \mathcal D \). +\begin{proposition} + Let \( X \) be Noetherian, integral, separated, and regular in codimension 1. + Suppose that all local rings \( \mathcal O_{X,x} \) are unique factorisation domains. + Then the association of a Weil divisor to each Cartier divisor is a bijection, and furthermore, is a bijection of principal divisors. +\end{proposition} +\begin{proof}[Proof sketch] + If \( R \) is a unique factorisation domain, then all height 1 prime ideals are principal. + If \( x \in X \), then \( \mathcal O_{X, x} \) is a unique factorisation domain by hypothesis, so given a Weil divisor \( D \), we can restrict it to \( \Spec \mathcal O_{X, x} \to X \). + But on \( \Spec \mathcal O_{X, x} \), \( D \) is given by \( \mathbb V(f_x) \) as \( \mathcal O_{X, x} \) is a unique factorisation domain. + \( f_x \) extends to some neighbourhood \( U_x \) containing \( x \), then the \( f_x \) can be glued to form a Cartier divisor. + This can be checked to be bijective. +\end{proof} +Given a Cartier divisor \( D \) on \( X \) with representative \( \qty{(U_i, f_i)} \), we can define \( L(\mathcal D) \subseteq \mathcal K_X \) to be the sub-\( \mathcal O_X \)-module generated on \( U_i \) by \( f_i^{-1} \). +Note that if \( X = \Spec A \) where \( A \) is integral, and \( \mathcal D = \qty{(X, f)} \) where \( f \in A \), then \( A_f \subseteq FF(A) \) is an \( A \)-module. +\begin{proposition} + The sheaf \( L(\mathcal D) \) is a line bundle. +\end{proposition} +\begin{proposition} + On \( U_i \), we have an isomorphism \( \mathcal O_{U_i} \to \eval{L(\mathcal D)}_{U_i} \) given by \( 1 \mapsto f_i^{-1} \). +\end{proposition} +Consider \( X = \mathbb P^n_k \), and let \( D \) be the Weil divisor \( \mathbb V(x_0) \). +Let \( \mathcal D \) be the corresponding Cartier divisor. +One can show that \( \mathcal O_{\mathbb P^n_k}(1) \cong L(\mathcal D) \). +\begin{remark} + A line bundle \( L \) on \( X \) has an `inverse' under the tensor product; that is, defining \( L^{-1} = \Hom_{\mathcal O_X}(L, \mathcal O_X) \), we obtain \( L \otimes_{\mathcal O_X} L^{-1} = \mathcal O_X \). + Tensor products of line bundles are also line bundles. + If all Weil divisors are Cartier, then \( L(\mathcal D + \mathcal E) = L(\mathcal D) \otimes L(\mathcal E) \). +\end{remark} +\begin{definition} + The \emph{Picard group} of \( X \) is the set of line bundles on \( X \) up to isomorphism, which forms an abelian group under the tensor product. \end{definition} +Under mild assumptions, for example assuming that \( X \) is integral, the map \( \mathcal D \mapsto L(\mathcal D) \) is surjective, and the kernel is exactly the set of principal Cartier divisors. diff --git a/iii/alggeom/07_sheaf_cohomology.tex b/iii/alggeom/07_sheaf_cohomology.tex new file mode 100644 index 0000000..fa658a6 --- /dev/null +++ b/iii/alggeom/07_sheaf_cohomology.tex @@ -0,0 +1,32 @@ +\subsection{???} +We have previously seen that if \( X = \mathbb A^2 \setminus \qty{(0, 0)} \), then \( \mathcal O_X(X) \cong \mathcal O_{\mathbb A^2}(\mathbb A^2) \cong k[x, y] \). +Given a topological space \( X \) and a sheaf \( \mathcal F \) of abelian groups, we will build a series of groups \( H^i(X, \mathcal F) \) for \( i \in \mathbb N \). +This will have the following features. +\begin{enumerate} + \item The group \( H^0(X, \mathcal F) \) is precisely \( \Gamma(X, \mathcal F) \). + \item If \( f : Y \to X \) is continuous, there is an induced map \( f^\star : H^i(X, \mathcal F) \to H^i(Y, f^{-1} \mathcal F) \). + \item Given a short exact sequence of sheaves + % https://q.uiver.app/#q=WzAsNSxbMCwwLCIwIl0sWzEsMCwiXFxtYXRoY2FsIEYiXSxbMiwwLCJcXG1hdGhjYWwgRiciXSxbMywwLCJcXG1hdGhjYWwgRicnIl0sWzQsMCwiMCJdLFswLDFdLFsxLDJdLFsyLDNdLFszLDRdXQ== +\[\begin{tikzcd} + 0 & {\mathcal F} & {\mathcal F'} & {\mathcal F''} & 0 + \arrow[from=1-1, to=1-2] + \arrow[from=1-2, to=1-3] + \arrow[from=1-3, to=1-4] + \arrow[from=1-4, to=1-5] +\end{tikzcd}\] + we obtain a long exact sequence + % https://q.uiver.app/#q=WzAsOSxbMCwwLCIwIl0sWzEsMCwiSF4wKFgsIFxcbWF0aGNhbCBGKSJdLFsyLDAsIkheMChYLCBcXG1hdGhjYWwgRicpIl0sWzMsMCwiSF4wKFgsIFxcbWF0aGNhbCBGJycpIl0sWzEsMSwiSF4xKFgsIFxcbWF0aGNhbCBGKSJdLFsyLDEsIkheMShYLCBcXG1hdGhjYWwgRicpIl0sWzMsMSwiSF4xKFgsIFxcbWF0aGNhbCBGJycpIl0sWzEsMiwiSF4yKFgsIFxcbWF0aGNhbCBGKSJdLFsyLDIsIlxcY2RvdHMiXSxbMCwxXSxbMSwyXSxbMiwzXSxbMyw0XSxbNCw1XSxbNSw2XSxbNiw3XSxbNyw4XV0= +\[\begin{tikzcd} + 0 & {H^0(X, \mathcal F)} & {H^0(X, \mathcal F')} & {H^0(X, \mathcal F'')} \\ + & {H^1(X, \mathcal F)} & {H^1(X, \mathcal F')} & {H^1(X, \mathcal F'')} \\ + & {H^2(X, \mathcal F)} & \cdots + \arrow[from=1-1, to=1-2] + \arrow[from=1-2, to=1-3] + \arrow[from=1-3, to=1-4] + \arrow[from=1-4, to=2-2] + \arrow[from=2-2, to=2-3] + \arrow[from=2-3, to=2-4] + \arrow[from=2-4, to=3-2] + \arrow[from=3-2, to=3-3] +\end{tikzcd}\] +\end{enumerate} diff --git a/iii/alggeom/main.tex b/iii/alggeom/main.tex index 59006a6..0f1f93a 100644 --- a/iii/alggeom/main.tex +++ b/iii/alggeom/main.tex @@ -24,5 +24,7 @@ \section{Modules over the structure sheaf} \input{05_modules_over_the_structure_sheaf.tex} \section{Divisors} \input{06_divisors.tex} +\subsection{Sheaf cohomology} +\input{07_sheaf_cohomology.tex} \end{document} diff --git a/iii/cat/04_limits.tex b/iii/cat/04_limits.tex index 6e61df6..f7ae3d8 100644 --- a/iii/cat/04_limits.tex +++ b/iii/cat/04_limits.tex @@ -444,7 +444,7 @@ \subsection{General adjoint functor theorem} \subsection{Well-poweredness} \begin{definition} Let \( A \in \ob \mathcal C \). - A \emph{subobject} of \( A \) is a monomorphism with codomain \( A \). + A \emph{subobject} of \( A \) is a monomorphism with codomain \( A \); dually, a \emph{quotient} of \( A \) is an epimorphism with domain \( A \). The subobjects of \( A \) in \( \mathcal C \) form a preorder \( \operatorname{Sub}_{\mathcal C}(A) \) by setting \( m \leq m' \) when \( m \) factors through \( m' \). \( \mathcal C \) is \emph{well-powered} if \( \operatorname{Sub}_{\mathcal C}(A) \) is equivalent to a (small) poset for any \( A \). Dually, we say \( \mathcal C \) is \emph{well-copowered}. diff --git a/iii/cat/07_additive_and_abelian_categories.tex b/iii/cat/07_additive_and_abelian_categories.tex index 4ac657c..de797d8 100644 --- a/iii/cat/07_additive_and_abelian_categories.tex +++ b/iii/cat/07_additive_and_abelian_categories.tex @@ -23,3 +23,166 @@ \subsection{Additive categories} \end{enumerate} \end{enumerate} \end{lemma} +\begin{proof} + In each part, as (a) and (b) are dual and (c) is self-dual, it suffices to prove the equivalence of (a) and (b). + + \emph{Part (i).} + If \( A \) is terminal, then it has exactly one morphism \( A \to A \), so this must be the zero morphism. + Conversely, if \( 1_A = 0 \), then \( A \) is terminal, as for any \( f : B \to A \), we have \( f = 1_A f = 0 f = 0 \), so the only morphism \( B \to A \) is the zero morphism. + + \emph{Part (ii).} + If (a) holds, take \( \nu_1, \nu_2 \) to be defined by the first four equations in (c); it suffices to verify the last equation, \( \nu_1 \pi_1 + \nu_2 \pi_2 = 1_C \). + Composing with \( \pi_1 \), + \[ \pi_1 \nu_1 \pi_1 = 1_A \pi_1 + 0 \pi_2 = \pi_1 \] + and similarly, composing with \( \pi_2 \) gives \( \pi_2 \). + So by uniqueness of factorisations through limit cones, \( \nu_1 \pi_1 + \nu_2 \pi_2 \) must be the identity. + Conversely, if (c) holds, given a pair \( f : D \to A \) and \( g : D \to B \), the morphism + \[ h = \nu_1 f + \nu_2 g \] + satisfies + \[ \pi_1 h = 1_A f + 0 g = f;\quad \pi_2 h = 0 f + 1_A g = g \] + giving a factorisation, and if \( h' \) also satisfies these equations, then + \[ h' = (\nu_1 \pi_1 + \nu_2 \pi_2) h' = \nu_1 f + \nu_2 g = h \] + so the factorisation is unique. +\end{proof} +In any category, an object which is both initial and terminal is called a \emph{zero object}, denoted \( 0 \). +An object that is a product and a coproduct of \( A \) and \( B \) is called a \emph{biproduct}, denoted \( A \oplus B \). +\begin{lemma} + Let \( \mathcal C \) be a locally small category. + \begin{enumerate} + \item If \( \mathcal C \) has a zero object, then it has a unique pointed structure. + \item Suppose \( \mathcal C \) has a zero object and has binary products and coproducts. + Suppose further that for each pair \( A, B \in \ob \mathcal C \), the canonical morphism \( c : A + B \to A \times B \) defined by + \[ \pi_i c \nu_j = \begin{cases} + 1 & \text{if } i = j \\ + 0 & \text{if } i \neq j + \end{cases} \] + is an isomorphism. + Then \( \mathcal C \) has a unique semi-additive structure. + \end{enumerate} +\end{lemma} +We adopt the convention that morphisms into a product are denoted with column vectors, and morphisms out of a product are denoted with row vectors. +\begin{proof} + \emph{Part (i).} + The unique morphism \( 0 \to 0 \) is both the identity and a zero morphism. + So for any two \( A, B : \ob \mathcal C \), the unique composite \( A \to 0 \to B \) must be the zero element of \( \mathcal C(A, B) \). + We can define a pointed structure on \( \mathcal C \) in this way. + + \emph{Part (ii).} + This technique is known as the \emph{Eckmann--Hilton argument}. + Given \( f, g : A \rightrightarrows B \), we define the \emph{left sum} \( f +_\ell g \) to be the composite + % https://q.uiver.app/#q=WzAsNCxbMCwwLCJBIl0sWzEsMCwiQiBcXHRpbWVzIEIiXSxbMiwwLCJCK0IiXSxbMywwLCJCIl0sWzAsMSwiXFxiZWdpbntwbWF0cml4fWYgXFxcXCBnXFxlbmR7cG1hdHJpeH0iXSxbMSwyLCJjXnstMX0iXSxbMiwzLCJcXGJlZ2lue3BtYXRyaXh9MSYxXFxlbmR7cG1hdHJpeH0iXV0= +\[\begin{tikzcd}[ampersand replacement=\&] + A \& {B \times B} \& {B+B} \& B + \arrow["{\begin{pmatrix}f \\ g\end{pmatrix}}", from=1-1, to=1-2] + \arrow["{c^{-1}}", from=1-2, to=1-3] + \arrow["{\begin{pmatrix}1&1\end{pmatrix}}", from=1-3, to=1-4] +\end{tikzcd}\] + and the \emph{right sum} \( f +_r g \) to be + % https://q.uiver.app/#q=WzAsNCxbMCwwLCJBIl0sWzEsMCwiQSBcXHRpbWVzIEEiXSxbMiwwLCJCK0IiXSxbMywwLCJCIl0sWzAsMSwiXFxiZWdpbntwbWF0cml4fTEgXFxcXCAxXFxlbmR7cG1hdHJpeH0iXSxbMSwyLCJjXnstMX0iXSxbMiwzLCJcXGJlZ2lue3BtYXRyaXh9ZiZnXFxlbmR7cG1hdHJpeH0iXV0= +\[\begin{tikzcd}[ampersand replacement=\&] + A \& {A \times A} \& {B+B} \& B + \arrow["{\begin{pmatrix}1 \\ 1\end{pmatrix}}", from=1-1, to=1-2] + \arrow["{c^{-1}}", from=1-2, to=1-3] + \arrow["{\begin{pmatrix}f&g\end{pmatrix}}", from=1-3, to=1-4] +\end{tikzcd}\] + Note that \( (f +_\ell g)h = fh +_\ell gh \), since + \[ \begin{pmatrix} + f \\ g + \end{pmatrix} h = \begin{pmatrix} + fh \\ gh + \end{pmatrix} \] + and similarly, + \[ k(f +_r g) = kf +_r kg \] + So if we show that the two sums coincide, we obtain the required distributive laws. + First, note that \( 0 : A \to B \) is a two-sided identity for both \( +_\ell \) and \( +_r \). + For example, \( f +_\ell 0 = f \), since + % https://q.uiver.app/#q=WzAsNSxbMCwwLCJBIl0sWzEsMSwiQiBcXHRpbWVzIEIiXSxbMiwwLCJCIl0sWzMsMSwiQiArIEIiXSxbNCwwLCJCIl0sWzAsMSwiXFxiZWdpbntwbWF0cml4fWYgXFxcXCAwXFxlbmR7cG1hdHJpeH0iLDJdLFswLDIsImYiXSxbMiwxLCJcXGJlZ2lue3BtYXRyaXh9MVxcXFwwXFxlbmR7cG1hdHJpeH0iXSxbMiwzLCJcXG51XzEiXSxbMSwzLCJjXnstMX0iLDJdLFsyLDQsIjFfQiJdLFszLDQsIlxcYmVnaW57cG1hdHJpeH0xJjFcXGVuZHtwbWF0cml4fSIsMl1d +\[\begin{tikzcd}[ampersand replacement=\&] + A \&\& B \&\& B \\ + \& {B \times B} \&\& {B + B} + \arrow["{\begin{pmatrix}f \\ 0\end{pmatrix}}"', from=1-1, to=2-2] + \arrow["f", from=1-1, to=1-3] + \arrow["{\begin{pmatrix}1\\0\end{pmatrix}}", from=1-3, to=2-2] + \arrow["{\nu_1}", from=1-3, to=2-4] + \arrow["{c^{-1}}"', from=2-2, to=2-4] + \arrow["{1_B}", from=1-3, to=1-5] + \arrow["{\begin{pmatrix}1&1\end{pmatrix}}"', from=2-4, to=1-5] +\end{tikzcd}\] + commutes. + Suppose we have morphisms \( f, g, h, k : A \to B \), and consider the composite + % https://q.uiver.app/#q=WzAsNixbMCwwLCJBIl0sWzEsMCwiQSBcXHRpbWVzIEEiXSxbMiwwLCJBICsgQSJdLFszLDAsIkIgXFx0aW1lcyBCIl0sWzQsMCwiQiArIEIiXSxbNSwwLCJCIl0sWzAsMSwiXFxiZWdpbntwbWF0cml4fTFcXFxcMVxcZW5ke3BtYXRyaXh9Il0sWzEsMiwiY157LTF9Il0sWzIsMywiXFxiZWdpbntwbWF0cml4fWYmZ1xcXFxoJmtcXGVuZHtwbWF0cml4fSJdLFszLDQsImNeey0xfSJdLFs0LDUsIlxcYmVnaW57cG1hdHJpeH0xJjFcXGVuZHtwbWF0cml4fSJdXQ== +\[\begin{tikzcd}[ampersand replacement=\&] + A \& {A \times A} \& {A + A} \& {B \times B} \& {B + B} \& B + \arrow["{\begin{pmatrix}1\\1\end{pmatrix}}", from=1-1, to=1-2] + \arrow["{c^{-1}}", from=1-2, to=1-3] + \arrow["{\begin{pmatrix}f&g\\h&k\end{pmatrix}}", from=1-3, to=1-4] + \arrow["{c^{-1}}", from=1-4, to=1-5] + \arrow["{\begin{pmatrix}1&1\end{pmatrix}}", from=1-5, to=1-6] +\end{tikzcd}\] + The composite of the first three factors is + \[ \begin{pmatrix} + f +_r g \\ + h +_r k + \end{pmatrix} \] + so the whole composite is \( (f +_r g) +_\ell (h +_r k) \). + Evaluating from other end, we obtain + \[ (f +_r g) +_\ell (h +_r k) = (f +_\ell h) +_r (g +_\ell k) \] + This is known as the \emph{interchange law}. + Substituting \( g = k = 0 \), we obtain \( f +_\ell k = f +_r k \). + Substituting \( f = k = 0 \) (and dropping the subscripts) we obtain the commutative law \( g + h = h + g \). + Substituting \( h = 0 \), we obtain the associativity law \( (f + g) + k = f + (g + k) \). + + For uniqueness, suppose we have some semi-additive structure \( + \) on \( \mathcal C \). + Then \( \nu_1 \pi_1 + \nu_2 \pi_2 \) must be the inverse of \( c = \begin{pmatrix} + 1 & 0 \\ 0 & 1 + \end{pmatrix} : A + B \to A \times B \), since + \[ \nu_1 \pi_1 c = \nu_1 \begin{pmatrix} + 1 & 0 + \end{pmatrix} = \begin{pmatrix} + \nu_1 & 0 + \end{pmatrix};\quad \nu_2 \pi_2 c =\begin{pmatrix} + 0 & \nu_2 + \end{pmatrix} \] + so + \[ (\nu_1 \pi_1 + \nu_2 \pi_2) c = \begin{pmatrix} + \nu_1 + 0 & 0 + \nu_2 + \end{pmatrix} = \begin{pmatrix} + \nu_1 & \nu_2 + \end{pmatrix} = 1_{A + B} \] + Hence the definitions of \( +_\ell \) and \( +_r \) both reduce to \( + \). +\end{proof} +Note that if \( \mathcal C \) and \( \mathcal D \) are semi-additive categories with finite biproducts, then a functor \( F : \mathcal C \to \mathcal D \) is semi-additive (that is, enriched over \( \mathbf{CMon} \)) if and only if it preserves either finite products or finite coproducts. +In particular, if \( F \) has either a left or right adjoint, then it is semi-additive, and the adjunction is enriched over \( \mathbf{CMon} \); the bijection \( \mathcal C(A, GB) \to \mathcal D(FA, B) \) is an isomorphism of commutative monoids, since the operations \( F(-) \) and \( (-) \epsilon_B \) both respect addition. + +\subsection{Kernels and cokernels} +\begin{definition} + Let \( f : A \to B \) be a morphism in a pointed category \( \mathcal C \). + The \emph{kernel} of \( f \) is the equaliser of the pair \( (f, 0) \); dually the \emph{cokernel} is the coequaliser of \( (f, 0) \). + A monomorphism that occurs as the kernel of a morphism is called \emph{normal}. +\end{definition} +In an additive category, the normal monomorphisms are precisely the regular monomorphisms, since the equaliser of \( (f, g) \) is the kernel of \( f - g \). +In \( \mathbf{Gp} \), all inclusions of subgroups are regular, but not all inclusions are normal, since a normal monomorphism corresponds to a normal subgroup. +In \( \mathbf{Set}_\star \), all surjections are regular epimorphisms, but \( (A, a_0) \to (B, b_0) \) is a normal epimorphism if \( f \) is bijective on elements not mapped to \( b_0 \). +We say that a morphism \( f : A \to B \) is a \emph{pseudomonomorphism} if its kernel is a zero morphism; that is, \( fg = 0 \) implies \( g = 0 \). +\begin{lemma} + In a pointed category with kernels and cokernels, \( f : A \to B \) is normal monic if and only if \( f \cong \ker \coker f \). +\end{lemma} +\begin{proof} + If \( f \cong \ker \coker f \), it is clearly normal. + Now suppose \( f = \ker g \). + Then \( g \) factors through the cokernel of \( f \), so \( g (\ker \coker f) = 0 \). + Thus \( \ker coker f \leq f \) in \( \operatorname{Sub}(B) \). + But \( (\coker f) f = 0 \), so \( f \leq \ker \coker f \), so they are isomorphic as subobjects of \( B \). +\end{proof} +\begin{corollary} + In a pointed category with kernels and cokernels, the operations \( \ker \) and \( \coker \) induce an order-reversing bijection between isomorphism classes of normal subobjects and isomorphism classes of normal quotients of any object. +\end{corollary} +\begin{remark} + For any morphism \( f : A \to B \) in such a category, \( \ker \coker f \) is the smallest normal subobject of \( B \) through which \( f \) factors. +\end{remark} + +\subsection{Abelian categories} +\begin{definition} + An \emph{abelian category} is an additive category with all finite limits and colimits. + Equivalently, an abelian category is a category with a zero object, finite biproducts, kernels, and cokernels, such that all monomorphisms and epimorphisms are normal. +\end{definition} diff --git a/iii/mtncl/06_intuitionistic_logic.tex b/iii/mtncl/06_intuitionistic_logic.tex index 7fb9ed4..457c372 100644 --- a/iii/mtncl/06_intuitionistic_logic.tex +++ b/iii/mtncl/06_intuitionistic_logic.tex @@ -372,7 +372,7 @@ \subsection{Propositions as types} \emph{Part (i).} We use induction over the derivation of \( \Gamma \Vdash M : \varphi \). If \( x \) is a variable not occurring in \( \Gamma' \), and the derivation is of the form \( \Gamma', x : \varphi \Vdash x : \varphi \), then we must prove that \( \abs{\Gamma', x : \varphi} \vdash \varphi \), and this holds as \( \varphi \vdash \varphi \). - + If the derivation has \( M \) of the form \( \lambda x:\sigma.\, N \) and \( \varphi = \sigma \to \tau \), then we must have that \( \Gamma, x: \sigma \Vdash N : \tau \). By the inductive hypothesis, we have \( \abs{\Gamma, x : \sigma} \vdash \tau \), so \( \abs{\Gamma}, \sigma \vdash \tau \). Thus we obtain a proof of \( \sigma \to \tau \) from \( \abs{\Gamma} \) by \( \to \)-I. @@ -421,13 +421,110 @@ \subsection{Propositions as types} \subsection{Full simply typed lambda calculus} The types of the full simply typed \( \lambda \)-calculus \( \mathsf{ST}\lambda\mathsf{C} \) are generated by the following grammar. -\[ \Pi \Coloneq \mathcal U \mid \Pi \to \Pi \mid \Pi \times \Pi \mid \Pi + \Pi | {1} | {0} \] +\[ \Pi \Coloneq \mathcal U \mid \Pi \to \Pi \mid \Pi \times \Pi \mid \Pi + \Pi \mid 1 \mid 0 \] where \( \mathcal U \) is a set of primitive types or type variables. The terms are of the form \begin{align*} \Lambda_\Pi \Coloneq\, & V \mid (\lambda x : \Pi.\, \Lambda_\Pi) \mid \Lambda_\Pi \, \Lambda_\Pi \mid \\ &\langle \Lambda_\Pi, \Lambda_\Pi \rangle \mid \pi_1(\Lambda_\Pi) \mid \pi_2(\Lambda_\Pi) \mid \\ &\iota_1(\Lambda_\Pi) \mid \iota_2(\Lambda_\Pi) \mid \mathsf{case}(\Lambda_\Pi;V.\Lambda_\Pi;V.\Lambda_\Pi) \mid \\ - &\star \mid {!_\Pi \Lambda_\Pi} + &\star \mid {!_\Pi\, \Lambda_\Pi} \end{align*} where \( V \) is an infinite set of variables, and \( \star \) is a constant. +This expanded syntax comes with new typing rules. +\begin{mathpar} + \inferrule{\Gamma \Vdash M : \psi \times \varphi}{\Gamma \Vdash \pi_1(M) : \psi} + \and + \inferrule{\Gamma \Vdash M : \psi \times \varphi}{\Gamma \Vdash \pi_2(M) : \varphi} + \and + \inferrule{\Gamma \Vdash M : \psi \and \Gamma \Vdash N : \varphi}{\Gamma \Vdash \langle M, N \rangle : \psi \times \varphi} + \and + \inferrule{\Gamma \Vdash M : \psi}{\Gamma \Vdash \iota_1(M) : \psi + \varphi} + \and + \inferrule{\Gamma \Vdash M : \varphi}{\Gamma \Vdash \iota_2(M) : \psi + \varphi} + \and + \inferrule{\Gamma \Vdash L : \psi + \varphi \and \Gamma, x : \psi \Vdash M : \rho \and \Gamma, y : \varphi \Vdash N : \rho}{\Gamma \Vdash \mathsf{case}(L;x^\psi.M;y^\varphi.N) : \rho} + \and + \inferrule{\ }{\Gamma \Vdash \star : 1} + \and + \inferrule{\Gamma \Vdash M : 0}{\Gamma \Vdash !_\varphi\, M : \varphi} +\end{mathpar} +This typing relation captures the Brouwer--Heyting--Kolmogorov interpretation when paired with new reduction rules. +\begin{mathpar} + \pi_1(\langle M, N \rangle) \to_\beta M + \and + \pi_2(\langle M, N \rangle) \to_\beta N + \and + \langle \pi_1(M), \pi_2(M) \rangle \to_\eta M + \and + \mathsf{case}(\iota_1(M);x^\psi.K;y^\varphi.L) \to_\beta K[x \coloneq M] + \and + \mathsf{case}(\iota_2(M);x^\psi.K;y^\varphi.L) \to_\beta L[y \coloneq M] + \and + \text{if } \Gamma \Vdash M : 1 \text{ then } M \to_\eta \star +\end{mathpar} +We can expand propositions-as-types to our new types: +\begin{enumerate} + \item \( 0 \) corresponds to \( \bot \); + \item \( 1 \) corresponds to \( \top \); + \item product types correspond to conjunctions; + \item coproduct types correspond to disjunctions. +\end{enumerate} +In this way, propositions correspond to types. +Redexes are now those expressions consisting of a constructor (pair formation, \( \lambda \)-abstraction, and injections) followed by the corresponding destructor (projections, applications, and case expressions). +\begin{example} + Consider the following proof of \( (\varphi \wedge \chi) \to (\psi \to \varphi) \). + \[ \inferrule{ + \inferrule{ + \inferrule{[\varphi \wedge \chi]}{\varphi} \and [\psi] + }{\psi \to \varphi} + }{(\varphi \wedge \chi) \to (\psi \to \varphi)} \] + Annotating the corresponding \( \lambda \)-terms, we obtain + \[ \inferrule{ + \inferrule{ + \inferrule{p : [\varphi \wedge \chi]}{\pi_1(p) : \varphi} \and b : [\psi] + }{\lambda b^\psi.\, \pi_1(p) : \psi \to \varphi} + }{\lambda p^{\varphi \times \chi}.\, \lambda b^\psi.\, \pi_1(p) : (\varphi \wedge \chi) \to (\psi \to \varphi)} \] + Hence this proof tree corresponds to the \( \lambda \)-term + \[ \lambda p^{\varphi \times \chi}.\, \lambda b^\psi.\, \pi_1(p) : (\varphi \times \chi) \to (\psi \to \varphi) \] +\end{example} +In summary, the Curry--Howard correspondence for the whole of \( \mathsf{IPC} \) and \( \mathsf{ST}\lambda\mathsf{C} \) states that +\begin{enumerate} + \item (primitive) types correspond to (primitive) propositions; + \item variables correspond to hypotheses; + \item \( \lambda \)-terms correspond to proofs; + \item inhabitation of a type corresponds to provability of a proposition; + \item term reduction corresponds to proof normalisation. +\end{enumerate} + +\subsection{Heyting semantics} +Boolean algebras represent truth-values of classical propositions. +We can generalise this notion to intuitionistic logic. +\begin{definition} + A \emph{Heyting algebra} \( H \) is a bounded lattice equipped with a binary operation \( \Rightarrow : H \times H \to H \) such that + \[ a \wedge b \leq c \iff a \leq b \Rightarrow c \] + A \emph{morphism} of Heyting algebras is a function that preserves all finite meets and joins (including true and false) and \( \Rightarrow \). +\end{definition} +In particular, if \( f \) is a morphism of Heyting algebras and \( a \leq b \), then \( f(a) \leq f(b) \). +\begin{example} + \begin{enumerate} + \item Every Boolean algebra is a Heyting algebra by defining \( a \Rightarrow b \) to be \( \neg a \vee b \). + Note that \( \neg a = a \Rightarrow \bot \). + \item Every topology is a Heyting algebra, where \( U \Rightarrow V = ((X \setminus U) \cup V)^\circ \). + \item Every finite distributive lattice is a Heyting algebra. + \item The Lindenbaum--Tarski algebra of a propositional theory \( \mathcal T \) with respect to \( \mathsf{IPC} \) is a Heyting algebra. + % important exercise + \end{enumerate} +\end{example} +\begin{definition} + Let \( H \) be a Heyting algebra and let \( \mathcal L \) be a propositional language with a set \( P \) of primitive propositions. + An \emph{\( H \)-valuation} is a function \( v : P \to H \), recursively expanded to \( \mathcal L \) by the rules + \begin{enumerate} + \item \( v(\bot) = \bot \); + \item \( v(A \wedge B) = v(A) \wedge v(B) \); + \item \( v(A \vee B) = v(A) \vee v(B) \); + \item \( v(A \to B) = v(A) \Rightarrow v(B) \). + \end{enumerate} + We say that a proposition \( A \) is \emph{\( H \)-valid} if \( v(A) = \top \) for all valuations \( v \). + \( A \) is an \emph{\( H \)-consequence} of a finite set of propositions \( \Gamma \) if \( v\qty(\bigwedge \Gamma) \leq v(A) \), and write \( \Gamma \vDash_H A \). +\end{definition}