Module

RigidifiedLineBundle_exists_gluing_openCover_of_bijective_sections.lean

Nyll.JacobianVarieties.Picard.RigidifiedLineBundle_exists_gluing_openCover_of_bijective_sections

95 declarations indexed from sourceView source ↗

Module documentation

Gluing rigidified line bundles

Pullback comparisons and descent glue compatible rigidified line bundles over an open cover.

Imports13

Mathlib.Util.WithWeakNamespace
Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime
Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
Nyll.AlgebraicCurves.Geometry.Schemes.SchemeHomOver
Nyll.AlgebraicCurves.Geometry.Picard.Functor
Nyll.SchemeTheory.Cohomology.Cech.TwoAffineOpenCover
Nyll.AlgebraicCurves.Geometry.Schemes.RigidifiedLineBundleOfInvertible
Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_isStackFor_openCover
Nyll.AlgebraicCurves.Geometry.Picard.RigidifiedLineBundle_exists_iso_map_pullback_rigSection_comp_eq
Nyll.JacobianVarieties.Picard.RigidifiedLineBundle_subsingleton_iso_map_pullback_rigSection_comp_eq
Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_pullbackComp_pullbackCongr_pasteSquares_app
Nyll.JacobianVarieties.Picard.Designation
Nyll.JacobianVarieties.Picard.Representation

Imported by2

theorem

pullbackComp_paste

L49 ↗

JacobianVarieties.Picard.Proofs.ZariskiGluing.ExZar.pullbackComp_paste

Source context 9 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ZariskiGluing
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
noncomputable section
namespace ExZar
section Coherence
variable {X₀ X₁ X₂ X₃ : Scheme.{u}}

Lean source · full declaration

