NYLL
Module

SectionComparisonBaseChange.lean

Nyll.JacobianVarieties.Picard.SectionComparisonBaseChange
3 declarations indexed from sourceView source ↗

Module documentation

Base change of the comparison between rigidifying sections

The tensor-inverse evaluations identify changing the section before and after scalar extension. The actual Poincare families then identify the comparison morphisms. All base rings are arbitrary commutative rings, including nonreduced tensor products.

Imports6
Imported by1

Declarations

def

toR_twistIso

L45 ↗
JacobianVarieties.Picard.SectionComparison.toR_twistIso
Documentation

Changing the rigidifying section commutes with restriction along the actual iterated-pullback isomorphism.

Source context 8 commands

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

universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory
open AlgebraicGeometry AlgebraicGeometry.RelPicard AlgebraicGeometry.SmoothProperCurve
open AlgebraicGeometry.RelPicard.BaseChange NeronModelInfra GoodReductionJacobian
open JacobianVarieties.Picard.Proofs.InversePairSections.Sub2c
open JacobianVarieties.Picard.Proofs.Exists_representsRelSubPic_baseChange.RepBCSketch
namespace JacobianVarieties.Picard.SectionComparison
variable {R : Type u} [CommRing R] {C : Scheme.{u}}
  {c : C ⟶ Spec (CommRingCat.of R)}
