NYLL
Module

abelJacobi_comp_eq_mul_abelJacobi_of_iso_of_classify.lean

Nyll.JacobianVarieties.Picard.abelJacobi_comp_eq_mul_abelJacobi_of_iso_of_classify
24 declarations indexed from sourceView source ↗

Module documentation

Abel–Jacobi morphisms under a curve isomorphism

Classified transport along a curve isomorphism compares the two Abel–Jacobi morphisms.

Imports24
Imported by1

Declarations

def

inverseIso

L68 ↗
JacobianVarieties.Picard.Proofs.AbelJacobiIsoComparison.Sub2c.inverseIso
Documentation

Tensor inverses of isomorphic objects are isomorphic via the given inverse evaluations.

Source context 14 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AbelJacobiIsoComparison
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open _root_.AlgebraicGeometry.RelPicard
universe u
noncomputable section
namespace Sub2c
section Monoidal
variable {𝒞 : Type*} [Category 𝒞] [MonoidalCategory 𝒞] [SymmetricCategory 𝒞]
Lean source · statement
def inverseIso {X X' Q Q' : 𝒞} (eX : X ≅ X') (hQ : X ⊗ Q ≅ 𝟙_ 𝒞) (hQ' : X' ⊗ Q' ≅ 𝟙_ 𝒞) : Q ≅ Q'
def

inverseOfIso

L73 ↗
JacobianVarieties.Picard.Proofs.AbelJacobiIsoComparison.Sub2c.inverseOfIso
Documentation

Transport the given tensor-inverse evaluation along an isomorphism of its first factor.

Source context 14 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AbelJacobiIsoComparison
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open _root_.AlgebraicGeometry.RelPicard
universe u
noncomputable section
namespace Sub2c
section Monoidal
variable {𝒞 : Type*} [Category 𝒞] [MonoidalCategory 𝒞] [SymmetricCategory 𝒞]
Lean source · statement
def inverseOfIso {X Y Q : 𝒞} (eX : X ≅ Y) (hQ : X ⊗ Q ≅ 𝟙_ 𝒞) : Y ⊗ Q ≅ 𝟙_ 𝒞
theorem

rigSection_snd

L82 ↗
JacobianVarieties.Picard.Proofs.AbelJacobiIsoComparison.Sub2c.rigSection_snd
Source context 14 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AbelJacobiIsoComparison
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open _root_.AlgebraicGeometry.RelPicard
universe u
noncomputable section
namespace Sub2c
section Modules
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
Lean source · statement
theorem rigSection_snd {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R))
    (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c) :
    rigSection c t ε ≫ pullback.snd c t = 𝟙 T
def

sectionPullbackIso

L88 ↗
JacobianVarieties.Picard.Proofs.AbelJacobiIsoComparison.Sub2c.sectionPullbackIso
Documentation

Pulling a base module to the curve and then back along the section recovers that module.

Source context 14 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AbelJacobiIsoComparison
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open _root_.AlgebraicGeometry.RelPicard
universe u
noncomputable section
namespace Sub2c
section Modules
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
Lean source · statement
def sectionPullbackIso {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R))
    (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c) (Q : T.Modules) :
    (Scheme.Modules.pullback (rigSection c t ε)).obj ((Scheme.Modules.pullback (pullback.snd c
      t)).obj Q) ≅ Q
theorem

nonempty_iso_unit_of_field

L98 ↗
JacobianVarieties.Picard.Proofs.AbelJacobiIsoComparison.Sub2c.nonempty_iso_unit_of_field
Source context 12 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AbelJacobiIsoComparison
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open _root_.AlgebraicGeometry.RelPicard
universe u
noncomputable section
namespace Sub2c
Lean source · statement
theorem nonempty_iso_unit_of_field {k : Type u} [Field k] (Q : (Spec (CommRingCat.of k)).Modules)
    (hQ : Scheme.Modules.IsInvertible Q) : Nonempty (Q ≅ 𝟙_ (Spec (CommRingCat.of k)).Modules)
def

qinv

L123 ↗
JacobianVarieties.Picard.Proofs.AbelJacobiIsoComparison.Sub2c.qinv
Documentation