theorem pullbackComp_paste (f : X₀ ⟶ X₁) (g : X₁ ⟶ X₂) (h : X₂ ⟶ X₃) :
    Functor.whiskerLeft (Scheme.Modules.pullback h) (Scheme.Modules.pullbackComp f g).hom ≫
        (Scheme.Modules.pullbackComp (f ≫ g) h).hom =
      (Functor.associator _ _ _).inv ≫
        Functor.whiskerRight (Scheme.Modules.pullbackComp g h).hom (Scheme.Modules.pullback f) ≫
        (Scheme.Modules.pullbackComp f (g ≫ h)).hom ≫ eqToHom (by rw [Category.assoc]) := by
  have H0 := Scheme.Modules.pseudofunctor_associativity f g h
  have H1 : Functor.whiskerLeft (Scheme.Modules.pullback h) (Scheme.Modules.pullbackComp f g).hom ≫
        (Scheme.Modules.pullbackComp (f ≫ g) h).hom =
      (Functor.associator _ _ _).inv ≫
        (Functor.isoWhiskerRight (Scheme.Modules.pullbackComp g h)
          (Scheme.Modules.pullback f)).hom ≫
        (Scheme.Modules.pullbackComp f (g ≫ h)).hom ≫
        ((Scheme.Modules.pullbackComp f (g ≫ h)).inv ≫
          Functor.whiskerRight (Scheme.Modules.pullbackComp g h).inv (Scheme.Modules.pullback f) ≫
          (Functor.associator _ _ _).hom ≫
            Functor.whiskerLeft (Scheme.Modules.pullback h) (Scheme.Modules.pullbackComp f g).hom ≫
            (Scheme.Modules.pullbackComp (f ≫ g) h).hom) := by
    rw [Iso.hom_inv_id_assoc, Functor.isoWhiskerRight_hom, ← Functor.whiskerRight_comp_assoc,
      Iso.hom_inv_id,
      Functor.whiskerRight_id', Category.id_comp, Iso.inv_hom_id_assoc]
  rw [H0] at H1
  exact H1

theorem

pullbackComp_paste_app

L73 ↗

JacobianVarieties.Picard.Proofs.ZariskiGluing.ExZar.pullbackComp_paste_app

Source context 9 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ZariskiGluing
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
noncomputable section
namespace ExZar
section Coherence
variable {X₀ X₁ X₂ X₃ : Scheme.{u}}

Lean source · full declaration

theorem pullbackComp_paste_app (f : X₀ ⟶ X₁) (g : X₁ ⟶ X₂) (h : X₂ ⟶ X₃) (M : X₃.Modules) :
    (Scheme.Modules.pullbackComp f g).hom.app ((Scheme.Modules.pullback h).obj M) ≫
        (Scheme.Modules.pullbackComp (f ≫ g) h).hom.app M =
      (Scheme.Modules.pullback f).map ((Scheme.Modules.pullbackComp g h).hom.app M) ≫
          (Scheme.Modules.pullbackComp f (g ≫ h)).hom.app M ≫
        eqToHom (by rw [Category.assoc]) := by
  have H := NatTrans.congr_app (pullbackComp_paste f g h) M
  simp only [NatTrans.comp_app, Functor.whiskerRight_app, Functor.whiskerLeft_app,
    Functor.associator_inv_app,
    Category.id_comp, eqToHom_app] at H
  exact H

def

τ

L86 ↗

JacobianVarieties.Picard.Proofs.ZariskiGluing.ExZar.τ

Documentation

The pullback comparison for a specified equality between a composite and a map.

Source context 9 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ZariskiGluing
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
noncomputable section
namespace ExZar
section Coherence
variable {X₀ X₁ X₂ X₃ : Scheme.{u}}

Lean source · statement

def τ (f : X₀ ⟶ X₁) (g : X₁ ⟶ X₂) (m : X₀ ⟶ X₂) (e : f ≫ g = m)
    : Scheme.Modules.pullback g ⋙ Scheme.Modules.pullback f ≅ Scheme.Modules.pullback m

theorem

τ_hom_app

L90 ↗

JacobianVarieties.Picard.Proofs.ZariskiGluing.ExZar.τ_hom_app

Source context 9 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ZariskiGluing
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
noncomputable section
namespace ExZar
section Coherence
variable {X₀ X₁ X₂ X₃ : Scheme.{u}}

Lean source · full declaration

theorem τ_hom_app (f : X₀ ⟶ X₁) (g : X₁ ⟶ X₂) (m : X₀ ⟶ X₂) (e : f ≫ g = m) (M : X₂.Modules) :
    (τ f g m e).hom.app M = (Scheme.Modules.pullbackComp f g).hom.app M ≫ eqToHom (by rw [e]) := by
  subst e
  rfl

theorem

τ_inv_app

L95 ↗

JacobianVarieties.Picard.Proofs.ZariskiGluing.ExZar.τ_inv_app

Source context 9 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ZariskiGluing
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
noncomputable section
namespace ExZar
section Coherence
variable {X₀ X₁ X₂ X₃ : Scheme.{u}}

Lean source · full declaration

theorem τ_inv_app (f : X₀ ⟶ X₁) (g : X₁ ⟶ X₂) (m : X₀ ⟶ X₂) (e : f ≫ g = m) (M : X₂.Modules) :
    (τ f g m e).inv.app M = eqToHom (by rw [e]) ≫ (Scheme.Modules.pullbackComp f g).inv.app M := by
  subst e
  rfl

theorem

τ_paste_app

L100 ↗

JacobianVarieties.Picard.Proofs.ZariskiGluing.ExZar.τ_paste_app

Source context 9 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ZariskiGluing
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
noncomputable section
namespace ExZar
section Coherence
variable {X₀ X₁ X₂ X₃ : Scheme.{u}}

Lean source · full declaration

theorem τ_paste_app (f : X₀ ⟶ X₁) (g : X₁ ⟶ X₂) (h : X₂ ⟶ X₃)
    (fg : X₀ ⟶ X₂) (gh : X₁ ⟶ X₃) (m : X₀ ⟶ X₃)
    (e₁ : f ≫ g = fg) (e₂ : g ≫ h = gh) (e₃ : fg ≫ h = m) (M : X₃.Modules) :
    (τ f g fg e₁).hom.app ((Scheme.Modules.pullback h).obj M) ≫ (τ fg h m e₃).hom.app M =
      (Scheme.Modules.pullback f).map ((τ g h gh e₂).hom.app M) ≫
          (τ f gh m (by rw [← e₂, ← Category.assoc, e₁, e₃])).hom.app M := by
  subst e₁ e₂ e₃
  simp only [τ_hom_app, eqToHom_refl, Category.comp_id]
  rw [pullbackComp_paste_app]

def

sqIso

L111 ↗

JacobianVarieties.Picard.Proofs.ZariskiGluing.ExZar.sqIso

Documentation

The natural isomorphism between pullback functors around a commutative square.

Source context 9 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ZariskiGluing
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
noncomputable section
namespace ExZar
section Coherence
variable {X₀ X₁ X₂ X₃ : Scheme.{u}}

Lean source · statement

def sqIso {W X Y Z : Scheme.{u}} {f : W ⟶ X} {g : X ⟶ Z} {h : W ⟶ Y} {k : Y ⟶ Z}
    (e : f ≫ g = h ≫ k)
    : Scheme.Modules.pullback g ⋙ Scheme.Modules.pullback f ≅
      Scheme.Modules.pullback k ⋙ Scheme.Modules.pullback h

theorem

route

L118 ↗

JacobianVarieties.Picard.Proofs.ZariskiGluing.ExZar.route

Source context 9 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ZariskiGluing
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
noncomputable section
namespace ExZar
section Coherence
variable {X₀ X₁ X₂ X₃ : Scheme.{u}}

Lean source · statement

theorem route {X X₀' X₁' Y Y₀ Y₁ : Scheme.{u}}
    (a : X₀' ⟶ X₁') (b : X₁' ⟶ X) (d : X₀' ⟶ X) (e : a ≫ b = d)
    (s₀ : Y₀ ⟶ X₀') (s₁ : Y₁ ⟶ X₁') (s : Y ⟶ X)
    (r : Y₀ ⟶ Y₁) (p : Y₁ ⟶ Y) (m : Y₀ ⟶ Y) (G : r ≫ p = m)
    (E : s₀ ≫ a = r ≫ s₁) (F : s₁ ≫ b = p ≫ s) (H : s₀ ≫ d = m ≫ s) (M : X.Modules) :
    (sqIso E).hom.app ((Scheme.Modules.pullback b).obj M) ≫
        (Scheme.Modules.pullback r).map ((sqIso F).hom.app M) ≫
        (τ r p m G).hom.app ((Scheme.Modules.pullback s).obj M) =
      (Scheme.Modules.pullback s₀).map ((τ a b d e).hom.app M) ≫ (sqIso H).hom.app M

abbrev

MOD

L133 ↗

JacobianVarieties.Picard.Proofs.ZariskiGluing.ExZar.MOD

Documentation

The pseudofunctor of scheme modules restricted from adjunctions to scheme morphisms.

Source context 7 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ZariskiGluing
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
noncomputable section
namespace ExZar

Lean source · statement

abbrev MOD : Pseudofunctor (LocallyDiscrete Scheme.{u}ᵒᵖ) Cat

theorem

MOD_mapComp'_eq_mapComp_app

L139 ↗

JacobianVarieties.Picard.Proofs.ZariskiGluing.ExZar.MOD_mapComp'_eq_mapComp_app

Source context 9 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ZariskiGluing
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
noncomputable section
namespace ExZar
section Bridge
variable {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z)

Lean source · statement

theorem MOD_mapComp'_eq_mapComp_app {a b d : LocallyDiscrete Scheme.{u}ᵒᵖ} (u : a ⟶ b) (v : b ⟶ d)
    (M : MOD.obj a) :
    (MOD.mapComp' u v (u ≫ v) rfl).hom.toNatTrans.app M
        = (MOD.mapComp u v).hom.toNatTrans.app M

theorem

MOD_mapComp'_eq_mapComp_inv_app

L145 ↗

JacobianVarieties.Picard.Proofs.ZariskiGluing.ExZar.MOD_mapComp'_eq_mapComp_inv_app

Source context 9 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ZariskiGluing
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
noncomputable section
namespace ExZar
section Bridge
variable {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z)

Lean source · statement

theorem MOD_mapComp'_eq_mapComp_inv_app {a b d : LocallyDiscrete Scheme.{u}ᵒᵖ}
    (u : a ⟶ b) (v : b ⟶ d)
    (M : MOD.obj a) :
    (MOD.mapComp' u v (u ≫ v) rfl).inv.toNatTrans.app M
        = (MOD.mapComp u v).inv.toNatTrans.app M

theorem

MOD_mapComp'_hom_app

L152 ↗

JacobianVarieties.Picard.Proofs.ZariskiGluing.ExZar.MOD_mapComp'_hom_app

Source context 9 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ZariskiGluing
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
noncomputable section
namespace ExZar
section Bridge
variable {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z)

Lean source · full declaration

theorem MOD_mapComp'_hom_app (fg : X ⟶ Z) (h : f ≫ g = fg) (L : Z.Modules) :
    (MOD.mapComp' g.op.toLoc f.op.toLoc fg.op.toLoc (by rw [← h]; rfl)).hom.toNatTrans.app L =
      (τ f g fg h).inv.app L := by
  subst h
  rw [τ_inv_app]
  simp only [eqToHom_refl, Category.id_comp]
  exact MOD_mapComp'_eq_mapComp_app g.op.toLoc f.op.toLoc L

theorem

MOD_mapComp'_inv_app

L160 ↗

JacobianVarieties.Picard.Proofs.ZariskiGluing.ExZar.MOD_mapComp'_inv_app

Source context 9 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ZariskiGluing
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
noncomputable section
namespace ExZar
section Bridge
variable {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z)

Lean source · full declaration

theorem MOD_mapComp'_inv_app (fg : X ⟶ Z) (h : f ≫ g = fg) (L : Z.Modules) :
    (MOD.mapComp' g.op.toLoc f.op.toLoc fg.op.toLoc (by rw [← h]; rfl)).inv.toNatTrans.app L =
      (τ f g fg h).hom.app L := by
  subst h
  rw [τ_hom_app]
  simp only [eqToHom_refl, Category.comp_id]
  exact MOD_mapComp'_eq_mapComp_inv_app g.op.toLoc f.op.toLoc L

theorem

pullHom_MOD

L171 ↗

JacobianVarieties.Picard.Proofs.ZariskiGluing.ExZar.pullHom_MOD

Source context 8 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ZariskiGluing
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
noncomputable section
namespace ExZar
open CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat in

Lean source · statement

theorem pullHom_MOD {X₁ X₂ Y Y' : Scheme.{u}} {M₁ : X₁.Modules} {M₂ : X₂.Modules}
    {f₁ : Y ⟶ X₁} {f₂ : Y ⟶ X₂}
    (φ : (Scheme.Modules.pullback f₁).obj M₁ ⟶ (Scheme.Modules.pullback f₂).obj M₂)
    (g : Y' ⟶ Y) (gf₁ : Y' ⟶ X₁) (gf₂ : Y' ⟶ X₂) (hgf₁ : g ≫ f₁ = gf₁) (hgf₂ : g ≫ f₂ = gf₂) :
    pullHom (F := MOD) (M₁ := M₁) (M₂ := M₂) φ g gf₁ gf₂ hgf₁ hgf₂ =
      ((τ g f₁ gf₁ hgf₁).inv.app M₁ ≫ (Scheme.Modules.pullback g).map φ ≫
          (τ g f₂ gf₂ hgf₂).hom.app M₂ :)

def

pullHomIso

L182 ↗

JacobianVarieties.Picard.Proofs.ZariskiGluing.ExZar.pullHomIso

Documentation

Pull back a line-bundle isomorphism and identify the composite pullbacks with chosen maps.

Source context 7 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ZariskiGluing
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
noncomputable section
namespace ExZar

Lean source · statement

def pullHomIso {X₁ X₂ Y Y' : Scheme.{u}} {M₁ : X₁.Modules} {M₂ : X₂.Modules}
    {f₁ : Y ⟶ X₁} {f₂ : Y ⟶ X₂}
    (Φ : (Scheme.Modules.pullback f₁).obj M₁ ≅ (Scheme.Modules.pullback f₂).obj M₂)
    (g : Y' ⟶ Y) (gf₁ : Y' ⟶ X₁) (gf₂ : Y' ⟶ X₂) (hgf₁ : g ≫ f₁ = gf₁) (hgf₂ : g ≫ f₂ = gf₂) :
    (Scheme.Modules.pullback gf₁).obj M₁ ≅ (Scheme.Modules.pullback gf₂).obj M₂

theorem

pullHomIso_hom'

L190 ↗

JacobianVarieties.Picard.Proofs.ZariskiGluing.ExZar.pullHomIso_hom'

Source context 7 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ZariskiGluing
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
noncomputable section
namespace ExZar

Lean source · statement

theorem pullHomIso_hom' {X₁ X₂ Y Y' : Scheme.{u}} {M₁ : X₁.Modules} {M₂ : X₂.Modules}
    {f₁ : Y ⟶ X₁} {f₂ : Y ⟶ X₂}
    (Φ : (Scheme.Modules.pullback f₁).obj M₁ ≅ (Scheme.Modules.pullback f₂).obj M₂)
    (g : Y' ⟶ Y) (gf₁ : Y' ⟶ X₁) (gf₂ : Y' ⟶ X₂) (hgf₁ : g ≫ f₁ = gf₁) (hgf₂ : g ≫ f₂ = gf₂) :
    (pullHomIso Φ g gf₁ gf₂ hgf₁ hgf₂).hom =
      (τ g f₁ gf₁ hgf₁).inv.app M₁ ≫ (Scheme.Modules.pullback g).map Φ.hom ≫
          (τ g f₂ gf₂ hgf₂).hom.app M₂

theorem

pullHomIso_hom

L200 ↗

JacobianVarieties.Picard.Proofs.ZariskiGluing.ExZar.pullHomIso_hom

Source context 8 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ZariskiGluing
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
noncomputable section
namespace ExZar
open CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat in

Lean source · statement

theorem pullHomIso_hom {X₁ X₂ Y Y' : Scheme.{u}} {M₁ : X₁.Modules} {M₂ : X₂.Modules}
    {f₁ : Y ⟶ X₁} {f₂ : Y ⟶ X₂}
    (Φ : (Scheme.Modules.pullback f₁).obj M₁ ≅ (Scheme.Modules.pullback f₂).obj M₂)
    (g : Y' ⟶ Y) (gf₁ : Y' ⟶ X₁) (gf₂ : Y' ⟶ X₂) (hgf₁ : g ≫ f₁ = gf₁) (hgf₂ : g ≫ f₂ = gf₂) :
    (pullHomIso Φ g gf₁ gf₂ hgf₁ hgf₂).hom =
      pullHom (F := MOD) (M₁ := M₁) (M₂ := M₂) Φ.hom g gf₁ gf₂ hgf₁ hgf₂

def

pullHomMap

L209 ↗

JacobianVarieties.Picard.Proofs.ZariskiGluing.ExZar.pullHomMap

Documentation

Pull back a module morphism and identify the composite pullbacks with chosen maps.

Source context 7 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ZariskiGluing
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
noncomputable section
namespace ExZar

Lean source · statement

def pullHomMap {X₁ X₂ Y Y' : Scheme.{u}} {M₁ : X₁.Modules} {M₂ : X₂.Modules}
    {f₁ : Y ⟶ X₁} {f₂ : Y ⟶ X₂}
    (φ : (Scheme.Modules.pullback f₁).obj M₁ ⟶ (Scheme.Modules.pullback f₂).obj M₂)
    (g : Y' ⟶ Y) (gf₁ : Y' ⟶ X₁) (gf₂ : Y' ⟶ X₂) (hgf₁ : g ≫ f₁ = gf₁) (hgf₂ : g ≫ f₂ = gf₂) :
    (Scheme.Modules.pullback gf₁).obj M₁ ⟶ (Scheme.Modules.pullback gf₂).obj M₂

theorem

pullHomIso_hom_eq_pullHomMap

L216 ↗

JacobianVarieties.Picard.Proofs.ZariskiGluing.ExZar.pullHomIso_hom_eq_pullHomMap

Source context 7 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ZariskiGluing
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
noncomputable section
namespace ExZar

Lean source · statement

theorem pullHomIso_hom_eq_pullHomMap {X₁ X₂ Y Y' : Scheme.{u}} {M₁ : X₁.Modules} {M₂ : X₂.Modules}
    {f₁ : Y ⟶ X₁} {f₂ : Y ⟶ X₂}
    (Φ : (Scheme.Modules.pullback f₁).obj M₁ ≅ (Scheme.Modules.pullback f₂).obj M₂)
    (g : Y' ⟶ Y) (gf₁ : Y' ⟶ X₁) (gf₂ : Y' ⟶ X₂) (hgf₁ : g ≫ f₁ = gf₁) (hgf₂ : g ≫ f₂ = gf₂) :
    (pullHomIso Φ g gf₁ gf₂ hgf₁ hgf₂).hom = pullHomMap Φ.hom g gf₁ gf₂ hgf₁ hgf₂

def

toMOD

L224 ↗

JacobianVarieties.Picard.Proofs.ZariskiGluing.ExZar.toMOD

Documentation

View a morphism of pulled-back modules as a morphism in the module pseudofunctor.

Source context 7 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ZariskiGluing
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
noncomputable section
namespace ExZar

Lean source · statement

def toMOD {X₁ X₂ Y : Scheme.{u}} {M₁ : X₁.Modules} {M₂ : X₂.Modules} (f₁ : Y ⟶ X₁) (f₂ : Y ⟶ X₂)
    (φ : (Scheme.Modules.pullback f₁).obj M₁ ⟶ (Scheme.Modules.pullback f₂).obj M₂) :
    (MOD.map f₁.op.toLoc).toFunctor.obj M₁ ⟶ (MOD.map f₂.op.toLoc).toFunctor.obj M₂

theorem

toMOD_eq

L228 ↗

JacobianVarieties.Picard.Proofs.ZariskiGluing.ExZar.toMOD_eq

Source context 7 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ZariskiGluing
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
noncomputable section
namespace ExZar

Lean source · statement

theorem toMOD_eq {X₁ X₂ Y : Scheme.{u}} {M₁ : X₁.Modules} {M₂ : X₂.Modules}
    (f₁ : Y ⟶ X₁) (f₂ : Y ⟶ X₂)
    (φ : (Scheme.Modules.pullback f₁).obj M₁ ⟶ (Scheme.Modules.pullback f₂).obj M₂) :
    toMOD f₁ f₂ φ = φ

theorem

pullHom_toMOD

L234 ↗

JacobianVarieties.Picard.Proofs.ZariskiGluing.ExZar.pullHom_toMOD

Source context 8 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ZariskiGluing
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
noncomputable section
namespace ExZar
open CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat in

Lean source · statement

theorem pullHom_toMOD {X₁ X₂ Y Y' : Scheme.{u}} {M₁ : X₁.Modules} {M₂ : X₂.Modules}
    {f₁ : Y ⟶ X₁} {f₂ : Y ⟶ X₂}
    (φ : (Scheme.Modules.pullback f₁).obj M₁ ⟶ (Scheme.Modules.pullback f₂).obj M₂)
    (g : Y' ⟶ Y) (gf₁ : Y' ⟶ X₁) (gf₂ : Y' ⟶ X₂) (hgf₁ : g ≫ f₁ = gf₁) (hgf₂ : g ≫ f₂ = gf₂) :
    pullHom (F := MOD) (M₁ := M₁) (M₂ := M₂) (toMOD f₁ f₂ φ) g gf₁ gf₂ hgf₁ hgf₂ =
      toMOD gf₁ gf₂ (pullHomMap φ g gf₁ gf₂ hgf₁ hgf₂)

theorem

toMOD_comp

L242 ↗

JacobianVarieties.Picard.Proofs.ZariskiGluing.ExZar.toMOD_comp

Source context 7 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ZariskiGluing
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
noncomputable section
namespace ExZar

Lean source · statement

theorem toMOD_comp {X₁ X₂ X₃ Y : Scheme.{u}} {M₁ : X₁.Modules} {M₂ : X₂.Modules} {M₃ : X₃.Modules}
    (f₁ : Y ⟶ X₁) (f₂ : Y ⟶ X₂) (f₃ : Y ⟶ X₃)
    (φ : (Scheme.Modules.pullback f₁).obj M₁ ⟶ (Scheme.Modules.pullback f₂).obj M₂)
    (ψ : (Scheme.Modules.pullback f₂).obj M₂ ⟶ (Scheme.Modules.pullback f₃).obj M₃) :
    toMOD f₁ f₂ φ ≫ toMOD f₂ f₃ ψ = toMOD f₁ f₃ (φ ≫ ψ)

theorem

toMOD_congr

L249 ↗

JacobianVarieties.Picard.Proofs.ZariskiGluing.ExZar.toMOD_congr

Source context 7 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ZariskiGluing
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
noncomputable section
namespace ExZar

Lean source · statement

theorem toMOD_congr {X₁ X₂ Y : Scheme.{u}} {M₁ : X₁.Modules} {M₂ : X₂.Modules}
    (f₁ : Y ⟶ X₁) (f₂ : Y ⟶ X₂)
    {φ ψ : (Scheme.Modules.pullback f₁).obj M₁ ⟶ (Scheme.Modules.pullback f₂).obj M₂} (h : φ = ψ) :
    toMOD f₁ f₂ φ = toMOD f₁ f₂ ψ

theorem

toMOD_id

L255 ↗

JacobianVarieties.Picard.Proofs.ZariskiGluing.ExZar.toMOD_id

Source context 7 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ZariskiGluing
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
noncomputable section
namespace ExZar

Lean source · statement

theorem toMOD_id {X₁ Y : Scheme.{u}} {M₁ : X₁.Modules} (f₁ : Y ⟶ X₁) :
    toMOD f₁ f₁ (𝟙 ((Scheme.Modules.pullback f₁).obj M₁)) = 𝟙 _

def

isoOfMOD

L260 ↗

JacobianVarieties.Picard.Proofs.ZariskiGluing.ExZar.isoOfMOD

Documentation

View an isomorphism in the module pseudofunctor as an isomorphism of scheme modules.

Source context 7 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ZariskiGluing
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
noncomputable section
namespace ExZar

Lean source · statement

def isoOfMOD {X Y : Scheme.{u}} {g : X ⟶ Y} {L : Y.Modules} {N : X.Modules}
    (e : @Iso (MOD.obj (.mk (op X))) _ ((MOD.map g.op.toLoc).toFunctor.obj L) N) :
    (Scheme.Modules.pullback g).obj L ≅ N

theorem

MOD_pullHom_eq_id_of_iso

L265 ↗

JacobianVarieties.Picard.Proofs.ZariskiGluing.ExZar.MOD_pullHom_eq_id_of_iso

Source context 8 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ZariskiGluing
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
noncomputable section
namespace ExZar
open CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat in

Lean source · statement

theorem MOD_pullHom_eq_id_of_iso {X₁ Y W : Scheme.{u}} {M₁ : X₁.Modules} {a₁ a₂ : Y ⟶ X₁}
    (Φ : (Scheme.Modules.pullback a₁).obj M₁ ≅ (Scheme.Modules.pullback a₂).obj M₁)
    (p : W ⟶ Y) (q : W ⟶ X₁)
    (h₁ : p ≫ a₁ = q) (h₂ : p ≫ a₂ = q) (H : pullHomIso Φ p q q h₁ h₂ = Iso.refl _) :
    pullHom (F := MOD) (M₁ := M₁) (M₂ := M₁) Φ.hom p q q h₁ h₂ = 𝟙 _

theorem

pullHomMap_comp_of

L277 ↗

JacobianVarieties.Picard.Proofs.ZariskiGluing.ExZar.pullHomMap_comp_of

Source context 9 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ZariskiGluing
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
noncomputable section
namespace ExZar
section PlainDescent
open CategoryTheory.Pseudofunctor CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat

Lean source · statement

theorem pullHomMap_comp_of {X₁ X₂ X₃ Y₁₂ Y₂₃ Y₁₃ W : Scheme.{u}}
    {M₁ : X₁.Modules} {M₂ : X₂.Modules} {M₃ : X₃.Modules}
    {a₁ : Y₁₂ ⟶ X₁} {a₂ : Y₁₂ ⟶ X₂} {b₂ : Y₂₃ ⟶ X₂} {b₃ : Y₂₃ ⟶ X₃} {c₁ : Y₁₃ ⟶ X₁} {c₃ : Y₁₃ ⟶ X₃}
    (Φ₁₂ : (Scheme.Modules.pullback a₁).obj M₁ ≅ (Scheme.Modules.pullback a₂).obj M₂)
    (Φ₂₃ : (Scheme.Modules.pullback b₂).obj M₂ ≅ (Scheme.Modules.pullback b₃).obj M₃)
    (Φ₁₃ : (Scheme.Modules.pullback c₁).obj M₁ ≅ (Scheme.Modules.pullback c₃).obj M₃)
    (p₁₂ : W ⟶ Y₁₂) (p₂₃ : W ⟶ Y₂₃) (p₁₃ : W ⟶ Y₁₃) (q₁ : W ⟶ X₁) (q₂ : W ⟶ X₂) (q₃ : W ⟶ X₃)
    (h₁ : p₁₂ ≫ a₁ = q₁) (h₂ : p₁₂ ≫ a₂ = q₂) (h₃ : p₂₃ ≫ b₂ = q₂) (h₄ : p₂₃ ≫ b₃ = q₃)
    (h₅ : p₁₃ ≫ c₁ = q₁) (h₆ : p₁₃ ≫ c₃ = q₃)
    (hc : pullHomIso Φ₁₂ p₁₂ q₁ q₂ h₁ h₂ ≪≫ pullHomIso Φ₂₃ p₂₃ q₂ q₃ h₃ h₄
        = pullHomIso Φ₁₃ p₁₃ q₁ q₃ h₅ h₆) :
    pullHomMap Φ₁₂.hom p₁₂ q₁ q₂ h₁ h₂ ≫ pullHomMap Φ₂₃.hom p₂₃ q₂ q₃ h₃ h₄
        = pullHomMap Φ₁₃.hom p₁₃ q₁ q₃ h₅ h₆

def

homG

L303 ↗

JacobianVarieties.Picard.Proofs.ZariskiGluing.ExZar.homG

Documentation

The transition morphism of the module pseudofunctor induced by the given gluing isomorphism.

Source context 10 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ZariskiGluing
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
noncomputable section
namespace ExZar
section PlainDescent
open CategoryTheory.Pseudofunctor CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {ι : Type u} {S : Scheme.{u}} {X : ι → Scheme.{u}} (g : ∀ i, X i ⟶ S)
  (sq : ∀ i j, ChosenPullback (g i) (g j))
  (sq₃ : ∀ i j k, ChosenPullback₃ (sq i j) (sq j k) (sq i k))
  (obj : ∀ i, (X i).Modules)
  (φ : ∀ i j, (Scheme.Modules.pullback (sq i j).p₁).obj (obj i)
      ≅ (Scheme.Modules.pullback (sq i j).p₂).obj (obj j))

Lean source · statement

def homG (i j : ι) :
    (MOD.map (sq i j).p₁.op.toLoc).toFunctor.obj (obj i)
        ⟶ (MOD.map (sq i j).p₂.op.toLoc).toFunctor.obj (obj j)

theorem

pullHom_homG

L309 ↗

JacobianVarieties.Picard.Proofs.ZariskiGluing.ExZar.pullHom_homG

Source context 11 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ZariskiGluing
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
noncomputable section
namespace ExZar
section PlainDescent
open CategoryTheory.Pseudofunctor CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {ι : Type u} {S : Scheme.{u}} {X : ι → Scheme.{u}} (g : ∀ i, X i ⟶ S)
  (sq : ∀ i j, ChosenPullback (g i) (g j))
  (sq₃ : ∀ i j k, ChosenPullback₃ (sq i j) (sq j k) (sq i k))
  (obj : ∀ i, (X i).Modules)
  (φ : ∀ i j, (Scheme.Modules.pullback (sq i j).p₁).obj (obj i)
      ≅ (Scheme.Modules.pullback (sq i j).p₂).obj (obj j))
open CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat in

Lean source · statement

theorem pullHom_homG (i j : ι) {W : Scheme.{u}} (p : W ⟶ (sq i j).pullback)
    (q₁ : W ⟶ X i) (q₂ : W ⟶ X j)
    (h₁ : p ≫ (sq i j).p₁ = q₁) (h₂ : p ≫ (sq i j).p₂ = q₂) :
    pullHom (F := MOD) (homG g sq obj φ i j) p q₁ q₂ h₁ h₂ =
      toMOD q₁ q₂ (pullHomMap (φ i j).hom p q₁ q₂ h₁ h₂)

def

dataG

L331 ↗

JacobianVarieties.Picard.Proofs.ZariskiGluing.ExZar.dataG

Documentation

The module descent datum determined by the transition isomorphisms and cocycle equations.

Source context 11 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ZariskiGluing
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
noncomputable section
namespace ExZar
section PlainDescent
open CategoryTheory.Pseudofunctor CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {ι : Type u} {S : Scheme.{u}} {X : ι → Scheme.{u}} (g : ∀ i, X i ⟶ S)
  (sq : ∀ i j, ChosenPullback (g i) (g j))
  (sq₃ : ∀ i j k, ChosenPullback₃ (sq i j) (sq j k) (sq i k))
  (obj : ∀ i, (X i).Modules)
  (φ : ∀ i j, (Scheme.Modules.pullback (sq i j).p₁).obj (obj i)
      ≅ (Scheme.Modules.pullback (sq i j).p₂).obj (obj j))
variable (δ : ∀ i, X i ⟶ (sq i i).pullback)
    (hδ₁ : ∀ i, δ i ≫ (sq i i).p₁ = 𝟙 _) (hδ₂ : ∀ i, δ i ≫ (sq i i).p₂ = 𝟙 _)
  (hself : ∀ i (h₁ : δ i ≫ (sq i i).p₁ = 𝟙 _) (h₂ : δ i ≫ (sq i i).p₂ = 𝟙 _),
    pullHomIso (φ i i) (δ i) (𝟙 _) (𝟙 _) h₁ h₂ = Iso.refl _)
  (hcomp : ∀ i j k (h₁ : (sq₃ i j k).p₁₂ ≫ (sq i j).p₁ = (sq₃ i j k).p₁)
    (h₂ : (sq₃ i j k).p₁₂ ≫ (sq i j).p₂ = (sq₃ i j k).p₂)
    (h₃ : (sq₃ i j k).p₂₃ ≫ (sq j k).p₁ = (sq₃ i j k).p₂)
    (h₄ : (sq₃ i j k).p₂₃ ≫ (sq j k).p₂ = (sq₃ i j k).p₃)
    (h₅ : (sq₃ i j k).p₁₃ ≫ (sq i k).p₁ = (sq₃ i j k).p₁)
    (h₆ : (sq₃ i j k).p₁₃ ≫ (sq i k).p₂ = (sq₃ i j k).p₃),
    pullHomIso (φ i j) (sq₃ i j k).p₁₂ (sq₃ i j k).p₁ (sq₃ i j k).p₂ h₁ h₂ ≪≫
      pullHomIso (φ j k) (sq₃ i j k).p₂₃ (sq₃ i j k).p₂ (sq₃ i j k).p₃ h₃ h₄ =
    pullHomIso (φ i k) (sq₃ i j k).p₁₃ (sq₃ i j k).p₁ (sq₃ i j k).p₃ h₅ h₆)

Lean source · full declaration

def dataG : MOD.DescentData' (f := g) sq sq₃ where
  obj := obj
  hom := homG g sq obj φ
  pullHom'_hom_self i := by
    rw [DescentData'.pullHom'_eq_pullHom (F := MOD) (f := g) (sq := sq) (obj := obj) (obj' := obj)
        (homG g sq obj φ)
      (g i) (𝟙 (X i)) (𝟙 (X i)) (δ i) _ _ (hδ₁ i) (hδ₂ i)]
    exact MOD_pullHom_eq_id_of_iso (φ i i) (δ i) (𝟙 _) _ _ (hself i _ _)
  pullHom'_hom_comp i j k := by
    rw [DescentData'.pullHom'₁₂_eq_pullHom_of_chosenPullback₃ (sq₃ := sq₃)
        (hom := homG g sq obj φ) i j k,
      DescentData'.pullHom'₂₃_eq_pullHom_of_chosenPullback₃ (sq₃ := sq₃)
        (hom := homG g sq obj φ) i j k,
      DescentData'.pullHom'₁₃_eq_pullHom_of_chosenPullback₃ (sq₃ := sq₃)
        (hom := homG g sq obj φ) i j k,
      pullHom_homG, pullHom_homG, pullHom_homG, toMOD_comp]
    exact congrArg (toMOD (sq₃ i j k).p₁ (sq₃ i j k).p₃)
      (pullHomMap_comp_of (φ i j) (φ j k) (φ i k) (sq₃ i j k).p₁₂ (sq₃ i j k).p₂₃ (sq₃ i j k).p₁₃
        (sq₃ i j k).p₁ (sq₃ i j k).p₂ (sq₃ i j k).p₃ _ _ _ _ _ _ (hcomp i j k _ _ _ _ _ _))

theorem

dataG_obj

L351 ↗

JacobianVarieties.Picard.Proofs.ZariskiGluing.ExZar.dataG_obj

Source context 11 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ZariskiGluing
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
noncomputable section
namespace ExZar
section PlainDescent
open CategoryTheory.Pseudofunctor CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {ι : Type u} {S : Scheme.{u}} {X : ι → Scheme.{u}} (g : ∀ i, X i ⟶ S)
  (sq : ∀ i j, ChosenPullback (g i) (g j))
  (sq₃ : ∀ i j k, ChosenPullback₃ (sq i j) (sq j k) (sq i k))
  (obj : ∀ i, (X i).Modules)
  (φ : ∀ i j, (Scheme.Modules.pullback (sq i j).p₁).obj (obj i)
      ≅ (Scheme.Modules.pullback (sq i j).p₂).obj (obj j))
variable (δ : ∀ i, X i ⟶ (sq i i).pullback)
    (hδ₁ : ∀ i, δ i ≫ (sq i i).p₁ = 𝟙 _) (hδ₂ : ∀ i, δ i ≫ (sq i i).p₂ = 𝟙 _)
  (hself : ∀ i (h₁ : δ i ≫ (sq i i).p₁ = 𝟙 _) (h₂ : δ i ≫ (sq i i).p₂ = 𝟙 _),
    pullHomIso (φ i i) (δ i) (𝟙 _) (𝟙 _) h₁ h₂ = Iso.refl _)
  (hcomp : ∀ i j k (h₁ : (sq₃ i j k).p₁₂ ≫ (sq i j).p₁ = (sq₃ i j k).p₁)
    (h₂ : (sq₃ i j k).p₁₂ ≫ (sq i j).p₂ = (sq₃ i j k).p₂)
    (h₃ : (sq₃ i j k).p₂₃ ≫ (sq j k).p₁ = (sq₃ i j k).p₂)
    (h₄ : (sq₃ i j k).p₂₃ ≫ (sq j k).p₂ = (sq₃ i j k).p₃)
    (h₅ : (sq₃ i j k).p₁₃ ≫ (sq i k).p₁ = (sq₃ i j k).p₁)
    (h₆ : (sq₃ i j k).p₁₃ ≫ (sq i k).p₂ = (sq₃ i j k).p₃),
    pullHomIso (φ i j) (sq₃ i j k).p₁₂ (sq₃ i j k).p₁ (sq₃ i j k).p₂ h₁ h₂ ≪≫
      pullHomIso (φ j k) (sq₃ i j k).p₂₃ (sq₃ i j k).p₂ (sq₃ i j k).p₃ h₃ h₄ =
    pullHomIso (φ i k) (sq₃ i j k).p₁₃ (sq₃ i j k).p₁ (sq₃ i j k).p₃ h₅ h₆)

Lean source · statement

theorem dataG_obj (i : ι) : (dataG g sq sq₃ obj φ δ hδ₁ hδ₂ hself hcomp).obj i = obj i

theorem

exists_iso_of_plainDescent

L354 ↗

JacobianVarieties.Picard.Proofs.ZariskiGluing.ExZar.exists_iso_of_plainDescent

Source context 12 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ZariskiGluing
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
noncomputable section
namespace ExZar
section PlainDescent
open CategoryTheory.Pseudofunctor CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {ι : Type u} {S : Scheme.{u}} {X : ι → Scheme.{u}} (g : ∀ i, X i ⟶ S)
  (sq : ∀ i j, ChosenPullback (g i) (g j))
  (sq₃ : ∀ i j k, ChosenPullback₃ (sq i j) (sq j k) (sq i k))
  (obj : ∀ i, (X i).Modules)
  (φ : ∀ i j, (Scheme.Modules.pullback (sq i j).p₁).obj (obj i)
      ≅ (Scheme.Modules.pullback (sq i j).p₂).obj (obj j))
variable (δ : ∀ i, X i ⟶ (sq i i).pullback)
    (hδ₁ : ∀ i, δ i ≫ (sq i i).p₁ = 𝟙 _) (hδ₂ : ∀ i, δ i ≫ (sq i i).p₂ = 𝟙 _)
  (hself : ∀ i (h₁ : δ i ≫ (sq i i).p₁ = 𝟙 _) (h₂ : δ i ≫ (sq i i).p₂ = 𝟙 _),
    pullHomIso (φ i i) (δ i) (𝟙 _) (𝟙 _) h₁ h₂ = Iso.refl _)
  (hcomp : ∀ i j k (h₁ : (sq₃ i j k).p₁₂ ≫ (sq i j).p₁ = (sq₃ i j k).p₁)
    (h₂ : (sq₃ i j k).p₁₂ ≫ (sq i j).p₂ = (sq₃ i j k).p₂)
    (h₃ : (sq₃ i j k).p₂₃ ≫ (sq j k).p₁ = (sq₃ i j k).p₂)
    (h₄ : (sq₃ i j k).p₂₃ ≫ (sq j k).p₂ = (sq₃ i j k).p₃)
    (h₅ : (sq₃ i j k).p₁₃ ≫ (sq i k).p₁ = (sq₃ i j k).p₁)
    (h₆ : (sq₃ i j k).p₁₃ ≫ (sq i k).p₂ = (sq₃ i j k).p₃),
    pullHomIso (φ i j) (sq₃ i j k).p₁₂ (sq₃ i j k).p₁ (sq₃ i j k).p₂ h₁ h₂ ≪≫
      pullHomIso (φ j k) (sq₃ i j k).p₂₃ (sq₃ i j k).p₂ (sq₃ i j k).p₃ h₃ h₄ =
    pullHomIso (φ i k) (sq₃ i j k).p₁₃ (sq₃ i j k).p₁ (sq₃ i j k).p₃ h₅ h₆)
include δ hδ₁ hδ₂ hself hcomp in

Lean source · statement

theorem exists_iso_of_plainDescent [(MOD.toDescentData g).IsEquivalence] :
    ∃ L : S.Modules, ∀ i, Nonempty ((Scheme.Modules.pullback (g i)).obj L ≅ obj i)

lemma

isPullback_baseChangeSnd_snd

L380 ↗

JacobianVarieties.Picard.Proofs.ZariskiGluing.ExZar.isPullback_baseChangeSnd_snd

Source context 9 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ZariskiGluing
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
noncomputable section
namespace ExZar
open NeronModelInfra AlgebraicGeometry.RelPicard
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))

Lean source · statement

lemma isPullback_baseChangeSnd_snd {T T' : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
    {t' : T' ⟶ Spec (CommRingCat.of R)} (ψ : SchemeHomOver t' t) :
    IsPullback (baseChangeSnd c ψ) (pullback.snd c t') (pullback.snd c t) ψ.1

lemma

isPullback_baseChangeSnd

L389 ↗

JacobianVarieties.Picard.Proofs.ZariskiGluing.ExZar.isPullback_baseChangeSnd

Source context 9 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ZariskiGluing
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
noncomputable section
namespace ExZar
open NeronModelInfra AlgebraicGeometry.RelPicard
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))

Lean source · statement

lemma isPullback_baseChangeSnd {X U V W : Scheme.{u}} {x : X ⟶ Spec (CommRingCat.of R)}
    {uS : U ⟶ Spec (CommRingCat.of R)} {vS : V ⟶ Spec (CommRingCat.of R)}
    {wS : W ⟶ Spec (CommRingCat.of R)}
    (u : SchemeHomOver uS x) (v : SchemeHomOver vS x)
    (a : SchemeHomOver wS uS) (b : SchemeHomOver wS vS)
    (h : IsPullback a.1 b.1 u.1 v.1) :
    IsPullback (baseChangeSnd c a) (baseChangeSnd c b) (baseChangeSnd c u) (baseChangeSnd c v)

abbrev

strMap₁₂

L412 ↗

JacobianVarieties.Picard.Proofs.ZariskiGluing.ExZar.strMap₁₂

Documentation

The structure map of the overlap of two schemes over the same base.

Source context 9 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ZariskiGluing
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
noncomputable section
namespace ExZar
open NeronModelInfra AlgebraicGeometry.RelPicard
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))

Lean source · statement

abbrev strMap₁₂ {T T₁ T₂ : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
    {t₁ : T₁ ⟶ Spec (CommRingCat.of R)}
    {t₂ : T₂ ⟶ Spec (CommRingCat.of R)} (ψ₁ : SchemeHomOver t₁ t) (ψ₂ : SchemeHomOver t₂ t) :
    Limits.pullback ψ₁.1 ψ₂.1 ⟶ Spec (CommRingCat.of R)

def

pr₁

L419 ↗

JacobianVarieties.Picard.Proofs.ZariskiGluing.ExZar.pr₁

Documentation

The first overlap projection as a morphism over the base.

Source context 9 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ZariskiGluing
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
noncomputable section
namespace ExZar
open NeronModelInfra AlgebraicGeometry.RelPicard
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))

Lean source · statement

def pr₁ {T T₁ T₂ : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)} {t₁ : T₁ ⟶ Spec (CommRingCat.of R)}
    {t₂ : T₂ ⟶ Spec (CommRingCat.of R)} (ψ₁ : SchemeHomOver t₁ t) (ψ₂ : SchemeHomOver t₂ t) :
    SchemeHomOver (strMap₁₂ ψ₁ ψ₂) t₁

def

pr₂

L425 ↗

JacobianVarieties.Picard.Proofs.ZariskiGluing.ExZar.pr₂

Documentation

The second overlap projection as a morphism over the base.

Source context 9 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ZariskiGluing
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
noncomputable section
namespace ExZar
open NeronModelInfra AlgebraicGeometry.RelPicard
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))

Lean source · statement

def pr₂ {T T₁ T₂ : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)} {t₁ : T₁ ⟶ Spec (CommRingCat.of R)}
    {t₂ : T₂ ⟶ Spec (CommRingCat.of R)} (ψ₁ : SchemeHomOver t₁ t) (ψ₂ : SchemeHomOver t₂ t) :
    SchemeHomOver (strMap₁₂ ψ₁ ψ₂) t₂

lemma

pr₁_val

L434 ↗

JacobianVarieties.Picard.Proofs.ZariskiGluing.ExZar.pr₁_val

Source context 9 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ZariskiGluing
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
noncomputable section
namespace ExZar
open NeronModelInfra AlgebraicGeometry.RelPicard
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))

Lean source · statement

lemma pr₁_val {T T₁ T₂ : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
    {t₁ : T₁ ⟶ Spec (CommRingCat.of R)}
    {t₂ : T₂ ⟶ Spec (CommRingCat.of R)} (ψ₁ : SchemeHomOver t₁ t) (ψ₂ : SchemeHomOver t₂ t) :
    (pr₁ ψ₁ ψ₂).1 = pullback.fst ψ₁.1 ψ₂.1

lemma

pr₂_val

L439 ↗

JacobianVarieties.Picard.Proofs.ZariskiGluing.ExZar.pr₂_val

Source context 9 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ZariskiGluing
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
noncomputable section
namespace ExZar
open NeronModelInfra AlgebraicGeometry.RelPicard
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))

Lean source · statement

lemma pr₂_val {T T₁ T₂ : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
    {t₁ : T₁ ⟶ Spec (CommRingCat.of R)}
    {t₂ : T₂ ⟶ Spec (CommRingCat.of R)} (ψ₁ : SchemeHomOver t₁ t) (ψ₂ : SchemeHomOver t₂ t) :
    (pr₂ ψ₁ ψ₂).1 = pullback.snd ψ₁.1 ψ₂.1

lemma

postComp_pr₁_eq_postComp_pr₂

L444 ↗

JacobianVarieties.Picard.Proofs.ZariskiGluing.ExZar.postComp_pr₁_eq_postComp_pr₂

Source context 9 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ZariskiGluing
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
noncomputable section
namespace ExZar
open NeronModelInfra AlgebraicGeometry.RelPicard
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))

Lean source · statement

lemma postComp_pr₁_eq_postComp_pr₂ {T T₁ T₂ : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
    {t₁ : T₁ ⟶ Spec (CommRingCat.of R)} {t₂ : T₂ ⟶ Spec (CommRingCat.of R)}
    (ψ₁ : SchemeHomOver t₁ t) (ψ₂ : SchemeHomOver t₂ t) :
    postComp ψ₁ (pr₁ ψ₁ ψ₂) = postComp ψ₂ (pr₂ ψ₁ ψ₂)

def

chosenPullback

L451 ↗

JacobianVarieties.Picard.Proofs.ZariskiGluing.ExZar.chosenPullback

Documentation

The chosen pullback square for the two induced base-change morphisms.

Source context 9 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ZariskiGluing
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
noncomputable section
namespace ExZar
open NeronModelInfra AlgebraicGeometry.RelPicard
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))

Lean source · full declaration

def chosenPullback {T T₁ T₂ : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
    {t₁ : T₁ ⟶ Spec (CommRingCat.of R)} {t₂ : T₂ ⟶ Spec (CommRingCat.of R)}
    (ψ₁ : SchemeHomOver t₁ t) (ψ₂ : SchemeHomOver t₂ t) :
    ChosenPullback (baseChangeSnd c ψ₁) (baseChangeSnd c ψ₂) where
  pullback := Limits.pullback c (strMap₁₂ ψ₁ ψ₂)
  p₁ := baseChangeSnd c (pr₁ ψ₁ ψ₂)
  p₂ := baseChangeSnd c (pr₂ ψ₁ ψ₂)
  condition := by
    rw [baseChangeSnd_comp, baseChangeSnd_comp, postComp_pr₁_eq_postComp_pr₂]
  isLimit := (isPullback_baseChangeSnd c ψ₁ ψ₂ (pr₁ ψ₁ ψ₂) (pr₂ ψ₁ ψ₂)
    (IsPullback.of_hasPullback ψ₁.1 ψ₂.1)).isLimit
  p := baseChangeSnd c (postComp ψ₁ (pr₁ ψ₁ ψ₂))
  hp₁ := baseChangeSnd_comp c _ _

abbrev

ρ₁₂

L472 ↗

JacobianVarieties.Picard.Proofs.ZariskiGluing.ExZar.ρ₁₂

Documentation

The projection from the triple overlap to the first two factors.

Source context 11 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ZariskiGluing
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
noncomputable section
namespace ExZar
open NeronModelInfra AlgebraicGeometry.RelPicard
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
section three
variable {T T₁ T₂ T₃ : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
    {t₁ : T₁ ⟶ Spec (CommRingCat.of R)} {t₂ : T₂ ⟶ Spec (CommRingCat.of R)}
    {t₃ : T₃ ⟶ Spec (CommRingCat.of R)}
    (ψ₁ : SchemeHomOver t₁ t) (ψ₂ : SchemeHomOver t₂ t) (ψ₃ : SchemeHomOver t₃ t)

Lean source · statement

abbrev ρ₁₂ : SchemeHomOver (strMap₁₂ (pr₂ ψ₁ ψ₂) (pr₁ ψ₂ ψ₃)) (strMap₁₂ ψ₁ ψ₂)

abbrev

ρ₂₃

L476 ↗

JacobianVarieties.Picard.Proofs.ZariskiGluing.ExZar.ρ₂₃

Documentation

The projection from the triple overlap to the last two factors.

Source context 11 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ZariskiGluing
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
noncomputable section
namespace ExZar
open NeronModelInfra AlgebraicGeometry.RelPicard
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
section three
variable {T T₁ T₂ T₃ : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
    {t₁ : T₁ ⟶ Spec (CommRingCat.of R)} {t₂ : T₂ ⟶ Spec (CommRingCat.of R)}
    {t₃ : T₃ ⟶ Spec (CommRingCat.of R)}
    (ψ₁ : SchemeHomOver t₁ t) (ψ₂ : SchemeHomOver t₂ t) (ψ₃ : SchemeHomOver t₃ t)

Lean source · statement

abbrev ρ₂₃ : SchemeHomOver (strMap₁₂ (pr₂ ψ₁ ψ₂) (pr₁ ψ₂ ψ₃)) (strMap₁₂ ψ₂ ψ₃)

def

ρ₁₃

L480 ↗

JacobianVarieties.Picard.Proofs.ZariskiGluing.ExZar.ρ₁₃

Documentation

The projection from the triple overlap to the first and third factors.

Source context 11 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ZariskiGluing
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
noncomputable section
namespace ExZar
open NeronModelInfra AlgebraicGeometry.RelPicard
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
section three
variable {T T₁ T₂ T₃ : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
    {t₁ : T₁ ⟶ Spec (CommRingCat.of R)} {t₂ : T₂ ⟶ Spec (CommRingCat.of R)}
    {t₃ : T₃ ⟶ Spec (CommRingCat.of R)}
    (ψ₁ : SchemeHomOver t₁ t) (ψ₂ : SchemeHomOver t₂ t) (ψ₃ : SchemeHomOver t₃ t)

Lean source · statement

def ρ₁₃ : SchemeHomOver (strMap₁₂ (pr₂ ψ₁ ψ₂) (pr₁ ψ₂ ψ₃)) (strMap₁₂ ψ₁ ψ₃)

lemma

ρ₁₃_pr₁

L499 ↗

JacobianVarieties.Picard.Proofs.ZariskiGluing.ExZar.ρ₁₃_pr₁

Source context 11 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ZariskiGluing
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
noncomputable section
namespace ExZar
open NeronModelInfra AlgebraicGeometry.RelPicard
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
section three
variable {T T₁ T₂ T₃ : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
    {t₁ : T₁ ⟶ Spec (CommRingCat.of R)} {t₂ : T₂ ⟶ Spec (CommRingCat.of R)}
    {t₃ : T₃ ⟶ Spec (CommRingCat.of R)}
    (ψ₁ : SchemeHomOver t₁ t) (ψ₂ : SchemeHomOver t₂ t) (ψ₃ : SchemeHomOver t₃ t)

Lean source · statement

lemma ρ₁₃_pr₁ : postComp (pr₁ ψ₁ ψ₃) (ρ₁₃ ψ₁ ψ₂ ψ₃) = postComp (pr₁ ψ₁ ψ₂) (ρ₁₂ ψ₁ ψ₂ ψ₃)

lemma

ρ₁₃_pr₂

L502 ↗

JacobianVarieties.Picard.Proofs.ZariskiGluing.ExZar.ρ₁₃_pr₂

Source context 11 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ZariskiGluing
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
noncomputable section
namespace ExZar
open NeronModelInfra AlgebraicGeometry.RelPicard
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
section three
variable {T T₁ T₂ T₃ : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
    {t₁ : T₁ ⟶ Spec (CommRingCat.of R)} {t₂ : T₂ ⟶ Spec (CommRingCat.of R)}
    {t₃ : T₃ ⟶ Spec (CommRingCat.of R)}
    (ψ₁ : SchemeHomOver t₁ t) (ψ₂ : SchemeHomOver t₂ t) (ψ₃ : SchemeHomOver t₃ t)

Lean source · statement

lemma ρ₁₃_pr₂ : postComp (pr₂ ψ₁ ψ₃) (ρ₁₃ ψ₁ ψ₂ ψ₃) = postComp (pr₂ ψ₂ ψ₃) (ρ₂₃ ψ₁ ψ₂ ψ₃)

lemma

ρ₂₃_pr₁

L505 ↗

JacobianVarieties.Picard.Proofs.ZariskiGluing.ExZar.ρ₂₃_pr₁

Source context 11 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ZariskiGluing
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
noncomputable section
namespace ExZar
open NeronModelInfra AlgebraicGeometry.RelPicard
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
section three
variable {T T₁ T₂ T₃ : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
    {t₁ : T₁ ⟶ Spec (CommRingCat.of R)} {t₂ : T₂ ⟶ Spec (CommRingCat.of R)}
    {t₃ : T₃ ⟶ Spec (CommRingCat.of R)}
    (ψ₁ : SchemeHomOver t₁ t) (ψ₂ : SchemeHomOver t₂ t) (ψ₃ : SchemeHomOver t₃ t)

Lean source · statement

lemma ρ₂₃_pr₁ : postComp (pr₁ ψ₂ ψ₃) (ρ₂₃ ψ₁ ψ₂ ψ₃) = postComp (pr₂ ψ₁ ψ₂) (ρ₁₂ ψ₁ ψ₂ ψ₃)

def

chosenPullback₃

L509 ↗

JacobianVarieties.Picard.Proofs.ZariskiGluing.ExZar.chosenPullback₃

Documentation

The compatible threefold pullback data for the induced base-change morphisms.

Source context 11 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ZariskiGluing
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
noncomputable section
namespace ExZar
open NeronModelInfra AlgebraicGeometry.RelPicard
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
section three
variable {T T₁ T₂ T₃ : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
    {t₁ : T₁ ⟶ Spec (CommRingCat.of R)} {t₂ : T₂ ⟶ Spec (CommRingCat.of R)}
    {t₃ : T₃ ⟶ Spec (CommRingCat.of R)}
    (ψ₁ : SchemeHomOver t₁ t) (ψ₂ : SchemeHomOver t₂ t) (ψ₃ : SchemeHomOver t₃ t)

Lean source · full declaration

def chosenPullback₃ :
    ChosenPullback₃ (chosenPullback c ψ₁ ψ₂) (chosenPullback c ψ₂ ψ₃) (chosenPullback c ψ₁ ψ₃) where
  chosenPullback := chosenPullback c (pr₂ ψ₁ ψ₂) (pr₁ ψ₂ ψ₃)
  p := baseChangeSnd c (postComp (postComp ψ₁ (pr₁ ψ₁ ψ₂)) (ρ₁₂ ψ₁ ψ₂ ψ₃))
  p₁ := baseChangeSnd c (postComp (pr₁ ψ₁ ψ₂) (ρ₁₂ ψ₁ ψ₂ ψ₃))
  p₃ := baseChangeSnd c (postComp (pr₂ ψ₂ ψ₃) (ρ₂₃ ψ₁ ψ₂ ψ₃))
  l :=
    { f := baseChangeSnd c (ρ₁₃ ψ₁ ψ₂ ψ₃)
      f_p₁ := by
        change baseChangeSnd c _ ≫ baseChangeSnd c (pr₁ ψ₁ ψ₃) = _
        rw [baseChangeSnd_comp, ρ₁₃_pr₁]
      f_p₂ := by
        change baseChangeSnd c _ ≫ baseChangeSnd c (pr₂ ψ₁ ψ₃) = _
        rw [baseChangeSnd_comp, ρ₁₃_pr₂]
      f_p := by
        change baseChangeSnd c _ ≫ baseChangeSnd c (postComp ψ₁ (pr₁ ψ₁ ψ₃)) = _
        rw [baseChangeSnd_comp]
        congr 1
        exact Subtype.ext (by
          change (ρ₁₃ ψ₁ ψ₂ ψ₃).1 ≫ (pr₁ ψ₁ ψ₃).1 ≫ ψ₁.1 = (ρ₁₂ ψ₁ ψ₂ ψ₃).1 ≫ (pr₁ ψ₁ ψ₂).1 ≫ ψ₁.1
          simp only [← Category.assoc]
          congr 1
          exact pullback.lift_fst _ _ _) }
  hp₁ := by
    change baseChangeSnd c (ρ₁₂ ψ₁ ψ₂ ψ₃) ≫ baseChangeSnd c (pr₁ ψ₁ ψ₂) = _
    rw [baseChangeSnd_comp]
  hp₃ := by
    change baseChangeSnd c (ρ₂₃ ψ₁ ψ₂ ψ₃) ≫ baseChangeSnd c (pr₂ ψ₂ ψ₃) = _
    rw [baseChangeSnd_comp]

theorem

isInvertible_of_iso

L553 ↗

JacobianVarieties.Picard.Proofs.ZariskiGluing.ExZar.isInvertible_of_iso

Source context 10 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ZariskiGluing
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
noncomputable section
namespace ExZar
open NeronModelInfra AlgebraicGeometry.RelPicard CategoryTheory.Pseudofunctor
open CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
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 isInvertible_of_iso {X : Scheme.{u}} {L L' : X.Modules} (e : L ≅ L')
    (h : Scheme.Modules.IsInvertible L') : Scheme.Modules.IsInvertible L

theorem

isInvertible_of_openCover

L559 ↗

JacobianVarieties.Picard.Proofs.ZariskiGluing.ExZar.isInvertible_of_openCover

Source context 10 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ZariskiGluing
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
noncomputable section
namespace ExZar
open NeronModelInfra AlgebraicGeometry.RelPicard CategoryTheory.Pseudofunctor
open CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
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 isInvertible_of_openCover {Y : Scheme.{u}} {ι : Type u} {V : ι → Scheme.{u}}
    (g : ∀ i, V i ⟶ Y)
    [∀ i, IsOpenImmersion (g i)] (hg : ∀ y : Y, ∃ i, y ∈ Set.range (g i).base) (L : Y.Modules)
    (h : ∀ i, Scheme.Modules.IsInvertible ((Scheme.Modules.pullback (g i)).obj L))
    : Scheme.Modules.IsInvertible L

instance

isOpenImmersion_baseChangeSnd

L580 ↗

JacobianVarieties.Picard.Proofs.ZariskiGluing.ExZar.isOpenImmersion_baseChangeSnd

Source context 12 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ZariskiGluing
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
noncomputable section
namespace ExZar
open NeronModelInfra AlgebraicGeometry.RelPicard CategoryTheory.Pseudofunctor
open CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section Cover
variable {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R))
  {ι : Type u} {U : ι → Scheme.{u}} (u : ∀ i, U i ⟶ Spec (CommRingCat.of R))
  (f : ∀ i, SchemeHomOver (u i) t)

Lean source · statement

instance isOpenImmersion_baseChangeSnd [∀ i, IsOpenImmersion (f i).1] (i : ι) :
    IsOpenImmersion (baseChangeSnd c (f i))

lemma

exists_mem_range_baseChangeSnd

L584 ↗

JacobianVarieties.Picard.Proofs.ZariskiGluing.ExZar.exists_mem_range_baseChangeSnd

Source context 12 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ZariskiGluing
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
noncomputable section
namespace ExZar
open NeronModelInfra AlgebraicGeometry.RelPicard CategoryTheory.Pseudofunctor
open CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section Cover
variable {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R))
  {ι : Type u} {U : ι → Scheme.{u}} (u : ∀ i, U i ⟶ Spec (CommRingCat.of R))
  (f : ∀ i, SchemeHomOver (u i) t)

Lean source · statement

lemma exists_mem_range_baseChangeSnd (hf : ∀ x : T, ∃ i, x ∈ Set.range (f i).1.base)
    (y : (Limits.pullback c t : Scheme.{u})) : ∃ i, y ∈ Set.range (baseChangeSnd c (f i)).base

def

coverBC

L597 ↗

JacobianVarieties.Picard.Proofs.ZariskiGluing.ExZar.coverBC

Documentation

The open cover induced on the base-changed curve by the given open cover of the base.

Source context 12 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ZariskiGluing
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
noncomputable section
namespace ExZar
open NeronModelInfra AlgebraicGeometry.RelPicard CategoryTheory.Pseudofunctor
open CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section Cover
variable {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R))
  {ι : Type u} {U : ι → Scheme.{u}} (u : ∀ i, U i ⟶ Spec (CommRingCat.of R))
  (f : ∀ i, SchemeHomOver (u i) t)

Lean source · statement

def coverBC [∀ i, IsOpenImmersion (f i).1] (hf : ∀ x : T, ∃ i, x ∈ Set.range (f i).1.base) :
    (Limits.pullback c t).OpenCover

abbrev

EE

L613 ↗

JacobianVarieties.Picard.Proofs.ZariskiGluing.ExZar.EE

Documentation

The unit module sheaf on the base scheme.

Source context 12 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ZariskiGluing
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
noncomputable section
namespace ExZar
open NeronModelInfra AlgebraicGeometry.RelPicard CategoryTheory.Pseudofunctor
open CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section Theta
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type u} {U : ι → Scheme.{u}} {u : ∀ i, U i ⟶ Spec (CommRingCat.of R)}
  (f : ∀ i, SchemeHomOver (u i) t) (M : ∀ i, RigidifiedLineBundle c ε (u i))

Lean source · statement

abbrev EE (T : Scheme.{u}) : T.Modules

def

β

L616 ↗

JacobianVarieties.Picard.Proofs.ZariskiGluing.ExZar.β

Documentation

The local rigidification, identified with the pullback of the unit module on the base.

Source context 12 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ZariskiGluing
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
noncomputable section
namespace ExZar
open NeronModelInfra AlgebraicGeometry.RelPicard CategoryTheory.Pseudofunctor
open CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section Theta
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type u} {U : ι → Scheme.{u}} {u : ∀ i, U i ⟶ Spec (CommRingCat.of R)}
  (f : ∀ i, SchemeHomOver (u i) t) (M : ∀ i, RigidifiedLineBundle c ε (u i))

Lean source · statement

def β (i : ι) :
    (Scheme.Modules.pullback (rigSection c (u i) ε)).obj (M i).L
        ≅ (Scheme.Modules.pullback (f i).1).obj (EE T)

def

Θ

L622 ↗

JacobianVarieties.Picard.Proofs.ZariskiGluing.ExZar.Θ

Documentation

Transport a local rigidification through the given commuting square and base morphism.

Source context 12 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ZariskiGluing
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
noncomputable section
namespace ExZar
open NeronModelInfra AlgebraicGeometry.RelPicard CategoryTheory.Pseudofunctor
open CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section Theta
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type u} {U : ι → Scheme.{u}} {u : ∀ i, U i ⟶ Spec (CommRingCat.of R)}
  (f : ∀ i, SchemeHomOver (u i) t) (M : ∀ i, RigidifiedLineBundle c ε (u i))

Lean source · statement

def Θ (i : ι) {Z : Scheme.{u}} (z : Z ⟶ Spec (CommRingCat.of R))
    (g₁ : Limits.pullback c z ⟶ Limits.pullback c (u i)) (ζ₁ : Z ⟶ U i)
    (S₁ : rigSection c z ε ≫ g₁ = ζ₁ ≫ rigSection c (u i) ε) (ζT : Z ⟶ T) (h₁ : ζ₁ ≫ (f i).1 = ζT) :
    (Scheme.Modules.pullback (rigSection c z ε)).obj
        ((Scheme.Modules.pullback g₁).obj (M i).L)
        ≅ (Scheme.Modules.pullback ζT).obj (EE T)

theorem

iso_eq_of_map_rigSection_eq

L636 ↗

JacobianVarieties.Picard.Proofs.ZariskiGluing.ExZar.iso_eq_of_map_rigSection_eq

Source context 12 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ZariskiGluing
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
noncomputable section
namespace ExZar
open NeronModelInfra AlgebraicGeometry.RelPicard CategoryTheory.Pseudofunctor
open CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section Rigidity
variable {Z : Scheme.{u}} (z : Z ⟶ Spec (CommRingCat.of R))

Lean source · full declaration

theorem iso_eq_of_map_rigSection_eq
    (hH0 : ∀ (A : Type u) [CommRing A] [Algebra R A],
      let : Algebra A
          Γ(Limits.pullback c (Scheme.TwoAffineOpenCover.specMap R A), ⊤) :=
        Scheme.TwoAffineOpenCover.algebraOfHom
        (Limits.pullback.snd c (Scheme.TwoAffineOpenCover.specMap R A)) ⊤
      Function.Bijective (algebraMap A
          Γ(Limits.pullback c (Scheme.TwoAffineOpenCover.specMap R A), ⊤)))
    {L₁ L₂ : (Limits.pullback c z).Modules}
    (h₁ : Scheme.Modules.IsInvertible L₁) (h₂ : Scheme.Modules.IsInvertible L₂)
    (r₂ : Nonempty ((Scheme.Modules.pullback (rigSection c z ε)).obj L₂
        ≅ SheafOfModules.unit Z.ringCatSheaf))
    (φ ψ : L₁ ≅ L₂)
    (h : (Scheme.Modules.pullback (rigSection c z ε)).map φ.hom
        = (Scheme.Modules.pullback (rigSection c z ε)).map ψ.hom) :
    φ = ψ := by
  let α' := r₂.some
  let α := (Scheme.Modules.pullback (rigSection c z ε)).mapIso φ ≪≫ α'
  let M₁ : RigidifiedLineBundle c ε z := ⟨L₁, h₁, ⟨α⟩⟩
  let M₂ : RigidifiedLineBundle c ε z := ⟨L₂, h₂, ⟨α'⟩⟩
  have hs := RigidifiedLineBundle.subsingleton_iso_map_pullback_rigSection_comp_eq
    R c ε hH0 z M₁ M₂ α α'
  have hφ : (Scheme.Modules.pullback (rigSection c z ε)).mapIso φ ≪≫ α' = α := rfl
  have hψ : (Scheme.Modules.pullback (rigSection c z ε)).mapIso ψ ≪≫ α' = α := by
    have e : (Scheme.Modules.pullback (rigSection c z ε)).mapIso ψ
        = (Scheme.Modules.pullback (rigSection c z ε)).mapIso φ :=
      Iso.ext h.symm
    rw [e]
  exact congrArg Subtype.val (hs.elim ⟨φ, hφ⟩ ⟨ψ, hψ⟩)

theorem

hom_eq_of_map_rigSection_eq

L666 ↗

JacobianVarieties.Picard.Proofs.ZariskiGluing.ExZar.hom_eq_of_map_rigSection_eq

Source context 12 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ZariskiGluing
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
noncomputable section
namespace ExZar
open NeronModelInfra AlgebraicGeometry.RelPicard CategoryTheory.Pseudofunctor
open CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section Rigidity
variable {Z : Scheme.{u}} (z : Z ⟶ Spec (CommRingCat.of R))

Lean source · full declaration

theorem hom_eq_of_map_rigSection_eq
    (hH0 : ∀ (A : Type u) [CommRing A] [Algebra R A],
      let : Algebra A
          Γ(Limits.pullback c (Scheme.TwoAffineOpenCover.specMap R A), ⊤) :=
        Scheme.TwoAffineOpenCover.algebraOfHom
        (Limits.pullback.snd c (Scheme.TwoAffineOpenCover.specMap R A)) ⊤
      Function.Bijective (algebraMap A
          Γ(Limits.pullback c (Scheme.TwoAffineOpenCover.specMap R A), ⊤)))
    {L₁ L₂ : (Limits.pullback c z).Modules}
    (h₁ : Scheme.Modules.IsInvertible L₁) (h₂ : Scheme.Modules.IsInvertible L₂)
    (r₂ : Nonempty ((Scheme.Modules.pullback (rigSection c z ε)).obj L₂
        ≅ SheafOfModules.unit Z.ringCatSheaf))
    (φ ψ : L₁ ⟶ L₂) (hφ : IsIso φ) (hψ : IsIso ψ)
    (h : (Scheme.Modules.pullback (rigSection c z ε)).map φ
        = (Scheme.Modules.pullback (rigSection c z ε)).map ψ) :
    φ = ψ :=
  congrArg Iso.hom (iso_eq_of_map_rigSection_eq c ε z hH0 h₁ h₂ r₂ (asIso φ) (asIso ψ) h)

theorem

exists_iso_map_rigSection_eq

L684 ↗

JacobianVarieties.Picard.Proofs.ZariskiGluing.ExZar.exists_iso_map_rigSection_eq

Source context 12 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ZariskiGluing
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
noncomputable section
namespace ExZar
open NeronModelInfra AlgebraicGeometry.RelPicard CategoryTheory.Pseudofunctor
open CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section Rigidity
variable {Z : Scheme.{u}} (z : Z ⟶ Spec (CommRingCat.of R))

Lean source · statement

theorem exists_iso_map_rigSection_eq {L₁ L₂ : (Limits.pullback c z).Modules}
    (h₁ : Scheme.Modules.IsInvertible L₁) (h₂ : Scheme.Modules.IsInvertible L₂) {W : Z.Modules}
    (θ₁ : (Scheme.Modules.pullback (rigSection c z ε)).obj L₁ ≅ W)
    (θ₂ : (Scheme.Modules.pullback (rigSection c z ε)).obj L₂ ≅ W)
    (ω : W ≅ SheafOfModules.unit Z.ringCatSheaf) (e : Nonempty (L₁ ≅ L₂)) :
    ∃ Φ : L₁ ≅ L₂, (Scheme.Modules.pullback (rigSection c z ε)).map Φ.hom = θ₁.hom ≫ θ₂.inv

def

fF

L717 ↗

JacobianVarieties.Picard.Proofs.ZariskiGluing.ExZar.fF

Documentation

The base-change morphism from a local curve chart to the curve over the full base.

Source context 12 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ZariskiGluing
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
noncomputable section
namespace ExZar
open NeronModelInfra AlgebraicGeometry.RelPicard CategoryTheory.Pseudofunctor
open CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section Datum
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type u} {U : ι → Scheme.{u}} {u : ∀ i, U i ⟶ Spec (CommRingCat.of R)}
  (f : ∀ i, SchemeHomOver (u i) t) (M : ∀ i, RigidifiedLineBundle c ε (u i))
  (hM : ∀ (i j : ι) (Z : Scheme.{u}) (z : Z ⟶ Spec (CommRingCat.of R))
    (p₁ : SchemeHomOver z (u i)) (p₂ : SchemeHomOver z (u j)),
    p₁.1 ≫ (f i).1 = p₂.1 ≫ (f j).1 →
        Nonempty (((M i).pullbackAlong p₁).L ≅ ((M j).pullbackAlong p₂).L))

Lean source · statement

def fF (i : ι) : Limits.pullback c (u i) ⟶ Limits.pullback c t

def

sqF

L720 ↗

JacobianVarieties.Picard.Proofs.ZariskiGluing.ExZar.sqF

Documentation

The chosen pullback square of two local curve charts.

Source context 12 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ZariskiGluing
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
noncomputable section
namespace ExZar
open NeronModelInfra AlgebraicGeometry.RelPicard CategoryTheory.Pseudofunctor
open CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section Datum
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type u} {U : ι → Scheme.{u}} {u : ∀ i, U i ⟶ Spec (CommRingCat.of R)}
  (f : ∀ i, SchemeHomOver (u i) t) (M : ∀ i, RigidifiedLineBundle c ε (u i))
  (hM : ∀ (i j : ι) (Z : Scheme.{u}) (z : Z ⟶ Spec (CommRingCat.of R))
    (p₁ : SchemeHomOver z (u i)) (p₂ : SchemeHomOver z (u j)),
    p₁.1 ≫ (f i).1 = p₂.1 ≫ (f j).1 →
        Nonempty (((M i).pullbackAlong p₁).L ≅ ((M j).pullbackAlong p₂).L))

Lean source · statement

def sqF (i j : ι) : ChosenPullback (fF c f i) (fF c f j)

def

sq₃F

L723 ↗

JacobianVarieties.Picard.Proofs.ZariskiGluing.ExZar.sq₃F

Documentation

The chosen threefold pullback data for three local curve charts.

Source context 12 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ZariskiGluing
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
noncomputable section
namespace ExZar
open NeronModelInfra AlgebraicGeometry.RelPicard CategoryTheory.Pseudofunctor
open CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section Datum
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type u} {U : ι → Scheme.{u}} {u : ∀ i, U i ⟶ Spec (CommRingCat.of R)}
  (f : ∀ i, SchemeHomOver (u i) t) (M : ∀ i, RigidifiedLineBundle c ε (u i))
  (hM : ∀ (i j : ι) (Z : Scheme.{u}) (z : Z ⟶ Spec (CommRingCat.of R))
    (p₁ : SchemeHomOver z (u i)) (p₂ : SchemeHomOver z (u j)),
    p₁.1 ≫ (f i).1 = p₂.1 ≫ (f j).1 →
        Nonempty (((M i).pullbackAlong p₁).L ≅ ((M j).pullbackAlong p₂).L))

Lean source · statement

def sq₃F (i j k : ι) : ChosenPullback₃ (sqF c f i j) (sqF c f j k) (sqF c f i k)

abbrev

wT

L727 ↗

JacobianVarieties.Picard.Proofs.ZariskiGluing.ExZar.wT

Documentation

The map from a pairwise overlap to the base.

Source context 12 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ZariskiGluing
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
noncomputable section
namespace ExZar
open NeronModelInfra AlgebraicGeometry.RelPicard CategoryTheory.Pseudofunctor
open CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section Datum
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type u} {U : ι → Scheme.{u}} {u : ∀ i, U i ⟶ Spec (CommRingCat.of R)}
  (f : ∀ i, SchemeHomOver (u i) t) (M : ∀ i, RigidifiedLineBundle c ε (u i))
  (hM : ∀ (i j : ι) (Z : Scheme.{u}) (z : Z ⟶ Spec (CommRingCat.of R))
    (p₁ : SchemeHomOver z (u i)) (p₂ : SchemeHomOver z (u j)),
    p₁.1 ≫ (f i).1 = p₂.1 ≫ (f j).1 →
        Nonempty (((M i).pullbackAlong p₁).L ≅ ((M j).pullbackAlong p₂).L))

Lean source · statement

abbrev wT (i j : ι) : Limits.pullback (f i).1 (f j).1 ⟶ T

lemma

pr₂_comp_eq_wT

L729 ↗

JacobianVarieties.Picard.Proofs.ZariskiGluing.ExZar.pr₂_comp_eq_wT

Source context 12 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ZariskiGluing
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
noncomputable section
namespace ExZar
open NeronModelInfra AlgebraicGeometry.RelPicard CategoryTheory.Pseudofunctor
open CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section Datum
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type u} {U : ι → Scheme.{u}} {u : ∀ i, U i ⟶ Spec (CommRingCat.of R)}
  (f : ∀ i, SchemeHomOver (u i) t) (M : ∀ i, RigidifiedLineBundle c ε (u i))
  (hM : ∀ (i j : ι) (Z : Scheme.{u}) (z : Z ⟶ Spec (CommRingCat.of R))
    (p₁ : SchemeHomOver z (u i)) (p₂ : SchemeHomOver z (u j)),
    p₁.1 ≫ (f i).1 = p₂.1 ≫ (f j).1 →
        Nonempty (((M i).pullbackAlong p₁).L ≅ ((M j).pullbackAlong p₂).L))

Lean source · statement

lemma pr₂_comp_eq_wT (i j : ι) : (pr₂ (f i) (f j)).1 ≫ (f j).1 = wT f i j

abbrev

Θ₁

L732 ↗

JacobianVarieties.Picard.Proofs.ZariskiGluing.ExZar.Θ₁

Documentation

The rigidification from the first chart transported to a pairwise overlap.

Source context 12 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ZariskiGluing
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
noncomputable section
namespace ExZar
open NeronModelInfra AlgebraicGeometry.RelPicard CategoryTheory.Pseudofunctor
open CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section Datum
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type u} {U : ι → Scheme.{u}} {u : ∀ i, U i ⟶ Spec (CommRingCat.of R)}
  (f : ∀ i, SchemeHomOver (u i) t) (M : ∀ i, RigidifiedLineBundle c ε (u i))
  (hM : ∀ (i j : ι) (Z : Scheme.{u}) (z : Z ⟶ Spec (CommRingCat.of R))
    (p₁ : SchemeHomOver z (u i)) (p₂ : SchemeHomOver z (u j)),
    p₁.1 ≫ (f i).1 = p₂.1 ≫ (f j).1 →
        Nonempty (((M i).pullbackAlong p₁).L ≅ ((M j).pullbackAlong p₂).L))

Lean source · statement

abbrev Θ₁ (i j : ι)

abbrev

Θ₂

L737 ↗

JacobianVarieties.Picard.Proofs.ZariskiGluing.ExZar.Θ₂

Documentation

The rigidification from the second chart transported to a pairwise overlap.

Source context 12 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ZariskiGluing
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
noncomputable section
namespace ExZar
open NeronModelInfra AlgebraicGeometry.RelPicard CategoryTheory.Pseudofunctor
open CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section Datum
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type u} {U : ι → Scheme.{u}} {u : ∀ i, U i ⟶ Spec (CommRingCat.of R)}
  (f : ∀ i, SchemeHomOver (u i) t) (M : ∀ i, RigidifiedLineBundle c ε (u i))
  (hM : ∀ (i j : ι) (Z : Scheme.{u}) (z : Z ⟶ Spec (CommRingCat.of R))
    (p₁ : SchemeHomOver z (u i)) (p₂ : SchemeHomOver z (u j)),
    p₁.1 ≫ (f i).1 = p₂.1 ≫ (f j).1 →
        Nonempty (((M i).pullbackAlong p₁).L ≅ ((M j).pullbackAlong p₂).L))

Lean source · statement

abbrev Θ₂ (i j : ι)

theorem

exists_homIso

L742 ↗

JacobianVarieties.Picard.Proofs.ZariskiGluing.ExZar.exists_homIso

Source context 13 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ZariskiGluing
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
noncomputable section
namespace ExZar
open NeronModelInfra AlgebraicGeometry.RelPicard CategoryTheory.Pseudofunctor
open CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section Datum
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type u} {U : ι → Scheme.{u}} {u : ∀ i, U i ⟶ Spec (CommRingCat.of R)}
  (f : ∀ i, SchemeHomOver (u i) t) (M : ∀ i, RigidifiedLineBundle c ε (u i))
  (hM : ∀ (i j : ι) (Z : Scheme.{u}) (z : Z ⟶ Spec (CommRingCat.of R))
    (p₁ : SchemeHomOver z (u i)) (p₂ : SchemeHomOver z (u j)),
    p₁.1 ≫ (f i).1 = p₂.1 ≫ (f j).1 →
        Nonempty (((M i).pullbackAlong p₁).L ≅ ((M j).pullbackAlong p₂).L))
