NYLL
Module

LineBundleSumInvariance.lean

Nyll.JacobianVarieties.Albanese.LineBundleSumInvariance
9 declarations indexed from sourceView source ↗

Module documentation

+# Finite sums depend only on the line bundle of an effective divisor

The universal divisor scheme is fixed throughout. Canonical divisor sections, transported to a common invertible module, either define an independent pencil or differ by a ground-field unit. In the pencil case the actual endpoint ideal identifies its finite-flat rank with the prescribed degree.

Imports30
Imported by3

Declarations

theorem

comap_injective_of_isIso

L60 ↗
JacobianVarieties.Albanese.comap_injective_of_isIso
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.LinearPencil
open NeronModelInfra GoodReductionJacobian
open AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_exists_unique_section_of_pullbackSection_closedCover
open AlgebraicGeometry.Scheme.Modules.GlueSect
open AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_zeroSchemeIdeal
namespace JacobianVarieties.Albanese
Lean source · full declaration
theorem comap_injective_of_isIso {X Y : Scheme.{u}} (f : X ⟶ Y) [IsIso f] :
    Function.Injective (fun I : Y.IdealSheafData => I.comap f) := by
  intro I J h
  have h' := congrArg (fun L : X.IdealSheafData => L.comap (inv f)) h
  simpa only [← Scheme.IdealSheafData.comap_comp, IsIso.inv_hom_id,
    Scheme.IdealSheafData.comap_id] using h'
theorem

invertible_ideal_ne_bot

L67 ↗
JacobianVarieties.Albanese.invertible_ideal_ne_bot
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.LinearPencil
open NeronModelInfra GoodReductionJacobian
open AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_exists_unique_section_of_pullbackSection_closedCover
open AlgebraicGeometry.Scheme.Modules.GlueSect
open AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_zeroSchemeIdeal
namespace JacobianVarieties.Albanese
Lean source · statement
theorem invertible_ideal_ne_bot {X : Scheme.{u}} [Nonempty X]
    {I : X.IdealSheafData} (hI : I.IsInvertible) : I ≠ ⊥
theorem

gsec_ne_zero_of_zeroSchemeIdeal

L81 ↗
JacobianVarieties.Albanese.gsec_ne_zero_of_zeroSchemeIdeal
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.LinearPencil
open NeronModelInfra GoodReductionJacobian
open AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_exists_unique_section_of_pullbackSection_closedCover
open AlgebraicGeometry.Scheme.Modules.GlueSect
open AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_zeroSchemeIdeal
namespace JacobianVarieties.Albanese
Lean source · statement
theorem gsec_ne_zero_of_zeroSchemeIdeal
    {X : Scheme.{u}} [Nonempty X] {M : X.Modules}
    (t : 𝟙_ X.Modules ⟶ M) {I : X.IdealSheafData}
    (hI : I.IsInvertible) (ht : Scheme.Modules.zeroSchemeIdeal t = I) :
    gsec t ≠ 0
theorem

homOfGsec_gsec

L98 ↗
JacobianVarieties.Albanese.homOfGsec_gsec
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.LinearPencil
open NeronModelInfra GoodReductionJacobian
open AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_exists_unique_section_of_pullbackSection_closedCover
open AlgebraicGeometry.Scheme.Modules.GlueSect
open AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_zeroSchemeIdeal
namespace JacobianVarieties.Albanese
Lean source · statement
theorem homOfGsec_gsec {X : Scheme.{u}} {M : X.Modules}
    (t : 𝟙_ X.Modules ⟶ M) : homOfGsec (gsec t) = t
theorem

degree_eq_of_ideal_eq

L103 ↗
JacobianVarieties.Albanese.degree_eq_of_ideal_eq
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.LinearPencil
open NeronModelInfra GoodReductionJacobian
open AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_exists_unique_section_of_pullbackSection_closedCover
open AlgebraicGeometry.Scheme.Modules.GlueSect
open AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_zeroSchemeIdeal
namespace JacobianVarieties.Albanese
Lean source · statement
theorem degree_eq_of_ideal_eq
    {K : Type u} [Field K] {C : Scheme.{u}}
    {c : C ⟶ Spec (CommRingCat.of K)} {r d : ℕ}
    (D : RelEffCartierDiv c r (𝟙 (Spec (CommRingCat.of K))))
    (E : RelEffCartierDiv c d (𝟙 (Spec (CommRingCat.of K))))
    (h : D.I = E.I) : r = d
theorem

lift_pullbackAlong

