Module

Nonempty_ajFamily_fibre_iso.lean

Nyll.JacobianVarieties.Picard.Nonempty_ajFamily_fibre_iso

1 declaration indexed from sourceView source ↗

Module documentation

Relative Picard varieties and fibre cohomology

Identify the fibres of the Abel–Jacobi family with the point-difference line bundles.

Imports5

Imported by2

theorem

nonempty_ajFamily_fibre_iso

L39 ↗

AlgebraicGeometry.RelPicard.nonempty_ajFamily_fibre_iso

Source context 10 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.Nonempty_ajFamily_fibre_iso
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian

Lean source · statement

theorem _root_.AlgebraicGeometry.RelPicard.nonempty_ajFamily_fibre_iso
    {k : Type u} [Field k] {A : Scheme.{u}} {a : A ⟶ Spec (CommRingCat.of k)}
    [IsSeparated a] [SmoothOfRelativeDimension 1 a]
    (ε t : SchemeHomOver (𝟙 (Spec (CommRingCat.of k))) a) :
    Nonempty ((Scheme.Modules.pullback (baseChangeSnd a t)).obj (ajFamily (a := a) ε) ≅
      pointSubBasepointModule (a := a) t ε)

Module documentation

Relative Picard varieties and fibre cohomology

Declarations

nonempty_ajFamily_fibre_iso