Module

DivisorPicardSumsField.lean

Nyll.JacobianVarieties.Albanese.DivisorPicardSumsField

3 declarations indexed from sourceView source ↗

Module documentation

Sums on divisor Picard charts over arbitrary fields

At a field-valued test map, rigidification changes a line bundle only by a trivial line from that test field. Tensor cancellation therefore identifies the divisor line bundles from an isomorphism of their actual twists.

On a reduced family locally of finite type over any ground field, equality of sums follows by applying this comparison to points over its algebraic closure and using actual geometric point density.

Imports21

Imported by2

theorem

nonempty_rigidify_iso_over_testField

L52 ↗

JacobianVarieties.Albanese.nonempty_rigidify_iso_over_testField

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_testField
    {L : Type u} [Field L] {X : Scheme.{u}}
    (σ : Spec (CommRingCat.of L) ⟶ X) (q : X ⟶ Spec (CommRingCat.of L))
    (M : X.Modules) (hM : Scheme.Modules.IsInvertible M) :
    Nonempty (Scheme.Modules.rigidify σ q M ≅ M)

theorem

nonempty_lineBundle_iso_of_twistModule_iso_of_fieldMap

L63 ↗

JacobianVarieties.Albanese.nonempty_lineBundle_iso_of_twistModule_iso_of_fieldMap

Documentation

Over any field-valued test map, isomorphic equal-degree divisor twists give isomorphic actual divisor line bundles.

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_of_fieldMap
    {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 : ℕ}
    (L : Type u) [Field L] (s : Spec (CommRingCat.of L) ⟶ Spec (CommRingCat.of K))
    (D₀ D₁ : RelEffCartierDiv c r s)
    (e : D₀.twistModule c ε ≅ D₁.twistModule c ε) :
    Nonempty (D₀.lineBundle ≅ D₁.lineBundle)

theorem

lift_comp_eq_of_twistModule_iso_of_field

L94 ↗

JacobianVarieties.Albanese.lift_comp_eq_of_twistModule_iso_of_field

Documentation

Over every ground field, isomorphic actual divisor twists induce equal sum morphisms on any reduced family locally of finite type over that field.

Source context 10 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
open AlgebraicCurves.Geometry.Schemes.Proofs
open SchemeHomOver_ext_of_forall_algebraicClosure_point_of_isReduced_of_flat
open RigKerGeomPoints renaming ext_of_forall_geometric_point → geometricHomExt in

Lean source · statement

theorem lift_comp_eq_of_twistModule_iso_of_field
    {K : Type u} [Field 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

Sums on divisor Picard charts over arbitrary fields

Declarations

nonempty_rigidify_iso_over_testField

nonempty_lineBundle_iso_of_twistModule_iso_of_fieldMap

lift_comp_eq_of_twistModule_iso_of_field