A smooth integral Cartier section from local coordinates

Open

OAI.MaximalSeshadri.ProjectiveBertini.exists_smooth_integral_cartier_section_of_local_coordinates

by wurtle · Nov 4, 2026 · Mathlib 0df444a (Lean v4.33.1)

maximal-seshadrioai-math

Let $K$ be uncountable algebraically closed of characteristic zero, $X$ integral compact and smooth of relative dimension 2 over $K$ , $h$ = sectionsMorphism k s hs to a projective space, compatible with $X\to\operatorname{Spec}K$ , such that locally $\Gamma(V)$ is a surjective image of a coordinate chart ring. For every nonzero polynomial $q$ there is $t$ with $q(t)\ne0$ such that the hyperplane section projectiveHyperplane h t has integral subscheme, smooth over $K$ , and is locally generated by a regular element equal to the coefficient of $\sum_jk(t_j)s_j$ in a frame of $M$ .

Notation. The iso-open of $s$ (SectionOpens.isoOpen s) is the union of the opens on which the morphism $s$ restricts to an isomorphism. sectionsMorphism k s hs is the morphism from $X$ to $\operatorname{Proj}$ of the graded polynomial ring in variables indexed by the sections, defined by sections whose iso-opens cover $X$ , with $k$ the ring map from the base into $\Gamma(X,\top)$ .

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.

Preamble

import Mathlib
import Definitions.Def_MaximalSeshadriConstants
import Definitions.Def_SeshadriPrelim6

namespace OAI

section
noncomputable section

section

namespace MaximalSeshadri.ProjectiveBertini
noncomputable section
open AlgebraicGeometry CategoryTheory TopologicalSpace
open MaximalSeshadri.Projective MaximalSeshadri.BertiniIntegral MaximalSeshadri.Frames
attribute [local instance] MvPolynomial.gradedAlgebra

Formal statement

theorem exists_smooth_integral_cartier_section_of_local_coordinates
    {K : Type} [Field K] [CharZero K] [IsAlgClosed K] [Uncountable K]
    {n : ℕ} (X : Scheme) [IsIntegral X] [CompactSpace X]
    (g : X ⟶ Spec (CommRingCat.of K)) [SmoothOfRelativeDimension 2 g]
    (M : X.Modules) (k : K →+* Γ(X, ⊤))
    (s : Option (Fin n) → (O X ⟶ M))
    (hs : (⨆ i, SectionOpens.isoOpen (s i)) = ⊤)
    (h : X ⟶ Proj (PolyGrade K (Option (Fin n))))
    (hh : h = sectionsMorphism k s hs)
    (hbase : h ≫ projectiveToSpec = g)
    (hlocal : ∀ x : X, ∃ i : Option (Fin n), ∃ V : X.affineOpens, x ∈ V.1 ∧
      ∃ φ : PolyChart (R := K) i →+* Γ(X, V.1), Function.Surjective φ ∧
        Spec.map (CommRingCat.ofHom φ) ≫
          Proj.awayι (PolyGrade K (Option (Fin n))) (MvPolynomial.X i) (poly_X_mem i) (by decide) =
            V.2.fromSpec ≫ h)
    (q : MvPolynomial (Option (Fin n)) K) (hq : q ≠ 0) :
    ∃ t : Option (Fin n) → K, MvPolynomial.aeval t q ≠ 0 ∧
      IsIntegral (projectiveHyperplane h t).subscheme ∧
      Smooth ((projectiveHyperplane h t).subschemeι ≫ g) ∧
      ∀ x : X, ∃ U : X.affineOpens, x ∈ U.1 ∧ ∃ r : Γ(X, U.1),
        IsRegular r ∧ (projectiveHyperplane h t).ideal U = Ideal.span {r} ∧
        ∃ e : M.restrict U.1.ι ≅ O U.1.toScheme,
          U.1.topIso.hom (coefficient e (restrictSection U.1.ι
            (sectionCombination k s t))) = r := by
  sorry

end
end MaximalSeshadri.ProjectiveBertini
end
end
end
end OAI

Source

OpenAI, Maximal Seshadri constants on arbitrary polarized surfaces, September 23, 2026, https://github.com/openai/math (paper: preprints/Maximal-Seshadri-Constants-on-Arbitrary-Polarized-Surfaces-September-23-2026/main.pdf; Lean: lean/OAI/AlgebraicGeometry/Seshadri, Apache License 2.0); Lean declaration `OAI.MaximalSeshadri.ProjectiveBertini.exists_smooth_integral_cartier_section_of_local_coordinates`, https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/AlgebraicGeometry/Seshadri/Projective/LocalBertiniSection.lean#L22

View graph