A projective embedding centered at a point
OpenOAI.MaximalSeshadri.Projective.exists_centered_embeddingLet be algebraically closed, integral, and sections indexed by with iso-opens covering defining a closed immersion. There are such sections giving a closed immersion, and a point with centeredOpen t if and only if .
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 . centeredOpen s is the union of the iso-opens of .
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
noncomputable section
section
namespace MaximalSeshadri.Projective
noncomputable section
open AlgebraicGeometry CategoryTheory TopologicalSpace
open MaximalSeshadri.Frames MaximalSeshadri.Geometry MaximalSeshadri.ProjectiveBertini
attribute [local instance] MvPolynomial.gradedAlgebra
variable {K σ : Type} [Field K] [Fintype σ] {X : Scheme}
theorem exists_centered_embedding [IsIntegral X] [IsAlgClosed K] {M : X.Modules}
(k : K →+* Γ(X, ⊤)) (s : Option σ → (O X ⟶ M))
(hs : (⨆ i, SectionOpens.isoOpen (s i)) = ⊤)
[IsClosedImmersion (sectionsMorphism k s hs)] :
∃ t : Option σ → (O X ⟶ M), ∃ ht : (⨆ i, SectionOpens.isoOpen (t i)) = ⊤,
IsClosedImmersion (sectionsMorphism k t ht) ∧
∃ y : X, ∀ x : X, x ∉ centeredOpen t ↔ x = y := by
sorry
end
end MaximalSeshadri.Projective
end
end
end
end OAI