Module

LineBundleSumBaseChange.lean

Nyll.JacobianVarieties.Albanese.LineBundleSumBaseChange

1 declaration indexed from sourceView source ↗

Module documentation

Line-bundle invariance of sums over arbitrary field-valued test maps

The curve, target group, universal divisor, and sum morphism are base changed along the same actual field-valued test map. The actual divisor equivalence and its inverse-ideal-module comparison transport the line bundles. Line-bundle invariance over the extended field then descends by projection from the actual target pullback.

Imports8

Imported by3

theorem

lift_comp_eq_of_lineBundle_iso_of_fieldMap

L37 ↗

JacobianVarieties.Albanese.lift_comp_eq_of_lineBundle_iso_of_fieldMap

Documentation

The sum morphism has the same value on linearly equivalent effective divisors over any field-valued test map into the ground field.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open NeronModelInfra GoodReductionJacobian
namespace JacobianVarieties.Albanese

Lean source · statement

theorem lift_comp_eq_of_lineBundle_iso_of_fieldMap
    {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)
    (L : Type u) [Field L] (s : Spec (CommRingCat.of L) ⟶ Spec (CommRingCat.of K))
    (D₀ D₁ : RelEffCartierDiv c r s) (e : D₀.lineBundle ≅ D₁.lineBundle) :
    hU.lift D₀ ≫ sum.1 = hU.lift D₁ ≫ sum.1

Module documentation

Line-bundle invariance of sums over arbitrary field-valued test maps

Declarations

lift_comp_eq_of_lineBundle_iso_of_fieldMap