include hM in

Lean source · statement

theorem exists_homIso (i j : ι) :
    ∃ Φ : (Scheme.Modules.pullback (baseChangeSnd c (pr₁ (f i) (f j)))).obj (M i).L ≅
        (Scheme.Modules.pullback (baseChangeSnd c (pr₂ (f i) (f j)))).obj (M j).L,
      (Scheme.Modules.pullback (rigSection c (strMap₁₂ (f i) (f j)) ε)).map Φ.hom =
        (Θ₁ c ε f M i j).hom ≫ (Θ₂ c ε f M i j).inv

def

homIso

L753 ↗

JacobianVarieties.Picard.Proofs.ZariskiGluing.ExZar.homIso

Documentation

Choose an isomorphism between the local line bundles on their pairwise overlap.

Source context 13 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ZariskiGluing
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
noncomputable section
namespace ExZar
open NeronModelInfra AlgebraicGeometry.RelPicard CategoryTheory.Pseudofunctor
open CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section Datum
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type u} {U : ι → Scheme.{u}} {u : ∀ i, U i ⟶ Spec (CommRingCat.of R)}
  (f : ∀ i, SchemeHomOver (u i) t) (M : ∀ i, RigidifiedLineBundle c ε (u i))
  (hM : ∀ (i j : ι) (Z : Scheme.{u}) (z : Z ⟶ Spec (CommRingCat.of R))
    (p₁ : SchemeHomOver z (u i)) (p₂ : SchemeHomOver z (u j)),
    p₁.1 ≫ (f i).1 = p₂.1 ≫ (f j).1 →
        Nonempty (((M i).pullbackAlong p₁).L ≅ ((M j).pullbackAlong p₂).L))
