Finiteness of the cokernel on the triple overlap
OpenOAI.MaximalSeshadri.Projective.finite_plane_cokernelLet be separated with sections defining a finite morphism to the plane as above. For a line bundle , the quotient of the sections over the triple overlap by the sum of images of sections over the three double overlaps (tripleBaseImage) is finite-dimensional over .
Notation. The iso-open of (SectionOpens.isoOpen s) is the union of the opens on which the morphism restricts to an isomorphism. sectionsMorphism k s hs is the morphism from to of the graded polynomial ring in variables indexed by the sections, defined by sections whose iso-opens cover , with the ring map from the base into .
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.Projective
noncomputable section
open AlgebraicGeometry CategoryTheory TopologicalSpace
open MaximalSeshadri.Frames MaximalSeshadri.Geometry MaximalSeshadri.Geometry.BaseSections
variable {K : Type} [Field K] {X : Scheme.{0}} {M : X.Modules}
theorem finite_plane_cokernel [X.IsSeparated] (k : K →+* Γ(X,⊤))
(s : Fin 3 → (O X ⟶ M)) (hs : (⨆ i, SectionOpens.isoOpen (s i)) = ⊤)
[IsFinite (sectionsMorphism k s hs)] (L : LineBundle X) :
Module.Finite K (Sections k L.sheaf (planeTriple s) ⧸
tripleBaseImage k L.sheaf (SectionOpens.isoOpen (s 1))
(SectionOpens.isoOpen (s 2)) (SectionOpens.isoOpen (s 0))) := by
sorry
end
end MaximalSeshadri.Projective
end
end OAI