Module

nonempty_poincare_pullbackAlong_iso_lineBundle_tensor_idealModule_of_abelJacobi_baseChange.lean

Nyll.JacobianVarieties.Picard.nonempty_poincare_pullbackAlong_iso_lineBundle_tensor_idealModule_of_abelJacobi_baseChange

3 declarations indexed from sourceView source ↗

Module documentation

The Abel-Jacobi Poincare comparison after base change

Pullback comparisons identify the Poincare bundle with the point and basepoint divisor modules.

Imports19

Imported by2

theorem

ker_comp_comap_of_isIso'

JacobianVarieties.Picard.Proofs.AbelJacobiPoincare.K6H6.ker_comp_comap_of_isIso'

Source context 13 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AbelJacobiPoincare
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
open _root_.AlgebraicGeometry.SmoothProperCurve
namespace K6H6
open _root_.AlgebraicGeometry.Scheme.IdealSheafData

Lean source · statement

theorem ker_comp_comap_of_isIso' {T P P' : Scheme.{u}} (a : T ⟶ P') [IsClosedImmersion a]
    (e : P' ⟶ P) [IsIso e] :
    (a ≫ e).ker.comap e = a.ker

theorem

nonempty_pullback_invModule_tensor_module_iso

JacobianVarieties.Picard.Proofs.AbelJacobiPoincare.K6H6.nonempty_pullback_invModule_tensor_module_iso

Source context 13 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AbelJacobiPoincare
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
open _root_.AlgebraicGeometry.SmoothProperCurve
namespace K6H6
open _root_.AlgebraicGeometry.Scheme.IdealSheafData

Lean source · statement

theorem nonempty_pullback_invModule_tensor_module_iso {Y Y' : Scheme.{u}} (f : Y' ⟶ Y)
    {I J : Y.IdealSheafData}
    (hI : I.IsInvertible) (hJ : J.IsInvertible) (hI' : (I.comap f).IsInvertible) (hJ' : (J.comap
      f).IsInvertible) :
    Nonempty ((Scheme.Modules.pullback f).obj (I.invModule ⊗ J.module) ≅ (I.comap f).invModule ⊗
      (J.comap f).module)

theorem

nonempty_poincare_pullbackAlong_iso_lineBundle_tensor_idealModule_of_abelJacobi_baseChange

AlgebraicGeometry.RelPicard.nonempty_poincare_pullbackAlong_iso_lineBundle_tensor_idealModule_of_abelJacobi_baseChange

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicGeometry.RelPicard
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory
open NeronModelInfra GoodReductionJacobian
open AlgebraicGeometry.SmoothProperCurve
universe u
open _root_.JacobianVarieties.Picard.Proofs.AbelJacobiPoincare.K6H6 in
open _root_.AlgebraicGeometry.Scheme.IdealSheafData in

Lean source · statement

theorem nonempty_poincare_pullbackAlong_iso_lineBundle_tensor_idealModule_of_abelJacobi_baseChange
    {R : Type u} [CommRing R] {X : Scheme.{u}} (cX : X ⟶ Spec (CommRingCat.of R)) [IsSeparated cX]
    (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) cX)
    (D : RelativePic0Designation R cX) (hrep : RepresentsRelSubPic cX ε (algEquivZeroCut cX ε) D)
    (L' : Type u) [CommRing L'] [Algebra R L'] (k' : Type u) [Field k'] [Algebra R k'] [Algebra L'
      k'] [IsScalarTower R L' k']
    [SmoothOfRelativeDimension 1 (baseChange R cX k')]
    (hDL : RepresentsRelSubPic (baseChange R cX L') (sectionBaseChange L' ε)
      (algEquivZeroCut (baseChange R cX L') (sectionBaseChange L' ε)) (D.baseChange L'))
    (hPL : Nonempty (hDL.poincare.L ≅ (BaseChange.ofR cX ε L'
      (hrep.poincare.pullbackAlong ⟨pullback.fst D.toBase (specMap R L'), pullback.condition⟩)).L))
    (hrepQ : RepresentsRelSubPic (baseChange R cX k') (sectionBaseChange k' ε)
      (algEquivZeroCut (baseChange R cX k') (sectionBaseChange k' ε)) (D.baseChange k'))
    (ajL : SchemeHomOver (baseChange R cX L') (D.baseChange L').toBase)
    (hajL : ∀ (x : SchemeHomOver (specMap L' k') (baseChange R cX L')),
      Nonempty ((hDL.poincare.pullbackAlong
          ⟨x.1 ≫ ajL.1, (Category.assoc _ _ _).trans ((congrArg (x.1 ≫ ·) ajL.2).trans x.2)⟩).L ≅
        (RelEffCartierDiv.ofPoint (baseChange R cX L') x.1 x.2).lineBundle ⊗
          (RelEffCartierDiv.ofPoint (baseChange R cX L') (specMap L' k' ≫ (sectionBaseChange L'
            ε).1)
            ((Category.assoc _ _ _).trans ((congrArg (specMap L' k' ≫ ·) (sectionBaseChange L'
              ε).2).trans
              (Category.comp_id _)))).idealModule))
    (kL : pullback cX (specMap R k') ⟶ pullback cX (specMap R L'))
    (hkL₁ : kL ≫ pullback.fst _ _ = pullback.fst _ _) (hkL₂ : kL ≫ pullback.snd _ _ = pullback.snd
      _ _ ≫ specMap L' k')
    (P : SchemeHomOver (𝟙 (Spec (CommRingCat.of k'))) (baseChange R cX k'))
    (G : SchemeHomOver (specMap R k') D.toBase) (hG : G.1 = P.1 ≫ kL ≫ ajL.1 ≫ pullback.fst
      D.toBase (specMap R L'))
    (g : SchemeHomOver (𝟙 (Spec (CommRingCat.of k'))) (D.baseChange k').toBase)
    (isoΘ : Nonempty ((hrep.poincare.pullbackAlong G).L ≅
      (Scheme.Modules.pullback (BaseChange.κ cX k' (𝟙 (Spec (CommRingCat.of k')))).inv).obj
        (hrepQ.poincare.pullbackAlong g).L)) :
    Nonempty ((hrepQ.poincare.pullbackAlong g).L ≅
      (RelEffCartierDiv.ofPoint (baseChange R cX k') P.1 P.2).lineBundle ⊗
        (RelEffCartierDiv.ofPoint (baseChange R cX k') (sectionBaseChange k' ε).1
          (sectionBaseChange k' ε).2).idealModule)