Module

SeparableDivisorCharts.lean

Nyll.JacobianVarieties.Albanese.SeparableDivisorCharts

2 declarations indexed from sourceView source ↗

Module documentation

Effective-divisor charts after a finite separable extension

Actual chart sections give cohomology-vanishing opens which cover the represented Picard scheme. On each open, an actual effective divisor of a common positive degree has normalized line bundle equal to the Poincare restriction.

Imports15

Imported by2

theorem

exists_divisor_charts

L52 ↗

JacobianVarieties.Albanese.exists_divisor_charts

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory
open AlgebraicGeometry AlgebraicGeometry.RelPicard AlgebraicGeometry.SmoothProperCurve
open NeronModelInfra GoodReductionJacobian
open JacobianVarieties.Picard.Proofs.OpenChart.AlgebraicGeometry.RelPicard.ChartOne
namespace JacobianVarieties.Albanese

Lean source · statement

theorem exists_divisor_charts
    {K : Type u} [Field K] {C : Scheme.{u}}
    (c : C ⟶ Spec (CommRingCat.of K)) [IsProper c]
    [SmoothOfRelativeDimension 1 c] [GeometricallyIntegral c]
    (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of K))) c)
    (n g r : ℕ) (hgr : 2 * g < r)
    (γ : Fin n → Fin (r - g) → SchemeHomOver (𝟙 (Spec (CommRingCat.of K))) c)
    (hγ : HasChartSections c γ)
    {P : RelativePic0Designation K c} [LocallyOfFiniteType P.toBase]
    (h : RepresentsRelSubPic c ε (algEquivZeroCut c ε) P) :
    ∃ (r : ℕ), 0 < r ∧ ∃ (n : ℕ) (V : Fin n → P.P.Opens),
      TopologicalSpace.IsOpenCover V ∧
      ∀ i : Fin n, ∃ E : RelEffCartierDiv c r ((V i).ι ≫ P.toBase),
        Nonempty (E.twistModule c ε ≅
          (h.poincare.pullbackAlong (⟨(V i).ι, rfl⟩ :
            SchemeHomOver ((V i).ι ≫ P.toBase) P.toBase)).L)

theorem

exists_finite_separable_divisor_charts

L114 ↗

JacobianVarieties.Albanese.exists_finite_separable_divisor_charts

Documentation

Over a finite separable field extension, the Picard scheme has a finite open cover whose Poincare bundle is represented by actual effective divisors of one common positive degree. The extension is constructed from the curve.