Module

Exists_finiteBySections_tensorPow_thetaBundle_of_isAlgClosed.lean

Nyll.JacobianVarieties.Picard.Exists_finiteBySections_tensorPow_thetaBundle_of_isAlgClosed

1 declaration indexed from sourceView source ↗

Module documentation

Construct finite presentations by sections for powers of the theta bundle over an algebraically closed field, using its translation law and stabilizer.

Imports37

Imported by2

theorem

exists_finiteBySections_tensorPow_thetaBundle_of_isAlgClosed

L337 ↗

AlgebraicGeometry.RelPicard.exists_finiteBySections_tensorPow_thetaBundle_of_isAlgClosed

Source context 15 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicGeometry.RelPicard
open _root_.JacobianVarieties.Picard.Proofs.ThetaFiniteSections
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.GoodReductionJacobian
open _root_.AlgebraicCurve hiding genus
open scoped _root_.CategoryTheory.MonObj
attribute [local instance] MvPolynomial.gradedAlgebra

Lean source · statement

theorem exists_finiteBySections_tensorPow_thetaBundle_of_isAlgClosed
    (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) (hgc : GeometricallyConnected 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)
    (r : ℕ) (hr : 2 * g ≤ r) :
    ∃ n : ℕ,
      Scheme.Modules.FiniteBySections
          ((thetaBundle c ε J.toBase h.poincare r (r + 1 - g)).tensorPow n) J.toBase ∧
        ∀ 𝒲 : J.P.OrderedAffineCover,
          Subsingleton
            ((OModulePresheaf.ofModules J.toBase
                ((thetaBundle c ε J.toBase h.poincare r (r + 1 - g)).tensorPow n)).HSucc 𝒲 0)

Module documentation

Declarations

exists_finiteBySections_tensorPow_thetaBundle_of_isAlgClosed