Module

AlbaneseChartGlue.lean

Nyll.JacobianVarieties.Albanese.AlbaneseChartGlue

5 declarations indexed from sourceView source ↗

Module documentation

Gluing the actual divisor sums on Picard charts

Riemann--Roch supplies a finite open cover of the Picard scheme by families of effective divisors of a common degree. Their sum morphisms agree on the actual overlaps, since their twists are restrictions of the same Poincare bundle. The resulting morphism has a calculation rule on every reduced family.

Imports26

Imported by2

theorem

exists_universal_over_field

L64 ↗

JacobianVarieties.Albanese.exists_universal_over_field

Source context 8 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
open JacobianVarieties.Picard.Proofs.ClosedFieldRepresentation
namespace JacobianVarieties.Albanese

Lean source · statement

theorem exists_universal_over_field
    {K : Type u} [Field K] {C : Scheme.{u}}
    (c : C ⟶ Spec (CommRingCat.of K)) [IsProper c]
    [SmoothOfRelativeDimension 1 c] [GeometricallyIntegral c] (r : ℕ) :
    ∃ (Y : Scheme.{u}) (y : Y ⟶ Spec (CommRingCat.of K))
      (U : RelEffCartierDiv c r y), U.IsUniversal

theorem

lift_pullbackAlong

L94 ↗

JacobianVarieties.Albanese.lift_pullbackAlong

Source context 8 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
open JacobianVarieties.Picard.Proofs.ClosedFieldRepresentation
namespace JacobianVarieties.Albanese

Lean source · statement

theorem lift_pullbackAlong
    {C S Y T T' : Scheme.{u}} {c : C ⟶ S} {r : ℕ}
    {y : Y ⟶ S} {U : RelEffCartierDiv c r y} (hU : U.IsUniversal)
    {g : T ⟶ S} (D : RelEffCartierDiv c r g)
    {g' : T' ⟶ S} (φ : T' ⟶ T) (hφ : φ ≫ g = g') :
    hU.lift (D.pullbackAlong φ hφ) = φ ≫ hU.lift D

def

pullback_twist_iso

L108 ↗

JacobianVarieties.Albanese.pullback_twist_iso

Source context 8 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
open JacobianVarieties.Picard.Proofs.ClosedFieldRepresentation
namespace JacobianVarieties.Albanese

Lean source · statement

def pullback_twist_iso
    {K : Type u} [Field K] {C P T T' : Scheme.{u}}
    (c : C ⟶ Spec (CommRingCat.of K)) [IsSeparated c]
    [SmoothOfRelativeDimension 1 c]
    (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of K))) c)
    {p : P ⟶ Spec (CommRingCat.of K)} (L : RigidifiedLineBundle c ε p)
    {t : T ⟶ Spec (CommRingCat.of K)} (a : SchemeHomOver t p)
    {r : ℕ} (D : RelEffCartierDiv c r t)
    (e : D.twistModule c ε ≅ (L.pullbackAlong a).L)
    {t' : T' ⟶ Spec (CommRingCat.of K)} (v : SchemeHomOver t' t) :
    (D.pullbackAlong v.1 v.2).twistModule c ε ≅
      (L.pullbackAlong (postComp a v)).L

theorem

exists_divisor_charts

L124 ↗

JacobianVarieties.Albanese.exists_divisor_charts

Source context 8 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
open JacobianVarieties.Picard.Proofs.ClosedFieldRepresentation
namespace JacobianVarieties.Albanese

Lean source · statement

theorem exists_divisor_charts
    {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)
    {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_divisorSum_glue

L181 ↗

JacobianVarieties.Albanese.exists_divisorSum_glue

Documentation

The sums of the actual effective divisors glue to a morphism on the Picard scheme. Its value is computed by the same universal degree-r divisor on every reduced finite-type family whose twist is the indicated Poincare pullback.

Source context 8 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
open JacobianVarieties.Picard.Proofs.ClosedFieldRepresentation
namespace JacobianVarieties.Albanese

Lean source · statement

theorem exists_divisorSum_glue
    {K : Type u} [Field K] [IsAlgClosed K] {C B : Scheme.{u}}
    (c : C ⟶ Spec (CommRingCat.of K)) [IsProper c]
    [SmoothOfRelativeDimension 1 c] [GeometricallyIntegral c]
    (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of K))) c)
    {P : RelativePic0Designation K c} [LocallyOfFiniteType P.toBase] [IsReduced P.P]
    (h : RepresentsRelSubPic c ε (algEquivZeroCut c ε) P)
    {b : B ⟶ Spec (CommRingCat.of K)} [Smooth b] [IsProper b]
    [GeometricallyIntegral b] (G : RelativeGroupLaw K b) (q : SchemeHomOver c b) :
    ∃ (r : ℕ) (_ : 0 < r) (Y : Scheme.{u}) (y : Y ⟶ Spec (CommRingCat.of K))
      (U : RelEffCartierDiv c r y) (hU : U.IsUniversal)
      (σ : finFibrePow c r ⟶ Y) (hσ : σ ≫ y = finFibrePow.toBase c r)
      (sum : SchemeHomOver y b) (ψ : SchemeHomOver P.toBase b),
      U.I.comap (mapOnProdOver c σ hσ) = fibrePowOver.tautIdeal c r ∧
      σ ≫ sum.1 = (G.finiteSumMap c q r).1 ∧
      ∀ (T : Scheme.{u}) (t : T ⟶ Spec (CommRingCat.of K))
        [LocallyOfFiniteType t] [IsReduced T] (D : RelEffCartierDiv c r t)
        (a : SchemeHomOver t P.toBase),
        Nonempty (D.twistModule c ε ≅ (h.poincare.pullbackAlong a).L) →
          a.1 ≫ ψ.1 = hU.lift D ≫ sum.1

Module documentation

Gluing the actual divisor sums on Picard charts

Declarations

exists_universal_over_field

lift_pullbackAlong

pullback_twist_iso

exists_divisor_charts

exists_divisorSum_glue