include hM in

Lean source · statement

def homIso (i j : ι) :
    (Scheme.Modules.pullback (baseChangeSnd c (pr₁ (f i) (f j)))).obj (M i).L ≅
      (Scheme.Modules.pullback (baseChangeSnd c (pr₂ (f i) (f j)))).obj (M j).L

theorem

map_homIso

L758 ↗

JacobianVarieties.Picard.Proofs.ZariskiGluing.ExZar.map_homIso

Source context 12 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ZariskiGluing
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
noncomputable section
namespace ExZar
open NeronModelInfra AlgebraicGeometry.RelPicard CategoryTheory.Pseudofunctor
open CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section Datum
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type u} {U : ι → Scheme.{u}} {u : ∀ i, U i ⟶ Spec (CommRingCat.of R)}
  (f : ∀ i, SchemeHomOver (u i) t) (M : ∀ i, RigidifiedLineBundle c ε (u i))
  (hM : ∀ (i j : ι) (Z : Scheme.{u}) (z : Z ⟶ Spec (CommRingCat.of R))
    (p₁ : SchemeHomOver z (u i)) (p₂ : SchemeHomOver z (u j)),
    p₁.1 ≫ (f i).1 = p₂.1 ≫ (f j).1 →
        Nonempty (((M i).pullbackAlong p₁).L ≅ ((M j).pullbackAlong p₂).L))

