Branch orders on a surface are bounded by the curve degree
OpenOAI.MaximalSeshadri.Geometry.nodal_ideal_branch_sum_le_degreeLet be a surface with ample , an ideal sheaf with integral one-dimensional subscheme, a line bundle, a section, an affine open of dimension at most 2 with a trivialization of , in the support of , an analytic family of -points of with exact jets, generating on , near 0, . If the coefficient of is not in , then the sum of orders of on the two axes is at most where is the curve of (IntegralCurve.ofIdeal).
Notation. is curveDegree, namely . IsAmple means that for each point and open , some positive power has a global section with nonvanishing open containing , inside , and affine. 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. The Taylor maps (analyticTaylor, bivariateTaylor) send a function to the power series of at .
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.Geometry noncomputable section open AlgebraicGeometry CategoryTheory TopologicalSpace open MaximalSeshadri.ProjectiveBertini MaximalSeshadri.Projective MaximalSeshadri.Frames open MaximalSeshadri.AnalyticCoordinates MaximalSeshadri.AlgebraicJets open MaximalSeshadri.LocalComparison MaximalSeshadri.NodalLocal open scoped Topology
theorem nodal_ideal_branch_sum_le_degree (S : Surface)
(A : LineBundle S.scheme) (hA : LineBundle.IsAmple S.scheme A)
(I : S.scheme.IdealSheafData) [IsIntegral I.subscheme]
(hd : topologicalKrullDim I.subscheme = 1)
(L : LineBundle S.scheme) (s : O S.scheme ⟶ L.sheaf)
(U : S.scheme.affineOpens) (y : S.scheme) (hyU : y ∈ U.1) (hyI : y ∈ I.support)
(e : L.sheaf.restrict U.1.ι ≅ O U.1.toScheme)
(hR : ringKrullDim Γ(S.scheme,U.1) ≤ 2)
(q : letI : Algebra ℂ Γ(S.scheme,U.1) := (openScalars S.structureMap U.1).toAlgebra
(ℂ × ℂ) → (Γ(S.scheme,U.1) →ₐ[ℂ] ℂ))
(hq : ∀ t, AnalyticAt ℂ (fun z => q z t) 0)
(hjets : letI : Algebra ℂ Γ(S.scheme,U.1) := (openScalars S.structureMap U.1).toAlgebra
∀ n : ℕ,
RingHom.ker ((Ideal.Quotient.mk (IsLocalRing.maximalIdeal
(MvPowerSeries (Fin 2) ℂ)^n)).comp (analyticTaylor q hq).toRingHom) =
(RingHom.ker (q 0))^n ∧
Function.Surjective ((Ideal.Quotient.mk (IsLocalRing.maximalIdeal
(MvPowerSeries (Fin 2) ℂ)^n)).comp (analyticTaylor q hq).toRingHom))
(g : Γ(S.scheme,U.1)) (hg0 : g ≠ 0)
(hI : I.ideal U = Ideal.span {g})
(u : (ℂ × ℂ) → ℂ) (hu : AnalyticAt ℂ u 0) (hu0 : u 0 ≠ 0)
(hg : ∀ᶠ z in 𝓝 0, q z g = u z*z.1*z.2)
(hf : U.1.topIso.hom (coefficient e (restrictSection U.1.ι s)) ∉ Ideal.span {g}) :
letI : Algebra ℂ Γ(S.scheme,U.1) := (openScalars S.structureMap U.1).toAlgebra
let f := U.1.topIso.hom (coefficient e (restrictSection U.1.ι s))
(((restrictX ℂ (bivariateTaylor q hq f)).order.toNat +
(restrictZ ℂ (bivariateTaylor q hq f)).order.toNat : ℕ) : ℤ) ≤
curveDegree S L (IntegralCurve.ofIdeal S I hd) := by
sorry
end
end MaximalSeshadri.Geometry
end
end
end
end OAI