Module

DivisorPicardSums.lean

Nyll.JacobianVarieties.Albanese.DivisorPicardSums

4 declarations indexed from sourceView source ↗

Module documentation

+# Sums on divisor Picard charts

Over a field, equal-degree divisor twists are isomorphic exactly when their divisor line bundles are isomorphic: rigidification contributes only a trivial line from the base and the common base-point twist cancels. Over an algebraically closed field this implies equality of the sum morphisms on reduced families.

Imports23

Imported by2

theorem

nonempty_rigidify_iso_over_field

L50 ↗

JacobianVarieties.Albanese.nonempty_rigidify_iso_over_field

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
open NeronModelInfra GoodReductionJacobian
open JacobianVarieties.Picard.Proofs.OpenChart.AlgebraicGeometry.RelPicard.ChartOne
namespace JacobianVarieties.Albanese

Lean source · statement

theorem nonempty_rigidify_iso_over_field
    {K : Type u} [Field K] {X : Scheme.{u}}
    (σ : Spec (CommRingCat.of K) ⟶ X) (q : X ⟶ Spec (CommRingCat.of K))
    (M : X.Modules) (hM : Scheme.Modules.IsInvertible M) :
    Nonempty (Scheme.Modules.rigidify σ q M ≅ M)

theorem

nonempty_lineBundle_iso_of_twistModule_iso

L61 ↗

JacobianVarieties.Albanese.nonempty_lineBundle_iso_of_twistModule_iso

Documentation

Rigidification over a field loses no line-bundle class. The common base-point twist of two degree-r divisors can then be cancelled.

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
open NeronModelInfra GoodReductionJacobian
open JacobianVarieties.Picard.Proofs.OpenChart.AlgebraicGeometry.RelPicard.ChartOne
namespace JacobianVarieties.Albanese

Lean source · statement

theorem nonempty_lineBundle_iso_of_twistModule_iso
    {K : Type u} [Field K] {C : Scheme.{u}}
    (c : C ⟶ Spec (CommRingCat.of K)) [IsSeparated c]
    [SmoothOfRelativeDimension 1 c]
    (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of K))) c) {r : ℕ}
    (D₀ D₁ : RelEffCartierDiv c r (𝟙 (Spec (CommRingCat.of K))))
    (e : D₀.twistModule c ε ≅ D₁.twistModule c ε) :
    Nonempty (D₀.lineBundle ≅ D₁.lineBundle)

theorem

lift_pullbackAlong

L83 ↗

JacobianVarieties.Albanese.lift_pullbackAlong

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
open NeronModelInfra GoodReductionJacobian
open JacobianVarieties.Picard.Proofs.OpenChart.AlgebraicGeometry.RelPicard.ChartOne
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

theorem

lift_comp_eq_of_twistModule_iso

L99 ↗

JacobianVarieties.Albanese.lift_comp_eq_of_twistModule_iso

Documentation

On a reduced family over an algebraically closed field, two equal-degree divisors with isomorphic actual twists have the same sum morphism.

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
open NeronModelInfra GoodReductionJacobian
open JacobianVarieties.Picard.Proofs.OpenChart.AlgebraicGeometry.RelPicard.ChartOne
namespace JacobianVarieties.Albanese

Lean source · statement

theorem lift_comp_eq_of_twistModule_iso
    {K : Type u} [Field K] [IsAlgClosed K] {C B Y T : Scheme.{u}}
    (c : C ⟶ Spec (CommRingCat.of K)) [IsProper c]
    [SmoothOfRelativeDimension 1 c] [GeometricallyIntegral c]
    (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of K))) c)
    {r : ℕ} {y : Y ⟶ Spec (CommRingCat.of K)}
    {U : RelEffCartierDiv c r y} (hU : U.IsUniversal)
    {b : B ⟶ Spec (CommRingCat.of K)} [Smooth b] [IsProper b]
    [GeometricallyIntegral b] (G : RelativeGroupLaw K b) (sum : SchemeHomOver y b)
    (t : T ⟶ Spec (CommRingCat.of K)) [LocallyOfFiniteType t] [IsReduced T]
    (D₀ D₁ : RelEffCartierDiv c r t)
    (e : D₀.twistModule c ε ≅ D₁.twistModule c ε) :
    hU.lift D₀ ≫ sum.1 = hU.lift D₁ ≫ sum.1

Module documentation

Declarations

nonempty_rigidify_iso_over_field

nonempty_lineBundle_iso_of_twistModule_iso

lift_pullbackAlong

lift_comp_eq_of_twistModule_iso