Lean source · statement

theorem map_homIso (i j : ι) :
    (Scheme.Modules.pullback (rigSection c (strMap₁₂ (f i) (f j)) ε)).map
        (homIso c ε f M hM i j).hom =
      (Θ₁ c ε f M i j).hom ≫ (Θ₂ c ε f M i j).inv

theorem

half_A

L774 ↗

JacobianVarieties.Picard.Proofs.ZariskiGluing.ExZar.half_A

Source context 15 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ZariskiGluing
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
noncomputable section
namespace ExZar
open NeronModelInfra AlgebraicGeometry.RelPicard CategoryTheory.Pseudofunctor
open CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section Datum
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type u} {U : ι → Scheme.{u}} {u : ∀ i, U i ⟶ Spec (CommRingCat.of R)}
  (f : ∀ i, SchemeHomOver (u i) t) (M : ∀ i, RigidifiedLineBundle c ε (u i))
  (hM : ∀ (i j : ι) (Z : Scheme.{u}) (z : Z ⟶ Spec (CommRingCat.of R))
    (p₁ : SchemeHomOver z (u i)) (p₂ : SchemeHomOver z (u j)),
    p₁.1 ≫ (f i).1 = p₂.1 ≫ (f j).1 →
        Nonempty (((M i).pullbackAlong p₁).L ≅ ((M j).pullbackAlong p₂).L))