Lean source · statement
def toR_twistIso
    (ε₁ ε₂ : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
    (R' : Type u) [CommRing R'] [Algebra R R']
    {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R')}
    (M : RigidifiedLineBundle (baseChange R c R') (sectionBaseChange R' ε₁) t) :
    (toR c ε₂ R' (twist (sectionBaseChange R' ε₁) (sectionBaseChange R' ε₂) M)).L ≅
      (twist ε₁ ε₂ (toR c ε₁ R' M)).L
theorem

classify_baseChange_fst

L72 ↗
JacobianVarieties.Picard.SectionComparison.classify_baseChange_fst
Source context 8 commands

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

universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory
open AlgebraicGeometry AlgebraicGeometry.RelPicard AlgebraicGeometry.SmoothProperCurve
open AlgebraicGeometry.RelPicard.BaseChange NeronModelInfra GoodReductionJacobian
open JacobianVarieties.Picard.Proofs.InversePairSections.Sub2c
open JacobianVarieties.Picard.Proofs.Exists_representsRelSubPic_baseChange.RepBCSketch
namespace JacobianVarieties.Picard.SectionComparison
variable {R : Type u} [CommRing R] {C : Scheme.{u}}
  {c : C ⟶ Spec (CommRingCat.of R)}
Lean source · statement
theorem classify_baseChange_fst
    (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
    (D : RelativePic0Designation R c) (h : RepresentsRelSubPic c ε (algEquivZeroCut c ε) D)
    (R' : Type u) [CommRing R'] [Algebra R R']
    (h' : RepresentsRelSubPic (baseChange R c R') (sectionBaseChange R' ε)
      (algEquivZeroCut (baseChange R c R') (sectionBaseChange R' ε)) (D.baseChange R'))
    (hP : Nonempty (h'.poincare.L ≅ (ofR c ε R'
      (h.poincare.pullbackAlong ⟨pullback.fst D.toBase (specMap R R'), pullback.condition⟩)).L))
    {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R'))
    (M : RigidifiedLineBundle (baseChange R c R') (sectionBaseChange R' ε) t)
    (hM : FibrewiseAlgEquivZero M) :
    (h'.classify t M hM).1 ≫ pullback.fst D.toBase (specMap R R') =
      (h.classify (t ≫ specMap R R') (toR c ε R' M)
        ((fibrewiseAlgEquivZero_toR_iff c ε R' M).2 hM)).1
theorem

sectionComparison_baseChange

L107 ↗
JacobianVarieties.Picard.SectionComparison.sectionComparison_baseChange
Documentation

The comparison obtained by changing sections commutes with scalar extension. The extended representations and their Poincare comparisons come from the proved base-change construction, rather than additional compatibility assumptions.

Source context 8 commands

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

universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory
open AlgebraicGeometry AlgebraicGeometry.RelPicard AlgebraicGeometry.SmoothProperCurve
open AlgebraicGeometry.RelPicard.BaseChange NeronModelInfra GoodReductionJacobian
open JacobianVarieties.Picard.Proofs.InversePairSections.Sub2c
open JacobianVarieties.Picard.Proofs.Exists_representsRelSubPic_baseChange.RepBCSketch
namespace JacobianVarieties.Picard.SectionComparison
variable {R : Type u} [CommRing R] {C : Scheme.{u}}
  {c : C ⟶ Spec (CommRingCat.of R)}
Lean source · full declaration
theorem sectionComparison_baseChange
    (ε₁ ε₂ : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
    {D₁ D₂ : RelativePic0Designation R c}
    (h₁ : RepresentsRelSubPic c ε₁ (algEquivZeroCut c ε₁) D₁)
    (h₂ : RepresentsRelSubPic c ε₂ (algEquivZeroCut c ε₂) D₂)
    (R' : Type u) [CommRing R'] [Algebra R R'] :
    let h₁' : RepresentsRelSubPic (baseChange R c R') (sectionBaseChange R' ε₁)
        (algEquivZeroCut (baseChange R c R') (sectionBaseChange R' ε₁)) (D₁.baseChange R') :=
      (exists_representsRelSubPic_baseChange R c ε₁ D₁ h₁ R').choose
    let h₂' : RepresentsRelSubPic (baseChange R c R') (sectionBaseChange R' ε₂)
        (algEquivZeroCut (baseChange R c R') (sectionBaseChange R' ε₂)) (D₂.baseChange R') :=
      (exists_representsRelSubPic_baseChange R c ε₂ D₂ h₂ R').choose
    let θ : SchemeHomOver D₁.toBase D₂.toBase := (exists_theta ε₁ ε₂ h₁ h₂).choose
    let θ' : SchemeHomOver (D₁.baseChange R').toBase (D₂.baseChange R').toBase :=
      (exists_theta (sectionBaseChange R' ε₁) (sectionBaseChange R' ε₂) h₁' h₂').choose
    θ'.1 ≫ pullback.fst D₂.toBase (specMap R R') =
      pullback.fst D₁.toBase (specMap R R') ≫ θ.1 := by
  intro h₁' h₂' θ θ'
  have hP₁ := (exists_representsRelSubPic_baseChange R c ε₁ D₁ h₁ R').choose_spec
  have hP₂ := (exists_representsRelSubPic_baseChange R c ε₂ D₂ h₂ R').choose_spec
  let t : (D₁.baseChange R').P ⟶ Spec (CommRingCat.of R') := (D₁.baseChange R').toBase
  let M : RigidifiedLineBundle (baseChange R c R') (sectionBaseChange R' ε₁) t := h₁'.poincare
  have hM : FibrewiseAlgEquivZero M := h₁'.poincare_mem
  have hid : h₁'.classify t M hM = ⟨𝟙 (D₁.baseChange R').P, Category.id_comp t⟩ :=
    (h₁'.classify_unique t M hM _
      ⟨(Scheme.Modules.pullbackCongr (baseChangeSnd_id (baseChange R c R') t)).app M.L ≪≫
        (Scheme.Modules.pullbackId (pullback (baseChange R c R') t)).app M.L⟩).symm
  have hθ' : postComp θ' (h₁'.classify t M hM) = h₂'.classify t
      (twist (sectionBaseChange R' ε₁) (sectionBaseChange R' ε₂) M)
      (twist_cut (sectionBaseChange R' ε₁) (sectionBaseChange R' ε₂) t M hM) :=
    (exists_theta (sectionBaseChange R' ε₁) (sectionBaseChange R' ε₂) h₁' h₂').choose_spec t M hM
  rw [hid] at hθ'
  have hθ'val : θ'.1 = (h₂'.classify t
      (twist (sectionBaseChange R' ε₁) (sectionBaseChange R' ε₂) M)
      (twist_cut (sectionBaseChange R' ε₁) (sectionBaseChange R' ε₂) t M hM)).1 := by
    simpa only [postComp, Category.id_comp] using congrArg Subtype.val hθ'
  have hfst := classify_baseChange_fst ε₁ D₁ h₁ R' h₁' hP₁ t M hM
  rw [hid, Category.id_comp] at hfst
  rw [hθ'val, classify_baseChange_fst ε₂ D₂ h₂ R' h₂' hP₂, hfst]
  have hθ : postComp θ (h₁.classify (t ≫ specMap R R') (toR c ε₁ R' M)
      ((fibrewiseAlgEquivZero_toR_iff c ε₁ R' M).2 hM)) =
      h₂.classify (t ≫ specMap R R') (twist ε₁ ε₂ (toR c ε₁ R' M))
        (twist_cut ε₁ ε₂ (t ≫ specMap R R') (toR c ε₁ R' M)
          ((fibrewiseAlgEquivZero_toR_iff c ε₁ R' M).2 hM)) :=
    (exists_theta ε₁ ε₂ h₁ h₂).choose_spec (t ≫ specMap R R')
      (toR c ε₁ R' M) ((fibrewiseAlgEquivZero_toR_iff c ε₁ R' M).2 hM)
  refine (congrArg Subtype.val (classify_congr h₂ (t ≫ specMap R R') _ _ _
    (twist_cut ε₁ ε₂ (t ≫ specMap R R') (toR c ε₁ R' M)
      ((fibrewiseAlgEquivZero_toR_iff c ε₁ R' M).2 hM))
    ⟨toR_twistIso ε₁ ε₂ R' M⟩)).trans ?_
  exact (congrArg Subtype.val hθ).symm

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