diff --git a/iii/alggeom/06_divisors.tex b/iii/alggeom/06_divisors.tex index cea5655..b6f2824 100644 --- a/iii/alggeom/06_divisors.tex +++ b/iii/alggeom/06_divisors.tex @@ -14,7 +14,8 @@ \subsection{Height and dimension} In the case of Weil divisors, we will assume that the ambient scheme \( X \) is Noetherian, integral, separated, and \emph{regular in codimension 1}. If \( X \) is integral and \( U = \Spec A \) is an open affine, then the ideal \( (0) \subseteq A \) is called the \emph{generic point} of \( X \). -The generic points given by each \( U \) coincide in \( X \). +Each open affine is dense as they are irreducible, so they have a nontrivial intersection, including their generic points. +The generic points given by each \( U \) therefore coincide in \( X \). This point is often denoted by \( \eta \) or \( \eta_X \). \begin{definition} Let \( X \) be a scheme. @@ -43,8 +44,78 @@ \subsection{Weil divisors} If \( X \) is integral, for \( \Spec A = U \subseteq X \), the local ring \( \mathcal O_{X, \eta} \) is a field, as it is in particular the fraction field of \( A \). Indeed, because \( \eta \) is contained in every open affine, \( \mathcal O_{X, \eta} \) permits arbitrary denominators. -Let \( f \in \mathcal O_{X, \eta_X} = k(X) \). +Let \( f \in \mathcal O_{X, \eta_X} = k(X) \) be nonzero. Since for every prime divisor \( Y \subseteq X \), the ring \( \mathcal O_{X, \eta_Y} \) is a discrete valuation ring, we can calculate the valuation \( \nu_Y(f) \) of \( f \) in this ring. We thus define the divisor \[ \operatorname{div}(f) = \sum_{Y \subseteq X \text{ prime}} \nu_Y(f) [Y] \] We claim that this is a Weil divisor; that is, the sum is finite. +\begin{proposition} + The sum + \[ \sum_{Y \subseteq X \text{ prime}} \nu_Y(f) [Y] \] + 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) \). + 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 \). + But \( \nu_Y(f) > 0 \) if and only if \( Y \) is contained in \( \mathbb V(f) \subseteq U \), and by the same argument, there are only finitely many such \( Y \). +\end{proof} +\begin{definition} + A Weil divisor of the form \( \operatorname{div}(f) \) is called \emph{principal}. +\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. + Then \( A \) is a unique factorisation domain if and only if \( A \) is integrally closed and \( \operatorname{Cl}(\Spec A) \) is trivial. + This is related to the fact that in unique factorisation domains, all primes of height 1 are principal. + In particular, there exist rings with nontrivial class groups of their spectra. + \item \( \operatorname{Cl}(\mathbb A^n_k) = 0 \). + \item \( \operatorname{Cl}(\mathbb P^n_k) \cong \mathbb Z \); we will prove this shortly. + % TODO: break here, organise into props/proofs + \item Let \( Z \subseteq X \) is closed, and let \( U = X \setminus Z \). + Then there is a surjective map \( \operatorname{Cl}(X) \twoheadrightarrow \operatorname{Cl}(U) \), defined by \( [Y] \mapsto [Y \cap U] \), but instead mapping \( [Y] \) to zero if \( Y \cap U = \varnothing \). + This is well-defined, as \( k(X) \) and \( k(U) \) are naturally isomorphic, so principal divisors are mapped to principal divisors. + For surjectivity, note that given a prime Weil divisor \( D \subseteq U \), its closure \( \overline D \) in \( X \) is a prime Weil divisor that restricts to \( D \) under the map. + \item If \( Z \) has codimension at least 2, then \( \operatorname{Cl}(X) \twoheadrightarrow \operatorname{Cl}(U) \) is an isomorphism. + This is because \( Z \) does not enter the definition of \( \operatorname{Cl}(X) \). + \item If \( Z \subseteq X \) is integral, closed, and of codimension 1, there is an exact sequence + % https://q.uiver.app/#q=WzAsNCxbMCwwLCJcXG1hdGhiYiBaIl0sWzEsMCwiXFxvcGVyYXRvcm5hbWV7Q2x9KFgpIl0sWzIsMCwiXFxvcGVyYXRvcm5hbWV7Q2x9KFUpIl0sWzMsMCwiMCJdLFswLDEsIjEgXFxtYXBzdG8gW1pdIl0sWzEsMl0sWzIsM11d + \[\begin{tikzcd} + {\mathbb Z} & {\operatorname{Cl}(X)} & {\operatorname{Cl}(U)} & 0 + \arrow["{1 \mapsto [Z]}", from=1-1, to=1-2] + \arrow[from=1-2, to=1-3] + \arrow[from=1-3, to=1-4] + \end{tikzcd}\] + called the \emph{excision} exact sequence. + Indeed, the kernel of \( \operatorname{Cl}(X) \to \operatorname{Cl}(U) \) are exactly the divisors in \( X \) contained in \( Z \). + \end{enumerate} +\end{remark} +\begin{proposition} + Let \( k \) be a field. + Then, \( \operatorname{Cl}(\mathbb P^n_k) \cong \mathbb Z \). +\end{proposition} +\begin{proof} + Let \( D \subseteq \mathbb P^n \) be integral, closed, and of codimension 1. + Then \( D = \mathbb V(f) \) where \( f \) is homogeneous of some degree \( d \); we will define \( \deg(D) = d \). + We extend linearly to obtain a homomorphism \( \deg : \operatorname{Div}(\mathbb P^n_k) \to \mathbb Z \). + We claim that this gives an isomorphism \( \operatorname{Cl}(\mathbb P^n_k) \to \mathbb Z \). + First, this is well defined on classes, since if \( f = \frac{g}{h} \) is a rational function, then \( g \) and \( h \) are homogeneous polynomials of the same degree, so \( \deg(\operatorname{div}(f)) = 0 \). + This is surjective, by taking \( H = \mathbb V(x_0) \) for \( x_0 \) homogeneous linear. + For injectivity, suppose \( D = \sum n_{Y_i} [Y_i] \) with \( \sum n_{Y_i} \deg(Y_i) = 0 \). + Write \( Y_i = \mathbb V(g_i) \), and let \( f = \prod g_i^{n_{Y_i}} \). + Now \( f \) is a homogeneous rational function of degree zero. +\end{proof} + +\subsection{Cartier divisors} +Let \( X \) be a scheme. +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. +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} \). +\end{definition} diff --git a/iii/cat/06_monoidal_and_enriched_categories.tex b/iii/cat/06_monoidal_and_enriched_categories.tex index d39b72c..4e09711 100644 --- a/iii/cat/06_monoidal_and_enriched_categories.tex +++ b/iii/cat/06_monoidal_and_enriched_categories.tex @@ -294,3 +294,104 @@ \subsection{Closed monoidal categories} Then \( S \subseteq (R \Rightarrow T) \) if and only if \( S \circ R \subseteq T \). \end{enumerate} \end{example} + +\subsection{Enriched categories} +\begin{definition} + Let \( (\mathcal E, \otimes, I) \) be a monoidal category. + An \emph{\( \mathcal E \)-enriched category} is + \begin{enumerate} + \item a collection \( \ob \mathcal C \) of objects; + \item an object \( \mathcal C(A, B) \) of \( \mathcal E \) for each pair of objects \( A, B \in \ob \mathcal C \); + \item morphisms \( \iota_A : I \to \mathcal C(A, A) \) for each \( A \); + \item morphisms \( \kappa_{A,B,C} : \mathcal C(B, C) \otimes \mathcal C(A, B) \to \mathcal C(A, C) \) for objects \( A, B, C \), + \end{enumerate} + such that the following diagrams commute. + % https://q.uiver.app/#q=WzAsMyxbMCwwLCJJIFxcb3RpbWVzIFxcbWF0aGNhbCBDKEEsIEIpIl0sWzEsMCwiXFxtYXRoY2FsIEMoQiwgQikgXFxvdGltZXMgXFxtYXRoY2FsIEMoQSwgQikiXSxbMSwxLCJcXG1hdGhjYWwgQyhBLCBCKSJdLFswLDEsIlxcaW90YV9CIFxcb3RpbWVzIDFfe1xcbWF0aGNhbCBDKEEsIEIpfSJdLFsxLDIsIlxca2FwcGFfe0EsQixCfSJdLFswLDIsIlxcbGFtYmRhX3tcXG1hdGhjYWwgQyhBLCBCKX0iLDJdXQ== +\[\begin{tikzcd} + {I \otimes \mathcal C(A, B)} & {\mathcal C(B, B) \otimes \mathcal C(A, B)} \\ + & {\mathcal C(A, B)} + \arrow["{\iota_B \otimes 1_{\mathcal C(A, B)}}", from=1-1, to=1-2] + \arrow["{\kappa_{A,B,B}}", from=1-2, to=2-2] + \arrow["{\lambda_{\mathcal C(A, B)}}"', from=1-1, to=2-2] +\end{tikzcd}\] +% https://q.uiver.app/#q=WzAsMyxbMCwwLCJcXG1hdGhjYWwgQyhBLCBCKSBcXG90aW1lcyBJIl0sWzEsMCwiXFxtYXRoY2FsIEMoQSwgQikgXFxvdGltZXMgXFxtYXRoY2FsIEMoQSwgQSkiXSxbMSwxLCJcXG1hdGhjYWwgQyhBLCBCKSJdLFswLDEsIlxcaW90YV9CIFxcb3RpbWVzIDFfe1xcbWF0aGNhbCBDKEEsIEIpfSJdLFsxLDIsIlxca2FwcGFfe0EsQSxCfSJdLFswLDIsIlxccmhvX3tcXG1hdGhjYWwgQyhBLCBCKX0iLDJdXQ== +\[\begin{tikzcd} + {\mathcal C(A, B) \otimes I} & {\mathcal C(A, B) \otimes \mathcal C(A, A)} \\ + & {\mathcal C(A, B)} + \arrow["{\iota_B \otimes 1_{\mathcal C(A, B)}}", from=1-1, to=1-2] + \arrow["{\kappa_{A,A,B}}", from=1-2, to=2-2] + \arrow["{\rho_{\mathcal C(A, B)}}"', from=1-1, to=2-2] +\end{tikzcd}\] +% https://q.uiver.app/#q=WzAsNSxbMCwwLCIoXFxtYXRoY2FsIEMoQywgRCkgXFxvdGltZXMgXFxtYXRoY2FsIEMoQiwgQykpIFxcb3RpbWVzIFxcbWF0aGNhbCBDKEEsIEIpIl0sWzEsMCwiXFxtYXRoY2FsIEMoQiwgRCkgXFxvdGltZXMgXFxtYXRoY2FsIEMoQSwgQikiXSxbMiwxLCJcXG1hdGhjYWwgQyhBLCBEKSJdLFswLDIsIlxcbWF0aGNhbCBDKEMsIEQpIFxcb3RpbWVzIChcXG1hdGhjYWwgQyhCLCBDKSBcXG90aW1lcyBcXG1hdGhjYWwgQyhBLCBCKSkiXSxbMSwyLCJcXG1hdGhjYWwgQyhDLCBEKSBcXG90aW1lcyBcXG1hdGhjYWwgQyhBLCBDKSJdLFswLDEsIlxca2FwcGEgXFxvdGltZXMgMSJdLFsxLDIsIlxca2FwcGEiXSxbMCwzLCJcXGFscGhhIiwyXSxbMyw0LCIxIFxcb3RpbWVzIFxca2FwcGEiLDJdLFs0LDIsIlxca2FwcGEiLDJdXQ== +\[\begin{tikzcd} + {(\mathcal C(C, D) \otimes \mathcal C(B, C)) \otimes \mathcal C(A, B)} & {\mathcal C(B, D) \otimes \mathcal C(A, B)} \\ + && {\mathcal C(A, D)} \\ + {\mathcal C(C, D) \otimes (\mathcal C(B, C) \otimes \mathcal C(A, B))} & {\mathcal C(C, D) \otimes \mathcal C(A, C)} + \arrow["{\kappa \otimes 1}", from=1-1, to=1-2] + \arrow["\kappa", from=1-2, to=2-3] + \arrow["\alpha"', from=1-1, to=3-1] + \arrow["{1 \otimes \kappa}"', from=3-1, to=3-2] + \arrow["\kappa"', from=3-2, to=2-3] +\end{tikzcd}\] +\end{definition} +\begin{definition} + Let \( \mathcal C, \mathcal D \) be \( \mathcal E \)-enriched categories. + An \emph{\( \mathcal E \)-enriched functor} \( \mathcal C \to \mathcal D \) consists of a map of objects \( F : \ob \mathcal C \to \ob \mathcal D \) together with morphisms \( F_{A,B} : \mathcal C(A, B) \to \mathcal D(FA, FB) \) for each pair of objects \( A, B \in \ob \mathcal C \), in such a way that is compatible with identities and composition. +\end{definition} +\begin{definition} + Let \( F, G : \mathcal C \rightrightarrows \mathcal D \) be \( \mathcal E \)-enriched functors between \( \mathcal E \)-enriched categories. + An \emph{\( \mathcal E \)-enriched natural transformation} \( F \to G \) assigns a morphism \( \theta_A : I \to \mathcal D(FA, GA) \) to each \( A \in \ob \mathcal C \), satisfying the naturality condition + % https://q.uiver.app/#q=WzAsOCxbMCwwLCJcXG1hdGhjYWwgQyhBLCBCKSJdLFsxLDAsIlxcbWF0aGNhbCBEKEZBLCBGQikiXSxbMiwwLCJJIFxcb3RpbWVzIEQoRkEsIEZCKSJdLFsyLDEsIlxcbWF0aGNhbCBEKEZCLCBHQikgXFxvdGltZXMgXFxtYXRoY2FsIEQoRkEsIEZCKSJdLFsyLDIsIlxcbWF0aGNhbCBEKEZBLCBHQikiXSxbMCwxLCJcXG1hdGhjYWwgRChHQSwgR0IpIl0sWzAsMiwiXFxtYXRoY2FsIEQoR0EsIEdCKSBcXG90aW1lcyBJIl0sWzEsMiwiXFxtYXRoY2FsIEQoR0EsIEdCKSBcXG90aW1lcyBcXG1hdGhjYWwgRChGQSwgR0EpIl0sWzAsMSwiRl97QSxCfSJdLFsxLDIsIlxcbGFtYmRhXnstMX0iXSxbMiwzLCJcXHRoZXRhX0IgXFxvdGltZXMgMSJdLFszLDQsIlxca2FwcGEiXSxbMCw1LCJHX3tBLEJ9IiwyXSxbNSw2LCJcXHJob157LTF9IiwyXSxbNiw3LCIxIFxcb3RpbWVzIFxcdGhldGFfQSIsMl0sWzcsNCwiXFxrYXBwYSIsMl1d +\[\begin{tikzcd} + {\mathcal C(A, B)} & {\mathcal D(FA, FB)} & {I \otimes D(FA, FB)} \\ + {\mathcal D(GA, GB)} && {\mathcal D(FB, GB) \otimes \mathcal D(FA, FB)} \\ + {\mathcal D(GA, GB) \otimes I} & {\mathcal D(GA, GB) \otimes \mathcal D(FA, GA)} & {\mathcal D(FA, GB)} + \arrow["{F_{A,B}}", from=1-1, to=1-2] + \arrow["{\lambda^{-1}}", from=1-2, to=1-3] + \arrow["{\theta_B \otimes 1}", from=1-3, to=2-3] + \arrow["\kappa", from=2-3, to=3-3] + \arrow["{G_{A,B}}"', from=1-1, to=2-1] + \arrow["{\rho^{-1}}"', from=2-1, to=3-1] + \arrow["{1 \otimes \theta_A}"', from=3-1, to=3-2] + \arrow["\kappa"', from=3-2, to=3-3] +\end{tikzcd}\] +\end{definition} +If \( \mathcal C \) is an \( \mathcal E \)-enriched category, its \emph{underlying ordinary category} \( \abs{\mathcal C} \) is the category where the objects are those of \( \mathcal C \), the morphisms \( A \to B \) are the morphisms \( I \to \mathcal C(A, B) \) in \( \mathcal E \), where the identity morphisms are given by \( \iota_A \), and the composition of \( g : C \to B \) and \( f : A \to B \) given by +\[\begin{tikzcd} + I & {I \otimes I} & {\mathcal C(B, C) \otimes \mathcal C(A, B)} & {\mathcal C(A, C)} + \arrow["{\lambda_I^{-1}}", from=1-1, to=1-2] + \arrow["{g \otimes f}", from=1-2, to=1-3] + \arrow["\kappa", from=1-3, to=1-4] +\end{tikzcd}\] +One can check that this indeed forms a category. +An \emph{\( \mathcal E \)-enrichment} of an ordinary category \( \mathcal C_0 \) is an \( \mathcal E \)-enriched category \( \mathcal C \) such that \( \abs{\mathcal C} \cong \mathcal C_0 \). +\begin{example} + \begin{enumerate} + \item A category enriched over \( (\mathbf{Set}, \times, 1) \) is a locally small category. + \item A category enriched over the poset \( 2 = \qty{0,1} \) with \( 0 < 1 \) is a preorder. + \item A category enriched over \( (\mathbf{Cat}, \times, \mathbf{1}) \) is a \emph{2-category}. + Its morphisms or \emph{1-arrows} \( A \to B \) are the objects of a category \( \mathcal C(A, B) \). + It has \emph{2-arrows} between parallel pairs \( f, g : A \rightrightarrows B \), which are the morphisms \( f \to g \) in the category \( \mathcal C(A, B) \). + \( \mathbf{Cat} \) is a 2-category, by taking the 2-arrows to be the natural transformations. + The category of small \( \mathcal E \)-enriched categories with \( \mathcal E \)-enriched functors is a 2-category. + \item A category enriched over \( (\mathbf{AbGp}, \otimes, \mathbb Z) \) is an \emph{additive category}. + \item If \( \mathcal E \) is a right closed monoidal category, it has a canonical enrichment structure over itself. + Take \( \mathcal E(A, B) \) to be \( [A, B] \), where \( [A, -] \) is the right adjoint of \( (-) \otimes A \). + The identity \( I \to [A, A] \) is the transpose \( \lambda_A : I \otimes A \to A \), and the composition \( \kappa \) is the transpose of + % https://q.uiver.app/#q=WzAsNCxbMCwwLCIoW0IsIENdIFxcb3RpbWVzIFtBLCBCXSkgXFxvdGltZXMgQSJdLFsxLDAsIltCLENdIFxcb3RpbWVzIChbQSxCXSBcXG90aW1lcyBBKSJdLFsyLDAsIltCLENdIFxcb3RpbWVzIEIiXSxbMywwLCJDIl0sWzAsMSwiXFxhbHBoYSJdLFsxLDIsIjEgXFxvdGltZXMgXFxtYXRocm17ZXZ9Il0sWzIsMywiXFxtYXRocm17ZXZ9Il1d +\[\begin{tikzcd} + {([B, C] \otimes [A, B]) \otimes A} & {[B,C] \otimes ([A,B] \otimes A)} & {[B,C] \otimes B} & C + \arrow["\alpha", from=1-1, to=1-2] + \arrow["{1 \otimes \mathrm{ev}}", from=1-2, to=1-3] + \arrow["{\mathrm{ev}}", from=1-3, to=1-4] +\end{tikzcd}\] + where \( \mathrm{ev} \) is the evaluation map, which is precisely the counit of the adjunction. + \item A one-object \( \mathcal E \)-enriched category is an \emph{(internal) monoid} in \( \mathcal E \); it consists of an object \( M \) of \( \mathcal E \), equipped with morphisms \( e : I \to M \) and \( m : M \otimes M \to M \) satisfying the left and right unit laws and the associativity law. + \begin{enumerate} + \item An internal monoid in \( \mathbf{Set} \) is a monoid. + \item An internal monoid in \( \mathbf{AbGp} \) is a ring. + \item An internal monoid in \( \mathbf{Cat} \) is a strict monoidal category. + \item An internal monoid in \( [\mathcal C, \mathcal C] \) is a monad on \( \mathcal C \). + \end{enumerate} + \end{enumerate} +\end{example} diff --git a/iii/cat/07_additive_and_abelian_categories.tex b/iii/cat/07_additive_and_abelian_categories.tex new file mode 100644 index 0000000..4ac657c --- /dev/null +++ b/iii/cat/07_additive_and_abelian_categories.tex @@ -0,0 +1,25 @@ +\subsection{Additive categories} +In this section, we will study categories enriched over \( (\mathbf{AbGp}, \otimes, \mathbb Z) \); these are called \emph{additive} categories. +We will also consider other weaker enrichments: a category enriched over \( (\mathbf{Set}_\star, \wedge, 2) \) is called \emph{pointed}, and a category enriched over \( (\mathbf{CMon}, \otimes, \mathbb N) \), where \( \mathbf{CMon} \) is the category of commutative monoids, is called \emph{semi-additive}. + +In a pointed category \( \mathcal C \), each \( \mathcal C(A, B) \) has a distinguished element 0, and all composites with zero morphisms are zero morphisms. +In a semi-additive category \( \mathcal C \), each \( \mathcal C(A, B) \) has a binary addition operation which is associative, commutative, and has an identity \( 0 \). +Composition in a semi-additive category is bilinear, so \( (f + g)(h + k) = fh + gh + fk + gk \) whenever the composites are defined. +In an additive category, each morphism \( f \in \mathcal C(A, B) \) has an additive inverse \( -f \in \mathcal C(A, B) \). +\begin{lemma} + \begin{enumerate} + \item For an object \( A \) in a pointed category \( \mathcal C \), the following are equivalent. + \begin{enumerate} + \item \( A \) is a terminal object of \( \mathcal C \). + \item \( A \) is an initial object of \( \mathcal C \). + \item \( 1_A = 0 : A \to A \). + \end{enumerate} + \item For objects \( A, B, C \) in a semi-additive category \( \mathcal C \), the following are equivalent. + \begin{enumerate} + \item there exist morphisms \( \pi_1 : C \to A \) and \( \pi_2 : C \to B \) making \( C \) into a product of \( A \) and \( B \); + \item there exist morphisms \( \nu_1 : A \to C \) and \( \nu_2 : B \to C \) making \( C \) into a coproduct of \( A \) and \( B \); + \item there exist morphisms \( \pi_1 : C \to A, \pi_2 : C \to B, \nu_1 : A \to C, \nu_2 : B \to C \) satisfying + \[ \pi_1 \nu_1 = 1_A;\quad \pi_2 \nu_2 = 1_B;\quad \pi_1 \nu_2 = 0;\quad \pi_2 \nu_1 = 0;\quad \nu_1 \pi_1 + \nu_2 \pi_1 = 1_C \] + \end{enumerate} + \end{enumerate} +\end{lemma} diff --git a/iii/cat/main.tex b/iii/cat/main.tex index f3987e5..b4575f7 100644 --- a/iii/cat/main.tex +++ b/iii/cat/main.tex @@ -22,5 +22,7 @@ \section{Monads} \input{05_monads.tex} \section{Monoidal and enriched categories} \input{06_monoidal_and_enriched_categories.tex} +\section{Additive and abelian categories} +\input{07_additive_and_abelian_categories.tex} \end{document} diff --git a/iii/mtncl/02_quantifier_elimination.tex b/iii/mtncl/02_quantifier_elimination.tex index 99af2b4..497a7b5 100644 --- a/iii/mtncl/02_quantifier_elimination.tex +++ b/iii/mtncl/02_quantifier_elimination.tex @@ -2,7 +2,7 @@ \subsection{Skolem functions} \begin{definition} Let \( \mathcal T \) be an \( \mathcal L \)-theory, and let \( \varphi(\vb x, y) \) be an \( \mathcal L \)-formula where \( \vb x \) is nonempty. A \emph{Skolem function} for \( \varphi \) is an \( \mathcal L \)-term \( t \) such that - \[ \mathcal T \vdash \forall \vb x.\, (\exists y.\, \varphi(\vb x, y) \Rightarrow \varphi(\vb x, t(\vb x))) \] + \[ \mathcal T \vdash \forall \vb x.\, (\exists y.\, \varphi(\vb x, y) \to \varphi(\vb x, t(\vb x))) \] A \emph{skolemisation} of an \( \mathcal L \)-theory \( \mathcal T \) is a language \( \mathcal L^+ \supseteq \mathcal L \) and an \( \mathcal L^+ \)-theory \( \mathcal T^+ \supseteq \mathcal T \) such that \begin{enumerate} \item every \( \mathcal L \)-structure that models \( \mathcal T \) can be expanded to an \( \mathcal L^+ \)-structure that models \( \mathcal T^+ \); @@ -39,7 +39,7 @@ \subsection{Skolem functions} \end{remark} \begin{proof} \emph{Part (i).} - Clearly, \( \varphi(\vb x, t(\vb x)) \Rightarrow \exists y.\, \varphi(\vb x, y) \) in any model. + Clearly, \( \varphi(\vb x, t(\vb x)) \to \exists y.\, \varphi(\vb x, y) \) in any model. So having Skolem functions means that \[ \mathcal T \vdash \forall \vb x.\, (\exists y.\, \varphi(\vb x, y) \Leftrightarrow \varphi(\vb x, t(\vb x))) \] completing the proof by the previous proposition. @@ -70,7 +70,7 @@ \subsection{Skolemisation theorem} If \( \chi(\vb x, y) \) is an \( \mathcal L \)-formula with \( \vb x \) nonempty, we add a function symbol \( F_\chi \) of arity \( \abs{\vb x} \). Performing this for all \( \mathcal L \)-formulae of this form, we obtain a language \( \mathcal L' \supseteq \mathcal L \). Next, define \( \Sigma(\mathcal L) \) to be the set of \( \mathcal L \)-sentences that enforce the correct behaviour of the \( F_\chi \): - \[ \forall \vb x.\, (\exists y.\, \chi(\vb x, y) \Rightarrow \chi(\vb x, F_\chi(\vb x))) \] + \[ \forall \vb x.\, (\exists y.\, \chi(\vb x, y) \to \chi(\vb x, F_\chi(\vb x))) \] Note that \( \Sigma(\mathcal L) \) is an \( \mathcal L' \)-theory, not an \( \mathcal L \)-theory; there may be existentials in \( \mathcal L' \) without explicit witnesses. We can overcome this issue by iterating this construction \( \omega \) times and taking the union. Formally, we recursively define @@ -174,11 +174,11 @@ \subsection{Elimination sets} \subsection{Amalgamation} \begin{definition} Let \( \mathcal M \) and \( \mathcal N \) be \( \mathcal L \)-structures. - We write \( \mathcal M \Rightarrow_1 \mathcal N \) if every existential sentence modelled by \( \mathcal M \) is also modelled by \( \mathcal N \). + We write \( \mathcal M \to_1 \mathcal N \) if every existential sentence modelled by \( \mathcal M \) is also modelled by \( \mathcal N \). \end{definition} \begin{theorem}[existential amalgamation] Let \( \mathcal M \) and \( \mathcal N \) be \( \mathcal L \)-structures, with \( S \subseteq \mathcal M \). - Suppose there is a homomorphism \( f : \langle S \rangle_{\mathcal M} \to \mathcal N \) such that \( (\mathcal N, f(S)) \Rightarrow_1 (\mathcal M, S) \). + Suppose there is a homomorphism \( f : \langle S \rangle_{\mathcal M} \to \mathcal N \) such that \( (\mathcal N, f(S)) \to_1 (\mathcal M, S) \). Then there is an elementary extension \( \mathcal K \) of \( \mathcal N \) and an embedding \( g : \mathcal M \rightarrowtail \mathcal K \) making the following diagram commute. \[\begin{tikzcd} & {\mathcal K} \\ @@ -203,7 +203,7 @@ \subsection{Amalgamation} \[ \mathcal T' \vdash \neg\psi(\vb s, \vb n') \] Now, note that \( \mathcal T' \) has nothing to say about \( \vb n' \), so in fact \[ \mathcal T' \vdash \forall \vb x.\, \neg\psi(\vb s, \vb x) \] - As \( (\mathcal N, f(S)) \Rightarrow_1 (\mathcal M, S) \), we can convert the universal quantifier above into the negation of an existential quantifier to conclude + As \( (\mathcal N, f(S)) \to_1 (\mathcal M, S) \), we can convert the universal quantifier above into the negation of an existential quantifier to conclude \[ \mathcal N \vdash \neg\exists \vb x.\, \psi(\vb s, \vb x) \] so \[ \mathcal N \vdash \neg\exists \vb x.\, \psi(\vb s, \vb x) \] @@ -365,7 +365,7 @@ \subsection{Characterisations of quantifier elimination} \emph{(ii) implies (iii).} We use the existential amalgamation theorem. - Take \( S \) to be the set of all elements of \( \mathcal A \), then by (ii), \( (\mathcal B, e(S)) \Rightarrow_1 (\mathcal A, S) \). + Take \( S \) to be the set of all elements of \( \mathcal A \), then by (ii), \( (\mathcal B, e(S)) \to_1 (\mathcal A, S) \). We obtain % https://q.uiver.app/#q=WzAsNCxbMSwyLCJcXG1hdGhjYWwgQSJdLFswLDEsIlxcbWF0aGNhbCBBIl0sWzEsMCwiXFxtYXRoY2FsIEQiXSxbMiwxLCJcXG1hdGhjYWwgQiJdLFswLDEsIjFfQSJdLFsxLDIsIlxccHJlY2VxIl0sWzAsMywiZSIsMix7InN0eWxlIjp7InRhaWwiOnsibmFtZSI6Im1vbm8ifX19XSxbMywyLCJnIiwyLHsic3R5bGUiOnsidGFpbCI6eyJuYW1lIjoibW9ubyJ9fX1dXQ== \[\begin{tikzcd} @@ -400,7 +400,7 @@ \subsection{Characterisations of quantifier elimination} Then the following are equivalent. \begin{enumerate} \item \( \mathcal T \) has quantifier elimination. - \item If \( \mathcal A, \mathcal B \vDash \mathcal T \) and \( \vb a \in \mathcal A, \vb b \in \mathcal B \) are tuples of the same length, then \( (\mathcal A, \vb a) \equiv_0 (\mathcal B, \vb b) \) implies \( (\mathcal A, \vb a) \Rightarrow_1 (\mathcal B, \vb b) \). + \item If \( \mathcal A, \mathcal B \vDash \mathcal T \) and \( \vb a \in \mathcal A, \vb b \in \mathcal B \) are tuples of the same length, then \( (\mathcal A, \vb a) \equiv_0 (\mathcal B, \vb b) \) implies \( (\mathcal A, \vb a) \to_1 (\mathcal B, \vb b) \). \item Whenever \( \mathcal A, \mathcal B \vDash \mathcal T \), \( S \subseteq \mathcal A \) and \( e : \langle S \rangle_{\mathcal A} \rightarrowtail \mathcal B \), then there is an elementary extension \( \mathcal D \) of \( \mathcal B \) and an embedding \( f : \mathcal A \rightarrowtail \mathcal D \) extending \( e \). \item \( \mathcal T \) is model-complete and \( \mathcal T_\forall \) has the amalgamation property. \item For every quantifier-free \( \mathcal L \)-formula \( \varphi(\vb x, y) \), the formula \( \exists y.\, \varphi(\vb x, y) \) is \( \mathcal T \)-equivalent to a quantifier-free formula \( \psi(\vb x) \). @@ -410,8 +410,8 @@ \subsection{Characterisations of quantifier elimination} (i) implies (ii) is clear. \emph{(ii) implies (iii).} - It suffices to show that \( (\mathcal A, \vb a) \Rightarrow_1 (\mathcal B, e(\vb a)) \) by the existential amalgamation theorem. - Since a sentence in \( \mathcal L_S \) is finite, it can only mention finitely many of the new constants in \( S \), so it is enough to check that \( (\mathcal A, \vb a) \Rightarrow_1 (\mathcal B, e(\vb a)) \) for all tuples \( \vb a \) obtainable from \( S \). + It suffices to show that \( (\mathcal A, \vb a) \to_1 (\mathcal B, e(\vb a)) \) by the existential amalgamation theorem. + Since a sentence in \( \mathcal L_S \) is finite, it can only mention finitely many of the new constants in \( S \), so it is enough to check that \( (\mathcal A, \vb a) \to_1 (\mathcal B, e(\vb a)) \) for all tuples \( \vb a \) obtainable from \( S \). Now, if \( \vb a \) is such a tuple and \( e : \langle S \rangle_{\mathcal A} \rightarrowtail \mathcal B \) is an embedding, then \( (\mathcal A, \vb a) \equiv_0 (\mathcal B, e(\vb a)) \), giving the required result by (ii). \emph{(iii) implies (iv).} @@ -489,7 +489,7 @@ \subsection{Characterisations of quantifier elimination} \[ (\mathcal A, \vb b) \vDash \exists \vb y.\, \varphi(\vb b, \vb y) \] then \( f(\vb m) \) must witness the truth of \[ (\mathcal A, \vb c) \vDash \exists \vb y.\, \varphi(\vb c, \vb y) \] - Thus, \( (\mathcal A, \vb b) \Rightarrow_1 (\mathcal A, \vb c) \) as required. + Thus, \( (\mathcal A, \vb b) \to_1 (\mathcal A, \vb c) \) as required. \end{proof} \begin{example} Let \( V \) be a finite vector space. @@ -507,7 +507,7 @@ \subsection{Characterisations of quantifier elimination} \begin{proof} We show that condition (ii) of the theorem above holds. Let \( \mathcal A, \mathcal B \) be models of \( \mathcal T \), and \( \vb a \in \mathcal A, \vb b \in \mathcal B \) be such that \( (\mathcal A, \vb a) \equiv_0 (\mathcal B, \vb b) \). - It suffices to show that \( (\mathcal A, \vb a) \Rightarrow_1 (\mathcal B, \vb b) \). + It suffices to show that \( (\mathcal A, \vb a) \to_1 (\mathcal B, \vb b) \). Let \( \varphi(\vb x, y) \) be quantifier-free, and such that \( \mathcal A \vDash \exists \vb y.\, \varphi(\vb a, \vb y) \). Let \( \vb c = (c_0, \dots, c_{k-1}) \in \mathcal A \) be such a witness, so \( \mathcal A \vDash \varphi(\vb a, \vb c) \). @@ -552,7 +552,7 @@ \subsection{Applications} There are only finitely many points \( c_0, \dots, c_{n-1} \in \mathcal A \) that are roots for the \( q_j(y) \). Since the real closed fields satisfy the intermediate value theorem for polynomials, the \( q_j(y) \) can only change sign at the \( c_i \). Note that - \[ \mathcal A \vDash \forall x y.\, x < y \Rightarrow \exists z.\, (x < z \wedge z < y) \] + \[ \mathcal A \vDash \forall x y.\, x < y \to \exists z.\, (x < z \wedge z < y) \] Since the \( c_i \) lie in \( \mathcal A \), there is an element of \( \mathcal A \) between any pair of distinct \( c_i \). Suppose \( b \) witnesses \( \exists y.\, \varphi(\vb a, y) \) in \( \mathcal B \). If there is a smallest interval \( (c_i, c_j) \) containing \( \mathcal B \), we can pick \( a \in \mathcal A \) also inside this interval, giving \( \mathcal A \vDash \varphi(\vb a, a) \) as required. diff --git a/iii/mtncl/04_types.tex b/iii/mtncl/04_types.tex index b64d8ce..06940a6 100644 --- a/iii/mtncl/04_types.tex +++ b/iii/mtncl/04_types.tex @@ -125,7 +125,7 @@ \subsection{Isolated points} \begin{definition} Let \( \mathcal T \) be an \( \mathcal L \)-theory. We say that a formula \( \varphi(x_1, \dots, x_n) \) \emph{isolates} the \( n \)-type \( p \) of \( \mathcal T \) if \( \mathcal T \cup \qty{\varphi} \) is satisfiable, and - \[ \mathcal T \vDash \forall \vb x.\, (\varphi(\vb x) \Rightarrow \psi(\vb x)) \] + \[ \mathcal T \vDash \forall \vb x.\, (\varphi(\vb x) \to \psi(\vb x)) \] for all \( \psi \in p \). \end{definition} \begin{proposition} @@ -150,7 +150,7 @@ \subsection{Omitting types} \begin{proof} Let \( C = \qty{c_0, c_1, \dots} \) be a countable set of new constants. We expand \( \mathcal T \) to a consistent \( \mathcal L_C \)-theory \( \mathcal T^\star \) by adding recursively defined sentences \( \theta_0, \theta_1, \dots \). - We will do this in such a way that \( \theta_t \Rightarrow \theta_s \) for all \( s < t \). + We will do this in such a way that \( \theta_t \to \theta_s \) for all \( s < t \). To build the \( \theta \), we first enumerate the \( n \)-tuples \( C^n = \qty{\vb d_0, \vb d_1, \dots} \), and enumerate the \( \mathcal L_C \)-sentences \( \varphi_0, \varphi_1, \dots \). Start with \( \theta_0 = \forall x.\, x = x \), which is trivially true. @@ -159,13 +159,13 @@ \subsection{Omitting types} First, suppose \( s = 2i \). These sentences will be designed to turn \( C \) into the domain of an elementary substructure of some model of \( \mathcal T^\star \). Suppose that \( \varphi_i = \exists x.\, \psi(x) \) is existential, with parameters in \( C \) as \( \varphi \) is an \( \mathcal L_C \)-formula. - Suppose \( \mathcal T \vDash \theta_s \Rightarrow \varphi_i \). + Suppose \( \mathcal T \vDash \theta_s \to \varphi_i \). As only finitely many constants from \( C \) have been used so far, we can find some unused \( c \in C \). Let \[ \theta_{s + 1} = \theta_s \wedge \psi(c) \] If \( \mathcal N \) models \( \mathcal T \cup \qty{\theta_s} \), then there is a witness to \( \psi \) in \( \mathcal N \), so we can interpret \( c \) as this witness. Thus, \( \mathcal N \) models \( \mathcal T \cup \qty{\theta_{s+1}} \), so this theory is consistent. - If \( \varphi_i \) is not existential, or \( \mathcal T \nvDash \theta_s \Rightarrow \varphi_i \), then define \( \theta_{s + 1} = \theta_s \). + If \( \varphi_i \) is not existential, or \( \mathcal T \nvDash \theta_s \to \varphi_i \), then define \( \theta_{s + 1} = \theta_s \). Now, suppose \( s = 2i + 1 \). These sentences will be designed to ensure that \( C \) omits \( p \). diff --git a/iii/mtncl/06_intuitionistic_logic.tex b/iii/mtncl/06_intuitionistic_logic.tex index 3b57550..7fb9ed4 100644 --- a/iii/mtncl/06_intuitionistic_logic.tex +++ b/iii/mtncl/06_intuitionistic_logic.tex @@ -4,7 +4,7 @@ \subsection{The Brouwer--Heyting--Kolmogorov interpretation} \begin{enumerate} \item \( \bot \) has no proof. \item To prove \( \varphi \wedge \psi \), one must provide a proof of \( \varphi \) together with a proof of \( \psi \). - \item To prove \( \varphi \Rightarrow \psi \), one must provide a mechanism for translating a proof of \( \varphi \) into a proof of \( \psi \). + \item To prove \( \varphi \to \psi \), one must provide a mechanism for translating a proof of \( \varphi \) into a proof of \( \psi \). In particular, to prove \( \neg\varphi \), we must provide a way to turn a proof of \( \varphi \) into a contradiction. \item To prove \( \varphi \vee \psi \), we must specify either \( \varphi \) or \( \psi \), and then provide a proof for it. Note that in a classical setting, a proof of \( \varphi \vee \psi \) need not specify which of the two disjuncts is true. @@ -82,9 +82,9 @@ \subsection{Natural deduction} We now define the introduction and elimination rules for implication. The elimination rule is known as \emph{modus ponens}. \begin{mathpar} - \inferrule[\( \Rightarrow \)-I]{\Gamma, A \vdash B}{\Gamma \vdash A \Rightarrow B} + \inferrule[\( \to \)-I]{\Gamma, A \vdash B}{\Gamma \vdash A \to B} \and - \inferrule[\( \Rightarrow \)-E]{\Gamma \vdash A \Rightarrow B \and \Gamma \vdash A}{\Gamma \vdash B} + \inferrule[\( \to \)-E]{\Gamma \vdash A \to B \and \Gamma \vdash A}{\Gamma \vdash B} \end{mathpar} We finally define a rule called the \emph{axiom schema}, that allows us to prove our assumptions. \[ \inferrule[Ax]{\ }{\Gamma, A \vdash A} \] @@ -99,8 +99,8 @@ \subsection{Natural deduction} We will additionally use the informal notation \[ \inferrule*[right={\( (A, B) \)}]{{\begin{matrix} [A]\\\vdots\\X \end{matrix}} \and {\begin{matrix} [B]\\\vdots\\Y \end{matrix}}}{C} \] to mean that if we can prove \( X \) assuming \( A \) and we can prove \( Y \) assuming \( B \), then we can infer \( C \) by discharging the open assumptions \( A \) and \( B \). -For example, we can write an instance of \( \Rightarrow \)-I as -\[ \inferrule*[right={\( (A) \)}]{\ {\begin{matrix} \Gamma, [A]\\\vdots\\B \end{matrix}}\ }{\Gamma \vdash A \Rightarrow B} \] +For example, we can write an instance of \( \to \)-I as +\[ \inferrule*[right={\( (A) \)}]{\ {\begin{matrix} \Gamma, [A]\\\vdots\\B \end{matrix}}\ }{\Gamma \vdash A \to B} \] To extend this to intuitionistic predicate logic \( \mathsf{IQC} \), we need to add rules for quantifiers. \begin{mathpar} \inferrule[\( \exists \)-I]{\Gamma \vdash \varphi[x \coloneq t]}{\Gamma \vdash \exists x.\, \varphi(x)} @@ -112,34 +112,34 @@ \subsection{Natural deduction} \inferrule[\( \forall \)-E]{\Gamma \vdash \forall x.\, \varphi}{\Gamma \vdash \varphi[x \coloneq t]} \end{mathpar} \begin{example} - We will show that \( \vdash_{\mathsf{IPC}} A \wedge B \Rightarrow B \wedge A \). - \[ \inferrule*[right=\( \Rightarrow \)-I]{\inferrule*[right=\( \wedge \)-I]{ + We will show that \( \vdash_{\mathsf{IPC}} A \wedge B \to B \wedge A \). + \[ \inferrule*[right=\( \to \)-I]{\inferrule*[right=\( \wedge \)-I]{ \inferrule*[right=\( \wedge \)-E]{[A \wedge B]}{B} \and \inferrule*[right=\( \wedge \)-E]{[A \wedge B]}{A} - }{B \wedge A}}{A \wedge B \Rightarrow B \wedge A} \] + }{B \wedge A}}{A \wedge B \to B \wedge A} \] \end{example} \begin{example} We will show that the logical axioms - \[ \varphi \Rightarrow (\psi \Rightarrow \varphi);\quad (\varphi \Rightarrow (\psi \Rightarrow \chi)) \Rightarrow ((\varphi \Rightarrow \psi) \Rightarrow (\varphi \Rightarrow \chi)) \] + \[ \varphi \to (\psi \to \varphi);\quad (\varphi \to (\psi \to \chi)) \to ((\varphi \to \psi) \to (\varphi \to \chi)) \] are intuitionistically valid. - \[ \inferrule*[right={(\( \Rightarrow \)-I, \( \varphi \))}]{ - \inferrule*[right={(\( \Rightarrow \)-I, \( \psi \))}]{ + \[ \inferrule*[right={(\( \to \)-I, \( \varphi \))}]{ + \inferrule*[right={(\( \to \)-I, \( \psi \))}]{ \inferrule*[right=Ax]{[\varphi]}{\varphi} \and [\psi] - }{\psi \Rightarrow \varphi} - }{\varphi \Rightarrow (\psi \Rightarrow \varphi)} \] + }{\psi \to \varphi} + }{\varphi \to (\psi \to \varphi)} \] For the second axiom, - \[ \inferrule*[right=\( (\varphi \Rightarrow (\psi \Rightarrow \chi)) \)]{ - \inferrule*[right=\( (\varphi \Rightarrow \psi) \)]{ + \[ \inferrule*[right=\( (\varphi \to (\psi \to \chi)) \)]{ + \inferrule*[right=\( (\varphi \to \psi) \)]{ \inferrule*[right=\( (\varphi) \)]{ - \inferrule*[right=\( \Rightarrow \)-E]{ - \inferrule*[right=\( \Rightarrow \)-E]{[\varphi \Rightarrow (\psi \Rightarrow \chi)] \and [\varphi]}{\psi \Rightarrow \chi} + \inferrule*[right=\( \to \)-E]{ + \inferrule*[right=\( \to \)-E]{[\varphi \to (\psi \to \chi)] \and [\varphi]}{\psi \to \chi} \and - \inferrule*[right=\( \Rightarrow \)-E]{[\varphi \Rightarrow \psi] \and [\varphi]}{\psi} + \inferrule*[right=\( \to \)-E]{[\varphi \to \psi] \and [\varphi]}{\psi} }{\chi} - }{\varphi \Rightarrow \chi} - }{(\varphi \Rightarrow \psi) \Rightarrow (\varphi \Rightarrow \chi)} - }{(\varphi \Rightarrow (\psi \Rightarrow \chi)) \Rightarrow ((\varphi \Rightarrow \psi) \Rightarrow (\varphi \Rightarrow \chi))} \] + }{\varphi \to \chi} + }{(\varphi \to \psi) \to (\varphi \to \chi)} + }{(\varphi \to (\psi \to \chi)) \to ((\varphi \to \psi) \to (\varphi \to \chi))} \] \end{example} \begin{lemma} If \( \Gamma \vdash_{\mathsf{IPC}} \varphi \), then \( \Gamma, \psi \vdash_{\mathsf{IPC}} \varphi \). @@ -164,7 +164,7 @@ \subsection{The simply typed lambda calculus} Given a context \( \Gamma \in \mathcal C \), we also write \( \Gamma, x : \tau \) for the context \( \Gamma \cup \qty{x : \tau} \). The \emph{domain} of \( \Gamma \) is the set \( \dom \Gamma \) of variables that appear in \( \Gamma \); similarly, the \emph{range} of \( \Gamma \) is the set \( \abs{\Gamma} \) of types that appear in \( \Gamma \). -The \emph{typability relation} \( (-) \Vdash (-) : (-) \) is a relation on \( C \times \Lambda_\Pi \times \Pi \), defined recursively using the following rules. +The \emph{typability relation} \( (-) \Vdash (-) : (-) \) is a relation on \( \mathcal C \times \Lambda_\Pi \times \Pi \), defined recursively using the following rules. \begin{enumerate} \item For every context \( \Gamma \), variable \( x \notin \dom \Gamma \), and type \( \tau \), we have \( \Gamma, x : \tau \Vdash x : \tau \). \item Let \( \Gamma \) be a context, \( x \notin \dom \Gamma \), let \( \sigma, \tau \) be types, and let \( M \) be a \( \lambda \)-term. @@ -344,3 +344,90 @@ \subsection{\texorpdfstring{\( \beta \)}{β}-normal form} So if \( M \to_\beta M' \) by reducing \( \Delta \), it is always the case that \( m(M') < m(M) \) in the lexicographic order. By the inductive hypothesis, \( M' \) can be reduced to \( \beta \)-normal form, so the result also holds for \( M \). \end{proof} +\begin{theorem}[strong normalisation theorem] + Let \( \Gamma \Vdash M : \sigma \). + Then there is no infinite sequence + \[ M \to_\beta M_1 \to_\beta M_2 \to_\beta \cdots \] +\end{theorem} +The proof is omitted. + +\subsection{Propositions as types} +We will work with the fragment of \( \mathsf{IPC} \), denoted \( \mathsf{IPC}(\to) \), where the only connective is \( \to \), and the deduction rules are \( \to \)-I, \( \to \)-E, \textsc{Ax}. + +If \( \mathcal L \) is a propositional language for \( \mathsf{IPC}(\to) \) and \( P \) is its set of primitive propositions, we can generate a simply typed \( \lambda \)-calculus \( \lambda(\to) \) by taking the set of primitive types \( \mathcal U \) to be \( P \). +Then the types \( \Pi \) and the propositions \( \mathcal L \) are generated by the same grammar +\[ \mathcal U \mid \Pi \to \Pi \] +A proposition is thus the type of its proofs, and a context is a set of hypotheses. +\begin{proposition}[Curry--Howard correspondence for \( \mathsf{IPC}(\to) \)] + Let \( \Gamma \) be a context for \( \lambda(\to) \), and let \( \varphi \) be a proposition. + Then + \begin{enumerate} + \item If \( \Gamma \Vdash M : \varphi \), then + \[ \abs{\Gamma} = \qty{\tau \in \Pi \mid \exists x.\, (x : \tau) \in \Gamma} \vdash_{\mathsf{IPC}(\to)} \varphi \] + \item If \( \Gamma \vdash_{\mathsf{IPC}(\to)} \varphi \), then there is a simply typed \( \lambda \)-term \( M \) such that + \[ \qty{(x_\tau : \tau) \mid \tau \in \Gamma} \Vdash M : \varphi \] + \end{enumerate} +\end{proposition} +\begin{proof} + \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. + + If the derivation is of the form \( \Gamma \Vdash (P\, Q) : \varphi \), then we must have \( \Gamma \Vdash P : \sigma \to \varphi \) and \( \Gamma \Vdash Q : \sigma \) for some \( \sigma \). + By the inductive hypothesis, \( \abs{\Gamma} \vdash \sigma \to \varphi \) and \( \abs{\Gamma} \vdash \sigma \). + Then the result holds by \( \to \)-E. + + \emph{Part (ii).} + We use induction over the proof tree of \( \Gamma \vdash_{\mathsf{IPC}(\to)} \varphi \). + We write + \[ \Delta = \qty{(x_\tau : \tau) \mid \tau \in \Gamma} \] + Suppose that we are at a stage of the proof that uses \textsc{Ax}, so \( \Gamma, \varphi \vdash \varphi \). + If \( \varphi \in \Gamma \), then clearly \( \Delta \Vdash x_\varphi : \varphi \). + Otherwise, \( \Delta, x_\varphi : \varphi \Vdash x_\varphi : \varphi \) as required. + + Suppose that we are at a stage of the proof that uses \( \to \)-E, so + \[ \inferrule{\Gamma \vdash \varphi \to \psi \and \Gamma \vdash \varphi}{\Gamma \vdash \psi} \] + By the inductive hypothesis, there are \( \lambda \)-terms \( M, N \) such that \( \Delta \Vdash M : \varphi \to \psi \) and \( \Delta \Vdash N : \varphi \). + Then \( \Delta \Vdash (M\, N) : \psi \) as required. + + Finally, suppose we are at a stage of the proof that uses \( \to \)-I, so + \[ \inferrule{\Gamma, \varphi \vdash \psi}{\Gamma \vdash \varphi \to \psi} \] + If \( \varphi \in \Gamma \), then by the inductive hypothesis, there is a \( \lambda \)-term \( M \) such that \( \Delta \Vdash M : \psi \). + By the weakening rule, \( \Delta, x : \varphi \Vdash M : \psi \) where \( x \) is a variable that does not occur in \( \Delta \). + Then \( \Delta \Vdash (\lambda x:\varphi.\, M) : \varphi \to \psi \) as required. + Now suppose \( \varphi \notin \Gamma \). + By the inductive hypothesis we obtain a \( \lambda \)-term \( M \) such that \( \Delta, x_\varphi : \varphi \Vdash M : \psi \). + Then similarly \( \Delta \Vdash (\lambda x_\varphi:\varphi.\, M) : \varphi \to \psi \). +\end{proof} +This justifies the Brouwer--Heyting--Kolmogorov interpretation of intuitionistic logic. +\begin{example} + Let \( \varphi, \psi \) be primitive propositions, and consider the \( \lambda \)-term + \[ \lambda f:(\varphi \to \psi) \to \varphi.\,\lambda g: \varphi \to \psi.\, g(fg) \] + This term has type + \[ ((\varphi \to \psi) \to \varphi) \to ((\varphi \to \psi) \to \psi) \] + The term encodes a proof of this proposition in \( \vdash_{\mathsf{IPC}(\to)} \). + The corresponding proof tree is + \[ \inferrule*[right=\( \to \)-I] + {\inferrule*[right=\( \to \)-I]{\inferrule*[right=\( \to \)-E]{ + \inferrule*[right=\( \to \)-E]{g : [\varphi \to \psi] \and f : [(\varphi \to \psi) \to \varphi]}{fg : \varphi} + \and g : [\varphi \to \psi]}{g(fg) : \psi}} + {\lambda g: \varphi \to \psi.\, g(fg) : (\varphi \to \psi) \to \psi}} + {\lambda f:(\varphi \to \psi) \to \varphi.\,\lambda g: \varphi \to \psi.\, g(fg) : ((\varphi \to \psi) \to \varphi) \to ((\varphi \to \psi) \to \psi)} \] +\end{example} + +\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} \] +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} +\end{align*} +where \( V \) is an infinite set of variables, and \( \star \) is a constant.