Definitions/Def_AlgebraicGeometry_CoherentBaseChangeFamily.lean

Fix a scheme T. The structure CoherentBaseChange.FibreH0Family T packages the following data. First, for every open U \subseteq T together with a proof that U is affine, a two-term complex G U hU of modules over the ring of sections \Gamma(T, U): by the definition of TwoTermComplex, this consists of two finite free \Gamma(T,U)-modules C_0, C_1 and a \Gamma(T,U)-linear map d \colon C_0 \to C_1. Second, a function h^0 \colon T \to \mathbb{N} on the points of the underlying space. Third, a compatibility field: for every affine open U, every proof hU of its affineness and every point t \in U, the value h^0(t) equals (G U hU).fibreH0 evaluated at the prime of \Gamma(T,U) corresponding to t (Mathlib's IsAffineOpen.primeIdealOf). Here fibreH0 of a two-term complex at a prime \mathfrak{p} is, by definition, the dimension over the residue field \kappa(\mathfrak{p}) of the kernel of the base-changed map d \otimes \kappa(\mathfrak{p}).

So the structure is indexed by presentations — an affine open together with a chosen affineness proof — and the third field is a theorem carried as data: it asserts that the fibrewise kernel dimension computed from any one of these complexes agrees with the single global function h^0, hence in particular is independent of the affine open and of the complex chosen over it. The ambient module also provides, for a two-term complex, the fibre dimension fibreH1 of the cokernel of d \otimes \kappa(\mathfrak{p}), the integer \chi = \operatorname{rank} C_0 - \operatorname{rank} C_1, the kernel H0 A of d \otimes A for an R-algebra A, and the natural A-linear comparison map A \otimes_R \ker d \to \ker(d \otimes A).