section Half
variable (k : ι) {W Z : Scheme.{u}} {w : W ⟶ Spec (CommRingCat.of R)}
    {z : Z ⟶ Spec (CommRingCat.of R)}
    (π : SchemeHomOver w (u k)) (wT' : W ⟶ T) (hw : π.1 ≫ (f k).1 = wT')
    (ζ : SchemeHomOver z w) (g : Limits.pullback c z ⟶ Limits.pullback c (u k))
    (hg : baseChangeSnd c ζ ≫ baseChangeSnd c π = g)
    (ζ₁ : Z ⟶ U k) (hζ₁ : ζ.1 ≫ π.1 = ζ₁) (S₁ : rigSection c z ε ≫ g = ζ₁ ≫ rigSection c (u k) ε)
    (ζT : Z ⟶ T) (h₁ : ζ₁ ≫ (f k).1 = ζT) (hT : ζ.1 ≫ wT' = ζT)
include hg hζ₁ S₁ in

Lean source · statement

theorem half_A :
    (Scheme.Modules.pullback (rigSection c z ε)).map
        ((τ (baseChangeSnd c ζ) (baseChangeSnd c π) g hg).inv.app (M k).L) ≫
      (sqIso (rigSection_baseChangeSnd c ε ζ)).hom.app
          ((Scheme.Modules.pullback (baseChangeSnd c π)).obj (M k).L) ≫
      (Scheme.Modules.pullback ζ.1).map ((sqIso (rigSection_baseChangeSnd c ε π)).hom.app (M k).L) =
    (sqIso S₁).hom.app (M k).L ≫
      (τ ζ.1 π.1 ζ₁ hζ₁).inv.app ((Scheme.Modules.pullback (rigSection c (u k) ε)).obj (M k).L)

theorem

half_B

L793 ↗

JacobianVarieties.Picard.Proofs.ZariskiGluing.ExZar.half_B

Source context 15 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ZariskiGluing
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
noncomputable section
namespace ExZar
open NeronModelInfra AlgebraicGeometry.RelPicard CategoryTheory.Pseudofunctor
open CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section Datum
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type u} {U : ι → Scheme.{u}} {u : ∀ i, U i ⟶ Spec (CommRingCat.of R)}
  (f : ∀ i, SchemeHomOver (u i) t) (M : ∀ i, RigidifiedLineBundle c ε (u i))
  (hM : ∀ (i j : ι) (Z : Scheme.{u}) (z : Z ⟶ Spec (CommRingCat.of R))
    (p₁ : SchemeHomOver z (u i)) (p₂ : SchemeHomOver z (u j)),
    p₁.1 ≫ (f i).1 = p₂.1 ≫ (f j).1 →
        Nonempty (((M i).pullbackAlong p₁).L ≅ ((M j).pullbackAlong p₂).L))
section Half
variable (k : ι) {W Z : Scheme.{u}} {w : W ⟶ Spec (CommRingCat.of R)}
    {z : Z ⟶ Spec (CommRingCat.of R)}
    (π : SchemeHomOver w (u k)) (wT' : W ⟶ T) (hw : π.1 ≫ (f k).1 = wT')
    (ζ : SchemeHomOver z w) (g : Limits.pullback c z ⟶ Limits.pullback c (u k))
    (hg : baseChangeSnd c ζ ≫ baseChangeSnd c π = g)
    (ζ₁ : Z ⟶ U k) (hζ₁ : ζ.1 ≫ π.1 = ζ₁) (S₁ : rigSection c z ε ≫ g = ζ₁ ≫ rigSection c (u k) ε)
    (ζT : Z ⟶ T) (h₁ : ζ₁ ≫ (f k).1 = ζT) (hT : ζ.1 ≫ wT' = ζT)
include hζ₁ in

Lean source · statement

theorem half_B :
    (τ ζ.1 π.1 ζ₁ hζ₁).inv.app ((Scheme.Modules.pullback (rigSection c (u k) ε)).obj (M k).L) ≫
      (Scheme.Modules.pullback ζ.1).map ((Scheme.Modules.pullback π.1).map (β c ε f M k).hom) =
    (Scheme.Modules.pullback ζ₁).map (β c ε f M k).hom ≫
      (τ ζ.1 π.1 ζ₁ hζ₁).inv.app ((Scheme.Modules.pullback (f k).1).obj (EE T))

theorem

half_C

L801 ↗

JacobianVarieties.Picard.Proofs.ZariskiGluing.ExZar.half_C

Source context 15 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ZariskiGluing
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
noncomputable section
namespace ExZar
open NeronModelInfra AlgebraicGeometry.RelPicard CategoryTheory.Pseudofunctor
open CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section Datum
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type u} {U : ι → Scheme.{u}} {u : ∀ i, U i ⟶ Spec (CommRingCat.of R)}
  (f : ∀ i, SchemeHomOver (u i) t) (M : ∀ i, RigidifiedLineBundle c ε (u i))
  (hM : ∀ (i j : ι) (Z : Scheme.{u}) (z : Z ⟶ Spec (CommRingCat.of R))
    (p₁ : SchemeHomOver z (u i)) (p₂ : SchemeHomOver z (u j)),
    p₁.1 ≫ (f i).1 = p₂.1 ≫ (f j).1 →
        Nonempty (((M i).pullbackAlong p₁).L ≅ ((M j).pullbackAlong p₂).L))
