NYLL
Module

Exists_abelJacobi_of_representsRelSubPic.lean

Nyll.JacobianVarieties.Picard.Exists_abelJacobi_of_representsRelSubPic
8 declarations indexed from sourceView source ↗

Module documentation

Abel-Jacobi morphisms from a relative Picard representation

Construct the Abel-Jacobi morphism using line bundles of relative points and rigidification.

Imports30
Imported by8

Declarations

theorem

ofPoint_congr_point

L74 ↗
JacobianVarieties.Picard.Proofs.Exists_abelJacobi_of_representsRelSubPic.AlgebraicGeometry.RelPicard.AbelJacobiGlue.ofPoint_congr_point
Source context 18 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.Exists_abelJacobi_of_representsRelSubPic
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
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace AbelJacobiGlue
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
Lean source · statement
theorem ofPoint_congr_point {𝒞 S : Scheme.{u}} (f : 𝒞 ⟶ S) [IsSeparated f] {T : Scheme.{u}}
    {g : T ⟶ S} {a b : T ⟶ 𝒞} (h : a = b) (ha : a ≫ f = g) (hb : b ≫ f = g) :
    RelEffCartierDiv.ofPoint f a ha = RelEffCartierDiv.ofPoint f b hb
theorem

nonempty_pullback_baseChangeSnd_ajFamilyOver_iso

