Module

CurveSectionComparisonCoherence.lean

Nyll.JacobianVarieties.Picard.CurveSectionComparisonCoherence

2 declarations indexed from sourceView source ↗

Module documentation

Composition of curve and rigidifying-section comparisons

The tensor corrections for two curve isomorphisms combine into the correction for their composite. Classification of the resulting families proves the cocycle equation for the actual comparison morphisms over any commutative base ring.

Imports4

Imported by1

Nyll.JacobianVarieties.Picard.All

theorem

transport_comp

L41 ↗

JacobianVarieties.Picard.CurveSectionComparison.transport_comp

Documentation

The underlying families agree for successive and composite curve comparisons.

Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory
open AlgebraicGeometry AlgebraicGeometry.RelPicard NeronModelInfra GoodReductionJacobian
open JacobianVarieties.Picard.Proofs.InversePairIsoSections
namespace JacobianVarieties.Picard.CurveSectionComparison
variable {R : Type u} [CommRing R] {C₁ C₂ C₃ : Scheme.{u}}
  {c₁ : C₁ ⟶ Spec (CommRingCat.of R)} {c₂ : C₂ ⟶ Spec (CommRingCat.of R)}
  {c₃ : C₃ ⟶ Spec (CommRingCat.of R)}

Lean source · full declaration

