Nyll.JacobianVarieties.Picard.RigidifiedLineBundleTwistCoherence

theorem

twist_trans

JacobianVarieties.Picard.Proofs.InversePairSections.Sub2c.twist_trans

Documentation

Two changes of rigidifying section give the same underlying line bundle as the direct change.

Source context 4 commands

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

open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory
open AlgebraicGeometry AlgebraicGeometry.RelPicard NeronModelInfra
universe u
namespace JacobianVarieties.Picard.Proofs.InversePairSections.Sub2c

Lean source · statement

theorem twist_trans {R : Type u} [CommRing R] {C : Scheme.{u}}
    {c : C ⟶ Spec (CommRingCat.of R)}
    (ε₁ ε₂ ε₃ : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
    {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
    (M : RigidifiedLineBundle c ε₁ t) :
    Nonempty ((twist ε₂ ε₃ (twist ε₁ ε₂ M)).L ≅ (twist ε₁ ε₃ M).L)

theorem

sectionComparison_comp

L73 ↗

JacobianVarieties.Picard.Proofs.InversePairSections.Sub2c.sectionComparison_comp

Documentation

The comparison morphisms constructed by changing rigidifying sections compose as the direct change from the first section to the third.

Source context 5 commands

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

open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory
open AlgebraicGeometry AlgebraicGeometry.RelPicard NeronModelInfra
universe u
namespace JacobianVarieties.Picard.Proofs.InversePairSections.Sub2c
open GoodReductionJacobian

Lean source · full declaration

theorem sectionComparison_comp {R : Type u} [CommRing R] {C : Scheme.{u}}
    {c : C ⟶ Spec (CommRingCat.of R)}
    (ε₁ ε₂ ε₃ : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
    {D₁ D₂ D₃ : RelativePic0Designation R c}
    (h₁ : RepresentsRelSubPic c ε₁ (algEquivZeroCut c ε₁) D₁)
    (h₂ : RepresentsRelSubPic c ε₂ (algEquivZeroCut c ε₂) D₂)
    (h₃ : RepresentsRelSubPic c ε₃ (algEquivZeroCut c ε₃) D₃) :
    let θ₁₂ : SchemeHomOver D₁.toBase D₂.toBase := (exists_theta ε₁ ε₂ h₁ h₂).choose
    let θ₂₃ : SchemeHomOver D₂.toBase D₃.toBase := (exists_theta ε₂ ε₃ h₂ h₃).choose
    let θ₁₃ : SchemeHomOver D₁.toBase D₃.toBase := (exists_theta ε₁ ε₃ h₁ h₃).choose
    θ₁₂.1 ≫ θ₂₃.1 = θ₁₃.1 := by
  intro θ₁₂ θ₂₃ θ₁₃
  have h₁₂ := (exists_theta ε₁ ε₂ h₁ h₂).choose_spec (T := D₁.P)
  have h₂₃ := (exists_theta ε₂ ε₃ h₂ h₃).choose_spec (T := D₁.P)
  have h₁₃ := (exists_theta ε₁ ε₃ h₁ h₃).choose_spec (T := D₁.P)
  have hid : h₁.classify D₁.toBase h₁.poincare h₁.poincare_mem =
      ⟨𝟙 D₁.P, Category.id_comp D₁.toBase⟩ :=
    (h₁.classify_unique D₁.toBase h₁.poincare h₁.poincare_mem _
      ⟨(Scheme.Modules.pullbackCongr (baseChangeSnd_id c D₁.toBase)).app h₁.poincare.L ≪≫
        (Scheme.Modules.pullbackId (pullback c D₁.toBase)).app h₁.poincare.L⟩).symm
  have key : postComp (postComp θ₂₃ θ₁₂)
        (h₁.classify D₁.toBase h₁.poincare h₁.poincare_mem) =
      postComp θ₁₃ (h₁.classify D₁.toBase h₁.poincare h₁.poincare_mem) := by
    have step : postComp (postComp θ₂₃ θ₁₂)
          (h₁.classify D₁.toBase h₁.poincare h₁.poincare_mem) =
        postComp θ₂₃ (postComp θ₁₂
          (h₁.classify D₁.toBase h₁.poincare h₁.poincare_mem)) :=
      Subtype.ext (Category.assoc _ _ _).symm
    refine step.trans ((congrArg (postComp θ₂₃)
      (h₁₂ D₁.toBase h₁.poincare h₁.poincare_mem)).trans ?_)
    refine (h₂₃ D₁.toBase (twist ε₁ ε₂ h₁.poincare)
      (twist_cut ε₁ ε₂ D₁.toBase h₁.poincare h₁.poincare_mem)).trans ?_
    refine (classify_congr h₃ D₁.toBase
      (twist ε₂ ε₃ (twist ε₁ ε₂ h₁.poincare)) (twist ε₁ ε₃ h₁.poincare)
      (twist_cut ε₂ ε₃ D₁.toBase (twist ε₁ ε₂ h₁.poincare)
        (twist_cut ε₁ ε₂ D₁.toBase h₁.poincare h₁.poincare_mem))
      (twist_cut ε₁ ε₃ D₁.toBase h₁.poincare h₁.poincare_mem)
      (twist_trans ε₁ ε₂ ε₃ h₁.poincare)).trans ?_
    exact (h₁₃ D₁.toBase h₁.poincare h₁.poincare_mem).symm
  rw [hid] at key
  have hval := congrArg Subtype.val key
  simpa only [postComp, Category.id_comp] using hval

RigidifiedLineBundleTwistCoherence.lean

Module documentation

Composition of changes of rigidifying section

twist_trans

sectionComparison_comp

Module documentation

Composition of changes of rigidifying section

Declarations

twist_trans

sectionComparison_comp