Definitions/Def_AlgebraicGeometry_FppfAmitsurTrivial.lean

For an fppf sheaf F of abelian groups on the big fppf site of schemes (an object of Sheaf Scheme.fppfTopology AddCommGrpCat) and a commutative ring A, AlgebraicGeometry.Scheme.FppfAmitsurTrivial F A asserts the vanishing of the first cohomology of the one-step Amitsur (Čech) complex attached to the single ring map \mathbb Z \to A. The rings and face maps are those of the descent-coface package instantiated at \mathbb Z \to A: R_2 = A \otimes_{\mathbb Z} A and R_3 = A \otimes_{\mathbb Z} (A \otimes_{\mathbb Z} A), with i_1, i_2 \colon A \to R_2 given by a \mapsto a \otimes 1 and a \mapsto 1 \otimes a, and c_{12}, c_{23}, c_{13} \colon R_2 \to R_3 given on generators by x \otimes y \mapsto x \otimes (y \otimes 1), x \otimes y \mapsto 1 \otimes (x \otimes y) and x \otimes y \mapsto x \otimes (1 \otimes y). Applying \mathrm{Spec} and passing to the opposite category turns each of these into a restriction map on sections of the presheaf underlying F. The predicate then says: for every section c of F over \mathrm{Spec}(A \otimes_{\mathbb Z} A) satisfying the additively written cocycle identity c_{12}^{*}c + c_{23}^{*}c = c_{13}^{*}c in F(\mathrm{Spec}\,R_3), there is a section b of F over \mathrm{Spec}\,A with c = i_1^{*}b - i_2^{*}b; that is, every 1-cocycle is a coboundary, with this sign convention. No flatness, finite presentation or faithfulness hypothesis on \mathbb Z \to A is imposed in the definition: the predicate is stated for an arbitrary commutative ring A, and is a condition on the chosen presentation \mathbb Z \to A rather than on a covering family of \mathrm{Spec}\,\mathbb Z. The sheaf F enters only through its underlying presheaf of abelian groups evaluated on affine schemes.