section Half
variable (k : ι) {W Z : Scheme.{u}} {w : W ⟶ Spec (CommRingCat.of R)}
    {z : Z ⟶ Spec (CommRingCat.of R)}
    (π : SchemeHomOver w (u k)) (wT' : W ⟶ T) (hw : π.1 ≫ (f k).1 = wT')
    (ζ : SchemeHomOver z w) (g : Limits.pullback c z ⟶ Limits.pullback c (u k))
    (hg : baseChangeSnd c ζ ≫ baseChangeSnd c π = g)
    (ζ₁ : Z ⟶ U k) (hζ₁ : ζ.1 ≫ π.1 = ζ₁) (S₁ : rigSection c z ε ≫ g = ζ₁ ≫ rigSection c (u k) ε)
    (ζT : Z ⟶ T) (h₁ : ζ₁ ≫ (f k).1 = ζT) (hT : ζ.1 ≫ wT' = ζT)
include hζ₁ hw h₁ hT in

Lean source · statement

theorem half_C :
    (τ ζ.1 π.1 ζ₁ hζ₁).inv.app ((Scheme.Modules.pullback (f k).1).obj (EE T)) ≫
      (Scheme.Modules.pullback ζ.1).map ((τ π.1 (f k).1 wT' hw).hom.app (EE T)) =
    (τ ζ₁ (f k).1 ζT h₁).hom.app (EE T) ≫ (τ ζ.1 wT' ζT hT).inv.app (EE T)

theorem

half

L810 ↗

JacobianVarieties.Picard.Proofs.ZariskiGluing.ExZar.half

Source context 15 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ZariskiGluing
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
noncomputable section
namespace ExZar
open NeronModelInfra AlgebraicGeometry.RelPicard CategoryTheory.Pseudofunctor
open CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section Datum
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type u} {U : ι → Scheme.{u}} {u : ∀ i, U i ⟶ Spec (CommRingCat.of R)}
  (f : ∀ i, SchemeHomOver (u i) t) (M : ∀ i, RigidifiedLineBundle c ε (u i))
  (hM : ∀ (i j : ι) (Z : Scheme.{u}) (z : Z ⟶ Spec (CommRingCat.of R))
    (p₁ : SchemeHomOver z (u i)) (p₂ : SchemeHomOver z (u j)),
    p₁.1 ≫ (f i).1 = p₂.1 ≫ (f j).1 →
        Nonempty (((M i).pullbackAlong p₁).L ≅ ((M j).pullbackAlong p₂).L))
section Half
variable (k : ι) {W Z : Scheme.{u}} {w : W ⟶ Spec (CommRingCat.of R)}
    {z : Z ⟶ Spec (CommRingCat.of R)}
    (π : SchemeHomOver w (u k)) (wT' : W ⟶ T) (hw : π.1 ≫ (f k).1 = wT')
    (ζ : SchemeHomOver z w) (g : Limits.pullback c z ⟶ Limits.pullback c (u k))
    (hg : baseChangeSnd c ζ ≫ baseChangeSnd c π = g)
    (ζ₁ : Z ⟶ U k) (hζ₁ : ζ.1 ≫ π.1 = ζ₁) (S₁ : rigSection c z ε ≫ g = ζ₁ ≫ rigSection c (u k) ε)
    (ζT : Z ⟶ T) (h₁ : ζ₁ ≫ (f k).1 = ζT) (hT : ζ.1 ≫ wT' = ζT)
include hζ₁ in

Lean source · statement

theorem half :
    (Scheme.Modules.pullback (rigSection c z ε)).map
        ((τ (baseChangeSnd c ζ) (baseChangeSnd c π) g hg).inv.app (M k).L) ≫
      (sqIso (rigSection_baseChangeSnd c ε ζ)).hom.app
          ((Scheme.Modules.pullback (baseChangeSnd c π)).obj (M k).L) ≫
      (Scheme.Modules.pullback ζ.1).map (Θ c ε f M k w (baseChangeSnd c π) π.1
          (rigSection_baseChangeSnd c ε π) wT' hw).hom =
    (Θ c ε f M k z g ζ₁ S₁ ζT h₁).hom ≫ (τ ζ.1 wT' ζT hT).inv.app (EE T)

theorem

half'

L830 ↗

JacobianVarieties.Picard.Proofs.ZariskiGluing.ExZar.half'

Source context 15 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ZariskiGluing
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
noncomputable section
namespace ExZar
open NeronModelInfra AlgebraicGeometry.RelPicard CategoryTheory.Pseudofunctor
open CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section Datum
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type u} {U : ι → Scheme.{u}} {u : ∀ i, U i ⟶ Spec (CommRingCat.of R)}
  (f : ∀ i, SchemeHomOver (u i) t) (M : ∀ i, RigidifiedLineBundle c ε (u i))
  (hM : ∀ (i j : ι) (Z : Scheme.{u}) (z : Z ⟶ Spec (CommRingCat.of R))
    (p₁ : SchemeHomOver z (u i)) (p₂ : SchemeHomOver z (u j)),
    p₁.1 ≫ (f i).1 = p₂.1 ≫ (f j).1 →
        Nonempty (((M i).pullbackAlong p₁).L ≅ ((M j).pullbackAlong p₂).L))
section Half
variable (k : ι) {W Z : Scheme.{u}} {w : W ⟶ Spec (CommRingCat.of R)}
    {z : Z ⟶ Spec (CommRingCat.of R)}
    (π : SchemeHomOver w (u k)) (wT' : W ⟶ T) (hw : π.1 ≫ (f k).1 = wT')
    (ζ : SchemeHomOver z w) (g : Limits.pullback c z ⟶ Limits.pullback c (u k))
    (hg : baseChangeSnd c ζ ≫ baseChangeSnd c π = g)
    (ζ₁ : Z ⟶ U k) (hζ₁ : ζ.1 ≫ π.1 = ζ₁) (S₁ : rigSection c z ε ≫ g = ζ₁ ≫ rigSection c (u k) ε)
    (ζT : Z ⟶ T) (h₁ : ζ₁ ≫ (f k).1 = ζT) (hT : ζ.1 ≫ wT' = ζT)
include hζ₁ in

Lean source · statement

theorem half' :
    (Scheme.Modules.pullback (rigSection c z ε)).map
        ((τ (baseChangeSnd c ζ) (baseChangeSnd c π) g hg).inv.app (M k).L) ≫
      (sqIso (rigSection_baseChangeSnd c ε ζ)).hom.app
          ((Scheme.Modules.pullback (baseChangeSnd c π)).obj (M k).L) ≫
      (Scheme.Modules.pullback ζ.1).map (Θ c ε f M k w (baseChangeSnd c π) π.1
          (rigSection_baseChangeSnd c ε π) wT' hw).hom =
    (Θ c ε f M k z g ζ₁ S₁ ζT h₁).hom ≫ (τ ζ.1 wT' ζT hT).inv.app (EE T)

theorem

half_inv

L846 ↗

JacobianVarieties.Picard.Proofs.ZariskiGluing.ExZar.half_inv

Source context 15 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ZariskiGluing
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
noncomputable section
namespace ExZar
open NeronModelInfra AlgebraicGeometry.RelPicard CategoryTheory.Pseudofunctor
open CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section Datum
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type u} {U : ι → Scheme.{u}} {u : ∀ i, U i ⟶ Spec (CommRingCat.of R)}
  (f : ∀ i, SchemeHomOver (u i) t) (M : ∀ i, RigidifiedLineBundle c ε (u i))
  (hM : ∀ (i j : ι) (Z : Scheme.{u}) (z : Z ⟶ Spec (CommRingCat.of R))
    (p₁ : SchemeHomOver z (u i)) (p₂ : SchemeHomOver z (u j)),
    p₁.1 ≫ (f i).1 = p₂.1 ≫ (f j).1 →
        Nonempty (((M i).pullbackAlong p₁).L ≅ ((M j).pullbackAlong p₂).L))
section Half
variable (k : ι) {W Z : Scheme.{u}} {w : W ⟶ Spec (CommRingCat.of R)}
    {z : Z ⟶ Spec (CommRingCat.of R)}
    (π : SchemeHomOver w (u k)) (wT' : W ⟶ T) (hw : π.1 ≫ (f k).1 = wT')
    (ζ : SchemeHomOver z w) (g : Limits.pullback c z ⟶ Limits.pullback c (u k))
    (hg : baseChangeSnd c ζ ≫ baseChangeSnd c π = g)
    (ζ₁ : Z ⟶ U k) (hζ₁ : ζ.1 ≫ π.1 = ζ₁) (S₁ : rigSection c z ε ≫ g = ζ₁ ≫ rigSection c (u k) ε)
    (ζT : Z ⟶ T) (h₁ : ζ₁ ≫ (f k).1 = ζT) (hT : ζ.1 ≫ wT' = ζT)
include hζ₁ in

Lean source · statement

theorem half_inv :
    (Scheme.Modules.pullback ζ.1).map (Θ c ε f M k w (baseChangeSnd c π) π.1
        (rigSection_baseChangeSnd c ε π) wT' hw).inv ≫
      (sqIso (rigSection_baseChangeSnd c ε ζ)).inv.app
          ((Scheme.Modules.pullback (baseChangeSnd c π)).obj (M k).L) ≫
      (Scheme.Modules.pullback (rigSection c z ε)).map
          ((τ (baseChangeSnd c ζ) (baseChangeSnd c π) g hg).hom.app (M k).L) =
    (τ ζ.1 wT' ζT hT).hom.app (EE T) ≫ (Θ c ε f M k z g ζ₁ S₁ ζT h₁).inv

theorem

key

L870 ↗

JacobianVarieties.Picard.Proofs.ZariskiGluing.ExZar.key

Source context 12 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ZariskiGluing
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
noncomputable section
namespace ExZar
open NeronModelInfra AlgebraicGeometry.RelPicard CategoryTheory.Pseudofunctor
open CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section Datum
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type u} {U : ι → Scheme.{u}} {u : ∀ i, U i ⟶ Spec (CommRingCat.of R)}
  (f : ∀ i, SchemeHomOver (u i) t) (M : ∀ i, RigidifiedLineBundle c ε (u i))
  (hM : ∀ (i j : ι) (Z : Scheme.{u}) (z : Z ⟶ Spec (CommRingCat.of R))
    (p₁ : SchemeHomOver z (u i)) (p₂ : SchemeHomOver z (u j)),
    p₁.1 ≫ (f i).1 = p₂.1 ≫ (f j).1 →
        Nonempty (((M i).pullbackAlong p₁).L ≅ ((M j).pullbackAlong p₂).L))

Lean source · statement

theorem key (i j : ι) {Z : Scheme.{u}} {z : Z ⟶ Spec (CommRingCat.of R)}
    (ζ : SchemeHomOver z (strMap₁₂ (f i) (f j)))
    (g : Limits.pullback c z ⟶ Limits.pullback c (strMap₁₂ (f i) (f j)))
    (hg : g = baseChangeSnd c ζ)
    (g₁ : Limits.pullback c z ⟶ Limits.pullback c (u i))
    (g₂ : Limits.pullback c z ⟶ Limits.pullback c (u j))
    (hg₁ : g ≫ baseChangeSnd c (pr₁ (f i) (f j)) = g₁)
    (hg₂ : g ≫ baseChangeSnd c (pr₂ (f i) (f j)) = g₂)
    (ζ₁ : Z ⟶ U i) (ζ₂ : Z ⟶ U j)
    (hζ₁ : ζ.1 ≫ (pr₁ (f i) (f j)).1 = ζ₁) (hζ₂ : ζ.1 ≫ (pr₂ (f i) (f j)).1 = ζ₂)
    (S₁ : rigSection c z ε ≫ g₁ = ζ₁ ≫ rigSection c (u i) ε)
    (S₂ : rigSection c z ε ≫ g₂ = ζ₂ ≫ rigSection c (u j) ε)
    (ζT : Z ⟶ T) (h₁ : ζ₁ ≫ (f i).1 = ζT) (h₂ : ζ₂ ≫ (f j).1 = ζT) :
    (Scheme.Modules.pullback (rigSection c z ε)).map
      (pullHomIso (homIso c ε f M hM i j) g g₁ g₂ hg₁ hg₂).hom =
      (Θ c ε f M i z g₁ ζ₁ S₁ ζT h₁).hom ≫ (Θ c ε f M j z g₂ ζ₂ S₂ ζT h₂).inv

def

δ

L918 ↗

JacobianVarieties.Picard.Proofs.ZariskiGluing.ExZar.δ

Documentation

The diagonal map to the self-overlap as a morphism over the base.

Source context 12 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ZariskiGluing
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
noncomputable section
namespace ExZar
open NeronModelInfra AlgebraicGeometry.RelPicard CategoryTheory.Pseudofunctor
open CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section Datum
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type u} {U : ι → Scheme.{u}} {u : ∀ i, U i ⟶ Spec (CommRingCat.of R)}
  (f : ∀ i, SchemeHomOver (u i) t) (M : ∀ i, RigidifiedLineBundle c ε (u i))
  (hM : ∀ (i j : ι) (Z : Scheme.{u}) (z : Z ⟶ Spec (CommRingCat.of R))
    (p₁ : SchemeHomOver z (u i)) (p₂ : SchemeHomOver z (u j)),
    p₁.1 ≫ (f i).1 = p₂.1 ≫ (f j).1 →
        Nonempty (((M i).pullbackAlong p₁).L ≅ ((M j).pullbackAlong p₂).L))

Lean source · statement

def δ (i : ι) : SchemeHomOver (u i) (strMap₁₂ (f i) (f i))

lemma

δ_pr₁

L921 ↗

JacobianVarieties.Picard.Proofs.ZariskiGluing.ExZar.δ_pr₁

Source context 12 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ZariskiGluing
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
noncomputable section
namespace ExZar
open NeronModelInfra AlgebraicGeometry.RelPicard CategoryTheory.Pseudofunctor
open CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section Datum
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type u} {U : ι → Scheme.{u}} {u : ∀ i, U i ⟶ Spec (CommRingCat.of R)}
  (f : ∀ i, SchemeHomOver (u i) t) (M : ∀ i, RigidifiedLineBundle c ε (u i))
  (hM : ∀ (i j : ι) (Z : Scheme.{u}) (z : Z ⟶ Spec (CommRingCat.of R))
    (p₁ : SchemeHomOver z (u i)) (p₂ : SchemeHomOver z (u j)),
    p₁.1 ≫ (f i).1 = p₂.1 ≫ (f j).1 →
        Nonempty (((M i).pullbackAlong p₁).L ≅ ((M j).pullbackAlong p₂).L))

Lean source · statement

lemma δ_pr₁ (i : ι) : baseChangeSnd c (δ f i) ≫ baseChangeSnd c (pr₁ (f i) (f i)) = 𝟙 _

lemma

δ_pr₂

L928 ↗

JacobianVarieties.Picard.Proofs.ZariskiGluing.ExZar.δ_pr₂

Source context 12 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ZariskiGluing
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
noncomputable section
namespace ExZar
open NeronModelInfra AlgebraicGeometry.RelPicard CategoryTheory.Pseudofunctor
open CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section Datum
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type u} {U : ι → Scheme.{u}} {u : ∀ i, U i ⟶ Spec (CommRingCat.of R)}
  (f : ∀ i, SchemeHomOver (u i) t) (M : ∀ i, RigidifiedLineBundle c ε (u i))
  (hM : ∀ (i j : ι) (Z : Scheme.{u}) (z : Z ⟶ Spec (CommRingCat.of R))
    (p₁ : SchemeHomOver z (u i)) (p₂ : SchemeHomOver z (u j)),
    p₁.1 ≫ (f i).1 = p₂.1 ≫ (f j).1 →
        Nonempty (((M i).pullbackAlong p₁).L ≅ ((M j).pullbackAlong p₂).L))

Lean source · statement

lemma δ_pr₂ (i : ι) : baseChangeSnd c (δ f i) ≫ baseChangeSnd c (pr₂ (f i) (f i)) = 𝟙 _

lemma

nonempty_rigidification

L935 ↗

JacobianVarieties.Picard.Proofs.ZariskiGluing.ExZar.nonempty_rigidification

Source context 12 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ZariskiGluing
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
noncomputable section
namespace ExZar
open NeronModelInfra AlgebraicGeometry.RelPicard CategoryTheory.Pseudofunctor
open CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section Datum
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type u} {U : ι → Scheme.{u}} {u : ∀ i, U i ⟶ Spec (CommRingCat.of R)}
  (f : ∀ i, SchemeHomOver (u i) t) (M : ∀ i, RigidifiedLineBundle c ε (u i))
  (hM : ∀ (i j : ι) (Z : Scheme.{u}) (z : Z ⟶ Spec (CommRingCat.of R))
    (p₁ : SchemeHomOver z (u i)) (p₂ : SchemeHomOver z (u j)),
    p₁.1 ≫ (f i).1 = p₂.1 ≫ (f j).1 →
        Nonempty (((M i).pullbackAlong p₁).L ≅ ((M j).pullbackAlong p₂).L))

Lean source · statement

lemma nonempty_rigidification (i : ι) {Z : Scheme.{u}} (z : Z ⟶ Spec (CommRingCat.of R))
    (g₁ : Limits.pullback c z ⟶ Limits.pullback c (u i)) (ζ₁ : Z ⟶ U i)
    (S₁ : rigSection c z ε ≫ g₁ = ζ₁ ≫ rigSection c (u i) ε) (ζT : Z ⟶ T) (h₁ : ζ₁ ≫ (f i).1 = ζT) :
    Nonempty
        ((Scheme.Modules.pullback (rigSection c z ε)).obj
          ((Scheme.Modules.pullback g₁).obj (M i).L) ≅
      SheafOfModules.unit Z.ringCatSheaf)

theorem

pullHomIso_self

L944 ↗

JacobianVarieties.Picard.Proofs.ZariskiGluing.ExZar.pullHomIso_self

Source context 12 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ZariskiGluing
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
noncomputable section
namespace ExZar
open NeronModelInfra AlgebraicGeometry.RelPicard CategoryTheory.Pseudofunctor
open CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section Datum
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type u} {U : ι → Scheme.{u}} {u : ∀ i, U i ⟶ Spec (CommRingCat.of R)}
  (f : ∀ i, SchemeHomOver (u i) t) (M : ∀ i, RigidifiedLineBundle c ε (u i))
  (hM : ∀ (i j : ι) (Z : Scheme.{u}) (z : Z ⟶ Spec (CommRingCat.of R))
    (p₁ : SchemeHomOver z (u i)) (p₂ : SchemeHomOver z (u j)),
    p₁.1 ≫ (f i).1 = p₂.1 ≫ (f j).1 →
        Nonempty (((M i).pullbackAlong p₁).L ≅ ((M j).pullbackAlong p₂).L))

Lean source · full declaration

theorem pullHomIso_self (hH0 : ∀ (A : Type u) [CommRing A] [Algebra R A],
      let : Algebra A
          Γ(Limits.pullback c (Scheme.TwoAffineOpenCover.specMap R A), ⊤) :=
        Scheme.TwoAffineOpenCover.algebraOfHom
        (Limits.pullback.snd c (Scheme.TwoAffineOpenCover.specMap R A)) ⊤
      Function.Bijective (algebraMap A
          Γ(Limits.pullback c (Scheme.TwoAffineOpenCover.specMap R A), ⊤)))
    (i : ι) :
    pullHomIso (homIso c ε f M hM i i) (baseChangeSnd c (δ f i)) (𝟙 _) (𝟙 _) (δ_pr₁ c f i)
        (δ_pr₂ c f i) =
      Iso.refl _ := by
  have S : rigSection c (u i) ε ≫ 𝟙 _ = 𝟙 _ ≫ rigSection c (u i) ε := by
    simp only [Category.comp_id, Category.id_comp]
  have K := key c ε f M hM i i (δ f i) _ rfl (𝟙 _) (𝟙 _) (δ_pr₁ c f i) (δ_pr₂ c f i) (𝟙 _) (𝟙 _)
    (pullback.lift_fst _ _ _) (pullback.lift_snd _ _ _) S S (f i).1
      (Category.id_comp _) (Category.id_comp _)
  exact iso_eq_of_map_rigSection_eq c ε (u i) hH0
    ((M i).isInvertible.pullback _) ((M i).isInvertible.pullback _)
    (nonempty_rigidification c ε f M i (u i) (𝟙 _) (𝟙 _) S (f i).1 (Category.id_comp _)) _ _ (by
      rw [K, Iso.hom_inv_id, Iso.refl_hom, CategoryTheory.Functor.map_id])

abbrev

ζT3

L969 ↗

JacobianVarieties.Picard.Proofs.ZariskiGluing.ExZar.ζT3

Documentation

The structure map from a triple overlap to the base.

Source context 14 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ZariskiGluing
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
noncomputable section
namespace ExZar
open NeronModelInfra AlgebraicGeometry.RelPicard CategoryTheory.Pseudofunctor
open CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section Datum
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type u} {U : ι → Scheme.{u}} {u : ∀ i, U i ⟶ Spec (CommRingCat.of R)}
  (f : ∀ i, SchemeHomOver (u i) t) (M : ∀ i, RigidifiedLineBundle c ε (u i))
  (hM : ∀ (i j : ι) (Z : Scheme.{u}) (z : Z ⟶ Spec (CommRingCat.of R))
    (p₁ : SchemeHomOver z (u i)) (p₂ : SchemeHomOver z (u j)),
    p₁.1 ≫ (f i).1 = p₂.1 ≫ (f j).1 →
        Nonempty (((M i).pullbackAlong p₁).L ≅ ((M j).pullbackAlong p₂).L))
section comp
variable (i j k : ι)

Lean source · statement

abbrev ζT3 : Limits.pullback (pr₂ (f i) (f j)).1 (pr₁ (f j) (f k)).1 ⟶ T

abbrev

χ₁

L973 ↗

JacobianVarieties.Picard.Proofs.ZariskiGluing.ExZar.χ₁

Documentation

The first chart projection from the triple overlap.

Source context 14 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ZariskiGluing
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
noncomputable section
namespace ExZar
open NeronModelInfra AlgebraicGeometry.RelPicard CategoryTheory.Pseudofunctor
open CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section Datum
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type u} {U : ι → Scheme.{u}} {u : ∀ i, U i ⟶ Spec (CommRingCat.of R)}
  (f : ∀ i, SchemeHomOver (u i) t) (M : ∀ i, RigidifiedLineBundle c ε (u i))
  (hM : ∀ (i j : ι) (Z : Scheme.{u}) (z : Z ⟶ Spec (CommRingCat.of R))
    (p₁ : SchemeHomOver z (u i)) (p₂ : SchemeHomOver z (u j)),
    p₁.1 ≫ (f i).1 = p₂.1 ≫ (f j).1 →
        Nonempty (((M i).pullbackAlong p₁).L ≅ ((M j).pullbackAlong p₂).L))
section comp
variable (i j k : ι)

Lean source · statement

abbrev χ₁ : Limits.pullback (pr₂ (f i) (f j)).1 (pr₁ (f j) (f k)).1 ⟶ U i

abbrev

χ₂

L976 ↗

JacobianVarieties.Picard.Proofs.ZariskiGluing.ExZar.χ₂

Documentation

The second chart projection from the triple overlap.

Source context 14 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ZariskiGluing
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
noncomputable section
namespace ExZar
open NeronModelInfra AlgebraicGeometry.RelPicard CategoryTheory.Pseudofunctor
open CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section Datum
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type u} {U : ι → Scheme.{u}} {u : ∀ i, U i ⟶ Spec (CommRingCat.of R)}
  (f : ∀ i, SchemeHomOver (u i) t) (M : ∀ i, RigidifiedLineBundle c ε (u i))
  (hM : ∀ (i j : ι) (Z : Scheme.{u}) (z : Z ⟶ Spec (CommRingCat.of R))
    (p₁ : SchemeHomOver z (u i)) (p₂ : SchemeHomOver z (u j)),
    p₁.1 ≫ (f i).1 = p₂.1 ≫ (f j).1 →
        Nonempty (((M i).pullbackAlong p₁).L ≅ ((M j).pullbackAlong p₂).L))
section comp
variable (i j k : ι)

Lean source · statement

abbrev χ₂ : Limits.pullback (pr₂ (f i) (f j)).1 (pr₁ (f j) (f k)).1 ⟶ U j

abbrev

χ₃

L979 ↗

JacobianVarieties.Picard.Proofs.ZariskiGluing.ExZar.χ₃

Documentation

The third chart projection from the triple overlap.

Source context 14 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ZariskiGluing
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
noncomputable section
namespace ExZar
open NeronModelInfra AlgebraicGeometry.RelPicard CategoryTheory.Pseudofunctor
open CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section Datum
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type u} {U : ι → Scheme.{u}} {u : ∀ i, U i ⟶ Spec (CommRingCat.of R)}
  (f : ∀ i, SchemeHomOver (u i) t) (M : ∀ i, RigidifiedLineBundle c ε (u i))
  (hM : ∀ (i j : ι) (Z : Scheme.{u}) (z : Z ⟶ Spec (CommRingCat.of R))
    (p₁ : SchemeHomOver z (u i)) (p₂ : SchemeHomOver z (u j)),
    p₁.1 ≫ (f i).1 = p₂.1 ≫ (f j).1 →
        Nonempty (((M i).pullbackAlong p₁).L ≅ ((M j).pullbackAlong p₂).L))
section comp
variable (i j k : ι)

Lean source · statement

abbrev χ₃ : Limits.pullback (pr₂ (f i) (f j)).1 (pr₁ (f j) (f k)).1 ⟶ U k

lemma

hχ₁

L982 ↗

JacobianVarieties.Picard.Proofs.ZariskiGluing.ExZar.hχ₁

Source context 14 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ZariskiGluing
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
noncomputable section
namespace ExZar
open NeronModelInfra AlgebraicGeometry.RelPicard CategoryTheory.Pseudofunctor
open CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section Datum
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type u} {U : ι → Scheme.{u}} {u : ∀ i, U i ⟶ Spec (CommRingCat.of R)}
  (f : ∀ i, SchemeHomOver (u i) t) (M : ∀ i, RigidifiedLineBundle c ε (u i))
  (hM : ∀ (i j : ι) (Z : Scheme.{u}) (z : Z ⟶ Spec (CommRingCat.of R))
    (p₁ : SchemeHomOver z (u i)) (p₂ : SchemeHomOver z (u j)),
    p₁.1 ≫ (f i).1 = p₂.1 ≫ (f j).1 →
        Nonempty (((M i).pullbackAlong p₁).L ≅ ((M j).pullbackAlong p₂).L))
section comp
variable (i j k : ι)

Lean source · statement

lemma hχ₁ : χ₁ f i j k ≫ (f i).1 = ζT3 f i j k

lemma

hχ₂

L983 ↗

JacobianVarieties.Picard.Proofs.ZariskiGluing.ExZar.hχ₂

