Nonvanishing of sections on geometric fibres #
A section of an elliptic curve misses zero at a point where N is invertible if its pullback
is nonzero over every algebraically closed field in which N is invertible
(EllipticCurveGeom.left_apply_ne_zero_of_forall_isAlgClosed). This reduction is shared by the
Drinfeld–naive comparisons for full level structures and for points of exact order.
theorem
TauCeti.AlgebraicGeometry.EllipticCurveGeom.left_apply_ne_zero_of_forall_isAlgClosed
{S : AlgebraicGeometry.Scheme}
{E : EllipticCurveGeom S}
(P : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ CategoryTheory.Over.mk E.structureMap)
{s : ↥S}
{N : ℕ}
(hN : ↑N ≠ 0)
(h :
∀ (K : Type u) [inst : Field K] [IsAlgClosed K] (t : AlgebraicGeometry.Spec ↧K ⟶ S),
↑N ≠ 0 → (pointsPullback ⋯ ⋯) P ≠ 1)
:
A section misses zero on a fibre where N is invertible if its pullback is nonzero over
every algebraically closed field in which N is invertible.