Bertini for the double-point quartics

Open

OAI.MaximalSeshadri.Projective.doublePointQuartics_bertini

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

maximal-seshadrioai-math

Let $K$ be uncountable algebraically closed of characteristic zero, $g:X\to\operatorname{Spec}K$ , and $s$ sections indexed by $\operatorname{Option}\sigma$ defining a closed immersion, with centeredOpen s integral, compact, smooth of relative dimension 2 over $K$ . Let $e$ be an equivalence from $\operatorname{Option}(\operatorname{Fin}n)$ to QuarticIndex σ. For every nonzero $P$ there is $v$ with $P(v)\neq0$ such that on the centered open $V$ , the hyperplane section for the morphism defined by the restricted quartics has integral subscheme, smooth over $K$ , and is locally generated by a regular element equal to the coefficient of the combination.

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)$ . centeredOpen s is the union of the iso-opens of $s_{\mathrm{some}\,i}$ . QuarticIndex σ is $\sigma\times\sigma\times\operatorname{Option}\sigma\times\operatorname{Option}\sigma$ ; doublePointQuartics are the corresponding degree-4 mixed products of the sections.

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.Projective
noncomputable section
open AlgebraicGeometry CategoryTheory TopologicalSpace MvPolynomial
open MaximalSeshadri.Frames MaximalSeshadri.Geometry MaximalSeshadri.BertiniIntegral
attribute [local instance] MvPolynomial.gradedAlgebra

variable {K σ : Type} [Field K] [CharZero K] [IsAlgClosed K] [Uncountable K]

Formal statement

theorem doublePointQuartics_bertini {X : Scheme} {M : X.Modules}
    (g : X ⟶ Spec (CommRingCat.of K))
    (s : Option σ → (O X ⟶ M))
    (hs : (⨆ i, SectionOpens.isoOpen (s i)) = ⊤)
    [IsClosedImmersion (sectionsMorphism
      (g.appTop.hom.comp (Scheme.ΓSpecIso (CommRingCat.of K)).inv.hom) s hs)]
    {n : ℕ} (e : Option (Fin n) ≃ QuarticIndex σ)
    [IsIntegral (centeredOpen s).toScheme] [CompactSpace (centeredOpen s)]
    [SmoothOfRelativeDimension 2 ((centeredOpen s).ι ≫ g)]
    (P : MvPolynomial (Option (Fin n)) K) (hP : P ≠ 0) :
    let k := g.appTop.hom.comp (Scheme.ΓSpecIso (CommRingCat.of K)).inv.hom
    let V := centeredOpen s
    let t (j : Option σ) := restrictSection V.ι (s j)
    let q := (doublePointQuartics t) ∘ e
    let hq := sections_cover_reindex _ (doublePointQuartics_cover t (restricted_centered_cover s)) e
    let h := sectionsMorphism (V.ι.appTop.hom.comp k) q hq
    ∃ v : Option (Fin n) → K, MvPolynomial.aeval v P ≠ 0 ∧
      IsIntegral (projectiveHyperplane h v).subscheme ∧
      Smooth ((projectiveHyperplane h v).subschemeι ≫ V.ι ≫ g) ∧
      ∀ x : V, ∃ U : V.toScheme.affineOpens, x ∈ U.1 ∧
        ∃ f : Γ(V.toScheme, U.1), IsRegular f ∧
          (projectiveHyperplane h v).ideal U = Ideal.span {f} ∧
          ∃ b : (modulePow V.toScheme (M.restrict V.ι) 4).restrict U.1.ι ≅ O U.1.toScheme,
            U.1.topIso.hom (coefficient b (restrictSection U.1.ι
              (sectionCombination (V.ι.appTop.hom.comp k) q v))) = f := by
  sorry

end
end MaximalSeshadri.Projective
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.Projective.doublePointQuartics_bertini`, https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/AlgebraicGeometry/Seshadri/Projective/QuarticBertini.lean#L22

View graph