Definitions/Def_WeierstrassCurve_DrinfeldBasisRelative.lean

Fix a commutative ring R and a projective Weierstrass curve V over R, with its graded Proj model E = projModelCR V and structure morphism f = projModelStrCR V to \operatorname{Spec} R, and let G be a RelativeGroupLaw for f: a choice, for every T \to \operatorname{Spec} R, of group operations on the set of T-points of f, with associativity, unit and inverse axioms and naturality of multiplication under base change along T' \to T. For a test morphism t : T \to \operatorname{Spec} R and T-points P, Q of f, linCombOver is the point aP + bQ, formed from the iterated multiplications G.\mathrm{nsmul} (repeated multiplication by P resp. Q starting from the unit point). Given q, basisTupleOver is the family of q^2 underlying morphisms T \to E indexed by i \in \mathrm{Fin}(q\cdot q) obtained from the coefficient pair (\lfloor i/q\rfloor, i \bmod q), and basisTupleOver_over records that each of these lies over t. Then basisDivisorOver is the product, over these q^2 indices, of the kernel ideal sheaves of the graphs T \to E \times_{\operatorname{Spec} R} T of the points, i.e. the ideal sheaf of the effective divisor \sum_{a,b<q} [aP+bQ] on E \times_{\operatorname{Spec} R} T. Independently of P,Q, torsionIdealOver is the kernel ideal sheaf, on E, of the first projection of the fibre product of the scheme-level multiplication-by-q morphism G.schemeNsmul q with the unit section, pulled back (comap) along E \times_{\operatorname{Spec} R} T \to E. Finally IsDrinfeldBasisOver is the predicate asserting the equality of these two ideal sheaves on E \times_{\operatorname{Spec} R} T.