NYLL
Module

RepresentsRelSubPicPullback.lean

Nyll.JacobianVarieties.Picard.RepresentsRelSubPicPullback
5 declarations indexed from sourceView source ↗

Module documentation

Pullback on representing Picard schemes

Classify pullback of the Poincare bundle to obtain the induced morphism of Picard schemes.

Imports5
Imported by41

Declarations

def

pullbackHom

L47 ↗
AlgebraicGeometry.RelPicard.RepresentsRelSubPic.pullbackHom
Documentation

The morphism of representing Picard schemes that classifies pullback along the curve map.

Source context 7 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
noncomputable section
namespace AlgebraicGeometry.RelPicard
variable {R : Type u} [CommRing R] {C C' : Scheme.{u}}
  {c : C ⟶ Spec (CommRingCat.of R)} {c' : C' ⟶ Spec (CommRingCat.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c}
  {ε' : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c'}
  (f : C' ⟶ C) (hf : f ≫ c = c') (hε : ε'.1 ≫ f = ε.1)
namespace RepresentsRelSubPic
variable {D : RelativePic0Designation R c} {D' : RelativePic0Designation R c'}
  (h : RepresentsRelSubPic c ε (algEquivZeroCut c ε) D)
  (h' : RepresentsRelSubPic c' ε' (algEquivZeroCut c' ε') D')
Lean source · statement
def pullbackHom : SchemeHomOver D.toBase D'.toBase
theorem

postComp_pullbackHom_classify

L51 ↗
AlgebraicGeometry.RelPicard.RepresentsRelSubPic.postComp_pullbackHom_classify
Source context 7 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
noncomputable section
namespace AlgebraicGeometry.RelPicard
variable {R : Type u} [CommRing R] {C C' : Scheme.{u}}
  {c : C ⟶ Spec (CommRingCat.of R)} {c' : C' ⟶ Spec (CommRingCat.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c}
  {ε' : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c'}
  (f : C' ⟶ C) (hf : f ≫ c = c') (hε : ε'.1 ≫ f = ε.1)
namespace RepresentsRelSubPic
variable {D : RelativePic0Designation R c} {D' : RelativePic0Designation R c'}
  (h : RepresentsRelSubPic c ε (algEquivZeroCut c ε) D)
  (h' : RepresentsRelSubPic c' ε' (algEquivZeroCut c' ε') D')
Lean source · statement
theorem postComp_pullbackHom_classify {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R))
    (M : RigidifiedLineBundle c ε t) (hM : (algEquivZeroCut c ε).P t M) :
    postComp (pullbackHom f hf hε h h') (h.classify t M hM) =
      h'.classify t (M.pullbackCurve f hf hε) (FibrewiseAlgEquivZero.pullbackCurve f hf hε hM)
theorem

pullbackHom_unique

L61 ↗
AlgebraicGeometry.RelPicard.RepresentsRelSubPic.pullbackHom_unique
Source context 7 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
noncomputable section
namespace AlgebraicGeometry.RelPicard
variable {R : Type u} [CommRing R] {C C' : Scheme.{u}}
  {c : C ⟶ Spec (CommRingCat.of R)} {c' : C' ⟶ Spec (CommRingCat.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c}
  {ε' : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c'}
  (f : C' ⟶ C) (hf : f ≫ c = c') (hε : ε'.1 ≫ f = ε.1)
namespace RepresentsRelSubPic
variable {D : RelativePic0Designation R c} {D' : RelativePic0Designation R c'}
  (h : RepresentsRelSubPic c ε (algEquivZeroCut c ε) D)
  (h' : RepresentsRelSubPic c' ε' (algEquivZeroCut c' ε') D')
Lean source · statement
theorem pullbackHom_unique (g : SchemeHomOver D.toBase D'.toBase)
    (hg : ∀ {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) (M : RigidifiedLineBundle c ε t)
      (hM : (algEquivZeroCut c ε).P t M),
      postComp g (h.classify t M hM) =
        h'.classify t (M.pullbackCurve f hf hε) (FibrewiseAlgEquivZero.pullbackCurve f hf hε hM)) :
    g = pullbackHom f hf hε h h'
theorem

zeroSection_pullbackHom

L77 ↗
AlgebraicGeometry.RelPicard.RepresentsRelSubPic.zeroSection_pullbackHom
Source context 7 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
noncomputable section
namespace AlgebraicGeometry.RelPicard
variable {R : Type u} [CommRing R] {C C' : Scheme.{u}}
  {c : C ⟶ Spec (CommRingCat.of R)} {c' : C' ⟶ Spec (CommRingCat.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c}
  {ε' : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c'}
  (f : C' ⟶ C) (hf : f ≫ c = c') (hε : ε'.1 ≫ f = ε.1)
namespace RepresentsRelSubPic
variable {D : RelativePic0Designation R c} {D' : RelativePic0Designation R c'}
  (h : RepresentsRelSubPic c ε (algEquivZeroCut c ε) D)
  (h' : RepresentsRelSubPic c' ε' (algEquivZeroCut c' ε') D')
Lean source · statement
theorem zeroSection_pullbackHom :
    D.zeroSection ≫ (pullbackHom f hf hε h h').1 = D'.zeroSection
theorem

existsUnique_pullbackHom

L89 ↗
AlgebraicGeometry.RelPicard.RepresentsRelSubPic.existsUnique_pullbackHom
Source context 7 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
noncomputable section
namespace AlgebraicGeometry.RelPicard
variable {R : Type u} [CommRing R] {C C' : Scheme.{u}}
  {c : C ⟶ Spec (CommRingCat.of R)} {c' : C' ⟶ Spec (CommRingCat.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c}
  {ε' : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c'}
  (f : C' ⟶ C) (hf : f ≫ c = c') (hε : ε'.1 ≫ f = ε.1)
namespace RepresentsRelSubPic
variable {D : RelativePic0Designation R c} {D' : RelativePic0Designation R c'}
  (h : RepresentsRelSubPic c ε (algEquivZeroCut c ε) D)
  (h' : RepresentsRelSubPic c' ε' (algEquivZeroCut c' ε') D')
Lean source · statement
theorem existsUnique_pullbackHom :
    ∃! fstar : SchemeHomOver D.toBase D'.toBase,
      ∀ {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) (M : RigidifiedLineBundle c ε t)
        (hM : (algEquivZeroCut c ε).P t M),
        postComp fstar (h.classify t M hM) =
          h'.classify t (M.pullbackCurve f hf hε)
            (FibrewiseAlgEquivZero.pullbackCurve f hf hε hM)

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