L80 ↗
JacobianVarieties.Picard.Proofs.Exists_abelJacobi_of_representsRelSubPic.AlgebraicGeometry.RelPicard.AbelJacobiGlue.nonempty_pullback_baseChangeSnd_ajFamilyOver_iso
Source context 18 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.Exists_abelJacobi_of_representsRelSubPic
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
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace AbelJacobiGlue
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
Lean source · statement
theorem nonempty_pullback_baseChangeSnd_ajFamilyOver_iso
    (R : Type u) [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
    [IsSeparated c] [SmoothOfRelativeDimension 1 c]
    (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
    {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) (x : SchemeHomOver t c) :
    Nonempty ((Scheme.Modules.pullback (baseChangeSnd c x)).obj
        ((RelEffCartierDiv.ofPoint c (𝟙 C) (Category.id_comp c)).lineBundle ⊗
          (RelEffCartierDiv.ofPoint c (c ≫ ε.1)
            ((Category.assoc _ _ _).trans
                ((congrArg (c ≫ ·) ε.2).trans (Category.comp_id c)))).idealModule) ≅
      (RelEffCartierDiv.ofPoint c x.1 x.2).lineBundle ⊗
        (RelEffCartierDiv.ofPoint c (t ≫ ε.1)
          ((Category.assoc _ _ _).trans
              ((congrArg (t ≫ ·) ε.2).trans (Category.comp_id t)))).idealModule)
theorem

baseChangeSnd_snd

L146 ↗
JacobianVarieties.Picard.Proofs.Exists_abelJacobi_of_representsRelSubPic.AlgebraicGeometry.RelPicard.AbelJacobiGlue.baseChangeSnd_snd
Source context 18 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.Exists_abelJacobi_of_representsRelSubPic
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
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace AbelJacobiGlue
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
Lean source · statement
theorem baseChangeSnd_snd {R : Type u} [CommRing R] {C T T' : Scheme.{u}}
    (c : C ⟶ Spec (CommRingCat.of R))
    {t : T ⟶ Spec (CommRingCat.of R)} {t' : T' ⟶ Spec (CommRingCat.of R)} (s : SchemeHomOver t' t) :
    baseChangeSnd c s ≫ pullback.snd c t = pullback.snd c t' ≫ s.1
theorem

rigSection_snd

L153 ↗
JacobianVarieties.Picard.Proofs.Exists_abelJacobi_of_representsRelSubPic.AlgebraicGeometry.RelPicard.AbelJacobiGlue.rigSection_snd
Source context 18 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.Exists_abelJacobi_of_representsRelSubPic
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
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace AbelJacobiGlue
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
Lean source · statement
theorem rigSection_snd {R : Type u} [CommRing R] {C T : Scheme.{u}}
    (c : C ⟶ Spec (CommRingCat.of R))
    (t : T ⟶ Spec (CommRingCat.of R)) (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c) :
    rigSection c t ε ≫ pullback.snd c t = 𝟙 T
def

pullbackBaseChangeSndPullbackSndIso

L162 ↗
JacobianVarieties.Picard.Proofs.Exists_abelJacobi_of_representsRelSubPic.AlgebraicGeometry.RelPicard.AbelJacobiGlue.pullbackBaseChangeSndPullbackSndIso
Documentation

Identify the two pullbacks of a module along a base-change square.

Source context 18 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.Exists_abelJacobi_of_representsRelSubPic
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
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace AbelJacobiGlue
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
Lean source · statement
def pullbackBaseChangeSndPullbackSndIso {R : Type u} [CommRing R] {C T T' : Scheme.{u}}
    (c : C ⟶ Spec (CommRingCat.of R))
    {t : T ⟶ Spec (CommRingCat.of R)} {t' : T' ⟶ Spec (CommRingCat.of R)}
    (s : SchemeHomOver t' t) (F : T.Modules) :
    (Scheme.Modules.pullback (baseChangeSnd c s)).obj
        ((Scheme.Modules.pullback (pullback.snd c t)).obj F) ≅
      (Scheme.Modules.pullback (pullback.snd c t')).obj ((Scheme.Modules.pullback s.1).obj F)
def

pullbackRigSectionPullbackSndIso

L175 ↗
JacobianVarieties.Picard.Proofs.Exists_abelJacobi_of_representsRelSubPic.AlgebraicGeometry.RelPicard.AbelJacobiGlue.pullbackRigSectionPullbackSndIso
Documentation

Pulling back a module from the base to the rigidifying section recovers that module.

Source context 18 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.Exists_abelJacobi_of_representsRelSubPic
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
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace AbelJacobiGlue
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
Lean source · statement
def pullbackRigSectionPullbackSndIso {R : Type u} [CommRing R] {C T : Scheme.{u}}
    (c : C ⟶ Spec (CommRingCat.of R))
    (t : T ⟶ Spec (CommRingCat.of R)) (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
    (F : T.Modules) :
    (Scheme.Modules.pullback (rigSection c t ε)).obj
        ((Scheme.Modules.pullback (pullback.snd c t)).obj F) ≅ F
theorem

nonempty_pullback_fst_pointBundle_iso_pointSubBasepointModule

L185 ↗
JacobianVarieties.Picard.Proofs.Exists_abelJacobi_of_representsRelSubPic.AlgebraicGeometry.RelPicard.AbelJacobiGlue.nonempty_pullback_fst_pointBundle_iso_pointSubBasepointModule
Source context 18 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.Exists_abelJacobi_of_representsRelSubPic
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
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace AbelJacobiGlue
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
Lean source · statement
theorem nonempty_pullback_fst_pointBundle_iso_pointSubBasepointModule
    (R : Type u) [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
    [IsSeparated c] [SmoothOfRelativeDimension 1 c]
    (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
    (k : Type u) [Field k] (s : Spec (CommRingCat.of k) ⟶ C) :
    Nonempty ((Scheme.Modules.pullback (pullback.fst (pullback.snd c (s ≫ c))
        (𝟙 (Spec (CommRingCat.of k))))).obj
        ((RelEffCartierDiv.ofPoint c s rfl).lineBundle ⊗
          (RelEffCartierDiv.ofPoint c ((s ≫ c) ≫ ε.1)
            ((Category.assoc _ _ _).trans
                ((congrArg ((s ≫ c) ≫ ·) ε.2).trans (Category.comp_id _)))).idealModule) ≅
      pointSubBasepointModule (a := pullback.snd c (s ≫ c))
        ⟨graphOver c s rfl, graphOver_snd c s rfl⟩
        ⟨rigSection c (s ≫ c) ε, rigSection_snd c (s ≫ c) ε⟩)
theorem

exists_abelJacobi_of_representsRelSubPic

L258 ↗
AlgebraicGeometry.RelPicard.exists_abelJacobi_of_representsRelSubPic
Source context 12 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.Exists_abelJacobi_of_representsRelSubPic
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
noncomputable section
open AlgebraicGeometry.RelPicard.AbelJacobiGlue in
Lean source · statement
theorem _root_.AlgebraicGeometry.RelPicard.exists_abelJacobi_of_representsRelSubPic
    (R : Type u) [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
    [IsProper c] [SmoothOfRelativeDimension 1 c] [GeometricallyIntegral c]
    (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
    (D : RelativePic0Designation R c) (h : RepresentsRelSubPic c ε (algEquivZeroCut c ε) D) :
    ∃ aj : SchemeHomOver c D.toBase,
      ε.1 ≫ aj.1 = D.zeroSection ∧
      ∀ (K : Type u) [Field K] (t : Spec (CommRingCat.of K) ⟶ Spec (CommRingCat.of R))
          (x : SchemeHomOver t c),
        Nonempty ((h.poincare.pullbackAlong
            ⟨x.1 ≫ aj.1, (Category.assoc _ _ _).trans ((congrArg (x.1 ≫ ·) aj.2).trans x.2)⟩).L ≅
          (RelEffCartierDiv.ofPoint c x.1 x.2).lineBundle ⊗
            (RelEffCartierDiv.ofPoint c (t ≫ ε.1)
              ((Category.assoc _ _ _).trans
                  ((congrArg (t ≫ ·) ε.2).trans (Category.comp_id t)))).idealModule)

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