Definitions/Def_AlgebraicGeometry_TwoGluedCurvesNodeUnitModule.lean

Throughout, \kappa is a field, x\colon X\to\operatorname{Spec}\kappa is a \kappa-scheme, c_1\colon C_1\to\operatorname{Spec}\kappa and c_2\colon C_2\to\operatorname{Spec}\kappa are \kappa-schemes equipped with morphisms over \kappa, i_1\colon C_1\to X and i_2\colon C_2\to X (elements of the project's SchemeHomOver, i.e. morphisms together with a proof of commutation over \operatorname{Spec}\kappa), together with families p_1,p_2 indexed by a type \iota of sections of c_1, resp. c_2, over \operatorname{Spec}\kappa, and a \kappa-scheme h\colon T\to\operatorname{Spec}\kappa.

nodeSectionFst and nodeSectionSnd are the sections T\to C_1\times_\kappa T and T\to C_2\times_\kappa T obtained from p_1 j, p_2 j by the project's rigSection, namely the morphism with components h followed by the given \kappa-point and \mathrm{id}_T. For an open W of X\times_\kappa T, nodeLocus is the open subset of T on which both j-th node sections land in the preimage of W under the base-changed maps \mathrm{curveChange}, i.e. i_1\times\mathrm{id}_T and i_2\times\mathrm{id}_T. Given units u_j\in\Gamma(T,\mathcal O_T)^\times, NodeCondition asserts, for sections f over (i_1\times\mathrm{id}_T)^{-1}W and g over (i_2\times\mathrm{id}_T)^{-1}W, the equality \sigma^{1*}_j f = u_j\cdot\sigma^{2*}_j g of sections over that node locus, all three terms being restricted there.

IsNodeUnitModule u M, for M a sheaf of modules on X\times_\kappa T, is the predicate: there exist morphisms j_1\colon M\to (i_1\times\mathrm{id}_T)_*\mathcal O and j_2\colon M\to (i_2\times\mathrm{id}_T)_*\mathcal O into the pushforwards of the unit sheaves of modules such that, for every open W, the map m\mapsto (j_1 m,\,j_2 m) on sections over W is injective with image exactly the pairs satisfying the node condition at every j\in\iota. It is thus a condition on a presentation of M as the fibre product of the two component structure sheaves along the prescribed gluing units, not a construction of such an M.