Source context 14 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ZariskiGluing
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
noncomputable section
namespace ExZar
open NeronModelInfra AlgebraicGeometry.RelPicard CategoryTheory.Pseudofunctor
open CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section Datum
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type u} {U : ι → Scheme.{u}} {u : ∀ i, U i ⟶ Spec (CommRingCat.of R)}
  (f : ∀ i, SchemeHomOver (u i) t) (M : ∀ i, RigidifiedLineBundle c ε (u i))
  (hM : ∀ (i j : ι) (Z : Scheme.{u}) (z : Z ⟶ Spec (CommRingCat.of R))
    (p₁ : SchemeHomOver z (u i)) (p₂ : SchemeHomOver z (u j)),
    p₁.1 ≫ (f i).1 = p₂.1 ≫ (f j).1 →
        Nonempty (((M i).pullbackAlong p₁).L ≅ ((M j).pullbackAlong p₂).L))
section comp
variable (i j k : ι)

Lean source · statement

lemma hχ₂ : χ₂ f i j k ≫ (f j).1 = ζT3 f i j k

lemma

hχ₃

L987 ↗

JacobianVarieties.Picard.Proofs.ZariskiGluing.ExZar.hχ₃

Source context 14 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ZariskiGluing
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
noncomputable section
namespace ExZar
open NeronModelInfra AlgebraicGeometry.RelPicard CategoryTheory.Pseudofunctor
open CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section Datum
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type u} {U : ι → Scheme.{u}} {u : ∀ i, U i ⟶ Spec (CommRingCat.of R)}
  (f : ∀ i, SchemeHomOver (u i) t) (M : ∀ i, RigidifiedLineBundle c ε (u i))
  (hM : ∀ (i j : ι) (Z : Scheme.{u}) (z : Z ⟶ Spec (CommRingCat.of R))
    (p₁ : SchemeHomOver z (u i)) (p₂ : SchemeHomOver z (u j)),
    p₁.1 ≫ (f i).1 = p₂.1 ≫ (f j).1 →
        Nonempty (((M i).pullbackAlong p₁).L ≅ ((M j).pullbackAlong p₂).L))
section comp
variable (i j k : ι)

Lean source · statement

lemma hχ₃ : χ₃ f i j k ≫ (f k).1 = ζT3 f i j k

lemma

S₁'

L996 ↗

JacobianVarieties.Picard.Proofs.ZariskiGluing.ExZar.S₁'

Source context 14 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ZariskiGluing
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
noncomputable section
namespace ExZar
open NeronModelInfra AlgebraicGeometry.RelPicard CategoryTheory.Pseudofunctor
open CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section Datum
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type u} {U : ι → Scheme.{u}} {u : ∀ i, U i ⟶ Spec (CommRingCat.of R)}
  (f : ∀ i, SchemeHomOver (u i) t) (M : ∀ i, RigidifiedLineBundle c ε (u i))
  (hM : ∀ (i j : ι) (Z : Scheme.{u}) (z : Z ⟶ Spec (CommRingCat.of R))
    (p₁ : SchemeHomOver z (u i)) (p₂ : SchemeHomOver z (u j)),
    p₁.1 ≫ (f i).1 = p₂.1 ≫ (f j).1 →
        Nonempty (((M i).pullbackAlong p₁).L ≅ ((M j).pullbackAlong p₂).L))
section comp
variable (i j k : ι)

Lean source · statement

lemma S₁' : rigSection c _ ε ≫ (sq₃F c f i j k).p₁ = χ₁ f i j k ≫ rigSection c (u i) ε

lemma

S₂'

L998 ↗

JacobianVarieties.Picard.Proofs.ZariskiGluing.ExZar.S₂'

Source context 14 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ZariskiGluing
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
noncomputable section
namespace ExZar
open NeronModelInfra AlgebraicGeometry.RelPicard CategoryTheory.Pseudofunctor
open CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section Datum
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type u} {U : ι → Scheme.{u}} {u : ∀ i, U i ⟶ Spec (CommRingCat.of R)}
  (f : ∀ i, SchemeHomOver (u i) t) (M : ∀ i, RigidifiedLineBundle c ε (u i))
  (hM : ∀ (i j : ι) (Z : Scheme.{u}) (z : Z ⟶ Spec (CommRingCat.of R))
    (p₁ : SchemeHomOver z (u i)) (p₂ : SchemeHomOver z (u j)),
    p₁.1 ≫ (f i).1 = p₂.1 ≫ (f j).1 →
        Nonempty (((M i).pullbackAlong p₁).L ≅ ((M j).pullbackAlong p₂).L))
section comp
variable (i j k : ι)

Lean source · statement

lemma S₂' : rigSection c _ ε ≫ (sq₃F c f i j k).p₂ = χ₂ f i j k ≫ rigSection c (u j) ε

lemma

S₃'

L1000 ↗

JacobianVarieties.Picard.Proofs.ZariskiGluing.ExZar.S₃'

Source context 14 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ZariskiGluing
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
noncomputable section
namespace ExZar
open NeronModelInfra AlgebraicGeometry.RelPicard CategoryTheory.Pseudofunctor
open CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section Datum
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type u} {U : ι → Scheme.{u}} {u : ∀ i, U i ⟶ Spec (CommRingCat.of R)}
  (f : ∀ i, SchemeHomOver (u i) t) (M : ∀ i, RigidifiedLineBundle c ε (u i))
  (hM : ∀ (i j : ι) (Z : Scheme.{u}) (z : Z ⟶ Spec (CommRingCat.of R))
    (p₁ : SchemeHomOver z (u i)) (p₂ : SchemeHomOver z (u j)),
    p₁.1 ≫ (f i).1 = p₂.1 ≫ (f j).1 →
        Nonempty (((M i).pullbackAlong p₁).L ≅ ((M j).pullbackAlong p₂).L))
section comp
variable (i j k : ι)

Lean source · statement

lemma S₃' : rigSection c _ ε ≫ (sq₃F c f i j k).p₃ = χ₃ f i j k ≫ rigSection c (u k) ε

theorem

pullHomIso_comp

L1004 ↗

JacobianVarieties.Picard.Proofs.ZariskiGluing.ExZar.pullHomIso_comp

Source context 14 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ZariskiGluing
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
noncomputable section
namespace ExZar
open NeronModelInfra AlgebraicGeometry.RelPicard CategoryTheory.Pseudofunctor
open CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section Datum
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type u} {U : ι → Scheme.{u}} {u : ∀ i, U i ⟶ Spec (CommRingCat.of R)}
  (f : ∀ i, SchemeHomOver (u i) t) (M : ∀ i, RigidifiedLineBundle c ε (u i))
  (hM : ∀ (i j : ι) (Z : Scheme.{u}) (z : Z ⟶ Spec (CommRingCat.of R))
    (p₁ : SchemeHomOver z (u i)) (p₂ : SchemeHomOver z (u j)),
    p₁.1 ≫ (f i).1 = p₂.1 ≫ (f j).1 →
        Nonempty (((M i).pullbackAlong p₁).L ≅ ((M j).pullbackAlong p₂).L))
section comp
variable (i j k : ι)

Lean source · full declaration

theorem pullHomIso_comp (hH0 : ∀ (A : Type u) [CommRing A] [Algebra R A],
      let : Algebra A
          Γ(Limits.pullback c (Scheme.TwoAffineOpenCover.specMap R A), ⊤) :=
        Scheme.TwoAffineOpenCover.algebraOfHom
        (Limits.pullback.snd c (Scheme.TwoAffineOpenCover.specMap R A)) ⊤
      Function.Bijective (algebraMap A
          Γ(Limits.pullback c (Scheme.TwoAffineOpenCover.specMap R A), ⊤))) :
    pullHomIso (Y' := Limits.pullback c (strMap₁₂ (pr₂ (f i) (f j)) (pr₁ (f j) (f k))))
        (homIso c ε f M hM i j) (sq₃F c f i j k).p₁₂ (sq₃F c f i j k).p₁ (sq₃F c f i j k).p₂
        (sq₃F c f i j k).p₁₂_p₁ (sq₃F c f i j k).p₁₂_p₂ ≪≫
      pullHomIso (Y' := Limits.pullback c (strMap₁₂ (pr₂ (f i) (f j)) (pr₁ (f j) (f k))))
          (homIso c ε f M hM j k) (sq₃F c f i j k).p₂₃ (sq₃F c f i j k).p₂ (sq₃F c f i j k).p₃
        (sq₃F c f i j k).p₂₃_p₂ (sq₃F c f i j k).p₂₃_p₃ =
      pullHomIso (Y' := Limits.pullback c (strMap₁₂ (pr₂ (f i) (f j)) (pr₁ (f j) (f k))))
          (homIso c ε f M hM i k) (sq₃F c f i j k).p₁₃ (sq₃F c f i j k).p₁ (sq₃F c f i j k).p₃
        (sq₃F c f i j k).p₁₃_p₁ (sq₃F c f i j k).p₁₃_p₃ := by
  have K₁₂ := key c ε f M hM i j (ρ₁₂ (f i) (f j) (f k))
    (sq₃F c f i j k).p₁₂ rfl (sq₃F c f i j k).p₁ (sq₃F c f i j k).p₂
    (sq₃F c f i j k).p₁₂_p₁ (sq₃F c f i j k).p₁₂_p₂ (χ₁ f i j k) (χ₂ f i j k) rfl rfl
      (S₁' c ε f i j k) (S₂' c ε f i j k)
    (ζT3 f i j k) (hχ₁ f i j k) (hχ₂ f i j k)
  have K₂₃ := key c ε f M hM j k (ρ₂₃ (f i) (f j) (f k))
    (sq₃F c f i j k).p₂₃ rfl (sq₃F c f i j k).p₂ (sq₃F c f i j k).p₃
    (sq₃F c f i j k).p₂₃_p₂ (sq₃F c f i j k).p₂₃_p₃ (χ₂ f i j k) (χ₃ f i j k)
      pullback.condition.symm rfl
    (S₂' c ε f i j k) (S₃' c ε f i j k) (ζT3 f i j k) (hχ₂ f i j k) (hχ₃ f i j k)
  have K₁₃ := key c ε f M hM i k (ρ₁₃ (f i) (f j) (f k))
    (sq₃F c f i j k).p₁₃ rfl (sq₃F c f i j k).p₁ (sq₃F c f i j k).p₃
    (sq₃F c f i j k).p₁₃_p₁ (sq₃F c f i j k).p₁₃_p₃ (χ₁ f i j k) (χ₃ f i j k)
      (pullback.lift_fst _ _ _)
    (pullback.lift_snd _ _ _) (S₁' c ε f i j k) (S₃' c ε f i j k) (ζT3 f i j k)
      (hχ₁ f i j k) (hχ₃ f i j k)
  exact iso_eq_of_map_rigSection_eq c ε _ hH0
    ((M i).isInvertible.pullback _) ((M k).isInvertible.pullback _)
    (nonempty_rigidification c ε f M k _ (sq₃F c f i j k).p₃ (χ₃ f i j k)
      (S₃' c ε f i j k) (ζT3 f i j k) (hχ₃ f i j k))
    _ _ (by
      rw [Iso.trans_hom, Functor.map_comp, K₁₂, K₂₃, K₁₃]
      simp only [Category.assoc, Iso.inv_hom_id_assoc])

theorem

main

L1047 ↗

JacobianVarieties.Picard.Proofs.ZariskiGluing.ExZar.main

Source context 13 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ZariskiGluing
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
noncomputable section
namespace ExZar
open NeronModelInfra AlgebraicGeometry.RelPicard CategoryTheory.Pseudofunctor
open CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section Datum
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type u} {U : ι → Scheme.{u}} {u : ∀ i, U i ⟶ Spec (CommRingCat.of R)}
  (f : ∀ i, SchemeHomOver (u i) t) (M : ∀ i, RigidifiedLineBundle c ε (u i))
  (hM : ∀ (i j : ι) (Z : Scheme.{u}) (z : Z ⟶ Spec (CommRingCat.of R))
    (p₁ : SchemeHomOver z (u i)) (p₂ : SchemeHomOver z (u j)),
    p₁.1 ≫ (f i).1 = p₂.1 ≫ (f j).1 →
        Nonempty (((M i).pullbackAlong p₁).L ≅ ((M j).pullbackAlong p₂).L))
include hM in

Lean source · full declaration

theorem main (hH0 : ∀ (A : Type u) [CommRing A] [Algebra R A],
      let : Algebra A
          Γ(Limits.pullback c (Scheme.TwoAffineOpenCover.specMap R A), ⊤) :=
        Scheme.TwoAffineOpenCover.algebraOfHom
        (Limits.pullback.snd c (Scheme.TwoAffineOpenCover.specMap R A)) ⊤
      Function.Bijective (algebraMap A
          Γ(Limits.pullback c (Scheme.TwoAffineOpenCover.specMap R A), ⊤)))
    [∀ i, IsOpenImmersion (f i).1]
    (hf : ∀ x : T, ∃ i, x ∈ Set.range (f i).1.base) :
    ∃ N : RigidifiedLineBundle c ε t, ∀ i, Nonempty ((N.pullbackAlong (f i)).L ≅ (M i).L) := by
  have hS := AlgebraicGeometry.Scheme.Modules.isStackFor_openCover
    (Limits.pullback c t) (coverBC c t u f hf)
  rw [Pseudofunctor.isStackFor_ofArrows_iff] at hS
  have : (MOD.toDescentData (fF c f)).IsEquivalence := hS
  obtain ⟨L, eL⟩ := exists_iso_of_plainDescent (fF c f) (sqF c f) (sq₃F c f) (fun i => (M i).L)
    (fun i j => homIso c ε f M hM i j) (fun i => baseChangeSnd c (δ f i)) (δ_pr₁ c f) (δ_pr₂ c f)
    (fun i _ _ => pullHomIso_self c ε f M hM hH0 i)
      (fun i j k _ _ _ _ _ _ => pullHomIso_comp c ε f M hM i j k hH0)
  have eᵢ : ∀ i, (Scheme.Modules.pullback (baseChangeSnd c (f i))).obj L ≅ (M i).L
      := fun i => (eL i).some
  have hL : Scheme.Modules.IsInvertible L :=
    isInvertible_of_openCover (fun i => baseChangeSnd c (f i))
      (exists_mem_range_baseChangeSnd c t u f hf) L
      (fun i => isInvertible_of_iso (eᵢ i) (M i).isInvertible)
  refine ⟨RigidifiedLineBundle.ofInvertible (ε := ε) L hL, fun i => ?_⟩
  obtain ⟨a⟩ := RigidifiedLineBundle.nonempty_ofInvertible_pullbackAlong_iso (ε := ε) (f i) hL
  obtain ⟨b⟩ := RigidifiedLineBundle.nonempty_ofInvertible_iso_of_iso
    (ε := ε) (hL.pullback _) (M i).isInvertible (eᵢ i)
  obtain ⟨d⟩ := RigidifiedLineBundle.nonempty_ofInvertible_iso_of_rigidified (M i)
  exact ⟨a ≪≫ b ≪≫ d⟩

theorem

exists_gluing_openCover_of_bijective_sections

L1086 ↗

AlgebraicGeometry.RelPicard.RigidifiedLineBundle.exists_gluing_openCover_of_bijective_sections

Source context 8 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ZariskiGluing
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
open NeronModelInfra AlgebraicGeometry.RelPicard in
open _root_.JacobianVarieties.Picard.Proofs.ZariskiGluing in
with_weak_namespace _root_.AlgebraicGeometry.RelPicard.RigidifiedLineBundle

Lean source · full declaration

theorem exists_gluing_openCover_of_bijective_sections
    (R : Type u) [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
    (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
    (hH0 : ∀ (A : Type u) [CommRing A] [Algebra R A],
      let : Algebra A
          Γ(Limits.pullback c (Scheme.TwoAffineOpenCover.specMap R A), ⊤) :=
        Scheme.TwoAffineOpenCover.algebraOfHom
        (Limits.pullback.snd c (Scheme.TwoAffineOpenCover.specMap R A)) ⊤
      Function.Bijective (algebraMap A
          Γ(Limits.pullback c (Scheme.TwoAffineOpenCover.specMap R A), ⊤)))
    {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R))
    {ι : Type u} {U : ι → Scheme.{u}} (u : ∀ i, U i ⟶ Spec (CommRingCat.of R))
    (f : ∀ i, SchemeHomOver (u i) t) [∀ i, IsOpenImmersion (f i).1]
    (hf : ∀ x : T, ∃ i, x ∈ Set.range (f i).1.base)
    (M : ∀ i, RigidifiedLineBundle c ε (u i))
    (hM : ∀ (i j : ι) (Z : Scheme.{u}) (z : Z ⟶ Spec (CommRingCat.of R))
      (p₁ : SchemeHomOver z (u i)) (p₂ : SchemeHomOver z (u j)),
      p₁.1 ≫ (f i).1 = p₂.1 ≫ (f j).1 →
        Nonempty (((M i).pullbackAlong p₁).L ≅ ((M j).pullbackAlong p₂).L)) :
    ∃ N : RigidifiedLineBundle c ε t, ∀ i, Nonempty ((N.pullbackAlong (f i)).L ≅ (M i).L) :=
  ExZar.main c ε f M hM hH0 hf

Module documentation

Gluing rigidified line bundles

Declarations