NYLL
Module

RepresentsRelSubPic_pullbackHom_baseChange_fst.lean

Nyll.JacobianVarieties.Picard.RepresentsRelSubPic_pullbackHom_baseChange_fst
4 declarations indexed from sourceView source ↗

Module documentation

Pullback on relative Picard schemes and base change

Pullback of rigidified line bundles commutes with the comparison back to the base ring. The represented pullback morphism therefore commutes with the first projection of base change.

Imports5
Imported by1

Declarations

theorem

κ_hom_curveChange

L84 ↗
JacobianVarieties.Picard.Proofs.PullbackBaseChange.AlgebraicGeometry.RelPicard.BCAux.κ_hom_curveChange
Source context 17 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.PullbackBaseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry.SmoothProperCurve
namespace AlgebraicGeometry
namespace RelPicard
namespace BCAux
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {C C' : Scheme.{u}}
  {c : C ⟶ Spec (CommRingCat.of R)} {c' : C' ⟶ Spec (CommRingCat.of R)}
  (f : C' ⟶ C) (hf : f ≫ c = c') (R' : Type u) [CommRing R'] [Algebra R R']
  (hf' : curveChange f hf (specMap R R') ≫ baseChange R c R' = baseChange R c' R')
include hf' in
Lean source · statement
theorem κ_hom_curveChange {T : Scheme.{u}} (t' : T ⟶ Spec (CommRingCat.of R')) :
    (BaseChange.κ c' R' t').hom ≫ curveChange f hf (t' ≫ specMap R R') =
      curveChange (curveChange f hf (specMap R R')) hf' t' ≫ (BaseChange.κ c R' t').hom
theorem

curveChange_κ_inv

L97 ↗
JacobianVarieties.Picard.Proofs.PullbackBaseChange.AlgebraicGeometry.RelPicard.BCAux.curveChange_κ_inv
Source context 17 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.PullbackBaseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry.SmoothProperCurve
namespace AlgebraicGeometry
namespace RelPicard
namespace BCAux
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {C C' : Scheme.{u}}
  {c : C ⟶ Spec (CommRingCat.of R)} {c' : C' ⟶ Spec (CommRingCat.of R)}
  (f : C' ⟶ C) (hf : f ≫ c = c') (R' : Type u) [CommRing R'] [Algebra R R']
  (hf' : curveChange f hf (specMap R R') ≫ baseChange R c R' = baseChange R c' R')
include hf' in
Lean source · statement
theorem curveChange_κ_inv {T : Scheme.{u}} (t' : T ⟶ Spec (CommRingCat.of R')) :
    curveChange f hf (t' ≫ specMap R R') ≫ (BaseChange.κ c R' t').inv =
      (BaseChange.κ c' R' t').inv ≫ curveChange (curveChange f hf (specMap R R')) hf' t'
def

toR_pullbackCurve_iso

L105 ↗
JacobianVarieties.Picard.Proofs.PullbackBaseChange.AlgebraicGeometry.RelPicard.BCAux.toR_pullbackCurve_iso
Documentation

Transport back to the base ring commutes with pullback along the curve morphism.

Source context 16 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.PullbackBaseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry.SmoothProperCurve
namespace AlgebraicGeometry
namespace RelPicard
namespace BCAux
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {C C' : Scheme.{u}}
  {c : C ⟶ Spec (CommRingCat.of R)} {c' : C' ⟶ Spec (CommRingCat.of R)}
  (f : C' ⟶ C) (hf : f ≫ c = c') (R' : Type u) [CommRing R'] [Algebra R R']
  (hf' : curveChange f hf (specMap R R') ≫ baseChange R c R' = baseChange R c' R')
Lean source · statement
def toR_pullbackCurve_iso
    {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c}
    {ε' : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c'}
    (hε : ε'.1 ≫ f = ε.1)
    (hεbc : (sectionBaseChange R' ε').1 ≫ curveChange f hf (specMap R R') =
      (sectionBaseChange R' ε).1)
    {T : Scheme.{u}} {t' : T ⟶ Spec (CommRingCat.of R')}
    (N : RigidifiedLineBundle (baseChange R c R') (sectionBaseChange R' ε) t') :
    (BaseChange.toR c' ε' R' (N.pullbackCurve (curveChange f hf (specMap R R')) hf' hεbc)).L ≅
      ((BaseChange.toR c ε R' N).pullbackCurve f hf hε).L
theorem

pullbackHom_baseChange_fst

L121 ↗
AlgebraicGeometry.RelPicard.RepresentsRelSubPic.pullbackHom_baseChange_fst
Source context 10 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.PullbackBaseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry.SmoothProperCurve
Lean source · statement
theorem _root_.AlgebraicGeometry.RelPicard.RepresentsRelSubPic.pullbackHom_baseChange_fst
    {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)
    {D : RelativePic0Designation R c} {D' : RelativePic0Designation R c'}
    (h : RepresentsRelSubPic c ε (algEquivZeroCut c ε) D)
    (h' : RepresentsRelSubPic c' ε' (algEquivZeroCut c' ε') D')
    (R' : Type u) [CommRing R'] [Algebra R R']
    (hR : RepresentsRelSubPic (baseChange R c R') (sectionBaseChange R' ε)
      (algEquivZeroCut (baseChange R c R') (sectionBaseChange R' ε)) (D.baseChange R'))
    (hPR : Nonempty (hR.poincare.L ≅ (BaseChange.ofR c ε R'
      (h.poincare.pullbackAlong ⟨pullback.fst D.toBase (specMap R R'), pullback.condition⟩)).L))
    (hR' : RepresentsRelSubPic (baseChange R c' R') (sectionBaseChange R' ε')
      (algEquivZeroCut (baseChange R c' R') (sectionBaseChange R' ε')) (D'.baseChange R'))
    (hPR' : Nonempty (hR'.poincare.L ≅ (BaseChange.ofR c' ε' R'
      (h'.poincare.pullbackAlong ⟨pullback.fst D'.toBase (specMap R R'), pullback.condition⟩)).L))
    (hf' : curveChange f hf (specMap R R') ≫ baseChange R c R' = baseChange R c' R')
    (hεbc : (sectionBaseChange R' ε').1 ≫ curveChange f hf (specMap R R') =
      (sectionBaseChange R' ε).1) :
    (RepresentsRelSubPic.pullbackHom (curveChange f hf (specMap R R')) hf' hεbc hR hR').1 ≫
        pullback.fst D'.toBase (specMap R R') =
      pullback.fst D.toBase (specMap R R') ≫ (RepresentsRelSubPic.pullbackHom f hf hε h h').1

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