NYLL
Module

RepresentsRelSubPic_pullbackHom_inv_comp_pullbackHom_hom_of_iso.lean

Nyll.JacobianVarieties.Picard.RepresentsRelSubPic_pullbackHom_inv_comp_pullbackHom_hom_of_iso
5 declarations indexed from sourceView source ↗

Module documentation

Pullback by inverse curve isomorphisms

Composition and identity comparisons for curve pullback show that the induced morphisms of the represented relative Picard functors are mutually inverse.

Imports9
Imported by1

Declarations

theorem

classify_congr

L43 ↗
JacobianVarieties.Picard.Proofs.PullbackInverse.Sub2.classify_congr
Source context 7 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.PullbackInverse
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open NeronModelInfra GoodReductionJacobian AlgebraicGeometry.RelPicard
universe u
namespace Sub2
variable {R : Type u} [CommRing R]
Lean source · statement
theorem classify_congr {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
    {ε : 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'
theorem

curveChange_comp

L57 ↗
JacobianVarieties.Picard.Proofs.PullbackInverse.Sub2.curveChange_comp
Source context 8 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.PullbackInverse
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open NeronModelInfra GoodReductionJacobian AlgebraicGeometry.RelPicard
universe u
namespace Sub2
variable {R : Type u} [CommRing R]
variable {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'}
Lean source · statement
theorem curveChange_comp {C'' : Scheme.{u}} {c'' : C'' ⟶ Spec (CommRingCat.of R)}
    (f : C' ⟶ C) (hf : f ≫ c = c') (g : C'' ⟶ C') (hg : g ≫ c' = c'')
    (k : C'' ⟶ C) (hk : k ≫ c = c'') (hgf : g ≫ f = k)
    {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
      = curveChange (c := c) (c' := c'') k hk t
theorem

curveChange_id

L69 ↗
JacobianVarieties.Picard.Proofs.PullbackInverse.Sub2.curveChange_id
Source context 8 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.PullbackInverse
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open NeronModelInfra GoodReductionJacobian AlgebraicGeometry.RelPicard
universe u
namespace Sub2
variable {R : Type u} [CommRing R]
variable {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'}
Lean source · statement
theorem curveChange_id {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) :
    curveChange (c := c) (c' := c) (𝟙 C) (Category.id_comp c) t = 𝟙 _
theorem

comp_eq_id

L75 ↗
JacobianVarieties.Picard.Proofs.PullbackInverse.Sub2.comp_eq_id
Source context 8 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.PullbackInverse
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open NeronModelInfra GoodReductionJacobian AlgebraicGeometry.RelPicard
universe u
namespace Sub2
variable {R : Type u} [CommRing R]
variable {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'}
Lean source · statement
theorem comp_eq_id (f : C' ⟶ C) (hf : f ≫ c = c') (hεf : ε'.1 ≫ f = ε.1)
    (g : C ⟶ C') (hg : g ≫ c' = c) (hεg : ε.1 ≫ g = ε'.1) (hgf : g ≫ f = 𝟙 C)
    {D : RelativePic0Designation R c} {D' : RelativePic0Designation R c'}
    (h : RepresentsRelSubPic c ε (algEquivZeroCut c ε) D)
    (h' : RepresentsRelSubPic c' ε' (algEquivZeroCut c' ε') D') :
    (RepresentsRelSubPic.pullbackHom f hf hεf h h').1 ≫
      (RepresentsRelSubPic.pullbackHom g hg hεg h' h).1 = 𝟙 D.P
theorem

pullbackHom_inv_comp_pullbackHom_hom_of_iso

L126 ↗
AlgebraicGeometry.RelPicard.RepresentsRelSubPic.pullbackHom_inv_comp_pullbackHom_hom_of_iso
Source context 7 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.PullbackInverse
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open NeronModelInfra GoodReductionJacobian AlgebraicGeometry.RelPicard
universe u
open Sub2 renaming comp_eq_id → pullback_comp_eq_id in
with_weak_namespace _root_.AlgebraicGeometry.RelPicard.RepresentsRelSubPic
Lean source · statement
theorem pullbackHom_inv_comp_pullbackHom_hom_of_iso
    {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'}
    (e : C ≅ C') (he : e.hom ≫ c' = c) (he' : e.inv ≫ c = c')
    (hε : ε.1 ≫ e.hom = ε'.1) (hε' : ε'.1 ≫ e.inv = ε.1)
    {D : RelativePic0Designation R c} {D' : RelativePic0Designation R c'}
    (h : RepresentsRelSubPic c ε (algEquivZeroCut c ε) D)
    (h' : RepresentsRelSubPic c' ε' (algEquivZeroCut c' ε') D') :
    (RepresentsRelSubPic.pullbackHom e.inv he' hε' h h').1 ≫
      (RepresentsRelSubPic.pullbackHom e.hom he hε h' h).1 = 𝟙 D.P ∧
    (RepresentsRelSubPic.pullbackHom e.hom he hε h' h).1 ≫
      (RepresentsRelSubPic.pullbackHom e.inv he' hε' h h').1 = 𝟙 D'.P

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