Division of a section vanishing on a curve
OpenOAI.MaximalSeshadri.Geometry.IntegralCurve.divide_sectionLet be an integral curve on , presenting the ideal of on (pullback along the identity), and a section of a line bundle whose pullback to vanishes. Then there is a unique section of with .
Notation. PresentsPullbackIdeal I f J ι says that is a monomorphism whose image on affine opens is the extension of along . A Surface is an integral scheme smooth of relative dimension 2 over with a closed immersion into some complex projective space over . An IntegralCurve on a surface is an integral closed subscheme of topological Krull dimension one, given by a closed immersion.
Formalization Note The statement is verbatim from OpenAI's Lean development, with Definitions files of this development imported in place of the upstream modules; these are supporting code for the statement.
import Mathlib
import Definitions.Def_MaximalSeshadriConstants
import Definitions.Def_SeshadriPrelim6
namespace OAI
section
namespace MaximalSeshadri.Geometry
noncomputable section
open AlgebraicGeometry CategoryTheory TopologicalSpace
open MaximalSeshadri.Frames MaximalSeshadri.Projective MaximalSeshadri.ProjectiveBertini
variable {X Y : Scheme.{0}}
theorem IntegralCurve.divide_section (S : Surface) (C : IntegralCurve S)
(J M : LineBundle S.scheme) (ι : J.sheaf ⟶ O S.scheme)
(hJ : PresentsPullbackIdeal C.embedding.ker (𝟙 S.scheme) J ι)
(s : O S.scheme ⟶ M.sheaf) (hs : pullbackSection C.embedding s = 0) :
∃! q : O S.scheme ⟶ (J.tensor M).sheaf, q ≫ tensorInclusion J M ι = s := by
sorry
end
end MaximalSeshadri.Geometry
end
end OAI