Module

ThetaBundle.lean

Nyll.JacobianVarieties.Picard.ThetaBundle

4 declarations indexed from sourceView source ↗

Module documentation

Relative Picard and theta bundles

The Picard bundle pushes a tensor product of a rigidified line bundle and a module forward to the test scheme. The theta bundle is the dual of the determinant of this pushforward after twisting by the chosen relative section.

Imports4

Imported by106

def

picardBundle

L39 ↗

AlgebraicGeometry.RelPicard.picardBundle

Documentation

Push the tensor product with M forward along the projection to the test scheme.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra MonoidalCategory
namespace AlgebraicGeometry.RelPicard
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c) {T : Scheme.{u}}
  (t : T ⟶ Spec (CommRingCat.of R))

Lean source · statement

def picardBundle (M : RigidifiedLineBundle c ε t) (N : (pullback c t).Modules) : T.Modules

def

thetaBundle

L43 ↗

AlgebraicGeometry.RelPicard.thetaBundle

Documentation

The dual determinant of the Picard bundle after a relative section twist.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra MonoidalCategory
namespace AlgebraicGeometry.RelPicard
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c) {T : Scheme.{u}}
  (t : T ⟶ Spec (CommRingCat.of R))

Lean source · statement

def thetaBundle (M : RigidifiedLineBundle c ε t) (r n : ℕ) : T.Modules

theorem

picardBundle_def

L46 ↗

AlgebraicGeometry.RelPicard.picardBundle_def

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra MonoidalCategory
namespace AlgebraicGeometry.RelPicard
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c) {T : Scheme.{u}}
  (t : T ⟶ Spec (CommRingCat.of R))

Lean source · statement

theorem picardBundle_def (M : RigidifiedLineBundle c ε t) (N : (pullback c t).Modules) :
    picardBundle c ε t M N = (Scheme.Modules.pushforward (pullback.snd c t)).obj (M.L ⊗ N)

theorem

thetaBundle_def

L49 ↗

AlgebraicGeometry.RelPicard.thetaBundle_def

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra MonoidalCategory
namespace AlgebraicGeometry.RelPicard
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c) {T : Scheme.{u}}
  (t : T ⟶ Spec (CommRingCat.of R))

Lean source · statement

theorem thetaBundle_def (M : RigidifiedLineBundle c ε t) (r n : ℕ) :
    thetaBundle c ε t M r n =
      Scheme.Modules.dual (Scheme.Modules.det n
        (picardBundle c ε t M (sectionTwist c ε t r)))

Module documentation

Relative Picard and theta bundles

Declarations

picardBundle

thetaBundle

picardBundle_def

thetaBundle_def