Diagonal is identity correspondence

Yep!

weil.tex

@@ -642,14 +642,62 @@ \section{Correspondences}
 \end{example}
 
 \begin{lemma}
-\label{lemma-identity-correspondence}
-Let $X$ be a smooth projective scheme over $k$. Consider the diagonal
-$\Delta \subset X \times X$ of $X$. The class of $\Delta$ is an
-unit element of the graded algebra $\text{Corr}^*(X, X)$.
+\label{lemma-category-correspondences}
+Smooth projective schemes over $k$ with correspondences and composition
+of correspondences as defined above form a graded category over
+$\mathbf{Q}$
+(Differential Graded Algebra, Definition \ref{dga-definition-graded-category}).
 \end{lemma}
 
 \begin{proof}
-Omitted.
+Everything is clear from the construction and
+Lemma \ref{lemma-composition-correspondences}
+except for the existence of identity morphisms.
+Given a smooth projective scheme $X$ consider
+the class $[\Delta]$ of the diagonal $\Delta \subset X \times X$
+in $\text{Corr}^0(X, X)$. We note that $\Delta$ is
+equal to the graph of the identity $\text{id}_X : X \to X$
+which is a fact we will use below.
+
+\medskip\noindent
+To prove that $[\Delta]$ can serve as an identity we have to show that
+$[\Delta] \circ c = c$ and $c' \circ [\Delta] = c'$ for any correspondences
+$c \in \text{Corr}^r(Y, X)$ and $c' \in \text{Corr}^s(X, Y)$.
+For the second case we have to show that
+$$
+c' = \text{pr}_{13, *}(\text{pr}_{12}^*[\Delta] \cdot \text{pr}_{23}^*c')
+$$
+where $\text{pr}_{12} : X \times X \times Y \to X \times X$ is the
+projection and simlarly for $\text{pr}_{13}$ and $\text{pr}_{23}$.
+We may write $c' = \sum a_i [Z_i]$ for some integral closed subschemes
+$Z_i \subset X \times Y$ and rational numers $a_i$. Thus it clearly
+suffices to show that
+$$
+[Z] = \text{pr}_{13, *}(\text{pr}_{12}^*[\Delta] \cdot \text{pr}_{23}^*[Z])
+$$
+in the chow group of $X \times Y$. After replacing $X$ and $Y$ by the
+irreducible component containing the image of $X$ under the two projections
+we may assume $X$ and $Y$ are integral as well. Then we have to show
+$$
+[Z] = \text{pr}_{13, *}([\Delta \times Y] \cdot [X \times Z])
+$$
+Denote $Z' \subset X \times X \times Y$ the image of $Z$ by the morphism
+$(\Delta, 1) : X \times Y \to X \times X \times Y$. Then $Z'$
+is a closed subscheme of $X \times X \times Y$ isomorphic to $Z$ and
+$Z' = \Delta \times Y \cap X \times Z$ scheme theoretically.
+By Chow Homology, Lemma \ref{chow-lemma-intersect-properly}\footnote{The
+reader verifies that $\dim(Z') = \dim(\Delta \times Y) + \dim(X \times Z) -
+\dim(X \times X \times Y)$ and that $Z'$ has a unique generic point
+mapping to the generic point of $Z$ (where the local ring is CM)
+and to some point of $X$ (where the local ring is CM). Thus all the
+hypothese of the lemma are indeed verified.}
+we conclude that
+$$
+[Z'] = [\Delta \times Y] \cdot [X \times Z]
+$$
+Since $Z'$ maps isomorphically to $Z$ by $\text{pr}_{13}$ also
+we conclude. The verification that
+$[\Delta] \circ c = c$ is similar and we omit it.
 \end{proof}
 
 \begin{lemma}
@@ -661,10 +709,30 @@ \section{Correspondences}
 \end{lemma}
 
 \begin{proof}
-To see this we have to show if $g : Z \to Y$ is another morphism of
-smooth projective schemes over $k$, then we have
-$[\Gamma_g] \circ [\Gamma_f] = [\Gamma_{g \circ f}]$ in
-$\text{Corr}^0(X, Z)$. Details omitted.
+In the proof of Lemma \ref{lemma-category-correspondences}
+we have seen that this construction sends identities to
+identities. To finish the proof we have to show if $g : Z \to Y$
+is another morphism of smooth projective schemes over $k$, then we have
+$[\Gamma_g] \circ [\Gamma_f] = [\Gamma_{f \circ g}]$ in
+$\text{Corr}^0(X, Z)$. Arguing as in the proof of
+Lemma \ref{lemma-category-correspondences} we see that it
+suffices to show
+$$
+[\Gamma_{f \circ g}] =
+\text{pr}_{13, *}([\Gamma_f \times Z] \cdot [X \times \Gamma_g])
+$$
+in $\CH^*(X \times Z)$ when $X$, $Y$, $Z$ are integral.
+Denote $Z' \subset X \times Y \times Z$ the image of the closed immersion
+$(f \circ g, g, 1) : Z \to X \times Y \times Z$.
+Then $Z' = \Gamma_f \times Z \cap X \times \Gamma_g$
+scheme theoretically and we conclude using
+Chow Homology, Lemma \ref{chow-lemma-intersect-properly}
+that
+$$
+[Z'] = [\Gamma_f \times Z] \cdot [X \times \Gamma_g]
+$$
+Since it is clear that $\text{pr}_{13, *}([Z']) = [\Gamma_{f \circ g}]$
+the proof is complete.
 \end{proof}
 
 \begin{remark}