theorem transport_comp
    (ε₁ : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c₁)
    (ε₂ : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c₂)
    (ε₃ : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c₃)
    (e₁₂ : C₁ ≅ C₂) (e₂₃ : C₂ ≅ C₃)
    (h₁₂ : e₁₂.hom ≫ c₂ = c₁) (h₁₂' : e₁₂.inv ≫ c₁ = c₂)
    (h₂₃ : e₂₃.hom ≫ c₃ = c₂) (h₂₃' : e₂₃.inv ≫ c₂ = c₃)
    {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R))
    (M : RigidifiedLineBundle c₁ ε₁ t) :
    let h₁₃ : (e₁₂ ≪≫ e₂₃).hom ≫ c₃ = c₁ :=
      (Category.assoc _ _ _).trans ((congrArg (e₁₂.hom ≫ ·) h₂₃).trans h₁₂)
    let h₁₃' : (e₁₂ ≪≫ e₂₃).inv ≫ c₁ = c₃ :=
      (Category.assoc _ _ _).trans ((congrArg (e₂₃.inv ≫ ·) h₁₂').trans h₂₃')
    Nonempty ((I2.Phi ε₂ ε₃ e₂₃.inv e₂₃.hom h₂₃' h₂₃ e₂₃.hom_inv_id t
      (I2.Phi ε₁ ε₂ e₁₂.inv e₁₂.hom h₁₂' h₁₂ e₁₂.hom_inv_id t M)).L ≅
      (I2.Phi ε₁ ε₃ (e₁₂ ≪≫ e₂₃).inv (e₁₂ ≪≫ e₂₃).hom h₁₃' h₁₃
        (e₁₂ ≪≫ e₂₃).hom_inv_id t M).L) := by
  intro h₁₃ h₁₃'
  let N : RigidifiedLineBundle c₂ ε₂ t :=
    I2.Phi ε₁ ε₂ e₁₂.inv e₁₂.hom h₁₂' h₁₂ e₁₂.hom_inv_id t M
  let M₁₂ := M.pullbackCurve e₁₂.inv h₁₂'
    (I2.epsT_comp ε₁ e₁₂.inv e₁₂.hom h₁₂ e₁₂.hom_inv_id)
  let N₂₃ := N.pullbackCurve e₂₃.inv h₂₃'
    (I2.epsT_comp ε₂ e₂₃.inv e₂₃.hom h₂₃ e₂₃.hom_inv_id)
  let M₁₃ := M.pullbackCurve (e₁₂ ≪≫ e₂₃).inv h₁₃'
    (I2.epsT_comp ε₁ (e₁₂ ≪≫ e₂₃).inv (e₁₂ ≪≫ e₂₃).hom h₁₃
      (e₁₂ ≪≫ e₂₃).hom_inv_id)
  let Q₁₂ : T.Modules := Sub2c.qinv (I2.epsT ε₁ e₁₂.hom h₁₂) ε₂ M₁₂
  let Q₂₃ : T.Modules := Sub2c.qinv (I2.epsT ε₂ e₂₃.hom h₂₃) ε₃ N₂₃
  let Q₁₃ : T.Modules := Sub2c.qinv (I2.epsT ε₁ (e₁₂ ≪≫ e₂₃).hom h₁₃) ε₃ M₁₃
  have hcc : curveChange e₂₃.inv h₂₃' t ≫ curveChange e₁₂.inv h₁₂' t =
      curveChange (e₁₂ ≪≫ e₂₃).inv h₁₃' t := by
    apply pullback.hom_ext
    · simp only [curveChange, Category.assoc, pullback.lift_fst,
        pullback.lift_fst_assoc, Iso.trans_inv]
    · simp only [curveChange, Category.assoc, pullback.lift_snd,
        Category.comp_id]
  have hX : N₂₃.L ≅ M₁₃.L ⊗ (Scheme.Modules.pullback (pullback.snd c₃ t)).obj Q₁₂ :=
    Scheme.Modules.pullbackTensorObjIso (curveChange e₂₃.inv h₂₃' t) M₁₂.L
        ((Scheme.Modules.pullback (pullback.snd c₂ t)).obj Q₁₂) ≪≫
      (((Scheme.Modules.pullbackComp _ _).app M.L ≪≫
        (Scheme.Modules.pullbackCongr hcc).app M.L) ⊗ᵢ
       ((Scheme.Modules.pullbackComp _ _).app Q₁₂ ≪≫
        (Scheme.Modules.pullbackCongr (curveChange_snd e₂₃.inv h₂₃' t)).app Q₁₂))
  let A : T.Modules := (Scheme.Modules.pullback (rigSection c₃ t ε₃)).obj M₁₃.L
  have hEvaluation : A ⊗ (Q₁₂ ⊗ Q₂₃) ≅ 𝟙_ T.Modules :=
    (α_ A Q₁₂ Q₂₃).symm ≪≫
      whiskerRightIso
        ((whiskerLeftIso A (Sub2c.sectionPullbackIso t ε₃ Q₁₂)).symm ≪≫
          (Scheme.Modules.pullbackTensorObjIso (rigSection c₃ t ε₃) M₁₃.L
            ((Scheme.Modules.pullback (pullback.snd c₃ t)).obj Q₁₂)).symm ≪≫
          (Scheme.Modules.pullback (rigSection c₃ t ε₃)).mapIso hX.symm) Q₂₃ ≪≫
      Sub2c.qinvIso (I2.epsT ε₂ e₂₃.hom h₂₃) ε₃ N₂₃
  have hInverse : Q₁₂ ⊗ Q₂₃ ≅ Q₁₃ :=
    Sub2c.inverseIso (Iso.refl A) hEvaluation
      (Sub2c.qinvIso (I2.epsT ε₁ (e₁₂ ≪≫ e₂₃).hom h₁₃) ε₃ M₁₃)
  exact ⟨(hX ⊗ᵢ Iso.refl ((Scheme.Modules.pullback (pullback.snd c₃ t)).obj Q₂₃)) ≪≫
    α_ M₁₃.L ((Scheme.Modules.pullback (pullback.snd c₃ t)).obj Q₁₂)
      ((Scheme.Modules.pullback (pullback.snd c₃ t)).obj Q₂₃) ≪≫
    whiskerLeftIso M₁₃.L
      ((Scheme.Modules.pullbackTensorObjIso (pullback.snd c₃ t) Q₁₂ Q₂₃).symm ≪≫
        (Scheme.Modules.pullback (pullback.snd c₃ t)).mapIso hInverse)⟩

theorem

comparison_comp

L107 ↗

JacobianVarieties.Picard.CurveSectionComparison.comparison_comp