From a2793fe122bf9d6e1280a507780916b6f1b8883e Mon Sep 17 00:00:00 2001 From: zeramorphic <50671761+zeramorphic@users.noreply.github.com> Date: Mon, 27 Nov 2023 12:57:32 +0000 Subject: [PATCH] Lectures 23B --- iii/alggeom/07_sheaf_cohomology.tex | 72 +++- iii/alggeom/main.tex | 2 +- .../07_additive_and_abelian_categories.tex | 379 ++++++++++++++++++ iii/mtncl/06_intuitionistic_logic.tex | 85 ++++ 4 files changed, 534 insertions(+), 4 deletions(-) diff --git a/iii/alggeom/07_sheaf_cohomology.tex b/iii/alggeom/07_sheaf_cohomology.tex index fa658a6..9198841 100644 --- a/iii/alggeom/07_sheaf_cohomology.tex +++ b/iii/alggeom/07_sheaf_cohomology.tex @@ -1,7 +1,8 @@ -\subsection{???} +\subsection{Introduction and properties} 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. +Given a topological space \( X \) and a sheaf \( \mathcal F \) of abelian groups, there is a series of \emph{cohomology} groups \( H^i(X, \mathcal F) \) for \( i \in \mathbb N \). +The definition will be omitted. +These groups 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) \). @@ -29,4 +30,69 @@ \subsection{???} \arrow[from=2-4, to=3-2] \arrow[from=3-2, to=3-3] \end{tikzcd}\] + \item If \( X \) is an affine scheme and \( \mathcal F \) is a quasi-coherent sheaf, then \( H^i(X, \mathcal F) = 0 \) for all \( i > 0 \). + \item If \( X \) is a Noetherian separated scheme, then \( H^i(X, \mathcal F) \) can be computed from the sections of \( \mathcal F \) on an open affine cover \( \qty{U_i} \) and from the data of the restrictions to \( \mathcal F(U_i \cap U_j), \mathcal F(U_i \cap U_j \cap U_k) \) and so on. + This is a property of \emph{\v{C}ech cohomology}. \end{enumerate} + +\subsection{\v{C}ech cohomology} +Let \( X \) be a topological space, and let \( \mathcal F \) be a sheaf on \( X \). +Let \( \mathcal U = \qty{U_i}_{i \in I} \) be a fixed open cover of \( X \), indexed by a well-ordered set \( I \). +In this course, we will take \( I = \qty{1, \dots, N} \), and write \( U_{i_0 \dots i_p} = U_{i_0} \cap \dots \cap U_{i_p} \). +\v{C}ech cohomology attaches data to the triple \( (X, \mathcal F, \mathcal U) \). +The group of \emph{\v{C}ech \( p \)-cochains} is +\[ C^p(\mathcal U, \mathcal F) = \prod_{i_0 < \dots < i_p} \mathcal F(U_{i_0 \dots i_p}) \] +There is a \emph{differential} +\[ d : C^p(\mathcal U, \mathcal F) \to C^{p+1}(\mathcal U, \mathcal F) \] +where the \( i_0, \dots, i_{p+1} \) component of \( d\alpha \) is given by +\[ (d\alpha)_{i_0 \dots i_{p+1}} = \sum_{k=0}^{p+1} (-1)^k \eval{\alpha_{i_0\dots \hat i_k \dots i_{p+1}}}_{U_{i_0 \dots i_{p+1}}} \] +where \( \hat i_k \) denotes that the element \( i_k \) of the sequence is omitted. +One can easily show that \( d^2 : C^p \to C^{p+2} \) is the zero map. +Thus, \( \qty{C^p(\mathcal U, \mathcal F)}_p \) has the structure of a \emph{cochain complex}. +\begin{definition} + The \emph{\( i \)th \v{C}ech cohomology} of \( (X, \mathcal F, \mathcal U) \) is the \( i \)th cohomology group of the cochain complex: + \[ \check{H}^i(X, \mathcal F) = \frac{\ker(C^i(\mathcal U, \mathcal F) \xrightarrow d C^{i+1}(\mathcal U, \mathcal F))}{\Im(C^{i-1}(\mathcal U, \mathcal F) \xrightarrow d C^i(\mathcal U, \mathcal F))} \] +\end{definition} +\begin{example} + Let \( X = S^1 \) be the usual circle. + Let \( \mathcal F \) be the constant sheaf \( \underline{\mathbb Z} \); on any connected open set this sheaf has value \( \mathbb Z \), and for a general open set with \( n \) connected components, this sheaf has value \( \mathbb Z^n \). + Let \( \mathcal U = \qty{U, V} \) where \( U, V \) are obtained by deleting disjoint closed intervals from the circle, giving an open cover with \( U, V \cong \mathbb R \). + We have + \[ C^0(\mathcal U, \underline{\mathbb Z}) = \mathbb Z^2 \] + as there is one copy of \( \mathbb Z \) for \( U \) and one for \( V \). + Also, + \[ C^1(\mathcal U, \underline{\mathbb Z}) = \mathbb Z^2 \] + given by \( \underline{\mathbb Z}(U \cap V) \). + The differential is \( (a, b) \mapsto (b-a, b-a) \), so + \[ \check{H}^0(\mathcal U, \underline{\mathbb Z}) \cong \mathbb Z = \ker d \] + and + \[ \check{H}^1(\mathcal U, \underline{\mathbb Z}) \cong \mathbb Z = \coker d \] +\end{example} +\begin{remark} + \begin{enumerate} + \item These \v{C}ech cohomology groups are equal to the corresponding singular cohomology groups of \( S^1 \). + \item Note that \( \check{H} \) is typically only well-behaved when \( \mathcal U \) is also well-behaved. + That is, \( \check{H}^i(\mathcal U, \mathcal F) \) depends on \( \mathcal U \) and not just \( X \). + In the example above, we could have chosen \( \mathcal U = \qty{S^1} \), and in this case, \( \check{H}^1(\mathcal U, \underline{\mathbb Z}) = 0 \). + Also note that \( \underline{\mathbb Z} \) is not a quasi-coherent sheaf. + \item Let \( X = \mathbb P^1_k, U = X \setminus \qty{0}, V = X \setminus \qty{\infty}, \mathcal U = \qty{U, V} \). + Then + \[ \check{H}^0(\mathcal U, \mathcal O_X) = k;\quad \check{H}^1(\mathcal U, \mathcal O_X) = 0 \] + \item Let \( X \) be Noetherian and separated, and let \( \qty{U_i}_{i \in I} \) be an affine cover of \( X \), so all \( U_{i_0 \dots i_p} \) are affine. + Let \( \mathcal F \) be a quasi-coherent sheaf on \( X \). + Then + \[ \check{H}^p(\mathcal U, \mathcal F) \cong H^p(X, \mathcal F) \] + and the isomorphism is natural. + Thus, in this particular case, the cohomology is easy to calculate by going via \v{C}ech cohomology. + \end{enumerate} +\end{remark} +\begin{theorem} + Let \( X = \mathbb P^n_k \) and \( \mathcal F = \bigoplus_{d \in \mathbb Z} \mathcal O_{\mathbb P^n}(d) \). + Then there are isomorphisms of graded \( k \)-vector spaces + \begin{enumerate} + \item \( H^0(X, \mathcal F) \cong k[x_0, \dots, x_n] \); + \item \( H^n(X, \mathcal F) \cong \frac{1}{x_0 \dots x_n} k[x_0^{-1}, \dots, x_n^{-1}] \); + \item \( H^p(X, \mathcal F) = 0 \) for \( p \neq 0, n \). + \end{enumerate} + In particular, \( H^0(\mathbb P^n_k, \mathcal O(d)) \) has dimension \( \binom{n+d}{d} \), and \( H^n(\mathbb P^n_k, \mathcal O(d)) \) has dimension \( \binom{-d-1}{n} \). +\end{theorem} diff --git a/iii/alggeom/main.tex b/iii/alggeom/main.tex index 0f1f93a..ac0bd92 100644 --- a/iii/alggeom/main.tex +++ b/iii/alggeom/main.tex @@ -24,7 +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} +\section{Sheaf cohomology} \input{07_sheaf_cohomology.tex} \end{document} diff --git a/iii/cat/07_additive_and_abelian_categories.tex b/iii/cat/07_additive_and_abelian_categories.tex index de797d8..a7a5b95 100644 --- a/iii/cat/07_additive_and_abelian_categories.tex +++ b/iii/cat/07_additive_and_abelian_categories.tex @@ -186,3 +186,382 @@ \subsection{Abelian categories} 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} +\begin{example} + \begin{enumerate} + \item The category \( \mathbf{AbGp} \) is abelian; more generally, for any ring \( R \), the category \( \mathbf{Mod}_R \) is abelian. + \item If \( \mathcal A \) is abelian and \( \mathcal C \) is small, then \( [\mathcal C, \mathcal A] \) is abelian, with all structures defined pointwise. + \item If \( \mathcal A \) is abelian and \( \mathcal C \) is small and additive, then the category of additive functors \( \mathcal C \to \mathcal A \), denoted \( \operatorname{Add}(\mathcal C, \mathcal A) \), is also abelian, as it is closed under all of the structures on \( [\mathcal C, \mathcal A] \). + Note that this covers the case of \( R \)-modules, as an additive category with a single object is a ring, and the category of modules over such a ring is isomorphic to the category of additive functors from this category to \( \mathbf{AbGp} \) + \end{enumerate} +\end{example} +\begin{remark} + If \( f : A \to B \) in an abelian category, then \( \ker \coker f \) is the smallest subobject \( I \rightarrowtail B \) through which \( f \) factors. + This is called the \emph{image} of \( f \), denoted \( \Im f = \ker \coker f \). + The other part of the factorisation \( A \to I \) is epic, as it cannot factor through the equaliser of any nonequal parallel pair \( I \rightrightarrows C \). + Thus, it is also the smallest quotient of \( A \) through which \( f \) factors, so it is the \emph{coimage} of \( f \), given by \( \coker \ker f \). + The composition \( A \twoheadrightarrow I \rightarrowtail B \) is the unique epi--mono factorisation of \( f \). +\end{remark} +To show that this factorisation is stable under pullback, it suffices to show that the pullback of an epimorphism in an abelian category is epic, as the corresponding statement for monomorphisms has already been shown. +\begin{lemma}[flattening lemma] + Consider a square + % https://q.uiver.app/#q=WzAsNCxbMCwwLCJBIl0sWzEsMCwiQiJdLFsxLDEsIkQiXSxbMCwxLCJDIl0sWzAsMSwiZiJdLFsxLDIsImgiXSxbMCwzLCJnIiwyXSxbMywyLCJrIiwyXV0= +\[\begin{tikzcd} + A & B \\ + C & D + \arrow["f", from=1-1, to=1-2] + \arrow["h", from=1-2, to=2-2] + \arrow["g"', from=1-1, to=2-1] + \arrow["k"', from=2-1, to=2-2] +\end{tikzcd}\] + in an abelian category \( \mathcal A \). + Its \emph{flattening} is the sequence + % https://q.uiver.app/#q=WzAsMyxbMCwwLCJBIl0sWzEsMCwiQiBcXG9wbHVzIEMiXSxbMiwwLCJEIl0sWzAsMSwiXFxiZWdpbntwbWF0cml4fWZcXFxcZ1xcZW5ke3BtYXRyaXh9Il0sWzEsMiwiXFxiZWdpbntwbWF0cml4fWgmLWtcXGVuZHtwbWF0cml4fSJdXQ== +\[\begin{tikzcd}[ampersand replacement=\&] + A \& {B \oplus C} \& D + \arrow["{\begin{pmatrix}f\\g\end{pmatrix}}", from=1-1, to=1-2] + \arrow["{\begin{pmatrix}h&-k\end{pmatrix}}", from=1-2, to=1-3] +\end{tikzcd}\] + Then + \begin{enumerate} + \item the square commutes if and only if the composite of the flattening \( \begin{pmatrix} + h & -k + \end{pmatrix} \begin{pmatrix} + f \\ g + \end{pmatrix} \) is the zero morphism; + \item the square is a pullback if and only if \( \begin{pmatrix} + f \\ g + \end{pmatrix} = \ker \begin{pmatrix} + h & -k + \end{pmatrix} \); + \item the square is a pushout if and only if \( \begin{pmatrix} + h & -k + \end{pmatrix} = \coker \begin{pmatrix} + f \\ g + \end{pmatrix} \). + \end{enumerate} +\end{lemma} +\begin{proof} + \emph{Part (i).} + The composite \( \begin{pmatrix} + h & -k + \end{pmatrix} \begin{pmatrix} + f \\ g + \end{pmatrix} \) is \( hf - kg \), so it vanishes if and only if the square commutes. + + \emph{Part (ii).} + \( \begin{pmatrix} + f \\ g + \end{pmatrix} \) is the kernel of \( \begin{pmatrix} + h \\ -k + \end{pmatrix} \) if and only if + % https://q.uiver.app/#q=WzAsMyxbMCwwLCJBIl0sWzEsMCwiQiJdLFswLDEsIkMiXSxbMCwxLCJmIl0sWzAsMiwiZyIsMl1d +\[\begin{tikzcd} + A & B \\ + C + \arrow["f", from=1-1, to=1-2] + \arrow["g"', from=1-1, to=2-1] +\end{tikzcd}\] + is universal among spans completing the cospan + % https://q.uiver.app/#q=WzAsMyxbMSwwLCJCIl0sWzEsMSwiRCJdLFswLDEsIkMiXSxbMCwxLCJoIl0sWzIsMSwiayIsMl1d +\[\begin{tikzcd} + & B \\ + C & D + \arrow["h", from=1-2, to=2-2] + \arrow["k"', from=2-1, to=2-2] +\end{tikzcd}\] + into a commutative square. + + \emph{Part (iii).} Follows by duality, taking care of the asymmetric negation. +\end{proof} +\begin{corollary} + In an abelian category \( \mathcal A \), epimorphisms are stable under pullback. +\end{corollary} +\begin{proof} + Suppose we have a pullback square + % https://q.uiver.app/#q=WzAsNCxbMCwwLCJBIl0sWzEsMCwiQiJdLFsxLDEsIkQiXSxbMCwxLCJDIl0sWzAsMSwiZiJdLFsxLDIsImgiLDAseyJzdHlsZSI6eyJoZWFkIjp7Im5hbWUiOiJlcGkifX19XSxbMCwzLCJnIiwyXSxbMywyLCJrIiwyXV0= +\[\begin{tikzcd} + A & B \\ + C & D + \arrow["f", from=1-1, to=1-2] + \arrow["h", two heads, from=1-2, to=2-2] + \arrow["g"', from=1-1, to=2-1] + \arrow["k"', from=2-1, to=2-2] +\end{tikzcd}\] + By part (ii) of the above result, \( \begin{pmatrix} + f \\ g + \end{pmatrix} = \ker \begin{pmatrix} + h & -k + \end{pmatrix} \). + But \( h \) is an epimorphism, so \( \begin{pmatrix} + h & -k + \end{pmatrix} \) is also an epimorphism. + Thus \( \begin{pmatrix} + h & -k + \end{pmatrix} = \coker \begin{pmatrix} + f \\ g + \end{pmatrix} \), so the square is also a pushout. + We show that \( g \) is a pseudoepimorphism; this suffices as \( \mathcal A \) is additive. + Suppose we have \( \ell : C \to E \) with \( \ell g = 0 \). + Then \( \begin{pmatrix} + \ell & (B \xrightarrow 0 E) + \end{pmatrix} \) factors uniquely through the pushout. + % https://q.uiver.app/#q=WzAsNSxbMCwwLCJBIl0sWzEsMCwiQiJdLFsxLDEsIkQiXSxbMCwxLCJDIl0sWzIsMiwiRSJdLFswLDEsImYiXSxbMSwyLCJoIiwwLHsic3R5bGUiOnsiaGVhZCI6eyJuYW1lIjoiZXBpIn19fV0sWzAsMywiZyIsMl0sWzMsMiwiayIsMl0sWzEsNCwiMCIsMCx7ImN1cnZlIjotMn1dLFszLDQsIlxcZWxsIiwyLHsiY3VydmUiOjJ9XSxbMiw0LCJtIl1d +\[\begin{tikzcd} + A & B \\ + C & D \\ + && E + \arrow["f", from=1-1, to=1-2] + \arrow["h", two heads, from=1-2, to=2-2] + \arrow["g"', from=1-1, to=2-1] + \arrow["k"', from=2-1, to=2-2] + \arrow["0", curve={height=-12pt}, from=1-2, to=3-3] + \arrow["\ell"', curve={height=12pt}, from=2-1, to=3-3] + \arrow["m", from=2-2, to=3-3] +\end{tikzcd}\] + But then \( mh = 0 \) and \( h \) is epic, so \( m = 0 \), giving \( \ell = mk = 0 \). +\end{proof} +Thus image factorisations are stable under pullback, and dually, under pushout. + +\subsection{Exact sequences} +\begin{definition} + A sequence% https://q.uiver.app/#q=WzAsNSxbMCwwLCJcXGNkb3RzIl0sWzEsMCwiQV97bisxfSJdLFsyLDAsIkFfbiJdLFszLDAsIkFfe24tMX0iXSxbNCwwLCJcXGNkb3RzIl0sWzAsMV0sWzEsMiwiZl97bisxfSJdLFsyLDMsImZfbiJdLFszLDRdXQ== + \[\begin{tikzcd} + \cdots & {A_{n+1}} & {A_n} & {A_{n-1}} & \cdots + \arrow[from=1-1, to=1-2] + \arrow["{f_{n+1}}", from=1-2, to=1-3] + \arrow["{f_n}", from=1-3, to=1-4] + \arrow[from=1-4, to=1-5] + \end{tikzcd}\] + in an abelian category \( \mathcal A \) is \emph{exact} at \( A_n \) if \( \ker f_n = \operatorname{im} f_{n+1} \). + The entire sequence is said to be \emph{exact} if it is exact at every vertex. +\end{definition} +By duality, the sequence is exact at \( A_n \) if and only if \( \coker f_{n+1} = \operatorname{coim} f_n \). +\begin{example} + % https://q.uiver.app/#q=WzAsNCxbMCwwLCIwIl0sWzEsMCwiQSJdLFsyLDAsIkIiXSxbMywwLCJDIl0sWzAsMV0sWzEsMiwiZiJdLFsyLDMsImciXV0= +\[\begin{tikzcd} + 0 & A & B & C + \arrow[from=1-1, to=1-2] + \arrow["f", from=1-2, to=1-3] + \arrow["g", from=1-3, to=1-4] +\end{tikzcd}\] + is exact at \( A \) if and only if \( f \) is monic, and is exact at \( A \) and \( B \) if and only if \( f = \ker g \). +\end{example} +\begin{definition} + A functor between abelian categories \( F : \mathcal A \to \mathcal B \) is \emph{exact} if it preserves arbitrary exact sequences. +\end{definition} +This implies that \( F \) preserves kernels and cokernels, and the converse is true as images are defined in terms of kernels and cokernels. +\begin{definition} + \( F \) is \emph{left exact} if it preserves exact sequences of the form + % https://q.uiver.app/#q=WzAsNCxbMCwwLCIwIl0sWzEsMCwiQSJdLFsyLDAsIkIiXSxbMywwLCJDIl0sWzAsMV0sWzEsMiwiZiJdLFsyLDMsImciXV0= +\[\begin{tikzcd} + 0 & A & B & C + \arrow[from=1-1, to=1-2] + \arrow["f", from=1-2, to=1-3] + \arrow["g", from=1-3, to=1-4] +\end{tikzcd}\] +\end{definition} +\begin{proposition} + Let \( F : \mathcal A \to \mathcal B \) be a functor between abelian categories. + Then + \begin{enumerate} + \item \( F \) is left exact if and only if it preserves all finite limits (and hence is additive); + \item \( F \) is exact if and only if it is left exact and preserves epimorphisms. + \end{enumerate} +\end{proposition} +\begin{proof} + \emph{Part (i).} + One direction is trivial as kernels are finite limits. + Conversely, note that for any \( A, B \), the sequence + % https://q.uiver.app/#q=WzAsNSxbMCwwLCIwIl0sWzEsMCwiQSJdLFsyLDAsIkEgXFxvcGx1cyBCIl0sWzMsMCwiQiJdLFs0LDAsIjAiXSxbMCwxXSxbMSwyLCJcXGJlZ2lue3BtYXRyaXh9MVxcXFwwXFxlbmR7cG1hdHJpeH0iXSxbMiwzLCJcXGJlZ2lue3BtYXRyaXh9MCYxXFxlbmR7cG1hdHJpeH0iXSxbMyw0XV0= +\[\begin{tikzcd}[ampersand replacement=\&] + 0 \& A \& {A \oplus B} \& B \& 0 + \arrow[from=1-1, to=1-2] + \arrow["{\begin{pmatrix}1\\0\end{pmatrix}}", from=1-2, to=1-3] + \arrow["{\begin{pmatrix}0&1\end{pmatrix}}", from=1-3, to=1-4] + \arrow[from=1-4, to=1-5] +\end{tikzcd}\] + is exact, and conversely, if we have an exact sequence + % https://q.uiver.app/#q=WzAsNSxbMCwwLCIwIl0sWzEsMCwiQSJdLFsyLDAsIkMiXSxbMywwLCJCIl0sWzQsMCwiMCJdLFswLDFdLFsxLDIsImYiXSxbMiwzLCJnIl0sWzMsNF1d +\[\begin{tikzcd} + 0 & A & C & B & 0 + \arrow[from=1-1, to=1-2] + \arrow["f", from=1-2, to=1-3] + \arrow["g", from=1-3, to=1-4] + \arrow[from=1-4, to=1-5] +\end{tikzcd}\] + and either \( f \) is a split monomorphism or \( g \) is a split epimorphism, then \( C \cong A \oplus B \). + Indeed, suppose that \( f \) is split, so \( rf = 1_A \). + Then \( g = \coker f = \coker fr \) is the equaliser of \( (1_C-fr, 1_C) \), so it is the epic part of a splitting of the idempotent \( 1_C - fr \). + If \( s : B \to C \) is the monic part of this splitting, then the four morphisms \( (r, g, f, s) \) satisfy the equations of a biproduct. + So \( F \) maps + % https://q.uiver.app/#q=WzAsNSxbMCwwLCIwIl0sWzEsMCwiQSJdLFsyLDAsIkEgXFxvcGx1cyBCIl0sWzMsMCwiQiJdLFs0LDAsIjAiXSxbMCwxXSxbMSwyLCJcXGJlZ2lue3BtYXRyaXh9MVxcXFwwXFxlbmR7cG1hdHJpeH0iXSxbMiwzLCJcXGJlZ2lue3BtYXRyaXh9MCYxXFxlbmR7cG1hdHJpeH0iXSxbMyw0XV0= +\[\begin{tikzcd}[ampersand replacement=\&] + 0 \& A \& {A \oplus B} \& B \& 0 + \arrow[from=1-1, to=1-2] + \arrow["{\begin{pmatrix}1\\0\end{pmatrix}}", from=1-2, to=1-3] + \arrow["{\begin{pmatrix}0&1\end{pmatrix}}", from=1-3, to=1-4] + \arrow[from=1-4, to=1-5] +\end{tikzcd}\] + to a sequence identifying \( F(A \oplus B) \) as \( FA \oplus FB \), and thus preserves biproducts. + Hence \( F \) preserves all finite limits. + + \emph{Part (ii).} + If \( F \) is left exact and preserves epimorphisms, then it preserves the exactness of sequences of the form + % https://q.uiver.app/#q=WzAsNSxbMCwwLCIwIl0sWzEsMCwiQSJdLFsyLDAsIkMiXSxbMywwLCJCIl0sWzQsMCwiMCJdLFswLDFdLFsxLDIsImYiXSxbMiwzLCJnIl0sWzMsNF1d +\[\begin{tikzcd} + 0 & A & C & B & 0 + \arrow[from=1-1, to=1-2] + \arrow["f", from=1-2, to=1-3] + \arrow["g", from=1-3, to=1-4] + \arrow[from=1-4, to=1-5] +\end{tikzcd}\] + Thus it preserves kernels and cokernels. +\end{proof} + +\subsection{The five lemma} +\begin{lemma} + Suppose we have a commutative diagram in an abelian category + % https://q.uiver.app/#q=WzAsMTAsWzAsMCwiQV8xIl0sWzEsMCwiQV8yIl0sWzIsMCwiQV8zIl0sWzMsMCwiQV80Il0sWzQsMCwiQV81Il0sWzQsMSwiQl81Il0sWzAsMSwiQl8xIl0sWzEsMSwiQl8yIl0sWzIsMSwiQl8zIl0sWzMsMSwiQl80Il0sWzAsMSwiZl8xIl0sWzEsMiwiZl8yIl0sWzIsMywiZl8zIl0sWzMsNCwiZl80Il0sWzQsNSwidV81Il0sWzAsNiwidV8xIl0sWzYsNywiZ18xIiwyXSxbNyw4LCJnXzIiLDJdLFs4LDksImdfMyIsMl0sWzksNSwiZ180IiwyXSxbMSw3LCJ1XzIiXSxbMiw4LCJ1XzMiXSxbMyw5LCJ1XzQiXV0= +\[\begin{tikzcd} + {A_1} & {A_2} & {A_3} & {A_4} & {A_5} \\ + {B_1} & {B_2} & {B_3} & {B_4} & {B_5} + \arrow["{f_1}", from=1-1, to=1-2] + \arrow["{f_2}", from=1-2, to=1-3] + \arrow["{f_3}", from=1-3, to=1-4] + \arrow["{f_4}", from=1-4, to=1-5] + \arrow["{u_5}", from=1-5, to=2-5] + \arrow["{u_1}", from=1-1, to=2-1] + \arrow["{g_1}"', from=2-1, to=2-2] + \arrow["{g_2}"', from=2-2, to=2-3] + \arrow["{g_3}"', from=2-3, to=2-4] + \arrow["{g_4}"', from=2-4, to=2-5] + \arrow["{u_2}", from=1-2, to=2-2] + \arrow["{u_3}", from=1-3, to=2-3] + \arrow["{u_4}", from=1-4, to=2-4] +\end{tikzcd}\] + where the rows are exact sequences. + Then, + \begin{enumerate} + \item if \( u_1 \) is epic and \( u_2, u_4 \) are monic, then \( u_3 \) is monic; + \item if \( u_5 \) is monic and \( u_2, u_4 \) are spic, then \( u_3 \) is epic. + \end{enumerate} + Thus if \( u_1, u_2, u_4, u_5 \) are isomorphisms, \( u_3 \) is an isomorphism. +\end{lemma} +\begin{proof} + By duality it suffices to show (i). + We show \( u_3 \) is a pseudomonomorphism. + Suppose we have \( x : C \to A_3 \) with \( u_3 x = 0 \). + Then \( u_4 f_3 x = g_4 u_3 x = 0 \), so as \( u_4 \) is a monomorphism, \( f_3 x = 0 \). + Hence \( x \) factors through the kernel of \( f_3 \), which is the image of \( f_2 \). + Form the pullback of \( f_2 \) and \( x \) to obtain + % https://q.uiver.app/#q=WzAsMTIsWzAsMSwiQV8xIl0sWzEsMSwiQV8yIl0sWzIsMSwiQV8zIl0sWzMsMSwiQV80Il0sWzAsMiwiQl8xIl0sWzEsMiwiQl8yIl0sWzIsMiwiQl8zIl0sWzMsMiwiQl80Il0sWzIsMCwiQyJdLFsxLDAsIkQiXSxbNCwyLCJCXzUiXSxbNCwxLCJBXzUiXSxbMCwxLCJmXzEiXSxbMSwyLCJmXzIiXSxbMiwzLCJmXzMiXSxbMCw0LCJ1XzEiXSxbNCw1LCJnXzEiLDJdLFs1LDYsImdfMiIsMl0sWzYsNywiZ18zIiwyXSxbMSw1LCJ1XzIiXSxbMiw2LCJ1XzMiXSxbMyw3LCJ1XzQiXSxbOCwyLCJ4Il0sWzksOCwieSJdLFs5LDEsInoiXSxbNywxMCwiZ180IiwyXSxbMywxMSwiZl80Il0sWzExLDEwLCJ1XzUiXV0= +\[\begin{tikzcd} + & D & C \\ + {A_1} & {A_2} & {A_3} & {A_4} & {A_5} \\ + {B_1} & {B_2} & {B_3} & {B_4} & {B_5} + \arrow["{f_1}", from=2-1, to=2-2] + \arrow["{f_2}", from=2-2, to=2-3] + \arrow["{f_3}", from=2-3, to=2-4] + \arrow["{u_1}", from=2-1, to=3-1] + \arrow["{g_1}"', from=3-1, to=3-2] + \arrow["{g_2}"', from=3-2, to=3-3] + \arrow["{g_3}"', from=3-3, to=3-4] + \arrow["{u_2}", from=2-2, to=3-2] + \arrow["{u_3}", from=2-3, to=3-3] + \arrow["{u_4}", from=2-4, to=3-4] + \arrow["x", from=1-3, to=2-3] + \arrow["y", from=1-2, to=1-3] + \arrow["z", from=1-2, to=2-2] + \arrow["{g_4}"', from=3-4, to=3-5] + \arrow["{f_4}", from=2-4, to=2-5] + \arrow["{u_5}", from=2-5, to=3-5] +\end{tikzcd}\] + Then \( y \) is also the pullback of this factorisation of \( x \) along \( \operatorname{coim} f_2 \), so \( y \) is an epimorphism as epimorphisms are stable under pullback. + Then \( g_2 u_2 z = u_3 f_2 z = u_3 x y = 0 \). + Thus \( u_2 z \) factors through \( \ker g_2 = \operatorname{im} g_1 \). + Consider the pullback square + % https://q.uiver.app/#q=WzAsNCxbMCwwLCJFIl0sWzEsMCwiRCJdLFsxLDEsIkJfMiJdLFswLDEsIkFfMSJdLFswLDEsInYiXSxbMSwyLCJ1XzIgeiJdLFswLDMsInUiLDJdLFszLDIsImdfMSB1XzEiLDJdXQ== +\[\begin{tikzcd} + E & D \\ + {A_1} & {B_2} + \arrow["v", from=1-1, to=1-2] + \arrow["{u_2 z}", from=1-2, to=2-2] + \arrow["w"', from=1-1, to=2-1] + \arrow["{g_1 u_1}"', from=2-1, to=2-2] +\end{tikzcd}\] + So \( v \) is epic, as it is the pullback of \( \operatorname{coim}(g_1 u_1) \). + % https://q.uiver.app/#q=WzAsMTMsWzAsMSwiQV8xIl0sWzEsMSwiQV8yIl0sWzIsMSwiQV8zIl0sWzMsMSwiQV80Il0sWzAsMiwiQl8xIl0sWzEsMiwiQl8yIl0sWzIsMiwiQl8zIl0sWzMsMiwiQl80Il0sWzIsMCwiQyJdLFsxLDAsIkQiXSxbNCwyLCJCXzUiXSxbNCwxLCJBXzUiXSxbMCwwLCJFIl0sWzAsMSwiZl8xIl0sWzEsMiwiZl8yIl0sWzIsMywiZl8zIl0sWzAsNCwidV8xIl0sWzQsNSwiZ18xIiwyXSxbNSw2LCJnXzIiLDJdLFs2LDcsImdfMyIsMl0sWzEsNSwidV8yIl0sWzIsNiwidV8zIl0sWzMsNywidV80Il0sWzgsMiwieCJdLFs5LDgsInkiXSxbOSwxLCJ6Il0sWzcsMTAsImdfNCIsMl0sWzMsMTEsImZfNCJdLFsxMSwxMCwidV81Il0sWzEyLDksInYiXSxbMTIsMCwidyJdXQ== +\[\begin{tikzcd} + E & D & C \\ + {A_1} & {A_2} & {A_3} & {A_4} & {A_5} \\ + {B_1} & {B_2} & {B_3} & {B_4} & {B_5} + \arrow["{f_1}", from=2-1, to=2-2] + \arrow["{f_2}", from=2-2, to=2-3] + \arrow["{f_3}", from=2-3, to=2-4] + \arrow["{u_1}", from=2-1, to=3-1] + \arrow["{g_1}"', from=3-1, to=3-2] + \arrow["{g_2}"', from=3-2, to=3-3] + \arrow["{g_3}"', from=3-3, to=3-4] + \arrow["{u_2}", from=2-2, to=3-2] + \arrow["{u_3}", from=2-3, to=3-3] + \arrow["{u_4}", from=2-4, to=3-4] + \arrow["x", from=1-3, to=2-3] + \arrow["y", from=1-2, to=1-3] + \arrow["z", from=1-2, to=2-2] + \arrow["{g_4}"', from=3-4, to=3-5] + \arrow["{f_4}", from=2-4, to=2-5] + \arrow["{u_5}", from=2-5, to=3-5] + \arrow["v", from=1-1, to=1-2] + \arrow["w", from=1-1, to=2-1] +\end{tikzcd}\] + Thus \( u_2 z v = g_1 u_1 w \), and \( u_2 \) is monic, so \( zv = f_1 w \). + Then \( xyv = f_2 zv = f_2 f_1 w = 0 \), and \( yv \) is epic, hence \( x = 0 \). +\end{proof} + +\subsection{The snake lemma} +\begin{lemma} + Consider a diagram in an abelian category + % https://q.uiver.app/#q=WzAsOCxbMSwwLCJCXzEiXSxbMiwwLCJCXzIiXSxbMywwLCJCXzMiXSxbNCwwLCIwIl0sWzAsMSwiMCJdLFsxLDEsIkNfMSJdLFsyLDEsIkNfMiJdLFszLDEsIkNfMyJdLFswLDFdLFsxLDJdLFsyLDNdLFs0LDVdLFs1LDZdLFs2LDddLFswLDUsInZfMSJdLFsxLDYsInZfMiJdLFsyLDcsInZfMyJdXQ== +\[\begin{tikzcd} + & {B_1} & {B_2} & {B_3} & 0 \\ + 0 & {C_1} & {C_2} & {C_3} + \arrow[from=1-2, to=1-3] + \arrow[from=1-3, to=1-4] + \arrow[from=1-4, to=1-5] + \arrow[from=2-1, to=2-2] + \arrow[from=2-2, to=2-3] + \arrow[from=2-3, to=2-4] + \arrow["{v_1}", from=1-2, to=2-2] + \arrow["{v_2}", from=1-3, to=2-3] + \arrow["{v_3}", from=1-4, to=2-4] +\end{tikzcd}\] + where the rows are exact and the squares commute. + Then we obtain an exact sequence + % https://q.uiver.app/#q=WzAsMTQsWzEsMSwiQl8xIl0sWzIsMSwiQl8yIl0sWzMsMSwiQl8zIl0sWzQsMSwiMCJdLFswLDIsIjAiXSxbMSwyLCJDXzEiXSxbMiwyLCJDXzIiXSxbMywyLCJDXzMiXSxbMSwwLCJcXG9wZXJhdG9ybmFtZXtLZXJ9IHZfMSJdLFsyLDAsIlxcb3BlcmF0b3JuYW1le0tlcn12XzIiXSxbMywwLCJcXG9wZXJhdG9ybmFtZXtLZXJ9dl8zIl0sWzEsMywiXFxvcGVyYXRvcm5hbWV7Q29rZXJ9dl8xIl0sWzIsMywiXFxvcGVyYXRvcm5hbWV7Q29rZXJ9dl8yIl0sWzMsMywiXFxvcGVyYXRvcm5hbWV7Q29rZXJ9IHZfMyJdLFswLDFdLFsxLDJdLFsyLDNdLFs0LDVdLFs1LDZdLFs2LDddLFswLDUsInZfMSJdLFsxLDYsInZfMiJdLFsyLDcsInZfMyJdLFs4LDldLFs5LDEwXSxbMTAsMTEsInMiXSxbMTEsMTJdLFsxMiwxM10sWzgsMF0sWzksMV0sWzEwLDJdLFs1LDExXSxbNiwxMl0sWzcsMTNdXQ== +\[\begin{tikzcd} + & {\operatorname{Ker} v_1} & {\operatorname{Ker}v_2} & {\operatorname{Ker}v_3} \\ + & {B_1} & {B_2} & {B_3} & 0 \\ + 0 & {C_1} & {C_2} & {C_3} \\ + & {\operatorname{Coker}v_1} & {\operatorname{Coker}v_2} & {\operatorname{Coker} v_3} + \arrow[from=2-2, to=2-3] + \arrow[from=2-3, to=2-4] + \arrow[from=2-4, to=2-5] + \arrow[from=3-1, to=3-2] + \arrow[from=3-2, to=3-3] + \arrow[from=3-3, to=3-4] + \arrow["{v_1}", from=2-2, to=3-2] + \arrow["{v_2}", from=2-3, to=3-3] + \arrow["{v_3}", from=2-4, to=3-4] + \arrow[from=1-2, to=1-3] + \arrow[from=1-3, to=1-4] + \arrow["s", from=1-4, to=4-2] + \arrow[from=4-2, to=4-3] + \arrow[from=4-3, to=4-4] + \arrow[from=1-2, to=2-2] + \arrow[from=1-3, to=2-3] + \arrow[from=1-4, to=2-4] + \arrow[from=3-2, to=4-2] + \arrow[from=3-3, to=4-3] + \arrow[from=3-4, to=4-4] +\end{tikzcd}\] +\end{lemma} diff --git a/iii/mtncl/06_intuitionistic_logic.tex b/iii/mtncl/06_intuitionistic_logic.tex index 4b6c5a2..7974de8 100644 --- a/iii/mtncl/06_intuitionistic_logic.tex +++ b/iii/mtncl/06_intuitionistic_logic.tex @@ -528,3 +528,88 @@ \subsection{Heyting semantics} 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} +\begin{lemma}[soundness] + Let \( H \) be a Heyting algebra and let \( v : \mathcal L \to H \) be an \( H \)-valuation. + If \( \Gamma \vdash_{\mathsf{IPC}} A \), then \( \Gamma \vDash_H A \). +\end{lemma} +\begin{proof} + We proceed by induction over the derivation of \( \Gamma \vdash_{\mathsf{IPC}} A \). + \begin{enumerate} + \item (\textsc{Ax}) \( v\qty((\bigwedge \Gamma) \wedge A) = v\qty(\bigwedge \Gamma) \wedge v(A) \leq v(A) \). + \item (\( \wedge \)-I) In this case, \( A = B \wedge C \) and we have derivations \( \Gamma_1 \vdash B, \Gamma_2 \vdash C \) with \( \Gamma_1, \Gamma_2 \subseteq \Gamma \). + By the inductive hypothesis, \( v(\Gamma_1) \leq v(B) \) and \( v(\Gamma_2) \leq v(C) \), hence + \[ v\qty(\bigwedge \Gamma) \leq v(\Gamma_1) \wedge v(\Gamma_2) \leq v(B) \wedge v(C) = v(B \wedge C) = v(A) \] + \item (\( \to \)-I) In this case, \( A = B \to C \) and we have \( \Gamma \cup \qty{B} \vdash C \). + By the inductive hypothesis, \( v\qty(\bigwedge\Gamma) \wedge v(B) \leq v(C) \). + But then \( v\qty(\bigwedge\Gamma) \leq v(B) \Rightarrow v(C) \) by definition, so \( v\qty(\bigwedge\Gamma) \leq v(B \to C) \) as required. + \item (\( \vee \)-I) In this case, \( A = B \vee C \), and without loss of generality, we have \( \Gamma \vdash B \). + By the inductive hypothesis, \( v\qty(\bigwedge \Gamma) \leq v(B) \), but \( v(B) \leq v(B) \vee v(C) = v(B \vee C) \) as required. + \item (\( \wedge \)-E) By the inductive hypothesis, we have \( v\qty(\bigwedge \Gamma) \leq v(A \wedge B) = v(A) \wedge v(B) \leq v(A), v(B) \) as required. + \item (\( \to \)-E) We know that \( v(A \to B) = (v(A) \Rightarrow v(B)) \). + From the inequality \( v(A \to B) \leq (v(A) \Rightarrow v(B)) \), we deduce \( v(A \to B) \wedge v(A) \leq v(B) \). + Thus, if \( v\qty(\bigwedge \Gamma) \leq v(A \to B) \) and \( v\qty(\bigwedge \Gamma) \leq v(A) \), we have \( v\qty(\bigwedge \Gamma) \leq v(B) \) as required. + \item (\( \vee \)-E) By the inductive hypothesis, + \[ v\qty(A \wedge \bigwedge \Gamma) \leq v(C);\quad v\qty(B \wedge \bigwedge \Gamma) \leq v(C);\quad v\qty(\bigwedge \Gamma) \leq v(A \vee B) = v(A) \vee v(B) \] + Hence, + \[ v\qty(\bigwedge \Gamma) = v\qty(\bigwedge \Gamma) \wedge (v(A) \vee v(B)) = \qty(v\qty(\bigwedge \Gamma) \wedge v(A)) \vee \qty(v\qty(\bigwedge \Gamma) \wedge v(B)) \leq v(C) \vee v(C) = v(C) \] + as every Heyting algebra is a distributive lattice. + \item (\( \bot \)-E) If \( v\qty(\bigwedge\Gamma) \leq v(\bot) = \bot \), then \( v\qty(\bigwedge \Gamma) = \bot \). + Hence, \( v\qty(\bigwedge \Gamma) \leq v(A) \) for any \( A \). + \end{enumerate} +\end{proof} +\begin{example} + The law of the excluded middle \( \mathsf{LEM} \) is not provable in \( \mathsf{IPC} \). + Let \( p \) be a primitive proposition, and consider the Heyting algebra given by the Sierpin\'nski topology \( \qty{\varnothing, \qty{1}, \qty{1, 2}} \) on \( X = \qty{1,2} \). + We define the valuation given by \( v(p) = \qty{1} \). + Then + \[ v(\neg p) = \qty{1} \Rightarrow \varnothing = (\qty{1, 2} \setminus \qty{1})^\circ = \qty{2}^\circ = \varnothing \] + Hence, + \[ v(p \vee \neg p) = \qty{1} \cup \varnothing = \qty{1} \neq \qty{1, 2} = \top \] + Thus, by soundness, \( p \vee \neg p \) is not provable (from the empty context, which has valuation \( \top = \qty{1, 2} \)) in \( \mathsf{IPC} \). +\end{example} +\begin{example} + Peirce's law \( ((p \to q) \to p) \to p \) is not intuitionistically valid. + Let \( H \) be the Heyting algebra given by the usual topology on the plane \( \mathbb R^2 \), and let + \[ v(p) = \mathbb R^2 \setminus \qty{(0, 0)};\quad v(q) = \varnothing \] + % TODO: complete +\end{example} +Classical completeness can be phrased as +\[ \Gamma \vdash_{\mathsf{CPC}} A \iff \Gamma \vDash_2 A \] +where \( 2 \) is the Boolean algebra \( \qty{0, 1} \). +For intuitionistic logic, we cannot replace \( 2 \) with a single finite Heyting algebra, so we will instead quantify over all Heyting algebras. +\begin{theorem}[completeness] + A proposition is provable in \( \mathsf{IPC} \) if and only if it is \( H \)-valid for every Heyting algebra \( H \). +\end{theorem} +\begin{proof} + For the forward direction, if \( \vdash_{\mathsf{IPC}} A \), then \( \top \leq v(A) \) for every Heyting algebra \( H \) and valuation \( v \), by soundness. + Then \( \top = v(A) \), so \( A \) is \( H \)-valid. + + For the backward direction, suppose \( A \) is \( H \)-valid for every Heyting algebra \( H \). + Note that the Lindenbaum--Tarski algebra \( \faktor{\mathcal L}{\sim} \) for the empty theory, with respect to \( \mathsf{IPC} \), is a Heyting algebra. + Consider the valuation given by mapping each primitive proposition to its equivalence class in \( \faktor{\mathcal L}{\sim} \). + Then, one can easily show by induction that \( v : \mathcal L \to \faktor{\mathcal L}{\sim} \) is the quotient map by considering the construction of the Lindenbaum--Tarski algebra. + Now, \( A \) is valid in every Heyting algebra and with respect to every valuation, so in particular, \( v(A) = \top \) in \( \faktor{\mathcal L}{\sim} \). + But then \( v(A) \in [\top] \), so \( \vdash_{\mathsf{IPC}} A \leftrightarrow \top \), so \( \vdash_{\mathsf{IPC}} A \) as required. +\end{proof} + +\subsection{Kripke semantics} +\begin{definition} + Let \( S \) be a poset. + For each \( a \in S \), we define its \emph{principal up-set} to be + \[ a \uparrow = \qty{s \in S \mid a \leq s} \] +\end{definition} +Note that \( U \subseteq S \) is a terminal segment if and only if it contains \( a \uparrow \) for each \( a \in U \). +\begin{proposition} + Let \( S \) be a poset. + Then the set \( T(S) \) of terminal segments of \( S \) has the structure of a Heyting algebra. +\end{proposition} +\begin{proof} + The order is given by inclusion: \( U \leq V \) if and only if \( U \subseteq V \). + We define + \begin{align*} + U \wedge V &= U \cap V \\ + U \vee V &= U \cup V \\ + U \Rightarrow V &= \qty{s \mid s \uparrow \cap U \subseteq V} + \end{align*} + One can check that this forms a Heyting algebra as required. +\end{proof}