AlgebraicGeometry.RelPicard.exists_pullbackSection_thetaBundle_poincare_eq_zero_iff
Source context 13 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicGeometry.RelPicard
open _root_.JacobianVarieties.Picard.Proofs.PoincareThetaVanishing
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.GoodReductionJacobian
open _root_.AlgebraicCurve hiding genusLean source · statement
theorem exists_pullbackSection_thetaBundle_poincare_eq_zero_iff
(k : Type u) [Field k] [IsAlgClosed k] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of k))
[IsProper c] [SmoothOfRelativeDimension 1 c] [GeometricallyIntegral c]
(ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of k))) c)
(h𝔉 : ∀ m₀ : ℕ, ∃ 𝔉 : SmoothProperCurve.FiniteMapData c ε, m₀ ≤ 𝔉.m)
(J : RelativePic0Designation k c) (h : RepresentsRelSubPic c ε (algEquivZeroCut c ε) J)
(hsm : Smooth J.toBase) (hpr : IsProper J.toBase)
(g : ℕ)
(hg : ∀ (L : Type u) [Field L] [Algebra k L] (M : CurveModel k L) (e : M.C ≅ C)
(_ : e.hom ≫ c = M.toBase) (Kc : Divisor k L) (g' : ℕ),
(∀ D : Divisor k L, (ell D : ℤ) - ell (Kc - D) = Divisor.degree D + 1 - g') → g' = g)
(hg₁ : 1 ≤ g) (r : ℕ) (hr : 2 * g ≤ r) :
∃ θ : 𝟙_ J.P.Modules ⟶ thetaBundle c ε J.toBase h.poincare r (r + 1 - g),
∀ x : Over.mk (𝟙 (Spec (CommRingCat.of k))) ⟶ Over.mk J.toBase,
Scheme.Modules.pullbackSection x.left θ = 0 ↔
∀ 𝒲 : (pullback (pullback.snd c J.toBase) x.left).TwoAffineOpenCover,
Nontrivial (𝒲.sectionsOf (fibreAt c J.toBase x.left)
(fibreModule c J.toBase x.left (h.poincare.L ⊗ sectionTwist c ε J.toBase (g -
1)))).H0