L115 ↗
JacobianVarieties.Albanese.lift_pullbackAlong
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.LinearPencil
open NeronModelInfra GoodReductionJacobian
open AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_exists_unique_section_of_pullbackSection_closedCover
open AlgebraicGeometry.Scheme.Modules.GlueSect
open AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_zeroSchemeIdeal
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

pencil_fibres_comp_eq

L129 ↗
JacobianVarieties.Albanese.pencil_fibres_comp_eq
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.LinearPencil
open NeronModelInfra GoodReductionJacobian
open AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_exists_unique_section_of_pullbackSection_closedCover
open AlgebraicGeometry.Scheme.Modules.GlueSect
open AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_zeroSchemeIdeal
namespace JacobianVarieties.Albanese
Lean source · statement
theorem pencil_fibres_comp_eq
    {K : Type u} [Field K] {C B Y : Scheme.{u}}
    {c : C ⟶ Spec (CommRingCat.of K)} {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)
    (P : RelEffCartierDiv c r lineMap) (a a' : K) :
    hU.lift (P.pullbackAlong (evaluate a) (evaluate_comp_lineMap a)) ≫ sum.1 =
      hU.lift (P.pullbackAlong (evaluate a') (evaluate_comp_lineMap a')) ≫ sum.1
theorem

lift_comp_eq_of_lineBundle_iso

L156 ↗
JacobianVarieties.Albanese.lift_comp_eq_of_lineBundle_iso
Documentation

A morphism from the universal degree-r divisor scheme to an abelian scheme has equal values on two effective divisors with isomorphic actual line bundles. The assertion holds over every field, without a rational-point hypothesis.

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.LinearPencil
open NeronModelInfra GoodReductionJacobian
open AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_exists_unique_section_of_pullbackSection_closedCover
open AlgebraicGeometry.Scheme.Modules.GlueSect
open AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_zeroSchemeIdeal
namespace JacobianVarieties.Albanese
Lean source · statement
theorem lift_comp_eq_of_lineBundle_iso
    {K : Type u} [Field K] {C B Y : Scheme.{u}}
    (c : C ⟶ Spec (CommRingCat.of K)) [IsProper c]
    [SmoothOfRelativeDimension 1 c] [GeometricallyIntegral 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)
    (D₀ D₁ : RelEffCartierDiv c r (𝟙 (Spec (CommRingCat.of K))))
    (e : D₀.lineBundle ≅ D₁.lineBundle) :
    hU.lift D₀ ≫ sum.1 = hU.lift D₁ ≫ sum.1
theorem

exists_unique_finiteSumMap_desc_lineBundle_invariant

L226 ↗
JacobianVarieties.Albanese.exists_unique_finiteSumMap_desc_lineBundle_invariant
Documentation

The actual finite sum descends uniquely to the fixed universal divisor scheme and takes the same value on effective divisors with isomorphic line bundles. The field and the degree are arbitrary.

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.LinearPencil
open NeronModelInfra GoodReductionJacobian
open AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_exists_unique_section_of_pullbackSection_closedCover
open AlgebraicGeometry.Scheme.Modules.GlueSect
open AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_zeroSchemeIdeal
namespace JacobianVarieties.Albanese
Lean source · statement
theorem exists_unique_finiteSumMap_desc_lineBundle_invariant
    {K : Type u} [Field K] {C B Y : Scheme.{u}}
    (c : C ⟶ Spec (CommRingCat.of K)) [IsProper c]
    [SmoothOfRelativeDimension 1 c] [GeometricallyIntegral c]
    (s : Spec (CommRingCat.of K) ⟶ C) (hs : s ≫ c = 𝟙 _)
    {b : B ⟶ Spec (CommRingCat.of K)} [Smooth b] [IsProper b]
    [GeometricallyIntegral b] (G : RelativeGroupLaw K b) (q : SchemeHomOver c b)
    {r : ℕ} {y : Y ⟶ Spec (CommRingCat.of K)}
    {U : RelEffCartierDiv c r y} (hU : U.IsUniversal) :
    ∃ (σ : finFibrePow c r ⟶ Y) (hσ : σ ≫ y = finFibrePow.toBase c r),
      U.I.comap (mapOnProdOver c σ hσ) = fibrePowOver.tautIdeal c r ∧
      IsFinite σ ∧ Flat σ ∧ Surjective σ ∧
      ∃! sum : SchemeHomOver y b,
        σ ≫ sum.1 = (G.finiteSumMap c q r).1 ∧
        ∀ (D₀ D₁ : RelEffCartierDiv c r (𝟙 (Spec (CommRingCat.of K)))),
          Nonempty (D₀.lineBundle ≅ D₁.lineBundle) →
          hU.lift D₀ ≫ sum.1 = hU.lift D₁ ≫ sum.1

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.