diff --git a/foundations/affine.tex b/foundations/affine.tex index e276d0e0..8b52dfbc 100644 --- a/foundations/affine.tex +++ b/foundations/affine.tex @@ -5,38 +5,38 @@ \subsection{Affine-open subtypes} \begin{definition}% A type $X$ is \notion{(qc-)affine}, - if there is a finitely presented $R$-algebra $A$, such that $X=\Spec A$. + if there is a finitely presented $\A$-algebra $A$, such that $X=\Spec A$. \end{definition} If $X$ is affine, it is possible to reconstruct the algebra directly. \begin{lemma}[using \axiomref{sqc}]% \label{algebra-from-affine-scheme} - Let $X$ be an affine scheme, then there is a natural equivalence $X=\Spec (R^X)$. + Let $X$ be an affine scheme, then there is a natural equivalence $X=\Spec (\A^X)$. \end{lemma} \begin{proof} - The natural map $X\to \Spec (R^X)$ is given by mapping $x:X$ to the + The natural map $X\to \Spec (\A^X)$ is given by mapping $x:X$ to the evaluation homomorphism at $x$. There merely is an $A$ such that $X=\Spec A$. - Applying $\Spec$ to the canonical map $A\to R^{\Spec A}$, + Applying $\Spec$ to the canonical map $A\to \A^{\Spec A}$, yields an equivalence by \axiomref{sqc}. This is a (one sided) inverse to the map above. - So we have $X=\Spec (R^X)$. + So we have $X=\Spec (\A^X)$. \end{proof} \begin{proposition}% Let $X$ be a type. - The type of all finitely presented $R$-algebras $A$, such that $X=\Spec A$, is a proposition. + The type of all finitely presented $\A$-algebras $A$, such that $X=\Spec A$, is a proposition. \end{proposition} -When we write ``$\Spec A$'' we implicitly assume $A$ is a finitely presented $R$-algebra. +When we write ``$\Spec A$'' we implicitly assume $A$ is a finitely presented $\A$-algebra. Recall from \Cref{basic-open-subset} that the basic open subset $D(f) \subseteq \Spec A$ is given by $D(f)(x)\colonequiv \inv(f(x))$. \begin{example}[using \axiomref{loc}, \axiomref{sqc}] - For $a_1, \dots, a_n : R$, we have + For $a_1, \dots, a_n : \A$, we have \[ D((X - a_1) \cdots (X - a_n)) = \A^1 \setminus \{ a_1, \dots, a_n \} \rlap{.}\] Indeed, for any $x : \A^1$, @@ -74,8 +74,8 @@ \subsection{Affine-open subtypes} \[ D(f) = \sum_{x : X} D(f)(x) = \sum_{x : \Spec A} \inv(f(x)) = - \sum_{x : \Hom_{\Alg{R}}(A, R)} \inv(x(f)) = - \Hom_{\Alg{R}}(A[f^{-1}], R) = + \sum_{x : \Hom_{\AAlg}(A, \A)} \inv(x(f)) = + \Hom_{\AAlg}(A[f^{-1}], \A) = \Spec A[f^{-1}] \] \end{proof} @@ -95,7 +95,7 @@ \subsection{Affine-open subtypes} Now $D(hf)$ is an affine-open in $X$, that coincides with $U$: \\ Let $x:X$, then $(hf)(x)$ is invertible, if and only if both $h(x)$ and $f(x)$ are invertible. - The latter means $x:D(f)$, so we can interpret $x$ as a homomorphism from $A_f$ to $R$. + The latter means $x:D(f)$, so we can interpret $x$ as a homomorphism from $A_f$ to $\A$. Then $x:D(g)$ means $x(g)$ is invertible, which is equivalent to $x(h)$ being invertible, since $x(f)^k$ is invertible anyway. \end{proof} @@ -114,13 +114,13 @@ \subsection{Affine-open subtypes} More generally, the Zariski-lattice consisting of the radicals -of finitely generated ideals of a finitely presented $R$-algebra $A$, +of finitely generated ideals of a finitely presented $\A$-algebra $A$, coincides with the lattice of open subtypes. This means, that internal to the Zariski-topos, it is not necessary to consider the full Zariski-lattice for a constructive treatment of schemes. \begin{lemma}[using \axiomref{sqc}]% - Let $A$ be a finitely presented $R$-algebra + Let $A$ be a finitely presented $\A$-algebra and let $f, g_1, \dots, g_n \in A$. Then we have $D(f) \subseteq D(g_1, \dots, g_n)$ as subsets of $\Spec A$ @@ -135,7 +135,7 @@ \subsection{Affine-open subtypes} $D(f) \cap V(g_1, \dots, g_n) = \varnothing$, that is, $\Spec((A/(g_1, \dots, g_n))[f^{-1}]) = \varnothing$. By (\axiomref{sqc}) - this means that the finitely presented $R$-algebra $(A/(g_1, \dots, g_n))[f^{-1}]$ + this means that the finitely presented $\A$-algebra $(A/(g_1, \dots, g_n))[f^{-1}]$ is zero. And this is the case if and only if $f$ is nilpotent in $A/(g_1, \dots, g_n)$, that is, if $f \in \sqrt{(g_1, \dots, g_n)}$, as stated. @@ -151,11 +151,11 @@ \subsection{Pullbacks of affine schemes} \label{affine-product} The product of two affine schemes is again an affine scheme, namely - $\Spec A \times \Spec B = \Spec (A \otimes_R B)$. + $\Spec A \times \Spec B = \Spec (A \otimes_\A B)$. \end{lemma} \begin{proof} - By the universal property of the tensor product $A \otimes_R B$. + By the universal property of the tensor product $A \otimes_\A B$. \end{proof} More generally we have: @@ -168,32 +168,32 @@ \subsection{Pullbacks of affine schemes} \end{lemma} \begin{proof} - The maps $f:X\to Z$, $g:Y\to Z$ are induced by $R$-algebra homomorphisms $f^*:A\to R$ and $g^*:B\to R$. + The maps $f:X\to Z$, $g:Y\to Z$ are induced by $\A$-algebra homomorphisms $f^*:A\to \A$ and $g^*:B\to \A$. Let \[ (h,k,p) : \Spec A \times_{\Spec C} \Spec B \] with $p:h\circ f^*=k\circ g^* $. - This defines a $R$-cocone on the diagram + This defines a $\A$-cocone on the diagram \[ \begin{tikzcd} A & C\ar[r,"g^*"]\ar[l,"f^*",swap] & B \end{tikzcd} \] - Since $A\otimes_C B$ is a pushout in $R$-algebras, - there is a unique $R$-algebra homomorphism $A\otimes_C B \to R$ corresponding to $(h,k,p)$. + Since $A\otimes_C B$ is a pushout in $\A$-algebras, + there is a unique $\A$-algebra homomorphism $A\otimes_C B \to \A$ corresponding to $(h,k,p)$. \end{proof} \subsection{Boundedness of functions to $\N$} While the axiom \axiomref{sqc} describes functions on an affine scheme -with values in $R$, +with values in $\A$, we can generalize it to functions taking values -in another finitely presented $R$-algebra, +in another finitely presented $\A$-algebra, as follows. \begin{lemma}[using \axiomref{sqc}]% \label{algebra-valued-functions-on-affine} - For finitely presented $R$-algebras $A$ and $B$, + For finitely presented $\A$-algebras $A$ and $B$, the function \begin{align*} A \otimes B &\xrightarrow{\sim} (\Spec A \to B) \\ @@ -208,9 +208,9 @@ \subsection{Boundedness of functions to $\N$} and calculate as follows. \begin{alignat*}{8} A \otimes B - &=& (\Spec (A \otimes B) \to R) - &=& (\Spec A \times \Spec B \to R) - &=& (\Spec A \to (\Spec B \to R)) + &=& (\Spec (A \otimes B) \to \A) + &=& (\Spec A \times \Spec B \to \A) + &=& (\Spec A \to (\Spec B \to \A)) &=& (\Spec A \to B) \\ c &\mapsto& (\chi \mapsto \chi(c)) @@ -219,15 +219,15 @@ \subsection{Boundedness of functions to $\N$} &\mapsto& (\varphi \mapsto (\varphi \otimes B)(c)) \end{alignat*} The last step is induced by the identification - $B = (\Spec B \to R),\, b \mapsto (\psi \mapsto \psi(b))$, + $B = (\Spec B \to \A),\, b \mapsto (\psi \mapsto \psi(b))$, and we use the fact that $\psi \circ (\varphi \otimes B) = \varphi \otimes \psi$. \end{proof} \begin{lemma}[using \axiomref{sqc}]% \label{eventually-vanishing-sequence-on-affine} - Let $A$ be a finitely presented $R$-algebra - and let $s : \Spec A \to (\N \to R)$ + Let $A$ be a finitely presented $\A$-algebra + and let $s : \Spec A \to (\N \to \A)$ be a family of sequences, each of which eventually vanishes: \[ \prod_{x : \Spec A} \propTrunc{\sum_{N : \N} \prod_{n \geq N} s(x)(n) = 0} \] @@ -236,16 +236,16 @@ \subsection{Boundedness of functions to $\N$} \end{lemma} \begin{proof} - The set of eventually vanishing sequences $\N \to R$ - is in bijection with the set $R[X]$ of polynomials, + The set of eventually vanishing sequences $\N \to \A$ + is in bijection with the set $\A[X]$ of polynomials, by taking the entries of a sequence as the coefficients of a polynomial. So the family of sequences $s$ - is equivalently a family of polynomials $s : \Spec A \to R[X]$. - Now we apply \Cref{algebra-valued-functions-on-affine} with $B = R[X]$ + is equivalently a family of polynomials $s : \Spec A \to \A[X]$. + Now we apply \Cref{algebra-valued-functions-on-affine} with $B = \A[X]$ to see that such a family corresponds to a polynomial $p : A[X]$. Note that for a point $x : \Spec A$, the homomorphism - \[ x \otimes R[X] : A[X] = A \otimes R[X] \to R \otimes R[X] = R[X] \] + \[ x \otimes \A[X] : A[X] = A \otimes \A[X] \to \A \otimes \A[X] = \A[X] \] simply applies the homomorphism $x$ to every coefficient of a polynomial, so we have $(s(x))_n = x(p_n)$. This concludes our argument, @@ -256,7 +256,7 @@ \subsection{Boundedness of functions to $\N$} \begin{theorem}[using \axiomref{loc}, \axiomref{sqc}]% \label{boundedness} - Let $A$ be a finitely presented $R$-algebra. + Let $A$ be a finitely presented $\A$-algebra. Then every function $f : \Spec A \to \N$ is bounded: \[ \Pi_{f : \Spec A \to \N} \propTrunc{\Sigma_{N : \N} \Pi_{x : \Spec A} f(x) \le N} \rlap{.} \] @@ -264,7 +264,7 @@ \subsection{Boundedness of functions to $\N$} \begin{proof} Given a function $f : \Spec A \to \N$, - we construct the family $s : \Spec A \to (\N \to R)$ + we construct the family $s : \Spec A \to (\N \to \A)$ of eventually vanishing sequences given by \[ @@ -274,7 +274,7 @@ \subsection{Boundedness of functions to $\N$} \,0 &\text{else} \rlap{.} \end{cases} \] - Since $0 \neq 1 : R$ by \axiomref{loc}, + Since $0 \neq 1 : \A$ by \axiomref{loc}, we in fact have $s(x)(n) = 0$ if and only if $n \geq f(x)$. Then the claim follows from \Cref{eventually-vanishing-sequence-on-affine}. \end{proof} @@ -286,7 +286,7 @@ \subsection{Boundedness of functions to $\N$} \begin{proposition}[using \axiomref{loc}, \axiomref{sqc}, \axiomref{Z-choice}]% \label{strengthened-boundedness} - Let $A$ be a finitely presented $R$-algebra. + Let $A$ be a finitely presented $\A$-algebra. Let $P : \Spec A \to (\N \to \Prop)$ be a family of upwards closed, merely inhabited subsets of $\N$. Then the set diff --git a/foundations/axioms.tex b/foundations/axioms.tex index e35b72d4..b2d32a51 100644 --- a/foundations/axioms.tex +++ b/foundations/axioms.tex @@ -1,27 +1,27 @@ \subsection{Statement of the axioms}% \label{statement-of-axioms} -We always assume there is a fixed commutative ring $R$. -In addition, we assume the following three axioms about $R$, +We always assume there is a fixed commutative ring $\A$. +In addition, we assume the following three axioms about $\A$, which were already mentioned in the introduction, but we will indicate which of these axioms are used to prove each statement by listing their shorthands. \begin{axiom}[Loc]% \label{loc}\index{Loc} - $R$ is a local ring (\Cref{local-ring}). + $\A$ is a local ring (\Cref{local-ring}). \end{axiom} \begin{axiom}[SQC]% \label{sqc}\index{sqc} - For any finitely presented $R$-algebra $A$, the homomorphism - \[ a \mapsto (\varphi\mapsto \varphi(a)) : A \to (\Spec A \to R)\] - is an isomorphism of $R$-algebras. + For any finitely presented $\A$-algebra $A$, the homomorphism + \[ a \mapsto (\varphi\mapsto \varphi(a)) : A \to (\Spec A \to \A)\] + is an isomorphism of $\A$-algebras. \end{axiom} \begin{axiom}[Z-choice]% \label{Z-choice}\index{Z-choice} - Let $A$ be a finitely presented $R$-algebra + Let $A$ be a finitely presented $\A$-algebra and let $B : \Spec A \to \mU$ be a family of inhabited types. Then there merely exist unimodular $f_1, \dots, f_n : A$ together with dependent functions $s_i : \Pi_{x : D(f_i)} B(x)$. @@ -40,9 +40,9 @@ \subsection{First consequences} \begin{proposition}[using \axiomref{sqc}]% \label{spec-embedding} - For all finitely presented $R$-algebras $A$ and $B$ we have an equivalence + For all finitely presented $\A$-algebras $A$ and $B$ we have an equivalence \[ - f\mapsto \Spec f : \Hom_{\Alg{R}}(A,B) = (\Spec B \to \Spec A) + f\mapsto \Spec f : \Hom_{\AAlg}(A,B) = (\Spec B \to \Spec A) \rlap{.} \] \end{proposition} @@ -50,15 +50,15 @@ \subsection{First consequences} \begin{proof} By \Cref{algebra-from-affine-scheme}, we have a natural equivalence \[ - X\to \Spec (R^X) + X\to \Spec (\A^X) \] and by \axiomref{sqc}, the natural map \[ - A\to R^{\Spec A} + A\to \A^{\Spec A} \] is an equivalence. We therefore have a contravariant equivalence between - the category of finitely presented $R$-algebras + the category of finitely presented $\A$-algebras and the category of affine schemes. In particular, $\Spec$ is an embedding. \end{proof} @@ -67,21 +67,21 @@ \subsection{First consequences} \begin{proposition}[using \axiomref{loc}, \axiomref{sqc}]% \label{weak-nullstellensatz} - If $A$ is a finitely presented $R$-algebra, + If $A$ is a finitely presented $\A$-algebra, then we have $\Spec A=\emptyset$ if and only if $A=0$. \end{proposition} \begin{proof} If $\Spec A = \emptyset$ - then $A = R^{\Spec A} = R^\emptyset = 0$ + then $A = \A^{\Spec A} = \A^\emptyset = 0$ by (\axiomref{sqc}). If $A = 0$ - then there are no homomorphisms $A \to R$ - since $1 \neq 0$ in $R$ by (\axiomref{loc}). + then there are no homomorphisms $A \to \A$ + since $1 \neq 0$ in $\A$ by (\axiomref{loc}). \end{proof} For example, this weak nullstellensatz suffices -to prove the following properties of the ring $R$, +to prove the following properties of the ring $\A$, which were already proven in \cite{ingo-thesis}[Section 18.4]. @@ -89,11 +89,11 @@ \subsection{First consequences} \label{nilpotence-double-negation}\label{non-zero-invertible}\label{generalized-field-property} \begin{enumerate}[(a)] - \item An element $x:R$ is invertible, + \item An element $x:\A$ is invertible, if and only if $x\neq 0$. - \item A vector $x:R^n$ is non-zero, + \item A vector $x:\A^n$ is non-zero, if and only if one of its entries is invertible. - \item An element $x:R$ is nilpotent, + \item An element $x:\A$ is nilpotent, if and only if $\neg \neg (x=0)$. \end{enumerate} \end{proposition} @@ -101,18 +101,18 @@ \subsection{First consequences} \begin{proof} Part (a) is the special case $n = 1$ of (b). For (b), - consider the $R$-algebra $A \colonequiv R/(x_1, \dots, x_n)$. - Then the set $\Spec A \equiv \Hom_{\Alg{R}}(A, R)$ + consider the $\A$-algebra $A \colonequiv \A/(x_1, \dots, x_n)$. + Then the set $\Spec A \equiv \Hom_{\AAlg}(A, \A)$ is a proposition (that is, it has at most one element), and, more precisely, it is equivalent to the proposition $x = 0$. By \Cref{weak-nullstellensatz}, the negation of this proposition is equivalent to $A = 0$ - and thus to $(x_1, \dots, x_n) = R$. + and thus to $(x_1, \dots, x_n) = \A$. Using (\axiomref{loc}), this is the case if and only if one of the $x_i$ is invertible. For (c), - we instead consider the algebra $A \colonequiv R_x \equiv R[\frac{1}{x}]$. + we instead consider the algebra $A \colonequiv \A_x \equiv \A[\frac{1}{x}]$. Here we have $A = 0$ if and only if $x$ is nilpotent, while $\Spec A$ is the proposition $\inv(x)$. Thus, we can finish by \Cref{weak-nullstellensatz}, @@ -121,22 +121,22 @@ \subsection{First consequences} The following lemma, which is a variant of \cite{ingo-thesis}[Proposition 18.32], -shows that $R$ is in a weak sense algebraically closed. +shows that $\A$ is in a weak sense algebraically closed. See \Cref{non-existence-of-roots} for a refutation of -a stronger formulation of algebraic closure of~$R$. +a stronger formulation of algebraic closure of~$\A$. \begin{lemma}[using \axiomref{loc}, \axiomref{sqc}]% \label{polynomials-notnot-decompose} - Let $f : R[X]$ be a polynomial. + Let $f : \A[X]$ be a polynomial. Then it is not not the case that: either $f = 0$ or $f = \alpha \cdot {(X - a_1)}^{e_1} \dots {(X - a_n)}^{e_n}$ - for some $\alpha : R^\times$, - $e_i \geq 1$ and pairwise distinct $a_i : R$. + for some $\alpha : \A^\times$, + $e_i \geq 1$ and pairwise distinct $a_i : \A$. \end{lemma} \begin{proof} - Let $f : R[X]$ be given. + Let $f : \A[X]$ be given. Since our goal is a proposition, we can assume we have a bound $n$ on the degree of $f$, so @@ -149,12 +149,12 @@ \subsection{First consequences} setting $\alpha \colonequiv c_0$. Otherwise, $f$ is not invertible (using $0 \neq 1$ by (\axiomref{loc})), - so $R[X]/(f) \neq 0$, + so $\A[X]/(f) \neq 0$, which by (\axiomref{sqc}) means that - $\Spec(R[X]/(f)) = \{ x : R \mid f(x) = 0 \}$ + $\Spec(\A[X]/(f)) = \{ x : \A \mid f(x) = 0 \}$ is not empty. Using the double-negation stability of our goal again, - we can assume $f(a) = 0$ for some $a : R$ + we can assume $f(a) = 0$ for some $a : \A$ and factor $f = (X - a_1) f_{n - 1}$. By induction, we get $f = \alpha \cdot (X - a_1) \dots (X - a_n)$. Finally, we decide each of the finitely many propositions $a_i = a_j$, diff --git a/foundations/cohomology.tex b/foundations/cohomology.tex index 35d4126e..3bce305b 100644 --- a/foundations/cohomology.tex +++ b/foundations/cohomology.tex @@ -4,15 +4,15 @@ a scheme is just a type satisfying a property. When we want to consider the structure sheaf as an object in its own right, we can represent it by the trivial bundle -that assigns to every point $x : X$ the set $R$. +that assigns to every point $x : X$ the set $\A$. Indeed, for an affine scheme $X = \Spec A$, taking the sections of this bundle over a basic open $D(f) \subseteq X$ -\[ \left(\prod_{x : D(f)} R\right) = (D(f) \to R) = A[f^{-1}] \] +\[ \left(\prod_{x : D(f)} \A\right) = (D(f) \to \A) = A[f^{-1}] \] yields the localizations of the ring $A$ expected from the structure sheaf $\mathcal{O}_X$. More generally, instead of sheaves of abelian groups, $\mathcal{O}_X$-modules, etc., -we will consider bundles of abelian groups, $R$-modules, etc., +we will consider bundles of abelian groups, $\A$-modules, etc., in the form of maps from $X$ to the respective type of algebraic structures. \subsection{Quasi-coherent bundles} @@ -28,7 +28,7 @@ \subsection{Quasi-coherent bundles} \begin{definition} \index{$M(U)$} \label{application-of-bundle-to-subtype} - Let $X$ be a type and $M:X\to \Mod{R}$ a dependent module. + Let $X$ be a type and $M:X\to \Mod{\A}$ a dependent module. Let $U\subseteq X$ be any subtype. \begin{enumerate}[(a)] \item We write: @@ -36,8 +36,8 @@ \subsection{Quasi-coherent bundles} M(U)\colonequiv \prod_{x:U}M_x \rlap{.} \] - \item With pointwise structure, $U\to R$ is an $R$-algebra - and $M(U)$ is a $(U\to R)$-module. + \item With pointwise structure, $U\to \A$ is an $\A$-algebra + and $M(U)$ is a $(U\to \A)$-module. \end{enumerate} \end{definition} @@ -46,12 +46,12 @@ \subsection{Quasi-coherent bundles} \begin{lemma}[using \axiomref{loc}, \axiomref{sqc}, \axiomref{Z-choice}]% \label{module-bundle-localization-pointwise} - Let $X$ be a scheme and $M:X\to \Mod{R}$ a dependent module. - For any $f:X\to R$, there is an equality + Let $X$ be a scheme and $M:X\to \Mod{\A}$ a dependent module. + For any $f:X\to \A$, there is an equality \[ M(X)_f=\prod_{x:X}(M_x)_{f(x)} \] - of $(X\to R)$-modules. + of $(X\to \A)$-modules. \end{lemma} \begin{proof} @@ -119,13 +119,13 @@ \subsection{Quasi-coherent bundles} \begin{remark}% \label{localization-to-module-if-non-zero} - Let $M$ be an $R$-module and $A$ a finitely presented $R$-algebra, - then there is an $R$-linear map + Let $M$ be an $\A$-module and $A$ a finitely presented $\A$-algebra, + then there is an $\A$-linear map \[ M\otimes A\to M^{\Spec A} \] induced by mapping $m\otimes f$ to $x\mapsto x(f)\cdot m$. - In particular, for any $f:R$, there is a + In particular, for any $f:\A$, there is a \[ M_f\to M^{D(f)} \rlap{.} @@ -135,8 +135,8 @@ \subsection{Quasi-coherent bundles} \begin{lemma}[using \axiomref{loc}, \axiomref{sqc}, \axiomref{Z-choice}]% \label{localization-to-restriction} - Let $X$ be a scheme, $M:X\to\Mod{R}$, $U\subseteq X$ open and $f:A$. - Then there is an $R$-linear map + Let $X$ be a scheme, $M:X\to\Mod{\A}$, $U\subseteq X$ open and $f:A$. + Then there is an $\A$-linear map \[ M(U)_f \to M(D(f)) \rlap{.} @@ -155,30 +155,30 @@ \subsection{Quasi-coherent bundles} A characterization of quasi coherent sheaves in the little Zariski-topos was found with \cite{ingo-thesis}[Theorem 8.3]. This characterization is similar to our following definition of weak quasi-coherence, -which will provide us with an abelian subcategory of the $R$-module bundles over a scheme, +which will provide us with an abelian subcategory of the $\A$-module bundles over a scheme, where we can show that higher cohomology vanishes if the scheme is affine. \begin{definition} \label{weakly-quasi-coherent-module} - An $R$-module $M$ is \notion{weakly quasi-coherent}, - if for all $f:R$, the canonical homomorphism + An $\A$-module $M$ is \notion{weakly quasi-coherent}, + if for all $f:\A$, the canonical homomorphism \[ M_f\to M^{D(f)} \] from \Cref{localization-to-module-if-non-zero} is an equivalence. - We denote the type of weakly quasi-coherent $R$-modules - with $\Mod{R}_{wqc}$\index{$\Mod{R}_{wqc}$}. + We denote the type of weakly quasi-coherent $\A$-modules + with $\Mod{\A}_{wqc}$\index{$\Mod{\A}_{wqc}$}. \end{definition} \begin{lemma} \label{kernel-wqc} - For any $R$-linear map $f:M\to N$ of weakly quasi-coherent modules $M$ and $N$, + For any $\A$-linear map $f:M\to N$ of weakly quasi-coherent modules $M$ and $N$, the kernel of $f$ is weakly quasi-coherent. \end{lemma} \begin{proof} Let $K\to M$ be the kernel of $f$. - For any $f:R$, the map $K^{D(f)}\to M^{D(f)}$ is the kernel of $M^{D(f)}\to N^{D(f)}$. + For any $f:\A$, the map $K^{D(f)}\to M^{D(f)}$ is the kernel of $M^{D(f)}\to N^{D(f)}$. The latter map is equal to $M_f\to N_f$ by weak quasi-coherence of $M$ and $N$ and $K_f\to M_f$ is the kernel of $M_f\to N_f$. Let the vertical maps in @@ -198,7 +198,7 @@ \subsection{Quasi-coherent bundles} \begin{definition}% \label{weakly-quasi-coherent-bundle} Let $X$ be a scheme. - A weakly quasi-coherent bundle on $X$, is a map $M:X\to \Mod{R}_{wqc}$. + A weakly quasi-coherent bundle on $X$, is a map $M:X\to \Mod{\A}_{wqc}$. \end{definition} An immediate consequence is, that @@ -207,8 +207,8 @@ \subsection{Quasi-coherent bundles} \begin{lemma}[using \axiomref{loc}, \axiomref{sqc}, \axiomref{Z-choice}] \label{weakly-quasi-coherent-open-localization} - Let $X$ be a scheme and $M:X\to \Mod{R}$ weakly quasi-coherent, - then for all open $U\subseteq X$ and $f:U\to R$ + Let $X$ be a scheme and $M:X\to \Mod{\A}$ weakly quasi-coherent, + then for all open $U\subseteq X$ and $f:U\to \A$ the canonical morphism \[ M(U)_f\to M(D(f)) @@ -224,14 +224,14 @@ \subsection{Quasi-coherent bundles} \begin{proposition}% \label{fp-algebra-bundle-is-quasi-coherent} - Let $X$ be a scheme and $C:X\to \Alg{R}_{fp}$. - Then $C$, as a bundle of $R$-modules, is weakly quasi coherent. + Let $X$ be a scheme and $C:X\to \AAlg_{fp}$. + Then $C$, as a bundle of $\A$-modules, is weakly quasi coherent. \end{proposition} \begin{proof} - Then for any $f:R$ and $x:X$, using \Cref{algebra-valued-functions-on-affine}, we have + Then for any $f:\A$ and $x:X$, using \Cref{algebra-valued-functions-on-affine}, we have \[ - (C_x)_f=C_x\otimes_R R_f=(\Spec R_f \to C_x)=(D(f)\to C_x)={C_x}^{D(f)} + (C_x)_f=C_x\otimes_\A \A_f=(\Spec \A_f \to C_x)=(D(f)\to C_x)={C_x}^{D(f)} \rlap{.} \] \end{proof} @@ -242,12 +242,12 @@ \subsection{Quasi-coherent bundles} \begin{lemma}[using \axiomref{loc}, \axiomref{sqc}, \axiomref{Z-choice}]% \label{weakly-quasi-coherent-pi} - Let $X=\Spec(A)$ be an affine scheme and $M_x$ a weakly quasi-coherent $R$-module for any $x:X$, + Let $X=\Spec(A)$ be an affine scheme and $M_x$ a weakly quasi-coherent $\A$-module for any $x:X$, then \[ \prod_{x:X}M_x \] - is a weakly quasi-coherent $R$-module. + is a weakly quasi-coherent $\A$-module. \end{lemma} \begin{proof} @@ -255,7 +255,7 @@ \subsection{Quasi-coherent bundles} \[ \left(\prod_{x:X}M_x\right)_r=\left(\prod_{x:X}M_x\right)^{D(r)} \] - for all $r:R$. + for all $r:\A$. By \Cref{module-bundle-localization-pointwise}, weak quasi-coherence and \Cref{weakly-quasi-coherent-open-localization} we know for all $f:A$: @@ -266,7 +266,7 @@ \subsection{Quasi-coherent bundles} =\left(\prod_{x:X}M_x\right)^{D(f)} \rlap{.} \] - So in particular, we can choose $f:A$ to be $r:R$ using the $R$-algebra structure. + So in particular, we can choose $f:A$ to be $r:\A$ using the $\A$-algebra structure. \end{proof} Quasi-coherent dependent modules turn out to have very good properties, @@ -277,12 +277,12 @@ \subsection{Quasi-coherent bundles} \label{pullback-push-forward} Let $X,Y$ be types and $f:X\to Y$ be a map. \begin{enumerate}[(a)] - \item \index{$f^*M$} For any dependent module $N:Y\to\Mod{R}$, + \item \index{$f^*M$} For any dependent module $N:Y\to\Mod{\A}$, the \notion{pullback} or \notion{inverse image} is the dependent module \[ f^*N\colonequiv (x:X) \mapsto M_{f(x)}\rlap{.} \] - \item \index{$f_*M$} For any dependent module $M:X\to\Mod{R}$, + \item \index{$f_*M$} For any dependent module $M:X\to\Mod{\A}$, the \notion{push-forward} or \notion{direct image} is the dependent module \[ f_*M\colonequiv (y:Y) \mapsto \prod_{x:\fib_f(y)}M_{\pi_1(x)}\rlap{.} @@ -294,9 +294,9 @@ \subsection{Quasi-coherent bundles} \label{pullback-push-forward-qcoh} Let $X,Y$ be schemes and $f:X\to Y$ be a map. \begin{enumerate}[(a)] - \item For any weakly quasi-coherent dependent module $N:Y\to\Mod{R}$, + \item For any weakly quasi-coherent dependent module $N:Y\to\Mod{\A}$, the inverse image $f^*N$ is weakly quasi-coherent. - \item For any weakly quasi-coherent dependent module $M:X\to\Mod{R}$, + \item For any weakly quasi-coherent dependent module $M:X\to\Mod{\A}$, the direct image $f_*M$ is weakly quasi-coherent. \end{enumerate} \end{theorem} @@ -308,7 +308,7 @@ \subsection{Quasi-coherent bundles} \[ \prod_{x:\fib_f(y)}M_{\pi_1(x)} \] - is a weakly quasi-coherent $R$-module. + is a weakly quasi-coherent $\A$-module. By \Cref{fiber-product-scheme}, the type $\fib_f(y)$ is a scheme. So by \Cref{weakly-quasi-coherent-pi}, @@ -320,13 +320,13 @@ \subsection{Quasi-coherent bundles} there is a short proof of the following: \begin{proposition}[using \axiomref{loc}, \axiomref{sqc}, \axiomref{Z-choice}]% - Let $f:M\to N$ be an $R$-linear map of weakly quasi-coherent $R$-modules $M$ and $N$, + Let $f:M\to N$ be an $\A$-linear map of weakly quasi-coherent $\A$-modules $M$ and $N$, then the cokernel $N/M$ is weakly quasi-coherent. \end{proposition} \begin{proof} - We will first show, that for an $R$-linear embedding $m:M\to N$ - of weakly quasi-coherent $R$-modules $M$ and $N$, + We will first show, that for an $\A$-linear embedding $m:M\to N$ + of weakly quasi-coherent $\A$-modules $M$ and $N$, the cokernel $N/M$ is weakly quasi-coherent. We need to show: \[ @@ -335,17 +335,17 @@ \subsection{Quasi-coherent bundles} By algebra: $(N/M)_f=N_f/M_f$. This means we are done, if $(N/M)^{D(f)}=N^{D(f)}/{M^{D(f)}}$. To see this holds, let us consider $0\to M\to N\to N/M\to 0$ as a short exact sequence of dependent modules, - over the subtype of the point $D(f)\subseteq 1=\Spec R$. + over the subtype of the point $D(f)\subseteq 1=\Spec \A$. Then, taking global sections, by \Cref{cohomology-les}, we have an exact sequence \[ 0\to M^{D(f)}\to N^{D(f)}\to (N/M)^{D(f)}\to H^1(D(f),M) \] - -- but $D(f)=\Spec R_f$ is affine, + -- but $D(f)=\Spec \A_f$ is affine, so the last term is 0 by \Cref{H1-wqc-module-affine-trivial} and $(N/M)^{D(f)}$ is the cokernel $N^{D(f)}/M^{D(f)}$. - Now we will show the statement for a general $R$-linear map $f:M\to N$. + Now we will show the statement for a general $\A$-linear map $f:M\to N$. By algebra, the cokernel of $f$ is the same as the cokernel of the induced map $M/K\to N$, where $K$ is the kernel of $f$. By \Cref{kernel-wqc}, $K$ is weakly quasi-coherent, so by the proof above, @@ -355,20 +355,20 @@ \subsection{Quasi-coherent bundles} \subsection{Finitely presented bundles} -We now investigate the relationship between bundles of $R$-modules on $X = \Spec A$ +We now investigate the relationship between bundles of $\A$-modules on $X = \Spec A$ and $A$-modules. \begin{proposition} - Let $A$ be a finitely presented $R$-algebra. + Let $A$ be a finitely presented $\A$-algebra. There is an adjunction \[ \begin{tikzcd}[row sep=tiny] M \ar[r, mapsto] & {(M \otimes x)}_{x : \Spec A} \\ \Mod{A} \ar[r, shift left=2] \ar[r, phantom, "\rotatebox{90}{$\vdash$}"] & - \Mod{R}^{\Spec A} \ar[l, shift left=2] \\ + \Mod{\A}^{\Spec A} \ar[l, shift left=2] \\ \prod_{x : \Spec A} N_x & N \ar[l, mapsto] \end{tikzcd} \] between the category of $A$-modules - and the category of bundles of $R$-modules on $\Spec A$. + and the category of bundles of $\A$-modules on $\Spec A$. \end{proposition} For an $A$-module $M$, @@ -380,7 +380,7 @@ \subsection{Finitely presented bundles} \begin{example}[using \axiomref{sqc}, \axiomref{loc}] It is not the case that - for every finitely presented $R$-algebra $A$ + for every finitely presented $\A$-algebra $A$ and every $A$-module $M$ the map $\eta_M$ is injective. \end{example} @@ -392,10 +392,10 @@ \subsection{Finitely presented bundles} \begin{theorem}% \label{fp-module} Let $X=\Spec(A)$ be affine and - let a bundle of finitely presented $R$-modules $M : X\to \fpMod{R}$ be given. + let a bundle of finitely presented $\A$-modules $M : X\to \fpMod{\A}$ be given. Then the $A$-module \[ \tilde{M}\coloneqq\prod_{x:X}M_x \] - is finitely presented and for any $x:X$ the $R$-module $\tilde{M}\otimes_A R$ is $M_x$. + is finitely presented and for any $x:X$ the $\A$-module $\tilde{M}\otimes_A \A$ is $M_x$. Under this correspondence, localizing $\tilde{M}$ at $f:A$ corresponds to restricting $M$ to $D(f)$. \end{theorem} @@ -487,7 +487,7 @@ \subsection{Cohomology on affine schemes} \begin{theorem}[using \axiomref{loc}, \axiomref{sqc}, \axiomref{Z-choice}]% \label{H1-wqc-module-affine-trivial} - For any affine scheme $X=\Spec(A)$ and coefficients $M: X\to \Mod{R}_{wqc}$, we have + For any affine scheme $X=\Spec(A)$ and coefficients $M: X\to \Mod{\A}_{wqc}$, we have \[ H^1(X,M)=0 \rlap{.} \] \end{theorem} @@ -612,7 +612,7 @@ \subsection{Čech-Cohomology} \begin{example} If $X$ is a scheme, $U_1,\dots,U_n$ a cover by affine open subtypes - and $\mathcal F$ pointwise a weakly quasi coherent $R$-module, + and $\mathcal F$ pointwise a weakly quasi coherent $\A$-module, then $U_1,\dots,U_n$ is 1-acyclic for $\mathcal F$ by \Cref{H1-wqc-module-affine-trivial}. \end{example} diff --git a/foundations/internal.tex b/foundations/internal.tex index 806fa819..66b49812 100644 --- a/foundations/internal.tex +++ b/foundations/internal.tex @@ -39,20 +39,20 @@ \subsubsection{Axioms for the presheaf model} We start from 4 axioms. The 3 first axioms can be seen as variation of our 3 axioms for synthetic algebraic geometric. \begin{enumerate}[(1)] -\item $R$ is a ring, -\item for any f.p.\ $R$-algebra $A$, the canonical map $A\rightarrow R^{\Spec(A)}$ is an equivalence -\item for any f.p.\ $R$-algebra $A$, the set $\Spec(A)$ satisfies choice, which can be formulated as +\item $\A$ is a ring, +\item for any f.p.\ $\A$-algebra $A$, the canonical map $A\rightarrow \A^{\Spec(A)}$ is an equivalence +\item for any f.p.\ $\A$-algebra $A$, the set $\Spec(A)$ satisfies choice, which can be formulated as the fact that for any family of types $P(x)$ for $x:\Spec(A)$ there is a map $(\Pi_{x:\Spec(A)}\norm{P(x)})\rightarrow \norm{\Pi_{x:\Spec(A)}P(x)}$. -\item for any f.p.\ $R$-algebra $A$, the diagonal map $\nats\rightarrow\nats^{\Spec(A)}$ is an equivalence. +\item for any f.p.\ $\A$-algebra $A$, the diagonal map $\nats\rightarrow\nats^{\Spec(A)}$ is an equivalence. \end{enumerate} -As before, $\Spec(A)$ denotes the type of $R$-algebra maps from $A$ to $R$, and -if $r$ is in $R$, we write $D(r)$ for the proposition $\Spec(R_r)$. +As before, $\Spec(A)$ denotes the type of $\A$-algebra maps from $A$ to $\A$, and +if $r$ is in $\A$, we write $D(r)$ for the proposition $\Spec(\A_r)$. Note that the first axiom does not require -$R$ to be local, and the third axiom states that $\Spec(A)$ satisfies \emph{choice} and not only Zariski local choice, -for any f.p. $R$-algebra $A$. +$\A$ to be local, and the third axiom states that $\Spec(A)$ satisfies \emph{choice} and not only Zariski local choice, +for any f.p. $\A$-algebra $A$. \subsubsection{Justification of the axioms for the presheaf model} @@ -71,7 +71,7 @@ \subsubsection{Justification of the axioms for the presheaf model} We first introduce the presheaf $\FP$ of {\em finite presentations}. This is internally the type $$ -\Sigma_{n:\nats}\Sigma_{m:\nats}R[X_1,\dots,X_n]^m +\Sigma_{n:\nats}\Sigma_{m:\nats}\A[X_1,\dots,X_n]^m $$ which is interpreted by $\FP(L) = \Sigma_{n:\nats}\Sigma_{m:\nats}L[X_1,\dots,X_n]^m$. If $\xi = (n,m,q_1,\dots,q_m)\in\FP(L)$ is such a presentation, we build a natural extension @@ -83,36 +83,36 @@ \subsubsection{Justification of the axioms for the presheaf model} \medskip -Internally, we have a map $A:\FP\rightarrow R\mathsf{-alg}(\UU_0)$, which to any presentation -$\xi = (n,m,q_1,\dots,q_m)$ associates the $R$-algebra $A(\xi) = L[X_1,\dots,X_n]/(q_1,\dots,q_m)$. +Internally, we have a map $A:\FP\rightarrow \A\mathsf{-alg}(\UU_0)$, which to any presentation +$\xi = (n,m,q_1,\dots,q_m)$ associates the $\A$-algebra $A(\xi) = L[X_1,\dots,X_n]/(q_1,\dots,q_m)$. This corresponds externally to the presheaf on the category of elements of $\FP$ defined by $A(L,\xi) = L_{\xi}$. -Internally, we have a map $\Spec(A):\FP\rightarrow \UU_0$, defined by $\Spec(A)(\xi) = Hom(A(\xi),R)$. +Internally, we have a map $\Spec(A):\FP\rightarrow \UU_0$, defined by $\Spec(A)(\xi) = Hom(A(\xi),\A)$. We can replace it by the isomorphic map which to $\xi = (n,m,q_1,\dots,q_m)$ associates the set -$S(\xi)$ of solutions of the system $q_1=\dots=q_m= 0$ in $R^n$. +$S(\xi)$ of solutions of the system $q_1=\dots=q_m= 0$ in $\A^n$. Externally, this corresponds to the presheaf on the category of elements of $\FP$ so that $\Spec(A)(L,n,m,q_1,\dots,q_m)$ is the set of solutions of the system $q_1=\dots=q_m=0$ in $L^n$. \medskip -We now define externally two inverse maps $\varphi:A(\xi)\rightarrow R^{\Spec(A(\xi))}$ and -$\psi:R^{\Spec(A(\xi))}\rightarrow A(\xi)$. +We now define externally two inverse maps $\varphi:A(\xi)\rightarrow \A^{\Spec(A(\xi))}$ and +$\psi:\A^{\Spec(A(\xi))}\rightarrow A(\xi)$. \medskip -Notice first that $R^{\Spec(A)}(L,\xi)$, for $\xi = (n,m,q_1,\dots,q_m)$, +Notice first that $\A^{\Spec(A)}(L,\xi)$, for $\xi = (n,m,q_1,\dots,q_m)$, is the set of families of elements $l_{f,s}:M$ indexed by $f:L\rightarrow M$ and $s:M^n$ a solution of $fq_1 = \dots = fq_m=0$, satisfying the uniformity condition $g(l_{f,s}) = l_{(g\circ f),gs}$ for $g:M\rightarrow N$. \medskip -For $u$ in $A(L,\xi) = L_{\xi}$ we define $\varphi~u$ in $R^{\Spec(A)}(L,\xi)$ by +For $u$ in $A(L,\xi) = L_{\xi}$ we define $\varphi~u$ in $\A^{\Spec(A)}(L,\xi)$ by $$ (\varphi~u)_{f,s} = i(f,s)~u $$ -and for $l$ in $R^{\Spec(A)}(L,\xi)$ we define $\psi~l$ in $A(L,\xi) = L_{\xi}$ by +and for $l$ in $\A^{\Spec(A)}(L,\xi)$ we define $\psi~l$ in $A(L,\xi) = L_{\xi}$ by $$ \psi~ l = l_{\iota,s_{\xi}} $$ @@ -126,7 +126,7 @@ \subsubsection{Justification of the axioms for the presheaf model} $$ which shows that $\varphi$ and $\xi$ are inverse natural transformations. -Furthermore, the map $\varphi$ is the external version of the canonical map $A(\xi)\rightarrow R^{\Spec(A(\xi))}$. +Furthermore, the map $\varphi$ is the external version of the canonical map $A(\xi)\rightarrow \A^{\Spec(A(\xi))}$. The fact that this map is an isomorphism is an (internally) equivalent statement of the second axiom. @@ -136,9 +136,9 @@ \subsubsection{Sheaf model obtained by localisation from the presheaf model} We define now a family of propositions. As before, if $A$ is a ring, we let $\Um(A)$ be the type of unimodular sequences (\Cref{unimodular}) $f_1,\dots,f_n$ in $A$, i.e.\ such that $(1) = (f_1,\dots,f_n)$. To any element $\vec{r} = r_1,\dots,r_n$ -in $\Um(R)$ we associate +in $\Um(\A)$ we associate the proposition $D(\vec{r}) = D(r_1)\vee\dots\vee D(r_n)$. If $\vec{r}$ is the empty sequence then -$D(\vec{r})$ is the proposition $1 =_R 0$. %For $n=0$, we get the proposition $1=_R 0$. +$D(\vec{r})$ is the proposition $1 =_\A 0$. %For $n=0$, we get the proposition $1=_\A 0$. Starting from any model of dependent type theory with univalence satisfying the 4 axioms above, we build a new model of univalent type theory by considering the types $T$ that are modal for all modalities defined by the propositions @@ -154,39 +154,39 @@ \subsubsection{Sheaf model obtained by localisation from the presheaf model} consider modal types. \begin{proposition}\label{modal} - The ring $R$ is modal. It follows that any f.p.\ $R$-algebra is modal. + The ring $\A$ is modal. It follows that any f.p.\ $\A$-algebra is modal. \end{proposition} \begin{proof} - If $r_1,\dots,r_n$ is in $\Um(R)$, we build a patch function $R^{D(r_1,\dots,r_n)}\rightarrow R$. - Any element $u:R^{D(r_1,\dots,r_n)}$ gives a compatible family of elements $u_i:R^{D(r_i)}$, hence - a compatible family of elements in $R_{r_i}$ by quasi-coherence. But then it follows from local-global - principle \cite{lombardi-quitte}, that we can patch this family to a unique element of $R$. + If $r_1,\dots,r_n$ is in $\Um(\A)$, we build a patch function $\A^{D(r_1,\dots,r_n)}\rightarrow \A$. + Any element $u:\A^{D(r_1,\dots,r_n)}$ gives a compatible family of elements $u_i:\A^{D(r_i)}$, hence + a compatible family of elements in $\A_{r_i}$ by quasi-coherence. But then it follows from local-global + principle \cite{lombardi-quitte}, that we can patch this family to a unique element of $\A$. - If $A$ is a f.p.\ $R$-algebra, then $A$ is isomorphic to $R^{\Spec(A)}$ and hence is modal. + If $A$ is a f.p.\ $\A$-algebra, then $A$ is isomorphic to $\A^{\Spec(A)}$ and hence is modal. \end{proof} \begin{proposition} - In this new sheaf model, $\perp_S$ is $1 =_R 0$. + In this new sheaf model, $\perp_S$ is $1 =_\A 0$. \end{proposition} \begin{proof} - The proposition $1=_R0$ is modal by the previous proposition. + The proposition $1=_\A0$ is modal by the previous proposition. If $T$ is modal, all diagonal maps $T\rightarrow T^{D(\vec{r})}$ are equivalences. For the empty sequence $\vec{r}$ - we have that $D(\vec{r})$ is $\perp$, and the empty sequence is unimodular exactly when $1 =_R 0$. So $1=_R0$ + we have that $D(\vec{r})$ is $\perp$, and the empty sequence is unimodular exactly when $1 =_\A 0$. So $1=_\A0$ implies that $T$ and $T^{\perp}$ are equivalent, and so implies that $T$ is contractible. By extensionality, - we get that $(1=_R0)\rightarrow T$ is contractible when $T$ is modal. + we get that $(1=_\A0)\rightarrow T$ is contractible when $T$ is modal. \end{proof} \begin{lemma}\label{Um} - For any f.p.\ $R$-algebra $A$, we have $\Um(R)^{\Spec(A)} = \Um(A)$. + For any f.p.\ $\A$-algebra $A$, we have $\Um(\A)^{\Spec(A)} = \Um(A)$. \end{lemma} \begin{proof} Note that the fact that $r_1,\dots,r_n$ is unimodular is expressed by - $$\norm{\Sigma_{s_1,\dots,s_n:R}r_1s_1+\dots+r_ns_n = 1}$$ + $$\norm{\Sigma_{s_1,\dots,s_n:\A}r_1s_1+\dots+r_ns_n = 1}$$ and we can use these axioms 2 and 3 to get - $$\norm{\Sigma_{s_1,\dots,s_n:R}r_1s_1+\dots+r_ns_n = 1}^{\Spec(A)} = \norm{\Sigma_{v_1,\dots,v_n:A}\Pi_{x:\Spec(A)}r_1v_1(x)+\dots+r_nv_n(x) = 1}$$ + $$\norm{\Sigma_{s_1,\dots,s_n:\A}r_1s_1+\dots+r_ns_n = 1}^{\Spec(A)} = \norm{\Sigma_{v_1,\dots,v_n:A}\Pi_{x:\Spec(A)}r_1v_1(x)+\dots+r_nv_n(x) = 1}$$ The result follows then from this and axiom 4. \end{proof} %, that $A$ is quasi-coherent. @@ -205,49 +205,49 @@ \subsubsection{Sheaf model obtained by localisation from the presheaf model} %% We write $Um(A)$ for $\Sigma_{n:\nats}\Um(A)$. %% \begin{corollary} -%% If $A$ is a f.p. ring, then any function in $Um(R)^{\Spec(A)}$ is given by +%% If $A$ is a f.p. ring, then any function in $Um(\A)^{\Spec(A)}$ is given by %% a fundamental system of orthogonal idempotents $e_1,\dots,e_p$, and corresponding elements in $Um(A_{e_1}),\dots,Um(A_{e_p})$. %% \end{corollary} - For an f.p.\ $R$-algebra $A$, we can define the type of presentations $Pr_{n,m}(A)$ as the type $A[X_1,\dots,X_n]^m$. + For an f.p.\ $\A$-algebra $A$, we can define the type of presentations $Pr_{n,m}(A)$ as the type $A[X_1,\dots,X_n]^m$. Each element in $Pr_{n,m}(A)$ defines an f.p.\ $A$-algebra. Since $Pr_{n,m}(A)$ is a modal type since $A$ is f.p., the type of presentations $Pr_{n,m}(A)_S$ in the sheaf model defined for $n$ and $m$ in $\nats_S$ will be such that $Pr_{\eta p,\eta q}(A)_S = Pr_{p,q}(A)$ \cite{CRS21}. -% We have $Pr(R)^{\Spec(A)} = Pr(A)$. \rednote{Def of Pr missing} +% We have $Pr(\A)^{\Spec(A)} = Pr(A)$. \rednote{Def of Pr missing} \begin{lemma}\label{propsheaf} If $P$ is a proposition, then the sheafification of $P$ is - $$\norm{\Sigma_{(r_1,\dots,r_n):\Um(R)}P^{D(r_1,\dots,r_n)}}$$ + $$\norm{\Sigma_{(r_1,\dots,r_n):\Um(\A)}P^{D(r_1,\dots,r_n)}}$$ \end{lemma} \begin{proof} If $Q$ is a modal proposition and $P\rightarrow Q$ we have - $$\norm{\Sigma_{(r_1,\dots,r_n):\Um(R)}P^{D(r_1,\dots,r_n)}}\rightarrow Q$$ + $$\norm{\Sigma_{(r_1,\dots,r_n):\Um(\A)}P^{D(r_1,\dots,r_n)}}\rightarrow Q$$ since $P^{D(r_1,\dots,r_n)}\rightarrow Q^{D(r_1,\dots,r_n)}$ and $Q^{D(r_1,\dots,r_n)}\rightarrow Q$. It is thus enough to show that - $$P_0 = \norm{\Sigma_{(r_1,\dots,r_n):\Um(R)}P^{D(r_1,\dots,r_n)}}$$ + $$P_0 = \norm{\Sigma_{(r_1,\dots,r_n):\Um(\A)}P^{D(r_1,\dots,r_n)}}$$ is modal. - If $s_1,\dots,s_m$ is in $\Um(R)$ we show $P_0^{D(s_1,\dots,s_m)}\rightarrow P_0$. This follows - from $\Um(R)^{D(r)} = \Um(R_r)$, Lemma \ref{Um}. + If $s_1,\dots,s_m$ is in $\Um(\A)$ we show $P_0^{D(s_1,\dots,s_m)}\rightarrow P_0$. This follows + from $\Um(\A)^{D(r)} = \Um(\A_r)$, Lemma \ref{Um}. \end{proof} \begin{proposition}\label{norm} For any modal type $T$, the proposition $\norm{T}_S$ is - $$\norm{\Sigma_{(r_1,\dots,r_n):\Um(R)}T^{D(r_1)}\times\dots\times T^{D(r_n)}}$$ + $$\norm{\Sigma_{(r_1,\dots,r_n):\Um(\A)}T^{D(r_1)}\times\dots\times T^{D(r_n)}}$$ \end{proposition} \begin{proof} It follows from Lemma \ref{propsheaf} that the proposition $\norm{T}_S$ is - $$\norm{\Sigma_{(r_1,\dots,r_n):\Um(R)}\norm{T}^{D(r_1,\dots,r_n)}} = \norm{\Sigma_{(r_1,\dots,r_n):\Um(R)}\norm{T}^{D(r_1)}\times\dots\times\norm{T}^{D(r_n)}}$$ + $$\norm{\Sigma_{(r_1,\dots,r_n):\Um(\A)}\norm{T}^{D(r_1,\dots,r_n)}} = \norm{\Sigma_{(r_1,\dots,r_n):\Um(\A)}\norm{T}^{D(r_1)}\times\dots\times\norm{T}^{D(r_n)}}$$ and we get the result using the fact that choice holds for each $D(r_i)$, so that \[\norm{T}^{D(r_1)}\times\dots\times\norm{T}^{D(r_n)} = \norm{T^{D(r_1)}}\times\dots\times\norm{T^{D(r_n)}} = \norm{T^{D(r_1)}\times\dots\times T^{D(r_n)}}\] \end{proof} \begin{proposition} - In the sheaf model, $R$ is a local ring. + In the sheaf model, $\A$ is a local ring. \end{proposition} \begin{proof} @@ -255,28 +255,28 @@ \subsubsection{Sheaf model obtained by localisation from the presheaf model} \end{proof} \begin{lemma}\label{localfp} - If $A$ is a $R$-algebra which is modal and there exists $r_1,\dots,r_n$ in $\Um(R)$ such that each - $A^{D(r_i)}$ is a f.p.\ $R_{r_i}$-algebra, then $A$ is a f.p.\ $R$-algebra. + If $A$ is a $\A$-algebra which is modal and there exists $r_1,\dots,r_n$ in $\Um(\A)$ such that each + $A^{D(r_i)}$ is a f.p.\ $\A_{r_i}$-algebra, then $A$ is a f.p.\ $\A$-algebra. \end{lemma} \begin{proof} - Using the local-global principles presented in \cite{lombardi-quitte}, we can patch together the f.p.\ $R_{r_i}$-algebra - to a global f.p.\ $R$-algebra. This f.p.\ $R$-algebra is modal by Proposition \ref{modal}, and is locally equal to $A$ + Using the local-global principles presented in \cite{lombardi-quitte}, we can patch together the f.p.\ $\A_{r_i}$-algebra + to a global f.p.\ $\A$-algebra. This f.p.\ $\A$-algebra is modal by Proposition \ref{modal}, and is locally equal to $A$ and hence equal to $A$ since $A$ is modal. \end{proof} \begin{corollary} - The type of f.p.\ $R$-algebras is modal and is the type of f.p.\ $R$-algebras in the sheaf model. + The type of f.p.\ $\A$-algebras is modal and is the type of f.p.\ $\A$-algebras in the sheaf model. \end{corollary} \begin{proof} - For any $R$-algebra $A$, we can form a type $\Phi(n,m,A)$ expressing that $A$ has a presentation for some $v:Pr_{n,m}(R)$, - as the type stating that there is some map $\alpha:R[X_1,\dots,X_n]\rightarrow A$ and that $(A,\alpha)$ is universal such that + For any $\A$-algebra $A$, we can form a type $\Phi(n,m,A)$ expressing that $A$ has a presentation for some $v:Pr_{n,m}(\A)$, + as the type stating that there is some map $\alpha:\A[X_1,\dots,X_n]\rightarrow A$ and that $(A,\alpha)$ is universal such that $\alpha$ is $0$ on all elements of $v$. We can also look at this type $\Phi(n,m,A)_S$ in the sheaf model. Using the translation from \cite{Quirin16,CRS21}, we see that the type $\Phi(\eta n,\eta m,A)_S$ is exactly the type stating that $A$ is presented by - some $v:Pr_{n,m}(A)$ among the modal $R$-algebras. This is actually equivalent to $\Phi(n,m,A)$ since any f.p. $R$-algebra is modal. + some $v:Pr_{n,m}(A)$ among the modal $\A$-algebras. This is actually equivalent to $\Phi(n,m,A)$ since any f.p. $\A$-algebra is modal. - If $A$ is a modal $R$-algebra which is f.p. in the sense of the sheaf model, this means that we have + If $A$ is a modal $\A$-algebra which is f.p. in the sense of the sheaf model, this means that we have $$\norm{\Sigma_{n:\nats_S}\Sigma_{m:\nats_S}\Phi(n,m,A)_S}_S$$ This is equivalent to $$\norm{\Sigma_{n:\nats}\Sigma_{m:\nats}\Phi(\eta n,\eta m,A)_S}_S$$ @@ -285,10 +285,10 @@ \subsubsection{Sheaf model obtained by localisation from the presheaf model} Using Lemma \ref{localfp} and Proposition \ref{norm}, this is equivalent to $\norm{\Sigma_{n:\nats}\Sigma_{m:\nats}\Phi(n,m,A)}$. \end{proof} - Note that the type of f.p. $R$-algebra is universe independent. + Note that the type of f.p. $\A$-algebra is universe independent. \begin{proposition} - For any f.p.\ $R$-algebra $A$, the type $\Spec(A)$ is modal and satisfies the axiom of Zariski local choice in + For any f.p.\ $\A$-algebra $A$, the type $\Spec(A)$ is modal and satisfies the axiom of Zariski local choice in the sheaf model. \end{proposition} @@ -326,7 +326,7 @@ \subsubsection{Sheaf model obtained by localisation from the presheaf model} A particular case is if $\CC$ is the opposite of the category of f.p.\@ $k$-algebras, where $k$ is a fixed commutative ring. - We have the presheaf $R$ defined by $R(J,A) = Hom(k[X],A)$ where $J$ object of $\BB$ and $A$ object of $\CC$. + We have the presheaf $\A$ defined by $\A(J,A) = Hom(k[X],A)$ where $J$ object of $\BB$ and $A$ object of $\CC$. The presheaf $\Gm$ is defined by $\Gm(J,A) = Hom(k[X,1/X],A) = A^{\times}$, the set of invertible elements of $A$. @@ -357,7 +357,7 @@ \subsection{Propositional truncation} \subsection{Choice} -We prove choice in the presheaf model: if $A$ is a f.p.\@ algebra over $R$ then we have a map +We prove choice in the presheaf model: if $A$ is a f.p.\@ algebra over $\A$ then we have a map $$ l:(\Pi_{x:\Spec(A)}\norm{P})\rightarrow \norm{\Pi_{x:\Spec(A)}P} $$ @@ -370,17 +370,16 @@ \subsection{Choice} \subsection{$1$-topos model} For any small category $\CC$ we can form the presheaf model of type theory over the base category $\CC$ \cite{hofmann,huber-phd-thesis}. -%\rednote{Reference to Hoffmann/Simon's thesis?}. \medskip We look at the special case where $\CC$ is the opposite of the category of finitely presented $k$-algebras for a fixed ring $k$. - In this model we have a presheaf $R(A) = Hom(k[X],A)$ which has a ring structure. + In this model we have a presheaf $\A(A) = Hom(k[X],A)$ which has a ring structure. - In the {\em presheaf} model, we can check that we have $\neg\neg (0=_R 1)$. Indeed, at any stage $A$ we have - a map $\alpha:A\rightarrow 0$ to the trivial f.p. algebra $0$, and $0 =_R 1$ is valid at the stage $0$. + In the {\em presheaf} model, we can check that we have $\neg\neg (0=_\A 1)$. Indeed, at any stage $A$ we have + a map $\alpha:A\rightarrow 0$ to the trivial f.p. algebra $0$, and $0 =_\A 1$ is valid at the stage $0$. The previous internal description of the sheaf model applies as well in the $1$-topos setting. @@ -401,15 +400,15 @@ \subsection{$1$-topos model} \begin{proposition} $M$ is internally quasi-coherent\footnote{In the sense that the canonical map $M\otimes A\rightarrow M^{\Spec(A)}$ is an isomorphism for any - f.p. $R$-algebra $A$.} iff we have $M(B,\alpha) = M_A\otimes_A B$ and the restriction map for + f.p. $\A$-algebra $A$.} iff we have $M(B,\alpha) = M_A\otimes_A B$ and the restriction map for $\gamma:B\rightarrow C$ is $M_A\otimes_A\gamma$. \end{proposition} \subsubsection{Projective space} -We have defined $\bP^n$ to be the set of lines in $V = R^{n+1}$, so we have +We have defined $\bP^n$ to be the set of lines in $V = \A^{n+1}$, so we have $$ -\bP^n ~=~ \Sigma_{L:V\rightarrow \Omega}[\exists_{v:V}\neg (v = 0)\wedge L = R v] +\bP^n ~=~ \Sigma_{L:V\rightarrow \Omega}[\exists_{v:V}\neg (v = 0)\wedge L = \A v] $$ The following was noticed in \cite{kockreyes}. @@ -418,8 +417,8 @@ \subsection{$1$-topos model} \end{proposition} \begin{proof} - $\bP^n$ is the set of pairs $L,0$ where $L:\Omega^V(A)$ satisfies the proposition $\exists_{v:V}\neg (v = 0)\wedge L = Rv$ at stage - $A$. This condition implies that $L$ is a quasicoherent submodule of $R^{n+1}$ defined at stage $A$. + $\bP^n$ is the set of pairs $L,0$ where $L:\Omega^V(A)$ satisfies the proposition $\exists_{v:V}\neg (v = 0)\wedge L = \A v$ at stage + $A$. This condition implies that $L$ is a quasicoherent submodule of $\A^{n+1}$ defined at stage $A$. It is thus determined by its value $L(A,\idd_A) = L_A$. Furthermore, the condition also implies that $L_A$ is locally free of rank $1$. By local-global principle \cite{lombardi-quitte}, @@ -429,17 +428,17 @@ \subsection{$1$-topos model} One point in this argument was to notice that the condition $$ -\exists_{v:V}\neg (v = 0)\wedge L = R v +\exists_{v:V}\neg (v = 0)\wedge L = \A v $$ -implies that $L$ is quasi-coherent. This would be direct in presence of univalence, since we would have then $L = R$ as a $R$-module -and $R$ is quasi-coherent. But it can also be proved without univalence by transport along isomorphism: a $R$-module which is +implies that $L$ is quasi-coherent. This would be direct in presence of univalence, since we would have then $L = \A$ as a $\A$-module +and $\A$ is quasi-coherent. But it can also be proved without univalence by transport along isomorphism: a $\A$-module which is isomorphic to a quasi-coherent module is itself quasi-coherent. \subsection{Global sections and Zariski global choice} We let $\Box T$ the type of global sections of a globally defined sheaf $T$. -If $c = r_1,\dots,r_n$ is in $\Um(R)$ we let $\Box_c T$ be the type $\Box T^{D(r_1)}\times\dots\times\Box T^{D(r_n)}$. +If $c = r_1,\dots,r_n$ is in $\Um(\A)$ we let $\Box_c T$ be the type $\Box T^{D(r_1)}\times\dots\times\Box T^{D(r_n)}$. Using these notations, we can state the principle of Zariski global choice $$ @@ -449,7 +448,7 @@ \subsection{Global sections and Zariski global choice} This principle is valid in the present model. Using this principle, we can show that $\Box K(\Gm,1)$ is equal to the type of projective modules of rank $1$ over $k$ -and that each $\Box K(R,n)$ for $n>0$ is contractible. +and that each $\Box K(\A,n)$ for $n>0$ is contractible. %This should work over $\bP^n$ as well. diff --git a/foundations/introduction.tex b/foundations/introduction.tex index b4c20bb2..dd79c9e0 100644 --- a/foundations/introduction.tex +++ b/foundations/introduction.tex @@ -17,7 +17,7 @@ with an additional property that can be defined within our synthetic theory. Following ideas of Ingo Blechschmidt and Anders Kock (\cite{ingo-thesis}, \cite{kock-sdg}[I.12]), -we use a base ring $R$ which is local and satisfies an axiom reminiscent of the Kock-Lawvere axiom. +we use a base ring $\A$ which is local and satisfies an axiom reminiscent of the Kock-Lawvere axiom. This more general axiom is called \emph{synthetic quasi coherence (SQC)} by Blechschmidt and a version quantifying over external algebras is called the \emph{comprehensive axiom}\footnote{ In \cite{kock-sdg}[I.12], Kock's ``axiom $2_k$'' could equivalently be Theorem 12.2, @@ -35,33 +35,33 @@ p_m(X_1, \dots, X_n) &= 0\rlap{,} \end{align*} the solution set -$\{\, x : R^n \mid \forall i.\; p_i(x_1, \dots, x_n) = 0 \,\}$ -is in canonical bijection to the set of $R$-algebra homomorphisms -\[ \Hom_{\Alg{R}}(R[X_1, \dots, X_n]/(p_1, \dots, p_m), R) \] +$\{\, x : \A^n \mid \forall i.\; p_i(x_1, \dots, x_n) = 0 \,\}$ +is in canonical bijection to the set of $\A$-algebra homomorphisms +\[ \Hom_{\AAlg}(\A[X_1, \dots, X_n]/(p_1, \dots, p_m), \A) \] by identifying a solution $(x_1,\dots,x_n)$ with the homomorphism that maps each $X_i$ to $x_i$. -Conversely, for any $R$-algebra $A$ which is merely of the form $R[X_1, \dots, X_n]/(p_1, \dots, p_m)$, +Conversely, for any $\A$-algebra $A$ which is merely of the form $\A[X_1, \dots, X_n]/(p_1, \dots, p_m)$, we define the \emph{spectrum} of $A$ to be \[ - \Spec A \colonequiv \Hom_{\Alg{R}}(A, R) + \Spec A \colonequiv \Hom_{\AAlg}(A, \A) \rlap{.} \] In contrast to classical, non-synthetic algebraic geometry, where this set needs to be equipped with additional structure, we postulate axioms that will ensure that $\Spec A$ has the expected geometric properties. -Namely, SQC is the statement that, for all finitely presented $R$-algebras $A$, the canonical map +Namely, SQC is the statement that, for all finitely presented $\A$-algebras $A$, the canonical map \begin{align*} - A&\xrightarrow{\sim} (\Spec A\to R) \\ + A&\xrightarrow{\sim} (\Spec A\to \A) \\ a&\mapsto (\varphi\mapsto \varphi(a)) \end{align*} is an equivalence. -A prime example of a spectrum is $\A^1\colonequiv \Spec R[X]$, -which turns out to be the underlying set of $R$. +A prime example of a spectrum is $\A^1\colonequiv \Spec \A[X]$, +which turns out to be the underlying set of $\A$. With the SQC axiom, -\emph{any} function $f:\A^1\to \A^1$ is given as a polynomial with coefficients in $R$. +\emph{any} function $f:\A^1\to \A^1$ is given as a polynomial with coefficients in $\A$. In fact, all functions between affine schemes are given by polynomials. Furthermore, for any affine scheme $\Spec A$, the axiom ensures that -the algebra $A$ can be reconstructed as the algebra of functions $\Spec A \to R$, +the algebra $A$ can be reconstructed as the algebra of functions $\Spec A \to \A$, therefore establishing a duality between affine schemes and algebras. The Kock-Lawvere axiom used in synthetic differential geometry @@ -82,11 +82,11 @@ This is where the \emph{homotopy} type theory really comes to bear -- instead of the hopeless adaption of classical, non-constructive definitions of cohomology, we make use of higher types, -for example the $n$-th Eilenberg-MacLane space $K(R,n)$ of the group $(R,+)$. +for example the $n$-th Eilenberg-MacLane space $K(\A,n)$ of the group $(\A,+)$. As an analogue of classical cohomology with values in the structure sheaf, we then define cohomology with coefficients in the base ring as: \[ - H^n(X,R):\equiv \propTrunc{X\to K(R,n)}_0 + H^n(X,\A):\equiv \propTrunc{X\to K(\A,n)}_0 \rlap{.} \] This definition is very convenient for proving abstract properties of cohomology. @@ -101,7 +101,7 @@ by functions on the scheme and the corresponding open is morally the collection of points where the function does not vanish. With Zariski-local choice, we were able to show that these notions of openness agree in our setup. -Apart from SQC, locality of the base ring $R$ and Zariski-local choice, +Apart from SQC, locality of the base ring $\A$ and Zariski-local choice, we only use homotopy type theory, including univalent universes, truncations and some very basic higher inductive types. Roughly, Zariski-local choice states that any surjection into an affine scheme merely has sections on a \emph{Zariski}-cover.% \footnote{It is related to the set-theoretic axiom called diff --git a/foundations/main.tex b/foundations/main.tex index 18c88f46..4a5a9cc9 100644 --- a/foundations/main.tex +++ b/foundations/main.tex @@ -2,6 +2,8 @@ % latexmk -pdf -pvc -interaction=nonstopmode main.tex \documentclass{../util/zariski} +\renewcommand{\A}{\mathcal O} + \title{A Foundation for Synthetic Algebraic Geometry} \author{Felix Cherubini, Thierry Coquand and Matthias Hutzler} diff --git a/foundations/negative-results.tex b/foundations/negative-results.tex index 383a96d3..505fed57 100644 --- a/foundations/negative-results.tex +++ b/foundations/negative-results.tex @@ -17,35 +17,35 @@ \begin{lemma}[using \axiomref{loc}, \axiomref{sqc}, \axiomref{Z-choice}]% \label{R-not-zero-dimensional} - The ring $R$ is not zero-dimensional. + The ring $\A$ is not zero-dimensional. \end{lemma} \begin{proof} - Assume that $R$ is zero-dimensional, - so for every $f : R$ there merely is some $k : \N$ with $f^k \in (f^{k + 1})$. - We note that $R = \A^1$ is an affine scheme and + Assume that $\A$ is zero-dimensional, + so for every $f : \A$ there merely is some $k : \N$ with $f^k \in (f^{k + 1})$. + We note that $\A = \A^1$ is an affine scheme and that if $f^k \in (f^{k + 1})$, then we also have $f^{k'} \in (f^{k' + 1})$ for every $k' \geq k$. This means that we can apply \Cref{strengthened-boundedness} and merely obtain a number $K : \N$ - such that $f^K \in (f^{K + 1})$ for all $f : R$. + such that $f^K \in (f^{K + 1})$ for all $f : \A$. In particular, $f^{K + 1} = 0$ implies $f^K = 0$, so the canonical map - $\Spec R[X]/(X^K) \to \Spec R[X]/(X^{K + 1})$ + $\Spec \A[X]/(X^K) \to \Spec \A[X]/(X^{K + 1})$ is a bijection. But this is a contradiction, - since the homomorphism $R[X]/(X^{K + 1}) \to R[X]/(X^K)$ + since the homomorphism $\A[X]/(X^{K + 1}) \to \A[X]/(X^K)$ is not an isomorphism. \end{proof} \begin{example}[using \axiomref{loc}, \axiomref{sqc}, \axiomref{Z-choice}]% \label{non-existence-of-roots} It is not the case that - every monic polynomial $f : R[X]$ with $\deg f \geq 1$ has a root. + every monic polynomial $f : \A[X]$ with $\deg f \geq 1$ has a root. More specifically, if $U \subseteq \A^1$ is an open subset with the property that - the polynomial $X^2 - a : R[X]$ merely has a root + the polynomial $X^2 - a : \A[X]$ merely has a root for every $a : U$, then $U = \emptyset$. \end{example} @@ -58,16 +58,16 @@ By \axiomref{Z-choice}, there exists in particular a basic open $D(f) \subseteq \A^1$ with $a_0 \in D(f)$ - and a function $g : D(f) \to R$ + and a function $g : D(f) \to \A$ such that ${(g(x))}^2 = x$ for all $x : D(f)$. By \axiomref{sqc}, - this corresponds to an element $\frac{p}{f^n} : R[X]_f$ - with ${(\frac{p}{f^n})}^2 = X : R[X]_f$. + this corresponds to an element $\frac{p}{f^n} : \A[X]_f$ + with ${(\frac{p}{f^n})}^2 = X : \A[X]_f$. We use \Cref{polynomial-with-regular-value-is-regular} together with the fact that $f(a_0)$ is invertible - to get that $f : R[X]$ is regular, - and therefore $p^2 = f^{2n}X : R[X]$. - Considering this equation over $R^{\mathrm{red}} = R/\sqrt{(0)}$ instead, + to get that $f : \A[X]$ is regular, + and therefore $p^2 = f^{2n}X : \A[X]$. + Considering this equation over $\A^{\mathrm{red}} = \A/\sqrt{(0)}$ instead, we can show by induction that all coefficients of $p$ and of $f^n$ are nilpotent, which contradicts the invertibility of $f(a_0)$. \end{proof} @@ -77,16 +77,16 @@ the axioms we are using here are incompatible with a natural axiom that is true for the structure sheaf of the big étale topos, - namely that $R$ admits roots for unramifiable monic polynomials. + namely that $\A$ admits roots for unramifiable monic polynomials. The polynomial $X^2 - a$ is even separable for invertible $a$, - assuming that $2$ is invertible in $R$. + assuming that $2$ is invertible in $\A$. To get rid of this last assumption, - we can use the fact that either $2$ or $3$ is invertible in the local ring $R$ + we can use the fact that either $2$ or $3$ is invertible in the local ring $\A$ and observe that the proof of \Cref{non-existence-of-roots} works just the same for $X^3 - a$. \end{remark} -We now give two different proofs that not all $R$-modules are weakly quasi-coherent +We now give two different proofs that not all $\A$-modules are weakly quasi-coherent in the sense of \Cref{weakly-quasi-coherent-module}. The first shows that the map \[ M_f \to M^{D(f)} \] @@ -95,37 +95,37 @@ \begin{proposition}[using \axiomref{loc}, \axiomref{sqc}, \axiomref{Z-choice}]% \label{RN-non-wqc} - The $R$-module $R^\N$ is not weakly quasi-coherent + The $\A$-module $\A^\N$ is not weakly quasi-coherent (in the sense of \Cref{weakly-quasi-coherent-module}). \end{proposition} \begin{proof} - For $f : R$, - we have ${(R^{\N})}^{D(f)} = {(R^{D(f)})}^\N = {(R_f)}^\N$, + For $f : \A$, + we have ${(\A^{\N})}^{D(f)} = {(\A^{D(f)})}^\N = {(\A_f)}^\N$, so the question is whether the canonical map - \[ {(R^\N)}_f \to {(R_f)}^\N \] + \[ {(\A^\N)}_f \to {(\A_f)}^\N \] is an equivalence. If it is, - for a fixed $f : R$, + for a fixed $f : \A$, then the sequence $(1, \frac{1}{f}, \frac{1}{f^2}, \dots)$ has a preimage, so there is an $n : \N$ such that for all $k : \N$, - $\frac{a_k}{f^n} = \frac{1}{f^k}$ in $R_f$ - for some $a_k : R$. - In particular, $\frac{a_{n+1}}{f^n} = \frac{1}{f^{n+1}}$ in $R_f$ - and therefore $a_{n+1} f^{n+1+\ell} = f^{n+\ell}$ in $R$ for some $\ell : \N$. - This shows that $R$ is zero-dimensional + $\frac{a_k}{f^n} = \frac{1}{f^k}$ in $\A_f$ + for some $a_k : \A$. + In particular, $\frac{a_{n+1}}{f^n} = \frac{1}{f^{n+1}}$ in $\A_f$ + and therefore $a_{n+1} f^{n+1+\ell} = f^{n+\ell}$ in $\A$ for some $\ell : \N$. + This shows that $\A$ is zero-dimensional (\Cref{zero-dimensional-ring}) - if $R^\N$ is weakly quasi-coherent. + if $\A^\N$ is weakly quasi-coherent. So we are done by \Cref{R-not-zero-dimensional}. \end{proof} \begin{proposition}[using \axiomref{loc}, \axiomref{sqc}, \axiomref{Z-choice}]% \label{non-wqc-module-family} The implication - \[ M^{D(f)} = 0 \quad\Rightarrow\quad M_f = 0 \] - does not hold for all $R$-modules $M$ and $f : R$. + \[ M^{D(f)} = 0 \quad\\Aightarrow\quad M_f = 0 \] + does not hold for all $\A$-modules $M$ and $f : \A$. In particular, the map $M_f \to M^{D(f)}$ from \Cref{weakly-quasi-coherent-module} is not always injective. @@ -133,39 +133,39 @@ \begin{proof} Assume that the implication always holds. - We construct a family of $R$-modules, - parametrized by the elements of $R$, + We construct a family of $\A$-modules, + parametrized by the elements of $\A$, and deduce a contradiction from the assumption - applied to the $R$-modules in this family. + applied to the $\A$-modules in this family. - Given an element $f : R$, - the $R$-module we want to consider is + Given an element $f : \A$, + the $\A$-module we want to consider is the countable product - \[ M(f) \colonequiv \prod_{n : \N} R/(f^n) \rlap{.} \] + \[ M(f) \colonequiv \prod_{n : \N} \A/(f^n) \rlap{.} \] If $f \neq 0$ then $M(f) = 0$ (using \Cref{non-zero-invertible}). - This implies that the $R$-module $M(f)^{f \neq 0}$ + This implies that the $\A$-module $M(f)^{f \neq 0}$ is trivial: any function $f \neq 0 \to M(f)$ can only assign the value $0$ to any of the at most one witnesses of $f \neq 0$. By assumption, this implies that $M(f)_f$ is also trivial. Noting that - $M(f)$ is not only an $R$-module - but even an $R$-algebra in a natural way, + $M(f)$ is not only an $\A$-module + but even an $\A$-algebra in a natural way, we have \begin{align*} M(f)_f = 0 &\;\Leftrightarrow\; \exists k : \N.\; \text{$f^k = 0$ in $M(f)$} \\ &\;\Leftrightarrow\; - \exists k : \N.\; \forall n : \N.\; f^k \in (f^n) \subseteq R \\ + \exists k : \N.\; \forall n : \N.\; f^k \in (f^n) \subseteq \A \\ &\;\Leftrightarrow\; - \exists k : \N.\; f^k \in (f^{k + 1}) \subseteq R + \exists k : \N.\; f^k \in (f^{k + 1}) \subseteq \A \rlap{.} \end{align*} In summary, - our assumption implies that the ring $R$ is zero-dimensional + our assumption implies that the ring $\A$ is zero-dimensional (in the sense of \Cref{zero-dimensional-ring}). But this is not the case, as we saw in \Cref{R-not-zero-dimensional}. @@ -174,14 +174,14 @@ \begin{example}[using \axiomref{loc}, \axiomref{sqc}] It is not the case that for any pair of lines $L, L' \subseteq \bP^2$, - the $R$-algebra $R^{L \cap L'}$ is - as an $R$-module free of rank $1$. + the $\A$-algebra $\A^{L \cap L'}$ is + as an $\A$-module free of rank $1$. \end{example} \begin{proof} - The $R$-algebra $R^{L \cap L'}$ is free of rank $1$ + The $\A$-algebra $\A^{L \cap L'}$ is free of rank $1$ if and only if the structure homomorphism - $\varphi : R \to R^{L \cap L'}$ is bijective. + $\varphi : \A \to \A^{L \cap L'}$ is bijective. We will show that it is not even always injective. Consider the lines @@ -189,26 +189,26 @@ and \[ L' = \{\, [x : y : z] : \bP^2 \mid \varepsilon x + \delta y + z = 0 \,\} \rlap{,} \] - where $\varepsilon$ and $\delta$ are elements of $R$ + where $\varepsilon$ and $\delta$ are elements of $\A$ with $\varepsilon^2 = \delta^2 = 0$. - Consider the element $\varphi(\epsilon \delta) : R^{L \cap L'}$, - which is the constant function $L \cap L' \to R$ + Consider the element $\varphi(\epsilon \delta) : \A^{L \cap L'}$, + which is the constant function $L \cap L' \to \A$ with value $\varepsilon \delta$. For any point $[x : y : z] : L \cap L'$, we have $z = 0$ and $\varepsilon x + \delta y = 0$. But also, by definition of $\bP^3$, - we have $(x, y, z) \neq 0 : R^3$, + we have $(x, y, z) \neq 0 : \A^3$, so one of $x, y$ must be invertible. This implies $\delta \divides \varepsilon$ or $\varepsilon \divides \delta$, and in both cases we can conclude $\varepsilon \delta = 0$. - Thus, $\varphi(\epsilon \delta) = 0 : R^{L \cap L'}$. + Thus, $\varphi(\epsilon \delta) = 0 : \A^{L \cap L'}$. If $\varphi$ was always injective then this would imply $\varepsilon \delta = 0$ - for any $\varepsilon, \delta : R$ + for any $\varepsilon, \delta : \A$ with $\varepsilon^2 = \delta^2 = 0$. In other words, the inclusion - \[ \Spec R[X, Y]/(X^2, Y^2, XY) \hookrightarrow \Spec R[X, Y]/(X^2, Y^2) \] + \[ \Spec \A[X, Y]/(X^2, Y^2, XY) \hookrightarrow \Spec \A[X, Y]/(X^2, Y^2) \] would be a bijection. - But the corresponding $R$-algebra homomorphism is not an isomorphism. + But the corresponding $\A$-algebra homomorphism is not an isomorphism. \end{proof} diff --git a/foundations/preliminaries.tex b/foundations/preliminaries.tex index 3df25924..6ccbd1c3 100644 --- a/foundations/preliminaries.tex +++ b/foundations/preliminaries.tex @@ -113,15 +113,15 @@ \subsection{Algebra} \begin{definition}% \label{local-ring} - A commutative ring $R$ is \notion{local} if $1\neq 0$ in $R$ and - if for all $x,y:R$ such that $x+y$ is invertible, $x$ is invertible or $y$ is invertible. + A commutative ring $\A$ is \notion{local} if $1\neq 0$ in $\A$ and + if for all $x,y:\A$ such that $x+y$ is invertible, $x$ is invertible or $y$ is invertible. \end{definition} \begin{definition}% - Let $R$ be a commutative ring. - A \notion{finitely presented} $R$-algebra is an $R$-algebra $A$, - such that there merely are natural numbers $n,m$ and polynomials $f_1,\dots,f_m:R[X_1,\dots,X_n]$ - and an equivalence of $R$-algebras $A\simeq R[X_1,\dots,X_n]/(f_1,\dots,f_m)$. + Let $\A$ be a commutative ring. + A \notion{finitely presented} $\A$-algebra is an $\A$-algebra $A$, + such that there merely are natural numbers $n,m$ and polynomials $f_1,\dots,f_m:\A[X_1,\dots,X_n]$ + and an equivalence of $\A$-algebras $A\simeq \A[X_1,\dots,X_n]/(f_1,\dots,f_m)$. \end{definition} \begin{definition}% @@ -208,17 +208,17 @@ \subsection{Algebra} \begin{definition} \label{spec} - The \notion{(synthetic) spectrum}\index{$\Spec A$} of a finitely presented $R$-algebra $A$ - is the set of $R$-algebra homomorphisms from $A$ to $R$: - \[ \Spec A \colonequiv \Hom_{\Alg{R}}(A, R) \] + The \notion{(synthetic) spectrum}\index{$\Spec A$} of a finitely presented $\A$-algebra $A$ + is the set of $\A$-algebra homomorphisms from $A$ to $\A$: + \[ \Spec A \colonequiv \Hom_{\AAlg}(A, \A) \] \end{definition} -We write $\A^n$ for $\Spec R[X_1, \dots, X_n]$, -which is canonically in bijection with $R^n$ +We write $\A^n$ for $\Spec \A[X_1, \dots, X_n]$, +which is canonically in bijection with $\A^n$ by the universal property of the polynomial ring. In particular, -$\A^1$ is (in bijection with) the underlying set of $R$. -Our convention is to use the letter $R$ +$\A^1$ is (in bijection with) the underlying set of $\A$. +Our convention is to use the letter $\A$ when we think of it as an algebraic object, and to write $\A^1$ (or $\A^n$) when we think of it as a set or a geometric object. @@ -226,15 +226,15 @@ \subsection{Algebra} \begin{definition} \label{spec-on-maps} - For an algebra homomorphism $f:\Hom_{\Alg{R}}(A,B)$ - between finitely presented $R$-algebras $A$ and $B$, + For an algebra homomorphism $f:\Hom_{\AAlg}(A,B)$ + between finitely presented $\A$-algebras $A$ and $B$, we write \notion{$\Spec f$} for the map from $\Spec B$ to $\Spec A$ given by precomposition with $f$. \end{definition} \begin{definition}% \label{basic-open-subset} - Let $A$ be a finitely presented $R$-algebra. + Let $A$ be a finitely presented $\A$-algebra. For $f:A$, the \notion{basic open subset} given by $f$, is the subtype \[ @@ -247,7 +247,7 @@ \subsection{Algebra} \begin{definition} \label{open-closed-affine-subsets} - Let $A$ be a finitely presented $R$-algebra. + Let $A$ be a finitely presented $\A$-algebra. For $n:\N$ and $f_1,\dots,f_n:A$, there are \begin{enumerate}[(i)] \item the ``open'' subset @@ -263,7 +263,7 @@ \subsection{Algebra} \end{definition} We will later also need the notion of a \emph{Zariski-Cover} of a spectrum $\Spec A$, -for some finitely presented $R$-algebra $A$. +for some finitely presented $\A$-algebra $A$. Intuitively, this is a collection of basic opens which jointly cover $\Spec A$. Since it is more practical, we will however stay on the side of algebras. A finite list of elements $f_1,\dots,f_n:A$ yields a Zariski-Cover, @@ -271,7 +271,7 @@ \subsection{Algebra} \begin{definition} \label{unimodular} - Let $A$ be a finitely presented $R$-algebra. + Let $A$ be a finitely presented $\A$-algebra. Then a list $f_1,\dots,f_n:A$ of elements of $A$ is called \notion{unimodular} if we have an identity of ideals $(f_1,\dots,f_n)=(1)$. We use $\Um(A)$\index{$\Um(A)$} to denote the type of unimodular sequences in $A$: diff --git a/foundations/projective-space.tex b/foundations/projective-space.tex index 45746140..8c3d2574 100644 --- a/foundations/projective-space.tex +++ b/foundations/projective-space.tex @@ -22,11 +22,11 @@ \subsection{Construction of projective spaces} \begin{definition}% \begin{enumerate}[(a)] - \item An $n$-dimensional $R$-\notion{vector space} is an $R$-module $V$, - such that $\propTrunc{ V = R^n }$. - \item We write $\Vect{R}{n}$ for the type of these vector spaces and $V\setminus\{0\}$ for the type + \item An $n$-dimensional $\A$-\notion{vector space} is an $\A$-module $V$, + such that $\propTrunc{ V = \A^n }$. + \item We write $\Vect{\A}{n}$ for the type of these vector spaces and $V\setminus\{0\}$ for the type \[ \sum_{x:V}x\neq 0\] - \item A \notion{vector bundle} on a type $X$ is a map $V:X\to \Vect{R}{n}$. + \item A \notion{vector bundle} on a type $X$ is a map $V:X\to \Vect{\A}{n}$. \end{enumerate} \end{definition} @@ -37,9 +37,9 @@ \subsection{Construction of projective spaces} \begin{definition}% \label{projective-space-as-space-of-lines} \begin{enumerate}[(a)] - \item A \notion{line} in an $R$-vector space $V$ is a subtype $L:V\to \Prop$, + \item A \notion{line} in an $\A$-vector space $V$ is a subtype $L:V\to \Prop$, such that there exists an $x:V\setminus\{0\}$ with - \[ \prod_{y:V}\left(L (y) \Leftrightarrow \exists c:R.y=c\cdot x\right)\] + \[ \prod_{y:V}\left(L (y) \Leftrightarrow \exists c:\A.y=c\cdot x\right)\] \item The space of all lines in a fixed $n$-dimensional vector space $V$ is the \notion{projectivization} of $V$: \[ \bP(V)\colonequiv \sum_{L:V\to \Prop} L \text{ is a line} \] \item \notion{Projective $n$-space} $\bP^n \colonequiv \bP(\A^{n+1})$ is the projectivization of $\A^{n+1}$. @@ -49,16 +49,16 @@ \subsection{Construction of projective spaces} \begin{proposition}% \label{lines-are-one-dimensional} For any vector space $V$ and line $L\subseteq V$, - $L$ is 1-dimensional in the sense that $\propTrunc{L=_{\Mod{R}}R}$. + $L$ is 1-dimensional in the sense that $\propTrunc{L=_{\Mod{\A}}\A}$. \end{proposition} \begin{proof} Let $L$ be a line. We merely have $x:V\setminus\{0\}$ such that - \[ \prod_{y:V}\left(L (y) \Leftrightarrow \exists c:R.y=c\cdot x\right)\] + \[ \prod_{y:V}\left(L (y) \Leftrightarrow \exists c:\A.y=c\cdot x\right)\] We may replace the ``$\exists$'' with a ``$\sum$'', since $c$ is uniquely determined for any $x,y$. - This means we can construct the map $\alpha\mapsto \alpha\cdot x:R\to L$ and it is an equivalence. + This means we can construct the map $\alpha\mapsto \alpha\cdot x:\A\to L$ and it is an equivalence. \end{proof} We now give the small construction: @@ -68,7 +68,7 @@ \subsection{Construction of projective spaces} Let $n:\N$. \notion{Projective $n$-space}\index{$\bP^n$} $\bP^n$ is the set quotient of the type $\A^{n+1}\setminus\{0\}$ by the relation \[ - x \sim y \colonequiv \sum_{\lambda : R} \lambda x=y\rlap{.} + x \sim y \colonequiv \sum_{\lambda : \A} \lambda x=y\rlap{.} \] By \Cref{generalized-field-property}, the non-zero vector $y$ has an invertible entry, so that the right hand side is a proposition and $\lambda$ is a unit. @@ -123,7 +123,7 @@ \subsection{Construction of projective spaces} that we can take as a preimage. To conclude, we note that $\varphi$ is also an embedding. So let $\varphi([x])=\varphi([y])$. - Then, since $\langle x\rangle=\langle y\rangle$, there is a $\lambda\in R^\times$, + Then, since $\langle x\rangle=\langle y\rangle$, there is a $\lambda\in \A^\times$, such that $x=\lambda y$, so $[x]=[y]$. \end{proof} @@ -146,7 +146,7 @@ \subsection{Construction of projective spaces} \begin{proof} $[x]$ and $[y]$ are equal, - if and only if there merely is a $\lambda:R^\times$, + if and only if there merely is a $\lambda:\A^\times$, such that $\lambda x = y$. By calculation, if there is such a $\lambda$, we always have $x_iy_j=y_ix_j$. @@ -178,7 +178,7 @@ \subsection{Construction of projective spaces} Note that if $x=z$ and $z=y$, it follows that $x=y$. So we have $\neg (x=y)\Rightarrow \neg (x=z\wedge z=y)$. By \Cref{equality-2-by-2-minor}, $x=y$ and $x=z\wedge z=y$ - are both equivalent to the statement that some vector with components in $R$ is zero, + are both equivalent to the statement that some vector with components in $\A$ is zero, so we can replace negated equality, with existence of a non-zero element, or more explicitly, the following are equivalent: \begin{align*} @@ -199,23 +199,23 @@ \subsection{Construction of projective spaces} \[ \sum_{[x:y]:\bP^1}[x^2:y^2]=[0:1]\rlap{.} \] - So for any $x:R$ with $x^2=0$, $[x:1]:\fib_s([0:1])$ and + So for any $x:\A$ with $x^2=0$, $[x:1]:\fib_s([0:1])$ and any other point $(x,y)$ such that $[x:y]$ is in $\fib_s([0:1])$, already yields an equivalent point, since $y$ has to be invertible. - This shows that the fiber over $[0:1]$ is a first order disk, i.e. $\D(1)=\{x:R|x^2=0\}$. + This shows that the fiber over $[0:1]$ is a first order disk, i.e. $\D(1)=\{x:\A|x^2=0\}$. The same applies to the point $[1:0]$. - To analyze $\fib_s([1:1])$, let us assume $2\neq 0$ (in $R$). + To analyze $\fib_s([1:1])$, let us assume $2\neq 0$ (in $\A$). Then we know, the two points $[1:-1]$ and $[1:1]$ are in $\fib_s([1:1])$ and they are different. It will turn out, that any point in $\fib_s([1:1])$ is equal to one of those two. For any $[x':y']:\fib_s([1:1])$, we can assume $[x':y']=[x:1]$ and $x^2=1$, or equivalently $(x-1)(x+1)=0$. By \Cref{projective-space-apartness-relation}, inequality in $\bP^n$ is an apartness relation. - So for each $x:R$, we know $x-1$ is invertible or $x+1$ is invertible. - But this means that for any $x:R$ with $(x-1)(x+1)=0$, that $x=1$ or $x=-1$. + So for each $x:\A$, we know $x-1$ is invertible or $x+1$ is invertible. + But this means that for any $x:\A$ with $(x-1)(x+1)=0$, that $x=1$ or $x=-1$. While the fibers are not the same in general, they are all affine and have the same size in the sense that for each $\Spec A_x\colonequiv \fib_s(x)$, - we have that $A_x$ is free of rank 2 as an $R$-module. + we have that $A_x$ is free of rank 2 as an $\A$-module. To see this, let us first note, that $\fib_s([x:y])$ is completely contained in an affine subset of $\bP^1$. This is a proposition, so we can use that either $x$ or $y$ is invertible. @@ -230,19 +230,19 @@ \subsection{Construction of projective spaces} Let us rewrite with $z\colonequiv \frac{x}{y}$. Then \[ - \fib_s([z:1])=\sum_{a:\A^1}(a^2=z)=\Spec R[X]/(X^2-z) + \fib_s([z:1])=\sum_{a:\A^1}(a^2=z)=\Spec \A[X]/(X^2-z) \] - and $R[X]/(X^2-z)$ is free of rank 2 as an $R$-module. + and $\A[X]/(X^2-z)$ is free of rank 2 as an $\A$-module. \end{example} \subsection{Functions on $\bP^n$} -Here we prove the classical fact that all functions $\bP^n\to R$ are constant. +Here we prove the classical fact that all functions $\bP^n\to \A$ are constant. We start with the case $n = 1$. \begin{lemma}[using \axiomref{loc}, \axiomref{sqc}]% \label{functions-on-projective-line-constant} - All functions $\bP^1 \to R$ are constant. + All functions $\bP^1 \to \A$ are constant. \end{lemma} \begin{proof} @@ -260,22 +260,22 @@ \subsection{Functions on $\bP^n$} \A^1 \ar[r] & \bP^1 \end{tikzcd} \] - If we apply the functor $X \mapsto R^X$ to this diagram, - we obtain a pullback square of $R$ algebras, - and we can insert the known $R$ algebras for the affine schemes involved. + If we apply the functor $X \mapsto \A^X$ to this diagram, + we obtain a pullback square of $\A$ algebras, + and we can insert the known $\A$ algebras for the affine schemes involved. \[ \begin{tikzcd} - R[X, Y]/(1 - XY) & - R[Y] \ar[l] \\ - R[X] \ar[u] & - R^{\bP^1} \ar[l] \ar[u] + \A[X, Y]/(1 - XY) & + \A[Y] \ar[l] \\ + \A[X] \ar[u] & + \A^{\bP^1} \ar[l] \ar[u] \ar[lu, phantom, very near start, "\ulcorner"] \end{tikzcd} \] Here, the different variable names $X$ and $Y$ indicate the resulting homomorphisms. Now it is an algebraic computation, - understanding the elements of $R[X, Y]/(1 - XY)$ as Laurent polynomials, - to see that the pullback is the algebra $R$, - so we have $R^{\bP^1} = R$ as desired. + understanding the elements of $\A[X, Y]/(1 - XY)$ as Laurent polynomials, + to see that the pullback is the algebra $\A$, + so we have $\A^{\bP^1} = \A$ as desired. \end{proof} \begin{lemma}[using \axiomref{loc}, \axiomref{sqc}]% @@ -323,16 +323,16 @@ \subsection{Functions on $\bP^n$} \begin{theorem}[using \axiomref{loc}, \axiomref{sqc}]% \label{functions-on-projective-space-constant} - All functions $\bP^n \to R$ are constant, + All functions $\bP^n \to \A$ are constant, that is, - \[ H^0(\bP^n, R) \colonequiv (\bP^n \to R) = R \rlap{.} \] + \[ H^0(\bP^n, \A) \colonequiv (\bP^n \to \A) = \A \rlap{.} \] \end{theorem} \begin{proof} - Let $f : \bP^n \to R$ be given. + Let $f : \bP^n \to \A$ be given. For any two distinct points $p \neq q : \bP^n$, we can apply \Cref{parametrized-line-through-two-points-in-projective-space} - and (merely) find a map $\widetilde{f} : \bP^1 \to R$ + and (merely) find a map $\widetilde{f} : \bP^1 \to \A$ with $\widetilde{f}([0 : 1]) = f(p)$ and $\widetilde{f}([1 : 0]) = f(q)$. Then we see $f(p) = f(q)$ @@ -345,23 +345,23 @@ \subsection{Functions on $\bP^n$} \begin{remark} Another proof of \Cref{functions-on-projective-space-constant} goes as follows: - A function $f : \bP^n \to R$ + A function $f : \bP^n \to \A$ is by definition of $\bP^n$ (\Cref{projective-space-hit}) - given by an $R^{\times}$-invariant function - $g : \A^{n+1}\setminus\{0\} \to R$. + given by an $\A^{\times}$-invariant function + $g : \A^{n+1}\setminus\{0\} \to \A$. But it is possible to show that the restriction function - \[ (\A^{n+1} \to R) \xrightarrow{\sim} (\A^{n+1}\setminus\{0\} \to R) \] + \[ (\A^{n+1} \to \A) \xrightarrow{\sim} (\A^{n+1}\setminus\{0\} \to \A) \] is bijective (as long as $n \geq 1$), - so $g$ corresponds to a function $\widetilde{g} : \A^{n+1} \to R$ + so $g$ corresponds to a function $\widetilde{g} : \A^{n+1} \to \A$ which is constant on every subset of the form - $\{\, rx \mid r : R^{\times} \,\}$ + $\{\, rx \mid r : \A^{\times} \,\}$ for $x : \A^{n+1} \setminus \{0\}$. But then it is constant on the whole line - $\{\, rx \mid r : R \,\}$, + $\{\, rx \mid r : \A \,\}$, since the restriction function - $(\A^1 \to R) \hookrightarrow (\A^1\setminus\{0\} \to R)$ + $(\A^1 \to \A) \hookrightarrow (\A^1\setminus\{0\} \to \A)$ is injective. From this it follows that $f$ is constant with value $\widetilde{g}(0)$. @@ -371,14 +371,14 @@ \subsection{Functions on $\bP^n$} so it is the colimit (in the category of sets) of a diagram of finite intersections of them, which are all affine schemes. - The set of functions $\bP^n \to R$ + The set of functions $\bP^n \to \A$ is thus the limit of a corresponding diagram of algebras. These algebras are most conveniently described as sub-algebras of the degree $0$ part of the graded algebra - ${R[X_0, \dots, X_n]}_{X_0 \dots X_n}$, + ${\A[X_0, \dots, X_n]}_{X_0 \dots X_n}$, for example - $(U_0 \to R) = R[\frac{X_1}{X_0}, \dots, \frac{X_n}{X_0}]$. - Then the limit can be computed to be $R$. + $(U_0 \to \A) = \A[\frac{X_1}{X_0}, \dots, \frac{X_n}{X_0}]$. + Then the limit can be computed to be $\A$. \end{remark} @@ -392,27 +392,27 @@ \subsection{Line Bundles} \begin{definition}% Let $X$ be a type. - A \notion{line bundle} is a map $\mathcal L : X\to \Mod{R}$, + A \notion{line bundle} is a map $\mathcal L : X\to \Mod{\A}$, such that - \[ \prod_{x:X} \propTrunc{\mathcal L_x=_{\Mod{R}}R} \rlap{.}\] + \[ \prod_{x:X} \propTrunc{\mathcal L_x=_{\Mod{\A}}\A} \rlap{.}\] The \notion{trivial line bundle} on $X$ is the line bundle - $X \to \Mod{R}, x \mapsto R$, + $X \to \Mod{\A}, x \mapsto \A$, and when we say that a line bundle $\mathcal{L}$ is trivial we mean that $\mathcal{L}$ is equal to the trivial line bundle, - or equivalently $\propTrunc{\prod_{x:X} \mathcal L_x=_{\Mod{R}}R}$. + or equivalently $\propTrunc{\prod_{x:X} \mathcal L_x=_{\Mod{\A}}\A}$. \end{definition} \begin{definition} \begin{enumerate}[(a)] - \item The \notion{tautological bundle} is the line bundle $\mathcal O_{\bP^n}(-1):\bP^n\to \Mod{R}$, + \item The \notion{tautological bundle} is the line bundle $\mathcal O_{\bP^n}(-1):\bP^n\to \Mod{\A}$, given by \[ (L:\bP^n)\mapsto L\rlap{.}\] - \item The \notion{dual}\index{$\mathcal L^\vee$} $\mathcal L^\vee$ of a line bundle $\mathcal L:\bP^n\to \Mod{R}$, + \item The \notion{dual}\index{$\mathcal L^\vee$} $\mathcal L^\vee$ of a line bundle $\mathcal L:\bP^n\to \Mod{\A}$, is the line bundle given by - \[ (x:\bP^n)\mapsto \Hom_{\Mod{R}}(\mathcal L_x,R)\rlap{.}\] - \item The \notion{tensor product} of $R$-module bundles $\mathcal F\otimes \mathcal G$\index{$\mathcal F\otimes \mathcal G$} + \[ (x:\bP^n)\mapsto \Hom_{\Mod{\A}}(\mathcal L_x,\A)\rlap{.}\] + \item The \notion{tensor product} of $\A$-module bundles $\mathcal F\otimes \mathcal G$\index{$\mathcal F\otimes \mathcal G$} on a scheme $X$ - is given by pointwise taking the tensor product of $R$-modules. + is given by pointwise taking the tensor product of $\A$-modules. \item For $k:\Z$, the $k$-th \notion{Serre twisting sheaf} $\mathcal{O}_{\bP^n}(k)$ on $\bP^n$ is given by taking the $-k$-th tensor power of $\mathcal O_{\bP^n}(-1)$ for negative $k$ and the $k$-th tensor power of $\mathcal O_{\bP^n}(-1)^{\vee}$ otherwise. @@ -428,7 +428,7 @@ \subsection{Line Bundles} we have not not: either $U = \emptyset$ or $U = D((X - a_1)\dots(X - a_n)) = \A^1 \setminus \{ a_1, \dots, a_n \}$ - for pairwise distinct numbers $a_1, \dots, a_n : R$. + for pairwise distinct numbers $a_1, \dots, a_n : \A$. \end{lemma} \begin{proof} @@ -441,7 +441,7 @@ \subsection{Line Bundles} by \Cref{qc-open-affine-open}, so we do not not get (that $U = \emptyset$ or) - a list of elements $a_1, \dots, a_n : R$ + a list of elements $a_1, \dots, a_n : \A$ such that $U = \A^1 \setminus \{ a_1, \dots, a_n \}$. Then we can not not get rid of any duplicates in the list. \end{proof} @@ -449,10 +449,10 @@ \subsection{Line Bundles} \begin{lemma}[using \axiomref{loc}, \axiomref{sqc}, \axiomref{Z-choice}]% \label{decompose-invertible-function-on-intersection-in-A1} Let $U, V : \A^1 \to \Prop$ be two open subsets - and let $f : U \cap V \to R^\times$ be a function. + and let $f : U \cap V \to \A^\times$ be a function. Then there do not not exist functions - $g : U \to R^\times$ and - $h : V \to R^\times$ + $g : U \to \A^\times$ and + $h : V \to \A^\times$ such that $f(x) = g(x)h(x)$ for all $x : U \cap V$. \end{lemma} @@ -467,7 +467,7 @@ \subsection{Line Bundles} \rlap{,} \end{align*} where all linear factors are distinct. - Then every function $f : U \cap V \to R^\times$ can + Then every function $f : U \cap V \to \A^\times$ can by (\axiomref{sqc}), \Cref{polynomials-notnot-decompose} and comparing linear factors not not be written in the form @@ -476,7 +476,7 @@ \subsection{Line Bundles} {(X - b_1)}^{e'_1} \dots {(X - b_l)}^{e'_l} {(X - c_1)}^{e''_1} \dots {(X - c_m)}^{e''_m} \] - with $\alpha : R^\times$, $e_i, e'_i, e''_i : \Z$. + with $\alpha : \A^\times$, $e_i, e'_i, e''_i : \Z$. Other linear factors can not appear, since they do not represent invertible functions on $U \cap V$. Now we can write $f = gh$ as desired, @@ -492,25 +492,25 @@ \subsection{Line Bundles} \begin{theorem}[using \axiomref{loc}, \axiomref{sqc}, \axiomref{Z-choice}]% \label{Gm-torsors-on-A1} - Every $R^\times$-torsor on $\A^1$ (\Cref{torsor}) + Every $\A^\times$-torsor on $\A^1$ (\Cref{torsor}) does not not have a global section. \end{theorem} \begin{proof} - Let $T$ be an $R^\times$-torsor on $\A^1$, + Let $T$ be an $\A^\times$-torsor on $\A^1$, that is, for every $x : \A^1$, - $T_x$ is a set with a free and transitive $R^\times$ action + $T_x$ is a set with a free and transitive $\A^\times$ action and $\propTrunc{T_x}$. By (\axiomref{Z-choice}), we get a cover of $\A^1$ by open subsets $\A^1 = \bigcup_{i = 1}^n U_i$ and local sections $s_i : (x : U_i) \to T_x$ of the bundle $T$. From this we can not not construct a global section by induction on $n$: Given any two local sections $s_i, s_j$ defined on $U_i, U_j$, - let $f : U_i \cap U_j \to R^\times$ be the unique function with + let $f : U_i \cap U_j \to \A^\times$ be the unique function with $f(x)s_i(x) = s_j(x)$ for all $x : U_i \cap U_j$. Then by \Cref{decompose-invertible-function-on-intersection-in-A1}, - we not not find $g : U_i \to R^\times$, $h : U_j \to R^\times$ + we not not find $g : U_i \to \A^\times$, $h : U_j \to \A^\times$ such that the sections $x \mapsto g(x)s_i(x)$ and $x \mapsto {h(x)}^{-1}s_j(x)$, defined on $U_i$ respectively $U_j$, @@ -530,19 +530,19 @@ \subsection{Line Bundles} \begin{proof} Given a line bundle $\mathcal{L}$, - we can construct an $R^\times$ torsor + we can construct an $\A^\times$ torsor \[ x \mapsto \mathcal{L}_x \setminus \{0\} \rlap{.} \] - Note that there is a well-defined $R^\times$ action on $M \setminus \{0\}$ - for every $R$ module $M$, + Note that there is a well-defined $\A^\times$ action on $M \setminus \{0\}$ + for every $\A$ module $M$, and the action on $\mathcal{L}_x \setminus \{0\}$ is free and transitive and we have $\propTrunc{\mathcal{L}_x \setminus \{0\}}$ - since we merely have $\mathcal{L}_x = R$ as $R$ modules. + since we merely have $\mathcal{L}_x = \A$ as $\A$ modules. By \Cref{Gm-torsors-on-A1}, there not not is a global section of this torsor, so we have a section $s : (x : \A^1) \to \mathcal{L}_x$ with $s(x) \neq 0$ for all $x : \A^1$. But this means that the line bundle $\mathcal{L}$ is trivial, - since we can build an identification $\mathcal{L}_x = R$ + since we can build an identification $\mathcal{L}_x = \A$ by sending $s(x)$ to $1$. \end{proof} @@ -550,15 +550,15 @@ \subsection{Line Bundles} \begin{lemma}[using \axiomref{loc}, \axiomref{sqc}] \label{invertible-laurent-polynomials} - Every invertible element of the ring of Laurent polynomials $R[X]_X$ + Every invertible element of the ring of Laurent polynomials $\A[X]_X$ is not not of the form $\alpha X^n$ - for some $\alpha : R^{\times}$ and $n : \Z$. + for some $\alpha : \A^{\times}$ and $n : \Z$. \end{lemma} \begin{proof} - Every element $f : R[X]_X$ is of the form + Every element $f : \A[X]_X$ is of the form $f = \sum_{i = m}^{m + n} a_i X^i$ - for some $m : \Z$, $n \geq 0$ and $a_i : R$. + for some $m : \Z$, $n \geq 0$ and $a_i : \A$. Every $a_i$ is not not either $0$ or invertible. Thus we can assume that either $f = 0$ or both $a_m$ and $a_{m+n}$ are invertible. @@ -576,20 +576,20 @@ \subsection{Line Bundles} \end{theorem} \begin{proof} - Let $\mathcal{L}:\bP^1\to \Mod{R}$ be a line bundle on $\bP^1$. - By pushout recursion, $\mathcal{L}$ is given by two line bundles $\mathcal L_0,\mathcal L_1:\A^1\to\Mod{R}$ + Let $\mathcal{L}:\bP^1\to \Mod{\A}$ be a line bundle on $\bP^1$. + By pushout recursion, $\mathcal{L}$ is given by two line bundles $\mathcal L_0,\mathcal L_1:\A^1\to\Mod{\A}$ and a glueing function $g:(x:\A^1\setminus\{0\})\to \mathcal L_0(x)=\mathcal L_1(\frac{1}{x})$. - Since we are proving a double negation, we can assume identifications $p_0:(x:\A^1)\to \mathcal L_0=R^1$ - and $p_1:(x:\A^1)\to \mathcal L_1=R^1$ by \Cref{line-bundle-A1-notnot-trivial}. + Since we are proving a double negation, we can assume identifications $p_0:(x:\A^1)\to \mathcal L_0=\A^1$ + and $p_1:(x:\A^1)\to \mathcal L_1=\A^1$ by \Cref{line-bundle-A1-notnot-trivial}. - Now we can define $g':(x:\A^1\setminus\{0\})\to R^1=R^1$ by $g'(x)\colonequiv p_0^{-1}(x)\cdot g(x)\cdot p_1(\frac{1}{x})$. - By synthetic quasi-coherence, equivalently, $g'$ is an invertible element of $R[X]_X$ - and therefore by \Cref{invertible-laurent-polynomials} given by $\alpha X^n$ for some $\alpha:R^\times$ and $n:\Z$. + Now we can define $g':(x:\A^1\setminus\{0\})\to \A^1=\A^1$ by $g'(x)\colonequiv p_0^{-1}(x)\cdot g(x)\cdot p_1(\frac{1}{x})$. + By synthetic quasi-coherence, equivalently, $g'$ is an invertible element of $\A[X]_X$ + and therefore by \Cref{invertible-laurent-polynomials} given by $\alpha X^n$ for some $\alpha:\A^\times$ and $n:\Z$. We can assume $\alpha=1$, since this just amounts to concatenating our final equality with the automorphism of line bundles given by $\alpha^{-1}$ at all points. By explicit calculation, the tautological bundle $\mathcal O_{\bP^1}(-1)$ on $\bP^1$ is given by glueing trivial line bundles along - a glueing function $g_{-1}:(x:\A^1\setminus\{0\})\to R^1=R^1$ with $g_{-1}(x)\colonequiv \lambda\mapsto x\cdot \lambda$. + a glueing function $g_{-1}:(x:\A^1\setminus\{0\})\to \A^1=\A^1$ with $g_{-1}(x)\colonequiv \lambda\mapsto x\cdot \lambda$. Note that an arbitrary choice of sign is involved, made by choosing the direction of the glueing function. Sticking with the same choice, calculation shows $g_1(x)\colonequiv \lambda\mapsto \frac{1}{x}\cdot \lambda$ is a glueing function for the dual of the tautological bundle $\mathcal O_{\bP^1}(1)$ diff --git a/foundations/schemes.tex b/foundations/schemes.tex index 79fc0c5f..fd5afee8 100644 --- a/foundations/schemes.tex +++ b/foundations/schemes.tex @@ -139,7 +139,7 @@ \subsection{Dependent sums} \begin{proof} We start with an affine $X=\Spec A$ and $Y_x=\Spec B_x$. Locally on $U_i = D(f_i)$, for a Zariski-cover $f_1,\dots,f_l$ of $X$, - we have $B_x=\Spec R[X_1,\dots,X_{n_i}]/(g_{i,x,1},\dots,g_{i,x,m_i})$ + we have $B_x=\Spec \A[X_1,\dots,X_{n_i}]/(g_{i,x,1},\dots,g_{i,x,m_i})$ with polynomials $g_{i,x,j}$. In other words, $B_x$ is the closed subtype of $\A^{n_i}$ where the functions $g_{i,x,1},\dots,g_{i,x,m_i}$ vanish. diff --git a/foundations/topology.tex b/foundations/topology.tex index 88b374d3..aaa939d7 100644 --- a/foundations/topology.tex +++ b/foundations/topology.tex @@ -7,13 +7,13 @@ \subsection{Closed subtypes} \item A \notion{closed proposition} is a proposition which is merely of the form $x_1 = 0 \land \dots \land x_n = 0$ - for some elements $x_1, \dots, x_n \in R$. + for some elements $x_1, \dots, x_n \in \A$. \item Let $X$ be a type. A subtype $U : X \to \Prop$ is \notion{closed} if for all $x : X$, the proposition $U(x)$ is closed. \item - For $A$ a finitely presented $R$-algebra + For $A$ a finitely presented $\A$-algebra and $f_1, \dots, f_n : A$, we set $V(f_1, \dots, f_n) \colonequiv @@ -27,10 +27,10 @@ \subsection{Closed subtypes} \begin{proposition}[using \axiomref{sqc}]% There is an order-reversing isomorphism of partial orders \begin{align*} - \text{f.g.-ideals}(R) &\xrightarrow{{\sim}} \Omega_{cl} \\ + \text{f.g.-ideals}(\A) &\xrightarrow{{\sim}} \Omega_{cl} \\ I &\mapsto (I = (0)) \end{align*} - between the partial order of finitely generated ideals of $R$ + between the partial order of finitely generated ideals of $\A$ and the partial order of closed propositions. \end{proposition} @@ -46,15 +46,15 @@ \subsection{Closed subtypes} \rlap{\text{.}} \] For this we use synthetic quasicoherence. - Note that the set $\Spec R/I = \Hom_{\Alg{R}}(R/I, R)$ is a proposition + Note that the set $\Spec \A/I = \Hom_{\AAlg}(\A/I, \A)$ is a proposition (has at most one element), namely it is equivalent to the proposition $I = (0)$. - Similarly, $\Hom_{\Alg{R}}(R/J, R/I)$ is a proposition + Similarly, $\Hom_{\AAlg}(\A/J, \A/I)$ is a proposition and equivalent to $J \subseteq I$. But then our claim is just the equation - \[ \Hom(\Spec R/I, \Spec R/J) = \Hom_{\Alg{R}}(R/J, R/I) \] + \[ \Hom(\Spec \A/I, \Spec \A/J) = \Hom_{\AAlg}(\A/J, \A/I) \] which holds by \Cref{spec-embedding}, - since $R/I$ and $R/J$ are finitely presented $R$-algebras + since $\A/I$ and $\A/J$ are finitely presented $\A$-algebras if $I$ and $J$ are finitely generated ideals. \end{proof} @@ -86,7 +86,7 @@ \subsection{Closed subtypes} By \axiomref{Z-choice} and boundedness, there is a cover $D(f_1),\dots,D(f_l)$, such that on each $D(f_i)$, $C$ is the vanishing set of functions - \[ g_1,\dots,g_n:D(f_i)\to R\rlap{.} \] + \[ g_1,\dots,g_n:D(f_i)\to \A\rlap{.} \] By \Cref{ideals-embed-into-closed-subsets}, the ideals generated by these functions agree in $A_{f_i f_j}$, @@ -106,7 +106,7 @@ \subsection{Open subtypes} \begin{definition}% \label{qc-open} \begin{enumerate}[(a)] - \item A proposition $P$ is \notion{(qc-)open}, if there merely are $f_1,\dots,f_n:R$, + \item A proposition $P$ is \notion{(qc-)open}, if there merely are $f_1,\dots,f_n:\A$, such that $P$ is equivalent to one of the $f_i$ being invertible. \item Let $X$ be a type. A subtype $U:X\to\Prop$ is \notion{(qc-)open}, if $U(x)$ is an open proposition for all $x:X$. @@ -198,12 +198,12 @@ \subsection{Open subtypes} \begin{theorem}[using \axiomref{loc}, \axiomref{sqc}, \axiomref{Z-choice}]% \label{qc-open-affine-open} Let $X=\Spec A$ and $U:X\to\Prop$ be an open subtype, - then $U$ is affine open, i.e. there merely are $h_1,\dots,h_n:X\to R$ such that + then $U$ is affine open, i.e. there merely are $h_1,\dots,h_n:X\to \A$ such that $U=D(h_1,\dots,h_n)$. \end{theorem} \begin{proof} - Let $L(x)$ be the type of finite lists of elements of $R$, + Let $L(x)$ be the type of finite lists of elements of $\A$, such that one of them being invertible is equivalent to $U(x)$. By assumption, we know \[\prod_{x:X}\propTrunc{L(x)}\rlap{.}\] @@ -211,7 +211,7 @@ \subsection{Open subtypes} We compose with the length function for lists to get functions $l_i:D(f_i)\to\N$. By \Cref{boundedness}, the $l_i$ are bounded. Since we are proving a proposition, we can assume we have actual bounds $b_i:\N$. - So we get functions $\tilde{s_i}:D(f_i)\to R^{b_i}$, + So we get functions $\tilde{s_i}:D(f_i)\to \A^{b_i}$, by append zeros to lists which are too short, i.e. $\widetilde{s}_i(x)$ is $s_i(x)$ with $b_i-l_i(x)$ zeros appended. @@ -260,7 +260,7 @@ \subsection{Open subtypes} \begin{proof} \begin{enumerate}[(a)] - \item Apply \Cref{qc-open-trans} to the point $\Spec R$. + \item Apply \Cref{qc-open-trans} to the point $\Spec \A$. \item Apply the above pointwise. \end{enumerate} \end{proof} diff --git a/util/zariski.sty b/util/zariski.sty index 799e0a0b..3f5000bd 100644 --- a/util/zariski.sty +++ b/util/zariski.sty @@ -43,19 +43,6 @@ \newcommand{\Sh}{\mathrm{Sh}} \newcommand{\yo}{\mathrm{y}} -% algebra -\newcommand{\inv}{\mathrm{inv}} -\newcommand{\divides}{\mathbin{|}} -\DeclareMathOperator{\AbGroup}{Ab} -\DeclareMathOperator{\im}{im} -\DeclareMathOperator{\coker}{coker} -\newcommand{\Tors}[1]{#1\text{-}\mathrm{Tors}} -\newcommand{\Mod}[1]{#1\text{-}\mathrm{Mod}} -\newcommand{\Vect}[2]{#1\text{-}\mathrm{Vect}_{#2}} -\newcommand{\fpMod}[1]{#1\text{-}\mathrm{Mod}_{\text{fp}}} -\newcommand{\Alg}[1]{#1\text{-}\mathrm{Alg}} -\newcommand{\Sym}{\mathrm{Sym}} - % algebraic geometry \DeclareMathOperator{\Spec}{Spec} \DeclareMathOperator{\Sch}{\mathrm{Sch}_{qc}} @@ -70,6 +57,20 @@ \newcommand{\Pic}{\mathrm{Pic}} \newcommand{\Aut}{\mathrm{Aut}} +% algebra +\newcommand{\inv}{\mathrm{inv}} +\newcommand{\divides}{\mathbin{|}} +\DeclareMathOperator{\AbGroup}{Ab} +\DeclareMathOperator{\im}{im} +\DeclareMathOperator{\coker}{coker} +\newcommand{\Tors}[1]{#1\text{-}\mathrm{Tors}} +\newcommand{\Mod}[1]{#1\text{-}\mathrm{Mod}} +\newcommand{\Vect}[2]{#1\text{-}\mathrm{Vect}_{#2}} +\newcommand{\fpMod}[1]{#1\text{-}\mathrm{Mod}_{\text{fp}}} +\newcommand{\Alg}[1]{#1\text{-}\mathrm{Alg}} +\newcommand{\AAlg}{\A\text{-}\mathrm{Alg}} +\newcommand{\Sym}{\mathrm{Sym}} + % misc \newcommand{\notion}[1]{\emph{#1}\index{#1}}