Definitions/Def_AlgebraicGeometry_TwoGluedProjectiveLinesNodeUnitModule.lean

Throughout, \kappa is an algebraically closed field, x : X \to \operatorname{Spec}\kappa a \kappa-scheme, and M_1, M_2 are objects of CurveModel κ (RatFunc κ): smooth proper integral curves over \kappa equipped with an identification of their function field with \kappa(t) under which closed points correspond bijectively to the places of \kappa(t)/\kappa. They are mapped into X by i_1, i_2, compatibly with the structure morphisms (i_1 followed by x equals M_1.\mathrm{toBase}, and likewise for i_2); a, b : \mathrm{Fin}\,s \to \kappa^{\times} record the gluing parameters, and h : T \to \operatorname{Spec}\kappa is a further base.

For c \in \kappa, pointAt M c is the section of M.\mathrm{toBase} corresponding, under the bijection pointEquivPlace between \kappa-points and places, to the place of \kappa(t) cut out by t - c. nodeSectionFst and nodeSectionSnd are the resulting constant sections T \to M_1.C \times_\kappa T and T \to M_2.C \times_\kappa T at the points a_i and b_i (given by rigSection: first component T \to \operatorname{Spec}\kappa \to M_j.C, second the identity of T). For an open W of X \times_\kappa T, nodeLocus i W is the open subset of T on which both node sections land in the preimage of W under the respective morphisms i_j \times \mathrm{id}_T (curveChange), namely the intersection of the two preimages.

Given units u_i \in \Gamma(T,\mathcal O_T)^{\times}, sections f over (i_1\times \mathrm{id}_T)^{-1}W and g over (i_2\times \mathrm{id}_T)^{-1}W, NodeCondition asserts the equality, on nodeLocus i W, of the pullback of f along the i-th first node section with u_i (restricted from \Gamma(T,\top)) times the pullback of g along the i-th second node section. Finally, IsNodeUnitModule u M, for a sheaf of modules M on X \times_\kappa T, asserts the existence of maps j_1, j_2 from M to the pushforwards along i_1\times\mathrm{id}_T and i_2\times\mathrm{id}_T of the respective unit (structure-sheaf) modules such that, for every open W, the map m \mapsto (j_1 m, j_2 m) on \Gamma(M,W) is injective and its image is exactly the set of pairs satisfying NodeCondition for all i. Thus the predicate characterises M as the sheaf of pairs of functions on the two components agreeing at each node up to the unit u_i; it is a condition on a given M, stated section-wise, with no invertibility of M demanded.