A chosen tensor inverse of the line bundle restricted to the second rigidifying section.

Source context 14 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AbelJacobiIsoComparison
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open _root_.AlgebraicGeometry.RelPicard
universe u
noncomputable section
namespace Sub2c
section Twist
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
  (ε₁ ε₂ : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
Lean source · statement
def qinv {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
    (M : RigidifiedLineBundle c ε₁ t) : T.Modules
theorem

qinv_isInvertible

L127 ↗
JacobianVarieties.Picard.Proofs.AbelJacobiIsoComparison.Sub2c.qinv_isInvertible
Source context 14 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AbelJacobiIsoComparison
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open _root_.AlgebraicGeometry.RelPicard
universe u
noncomputable section
namespace Sub2c
section Twist
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
  (ε₁ ε₂ : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
Lean source · statement
theorem qinv_isInvertible {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
    (M : RigidifiedLineBundle c ε₁ t) :
    Scheme.Modules.IsInvertible (qinv ε₁ ε₂ M)
def

qinvIso

L133 ↗
JacobianVarieties.Picard.Proofs.AbelJacobiIsoComparison.Sub2c.qinvIso
Documentation

The chosen inverse evaluates the restriction at the second section to the unit module.

Source context 14 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AbelJacobiIsoComparison
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open _root_.AlgebraicGeometry.RelPicard
universe u
noncomputable section
namespace Sub2c
section Twist
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
  (ε₁ ε₂ : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
Lean source · statement
def qinvIso {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
    (M : RigidifiedLineBundle c ε₁ t) :
    (Scheme.Modules.pullback (rigSection c t ε₂)).obj M.L ⊗ qinv ε₁ ε₂ M ≅ 𝟙_ _
def

twist

L139 ↗
JacobianVarieties.Picard.Proofs.AbelJacobiIsoComparison.Sub2c.twist
Documentation

Change the rigidifying section using the inverse of the restricted line bundle.

Source context 14 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AbelJacobiIsoComparison
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open _root_.AlgebraicGeometry.RelPicard
universe u
noncomputable section
namespace Sub2c
section Twist
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
  (ε₁ ε₂ : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
Lean source · full declaration
def twist {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
    (M : RigidifiedLineBundle c ε₁ t) :
    RigidifiedLineBundle c ε₂ t where
  L := M.L ⊗ (Scheme.Modules.pullback (pullback.snd c t)).obj (qinv ε₁ ε₂ M)
  isInvertible := M.isInvertible.tensor ((qinv_isInvertible ε₁ ε₂ M).pullback _)
  rigidified := ⟨Scheme.Modules.pullbackTensorObjIso _ _ _ ≪≫
    whiskerLeftIso _ (sectionPullbackIso t ε₂ _) ≪≫ qinvIso ε₁ ε₂ M⟩
theorem

twist_L

L147 ↗
JacobianVarieties.Picard.Proofs.AbelJacobiIsoComparison.Sub2c.twist_L
Source context 14 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AbelJacobiIsoComparison
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open _root_.AlgebraicGeometry.RelPicard
universe u
noncomputable section
namespace Sub2c
section Twist
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
  (ε₁ ε₂ : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
Lean source · statement
theorem twist_L {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)} (M : RigidifiedLineBundle c ε₁ t)
    :
    (twist ε₁ ε₂ M).L = M.L ⊗ (Scheme.Modules.pullback (pullback.snd c t)).obj (qinv ε₁ ε₂ M)
theorem

twist_cut

L151 ↗
JacobianVarieties.Picard.Proofs.AbelJacobiIsoComparison.Sub2c.twist_cut
Source context 14 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AbelJacobiIsoComparison
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open _root_.AlgebraicGeometry.RelPicard
universe u
noncomputable section
namespace Sub2c
section Twist
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
  (ε₁ ε₂ : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
Lean source · statement
theorem twist_cut {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R))
    (M : RigidifiedLineBundle c ε₁ t)
    (hM : FibrewiseAlgEquivZero M) : FibrewiseAlgEquivZero (twist ε₁ ε₂ M)
theorem

classify_congr

L180 ↗
JacobianVarieties.Picard.Proofs.AbelJacobiIsoComparison.Sub2c.classify_congr
Source context 14 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AbelJacobiIsoComparison
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open _root_.AlgebraicGeometry.RelPicard
universe u
noncomputable section
namespace Sub2c
section Rep
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
  (ε₁ ε₂ : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
  {D₁ D₂ : RelativePic0Designation R c}
  (h₁ : RepresentsRelSubPic c ε₁ (algEquivZeroCut c ε₁) D₁)
  (h₂ : RepresentsRelSubPic c ε₂ (algEquivZeroCut c ε₂) D₂)
Lean source · statement
theorem classify_congr {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c} {P : SubPicCondition c ε}
    {D : RelativePic0Designation R c}
    (h : RepresentsRelSubPic c ε P D) {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R))
    (M M' : RigidifiedLineBundle c ε t) (hM : P.P t M) (hM' : P.P t M') (i : Nonempty (M.L ≅ M'.L))
      :
    h.classify t M hM = h.classify t M' hM'
def

epsT

L203 ↗
JacobianVarieties.Picard.Proofs.AbelJacobiIsoComparison.I2.epsT
Documentation

Transport the section along the specified inverse curve morphism.

Source context 14 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AbelJacobiIsoComparison
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open _root_.AlgebraicGeometry.RelPicard
universe u
noncomputable section
namespace I2
section Transform
variable {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) (g : C ⟶ C') (hf : f ≫ c = c') (hg : g ≫ c' = c) (hgf : g ≫ f = 𝟙 C)
Lean source · statement
def epsT : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c'
theorem

epsT_comp

L207 ↗
JacobianVarieties.Picard.Proofs.AbelJacobiIsoComparison.I2.epsT_comp
Source context 15 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AbelJacobiIsoComparison
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open _root_.AlgebraicGeometry.RelPicard
universe u
noncomputable section
namespace I2
section Transform
variable {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) (g : C ⟶ C') (hf : f ≫ c = c') (hg : g ≫ c' = c) (hgf : g ≫ f = 𝟙 C)
include hgf in
Lean source · statement
theorem epsT_comp : (epsT ε g hg).1 ≫ f = ε.1
def

Phi

L212 ↗
JacobianVarieties.Picard.Proofs.AbelJacobiIsoComparison.I2.Phi
Documentation

Pull back the line bundle and adjust its rigidifying section.

Source context 14 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AbelJacobiIsoComparison
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open _root_.AlgebraicGeometry.RelPicard
universe u
noncomputable section
namespace I2
section Transform
variable {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) (g : C ⟶ C') (hf : f ≫ c = c') (hg : g ≫ c' = c) (hgf : g ≫ f = 𝟙 C)
Lean source · statement
def Phi {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) (M : RigidifiedLineBundle c ε t) :
    RigidifiedLineBundle c' ε' t
theorem

Phi_L

L216 ↗
JacobianVarieties.Picard.Proofs.AbelJacobiIsoComparison.I2.Phi_L
Source context 14 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AbelJacobiIsoComparison
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open _root_.AlgebraicGeometry.RelPicard
universe u
noncomputable section
namespace I2
section Transform
variable {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) (g : C ⟶ C') (hf : f ≫ c = c') (hg : g ≫ c' = c) (hgf : g ≫ f = 𝟙 C)
Lean source · statement
theorem Phi_L {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) (M : RigidifiedLineBundle c ε t) :
    (Phi ε ε' f g hf hg hgf t M).L =
      (Scheme.Modules.pullback (curveChange f hf t)).obj M.L ⊗
        (Scheme.Modules.pullback (pullback.snd c' t)).obj
          (Sub2c.qinv (epsT ε g hg) ε' (M.pullbackCurve f hf (epsT_comp ε f g hg hgf)))
theorem

Phi_cut

L222 ↗
JacobianVarieties.Picard.Proofs.AbelJacobiIsoComparison.I2.Phi_cut
Source context 14 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AbelJacobiIsoComparison
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open _root_.AlgebraicGeometry.RelPicard
universe u
noncomputable section
namespace I2
section Transform
variable {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) (g : C ⟶ C') (hf : f ≫ c = c') (hg : g ≫ c' = c) (hgf : g ≫ f = 𝟙 C)
Lean source · statement
theorem Phi_cut {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) (M : RigidifiedLineBundle c ε t)
    (hM : FibrewiseAlgEquivZero M) : FibrewiseAlgEquivZero (Phi ε ε' f g hf hg hgf t M)
theorem

curveChange_comp_eq_id

L227 ↗
JacobianVarieties.Picard.Proofs.AbelJacobiIsoComparison.I2.curveChange_comp_eq_id
Source context 15 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AbelJacobiIsoComparison
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open _root_.AlgebraicGeometry.RelPicard
universe u
noncomputable section
namespace I2
section Transform
variable {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) (g : C ⟶ C') (hf : f ≫ c = c') (hg : g ≫ c' = c) (hgf : g ≫ f = 𝟙 C)
include hgf in
Lean source · statement
theorem curveChange_comp_eq_id {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) :
    curveChange (c := c') (c' := c) g hg t ≫ curveChange (c := c) (c' := c') f hf t = 𝟙 _
theorem

poincare_mul

L241 ↗
JacobianVarieties.Picard.Proofs.AbelJacobiIsoComparison.AJT.poincare_mul
Source context 12 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AbelJacobiIsoComparison
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open _root_.AlgebraicGeometry.RelPicard
universe u
noncomputable section
namespace AJT
Lean source · statement
theorem poincare_mul {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
    {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c}
    {P : SubPicGroupCondition c ε} {D : RelativePic0Designation R c}
    (h : RepresentsRelSubPic c ε P.toSubPicCondition D)
    {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) (x y : SchemeHomOver t D.toBase) :
    Nonempty ((h.poincare.pullbackAlong (h.relativeGroupLaw.mul t x y)).L ≅
      (h.poincare.pullbackAlong x).L ⊗ (h.poincare.pullbackAlong y).L)
theorem

isIso_curveChange

L258 ↗
JacobianVarieties.Picard.Proofs.AbelJacobiIsoComparison.AJT.isIso_curveChange
Source context 15 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AbelJacobiIsoComparison
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open _root_.AlgebraicGeometry.RelPicard
universe u
noncomputable section
namespace AJT
section Transport
variable {R : Type u} [CommRing R] {C C' : Scheme.{u}}
  {c : C ⟶ Spec (CommRingCat.of R)} {c' : C' ⟶ Spec (CommRingCat.of R)}
  (e : C ≅ C') (he : e.hom ≫ c' = c) (he' : e.inv ≫ c = c')
include he in
Lean source · statement
theorem isIso_curveChange {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) :
    IsIso (curveChange (c := c) (c' := c') e.inv he' t)
theorem

graphOver_comp_curveChange

L264 ↗
JacobianVarieties.Picard.Proofs.AbelJacobiIsoComparison.AJT.graphOver_comp_curveChange
Source context 14 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AbelJacobiIsoComparison
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open _root_.AlgebraicGeometry.RelPicard
universe u
noncomputable section
namespace AJT
section Transport
variable {R : Type u} [CommRing R] {C C' : Scheme.{u}}
  {c : C ⟶ Spec (CommRingCat.of R)} {c' : C' ⟶ Spec (CommRingCat.of R)}
  (e : C ≅ C') (he : e.hom ≫ c' = c) (he' : e.inv ≫ c = c')
Lean source · statement
theorem graphOver_comp_curveChange {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
    (a : T ⟶ C) (ha : a ≫ c = t) (a' : T ⟶ C') (ha' : a' ≫ c' = t) (haa' : a' = a ≫ e.hom) :
    graphOver c' a' ha' ≫ curveChange (c := c) (c' := c') e.inv he' t = graphOver c a ha
theorem

transport_ofPoint

L274 ↗
JacobianVarieties.Picard.Proofs.AbelJacobiIsoComparison.AJT.transport_ofPoint
Source context 15 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AbelJacobiIsoComparison
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open _root_.AlgebraicGeometry.RelPicard
universe u
noncomputable section
namespace AJT
section Transport
variable {R : Type u} [CommRing R] {C C' : Scheme.{u}}
  {c : C ⟶ Spec (CommRingCat.of R)} {c' : C' ⟶ Spec (CommRingCat.of R)}
  (e : C ≅ C') (he : e.hom ≫ c' = c) (he' : e.inv ≫ c = c')
include he in
Lean source · statement
theorem transport_ofPoint [IsSeparated c] [SmoothOfRelativeDimension 1 c]
    [IsSeparated c'] [SmoothOfRelativeDimension 1 c']
    {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
    (a : T ⟶ C) (ha : a ≫ c = t) (a' : T ⟶ C') (ha' : a' ≫ c' = t) (haa' : a' = a ≫ e.hom) :
    Nonempty ((Scheme.Modules.pullback (curveChange (c := c) (c' := c') e.inv he' t)).obj
        (RelEffCartierDiv.ofPoint c a ha).lineBundle ≅ (RelEffCartierDiv.ofPoint c' a'
          ha').lineBundle) ∧
    Nonempty ((Scheme.Modules.pullback (curveChange (c := c) (c' := c') e.inv he' t)).obj
        (RelEffCartierDiv.ofPoint c a ha).idealModule ≅ (RelEffCartierDiv.ofPoint c' a'
          ha').idealModule)
theorem

Phi_L_iso_of_field

L303 ↗
JacobianVarieties.Picard.Proofs.AbelJacobiIsoComparison.AJT.Phi_L_iso_of_field
Source context 12 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AbelJacobiIsoComparison
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open _root_.AlgebraicGeometry.RelPicard
universe u
noncomputable section
namespace AJT
Lean source · statement
theorem Phi_L_iso_of_field {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) (g : C ⟶ C') (hf : f ≫ c = c') (hg : g ≫ c' = c) (hgf : g ≫ f = 𝟙 C)
    {K : Type u} [Field K] (t : Spec (CommRingCat.of K) ⟶ Spec (CommRingCat.of R)) (M :
      RigidifiedLineBundle c ε t) :
    Nonempty ((I2.Phi ε ε' f g hf hg hgf t M).L ≅ (Scheme.Modules.pullback (curveChange f hf
      t)).obj M.L)
theorem

abelJacobi_comp_eq_mul_abelJacobi_of_iso_of_classify

L336 ↗
AlgebraicGeometry.RelPicard.abelJacobi_comp_eq_mul_abelJacobi_of_iso_of_classify
Documentation

Classified transport along a curve isomorphism compares the two Abel–Jacobi morphisms.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicGeometry.RelPicard
open _root_.JacobianVarieties.Picard.Proofs.AbelJacobiIsoComparison
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open _root_.AlgebraicGeometry.RelPicard
universe u
Lean source · full declaration
theorem abelJacobi_comp_eq_mul_abelJacobi_of_iso_of_classify
    {R : Type u} [CommRing R] {C C' : Scheme.{u}}
    {c : C ⟶ Spec (CommRingCat.of R)} {c' : C' ⟶ Spec (CommRingCat.of R)}
    [IsProper c] [SmoothOfRelativeDimension 1 c] [GeometricallyIntegral c]
    [IsProper c'] [SmoothOfRelativeDimension 1 c'] [GeometricallyIntegral c']
    (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c) (ε' : SchemeHomOver (𝟙 (Spec
      (CommRingCat.of R))) c')
    (e : C ≅ C') (he : e.hom ≫ c' = c) (he' : e.inv ≫ c = c')
    {D : RelativePic0Designation R c} {D' : RelativePic0Designation R c'}
    (h : RepresentsRelSubPic c ε (algEquivZeroCut c ε) D)
    (h' : RepresentsRelSubPic c' ε' (algEquivZeroCut c' ε') D')
    (aj : SchemeHomOver c D.toBase) (aj' : SchemeHomOver c' D'.toBase)
    (haj : ∀ (K : Type u) [Field K] (t : Spec (CommRingCat.of K) ⟶ Spec (CommRingCat.of R)) (x :
      SchemeHomOver t c),
        Nonempty ((h.poincare.pullbackAlong
            ⟨x.1 ≫ aj.1, (Category.assoc _ _ _).trans ((congrArg (x.1 ≫ ·) aj.2).trans x.2)⟩).L ≅
          (RelEffCartierDiv.ofPoint c x.1 x.2).lineBundle ⊗
            (RelEffCartierDiv.ofPoint c (t ≫ ε.1)
              ((Category.assoc _ _ _).trans ((congrArg (t ≫ ·) ε.2).trans (Category.comp_id
                t)))).idealModule))
    (haj' : ∀ (K : Type u) [Field K] (t : Spec (CommRingCat.of K) ⟶ Spec (CommRingCat.of R)) (x :
      SchemeHomOver t c'),
        Nonempty ((h'.poincare.pullbackAlong
            ⟨x.1 ≫ aj'.1, (Category.assoc _ _ _).trans ((congrArg (x.1 ≫ ·) aj'.2).trans x.2)⟩).L ≅
          (RelEffCartierDiv.ofPoint c' x.1 x.2).lineBundle ⊗
            (RelEffCartierDiv.ofPoint c' (t ≫ ε'.1)
              ((Category.assoc _ _ _).trans ((congrArg (t ≫ ·) ε'.2).trans (Category.comp_id
                t)))).idealModule))
    (θ : SchemeHomOver D.toBase D'.toBase)
    (hθ : ∀ {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R))
        (M : RigidifiedLineBundle c ε t) (hM : FibrewiseAlgEquivZero M)
        (N : RigidifiedLineBundle c' ε' t) (hN : FibrewiseAlgEquivZero N)
        (Q : T.Modules), Scheme.Modules.IsInvertible Q →
        Nonempty (N.L ≅ (Scheme.Modules.pullback (curveChange (c := c) (c' := c') e.inv he' t)).obj
          M.L ⊗
          (Scheme.Modules.pullback (pullback.snd c' t)).obj Q) →
        postComp θ (h.classify t M hM) = h'.classify t N hN)
    (K : Type u) [Field K] (t : Spec (CommRingCat.of K) ⟶ Spec (CommRingCat.of R)) (x :
      SchemeHomOver t c) :
    (RepresentsRelSubPic.relativeGroupLaw (P := algEquivZeroGroupCut c' ε') h').mul t
        ⟨x.1 ≫ aj.1 ≫ θ.1, by rw [Category.assoc, Category.assoc, θ.2, aj.2, x.2]⟩
        ⟨t ≫ ε.1 ≫ e.hom ≫ aj'.1, by
          rw [Category.assoc, Category.assoc, Category.assoc, aj'.2, he, ε.2, Category.comp_id]⟩ =
      ⟨(x.1 ≫ e.hom) ≫ aj'.1, by rw [Category.assoc, Category.assoc, aj'.2, he, x.2]⟩ := by
  let a : SchemeHomOver t D.toBase :=
    ⟨x.1 ≫ aj.1, (Category.assoc _ _ _).trans ((congrArg (x.1 ≫ ·) aj.2).trans x.2)⟩
  have hAa : (⟨x.1 ≫ aj.1 ≫ θ.1, by rw [Category.assoc, Category.assoc, θ.2, aj.2, x.2]⟩ :
      SchemeHomOver t D'.toBase) = postComp θ a := Subtype.ext (Category.assoc _ _ _).symm
  have pε : (t ≫ ε.1) ≫ c = t := (Category.assoc _ _ _).trans ((congrArg (t ≫ ·) ε.2).trans
    (Category.comp_id t))
  have peε : (t ≫ ε.1 ≫ e.hom) ≫ c' = t := by
    rw [Category.assoc, Category.assoc, he, ε.2, Category.comp_id]
  have pex : (x.1 ≫ e.hom) ≫ c' = t := by rw [Category.assoc, he, x.2]
  let xB : SchemeHomOver t c' := ⟨t ≫ ε.1 ≫ e.hom, peε⟩
  let xg : SchemeHomOver t c' := ⟨x.1 ≫ e.hom, pex⟩
  have hB : (⟨t ≫ ε.1 ≫ e.hom ≫ aj'.1, by
          rw [Category.assoc, Category.assoc, Category.assoc, aj'.2, he, ε.2, Category.comp_id]⟩ :
      SchemeHomOver t D'.toBase) =
      ⟨xB.1 ≫ aj'.1, (Category.assoc _ _ _).trans ((congrArg (xB.1 ≫ ·) aj'.2).trans xB.2)⟩ :=
    Subtype.ext (by simp only [xB, Category.assoc])
  rw [hAa, hB]
  let M : RigidifiedLineBundle c ε t := h.poincare.pullbackAlong a
  have hM : FibrewiseAlgEquivZero M := (algEquivZeroCut c ε).pullback_mem _ _ a _ h.poincare_mem
  have ha : a = h.classify t M hM := h.classify_unique _ M hM a ⟨Iso.refl _⟩
  have hθa : postComp θ a = h'.classify t (I2.Phi ε ε' e.inv e.hom he' he e.hom_inv_id t M)
      (I2.Phi_cut ε ε' e.inv e.hom he' he e.hom_inv_id t M hM) := by
    conv_lhs => rw [ha]
    exact hθ t M hM _ _ _ (Sub2c.qinv_isInvertible _ ε' _) ⟨Iso.refl _⟩
  obtain ⟨e1⟩ : Nonempty ((h'.poincare.pullbackAlong (postComp θ a)).L ≅
      (I2.Phi ε ε' e.inv e.hom he' he e.hom_inv_id t M).L) := by
    rw [hθa]
    exact h'.classify_spec _ _ _
  obtain ⟨e2⟩ := AJT.Phi_L_iso_of_field ε ε' e.inv e.hom he' he e.hom_inv_id t M
  obtain ⟨iM⟩ := haj K t x
  obtain ⟨iB⟩ := haj' K t xB
  obtain ⟨ig⟩ := haj' K t xg
  obtain ⟨⟨T1⟩, -⟩ := AJT.transport_ofPoint e he he' x.1 x.2 (x.1 ≫ e.hom) pex rfl
  obtain ⟨-, ⟨T2⟩⟩ := AJT.transport_ofPoint e he he' (t ≫ ε.1) pε (t ≫ ε.1 ≫ e.hom) peε
    (Category.assoc _ _ _).symm
  obtain ⟨dd⟩ := ((RelEffCartierDiv.ofPoint c' (t ≫ ε.1 ≫ e.hom)
    peε).isInvertible_I).isInvertible_module.dual.2
  have key : (I2.Phi ε ε' e.inv e.hom he' he e.hom_inv_id t M).L ⊗
      (h'.poincare.pullbackAlong
        ⟨xB.1 ≫ aj'.1, (Category.assoc _ _ _).trans ((congrArg (xB.1 ≫ ·) aj'.2).trans xB.2)⟩).L ≅
      (h'.poincare.pullbackAlong
        ⟨xg.1 ≫ aj'.1, (Category.assoc _ _ _).trans ((congrArg (xg.1 ≫ ·) aj'.2).trans xg.2)⟩).L :=
    ((e2 ≪≫ (Scheme.Modules.pullback _).mapIso iM ≪≫ Scheme.Modules.pullbackTensorObjIso _ _ _ ≪≫
        (T1 ⊗ᵢ T2)) ⊗ᵢ iB) ≪≫
      α_ _ _ _ ≪≫ whiskerLeftIso _ ((α_ _ _ _).symm ≪≫ (dd ⊗ᵢ Iso.refl _) ≪≫ λ_ _) ≪≫ ig.symm
  obtain ⟨emul⟩ := AJT.poincare_mul (P := algEquivZeroGroupCut c' ε') h' t (postComp θ a)
    ⟨xB.1 ≫ aj'.1, (Category.assoc _ _ _).trans ((congrArg (xB.1 ≫ ·) aj'.2).trans xB.2)⟩
  exact h'.ext_of_iso t _ _ ⟨emul ≪≫ (e1 ⊗ᵢ Iso.refl _) ≪≫ key⟩

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