Module

RigidifiedLineBundle_exists_descent_of_isAffineHom_of_flat_of_surjective_of_bijective_sections.lean

Nyll.JacobianVarieties.Picard.RigidifiedLineBundle_exists_descent_of_isAffineHom_of_flat_of_surjective_of_bijective_sections

97 declarations indexed from sourceView source ↗

Module documentation

Affine descent of rigidified line bundles

Normalized overlap isomorphisms satisfy the diagonal and cocycle laws by rigidity. Effective descent for invertible module sheaves then gives the descended rigidified bundle.

Imports12

Imported by1

Nyll.JacobianVarieties.Picard.All

theorem

pullbackComp_paste

L56 ↗

JacobianVarieties.Picard.Proofs.AffineRigidDescent.ExZar.pullbackComp_paste

Source context 10 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AffineRigidDescent
attribute [-simp]
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
  Algebra.DescentCofaces.i₁_apply
  Algebra.DescentCofaces.i₂_apply
  Algebra.DescentCofaces.c₁₂_tmul
  Algebra.DescentCofaces.c₂₃_tmul
  Algebra.DescentCofaces.c₁₃_tmul
universe u w
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

L79 ↗

JacobianVarieties.Picard.Proofs.AffineRigidDescent.ExZar.pullbackComp_paste_app

Source context 10 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AffineRigidDescent
attribute [-simp]
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
  Algebra.DescentCofaces.i₁_apply
  Algebra.DescentCofaces.i₂_apply
  Algebra.DescentCofaces.c₁₂_tmul
  Algebra.DescentCofaces.c₂₃_tmul
  Algebra.DescentCofaces.c₁₃_tmul
universe u w
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

τ

L92 ↗

JacobianVarieties.Picard.Proofs.AffineRigidDescent.ExZar.τ

Documentation

Identify iterated module pullback with pullback along the specified composite.

Source context 10 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AffineRigidDescent
attribute [-simp]
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
  Algebra.DescentCofaces.i₁_apply
  Algebra.DescentCofaces.i₂_apply
  Algebra.DescentCofaces.c₁₂_tmul
  Algebra.DescentCofaces.c₂₃_tmul
  Algebra.DescentCofaces.c₁₃_tmul
universe u w
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

L96 ↗

JacobianVarieties.Picard.Proofs.AffineRigidDescent.ExZar.τ_hom_app

Source context 10 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AffineRigidDescent
attribute [-simp]
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
  Algebra.DescentCofaces.i₁_apply
  Algebra.DescentCofaces.i₂_apply
  Algebra.DescentCofaces.c₁₂_tmul
  Algebra.DescentCofaces.c₂₃_tmul
  Algebra.DescentCofaces.c₁₃_tmul
universe u w
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
  simp only [τ, Scheme.Modules.pullbackCongr, eqToIso_refl, Iso.trans_refl,
    eqToHom_refl, Category.comp_id]

theorem

τ_inv_app

L102 ↗

JacobianVarieties.Picard.Proofs.AffineRigidDescent.ExZar.τ_inv_app

Source context 10 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AffineRigidDescent
attribute [-simp]
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
  Algebra.DescentCofaces.i₁_apply
  Algebra.DescentCofaces.i₂_apply
  Algebra.DescentCofaces.c₁₂_tmul
  Algebra.DescentCofaces.c₂₃_tmul
  Algebra.DescentCofaces.c₁₃_tmul
universe u w
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
  simp only [τ, Scheme.Modules.pullbackCongr, eqToIso_refl, Iso.trans_refl,
    eqToHom_refl, Category.id_comp]

theorem

τ_paste_app

L108 ↗

JacobianVarieties.Picard.Proofs.AffineRigidDescent.ExZar.τ_paste_app

Source context 10 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AffineRigidDescent
attribute [-simp]
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
  Algebra.DescentCofaces.i₁_apply
  Algebra.DescentCofaces.i₂_apply
  Algebra.DescentCofaces.c₁₂_tmul
  Algebra.DescentCofaces.c₂₃_tmul
  Algebra.DescentCofaces.c₁₃_tmul
universe u w
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

L119 ↗

JacobianVarieties.Picard.Proofs.AffineRigidDescent.ExZar.sqIso

Documentation

Compare module pullback along the two paths of a commutative square.

Source context 10 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AffineRigidDescent
attribute [-simp]
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
  Algebra.DescentCofaces.i₁_apply
  Algebra.DescentCofaces.i₂_apply
  Algebra.DescentCofaces.c₁₂_tmul
  Algebra.DescentCofaces.c₂₃_tmul
  Algebra.DescentCofaces.c₁₃_tmul
universe u w
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

L125 ↗

JacobianVarieties.Picard.Proofs.AffineRigidDescent.ExZar.route

Source context 10 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AffineRigidDescent
attribute [-simp]
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
  Algebra.DescentCofaces.i₁_apply
  Algebra.DescentCofaces.i₂_apply
  Algebra.DescentCofaces.c₁₂_tmul
  Algebra.DescentCofaces.c₂₃_tmul
  Algebra.DescentCofaces.c₁₃_tmul
universe u w
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

L140 ↗

JacobianVarieties.Picard.Proofs.AffineRigidDescent.ExZar.MOD

Documentation

Module pullback as a pseudofunctor on the locally discrete opposite of schemes.

Source context 8 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AffineRigidDescent
attribute [-simp]
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
  Algebra.DescentCofaces.i₁_apply
  Algebra.DescentCofaces.i₂_apply
  Algebra.DescentCofaces.c₁₂_tmul
  Algebra.DescentCofaces.c₂₃_tmul
  Algebra.DescentCofaces.c₁₃_tmul
universe u w
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

L146 ↗

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

Source context 10 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AffineRigidDescent
attribute [-simp]
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
  Algebra.DescentCofaces.i₁_apply
  Algebra.DescentCofaces.i₂_apply
  Algebra.DescentCofaces.c₁₂_tmul
  Algebra.DescentCofaces.c₂₃_tmul
  Algebra.DescentCofaces.c₁₃_tmul
universe u w
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

L152 ↗

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

Source context 10 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AffineRigidDescent
attribute [-simp]
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
  Algebra.DescentCofaces.i₁_apply
  Algebra.DescentCofaces.i₂_apply
  Algebra.DescentCofaces.c₁₂_tmul
  Algebra.DescentCofaces.c₂₃_tmul
  Algebra.DescentCofaces.c₁₃_tmul
universe u w
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

L159 ↗

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

Source context 10 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AffineRigidDescent
attribute [-simp]
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
  Algebra.DescentCofaces.i₁_apply
  Algebra.DescentCofaces.i₂_apply
  Algebra.DescentCofaces.c₁₂_tmul
  Algebra.DescentCofaces.c₂₃_tmul
  Algebra.DescentCofaces.c₁₃_tmul
universe u w
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

L167 ↗

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

Source context 10 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AffineRigidDescent
attribute [-simp]
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
  Algebra.DescentCofaces.i₁_apply
  Algebra.DescentCofaces.i₂_apply
  Algebra.DescentCofaces.c₁₂_tmul
  Algebra.DescentCofaces.c₂₃_tmul
  Algebra.DescentCofaces.c₁₃_tmul
universe u w
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

L178 ↗

JacobianVarieties.Picard.Proofs.AffineRigidDescent.ExZar.pullHom_MOD

Source context 9 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AffineRigidDescent
attribute [-simp]
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
  Algebra.DescentCofaces.i₁_apply
  Algebra.DescentCofaces.i₂_apply
  Algebra.DescentCofaces.c₁₂_tmul
  Algebra.DescentCofaces.c₂₃_tmul
  Algebra.DescentCofaces.c₁₃_tmul
universe u w
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

L189 ↗

JacobianVarieties.Picard.Proofs.AffineRigidDescent.ExZar.pullHomIso

Documentation

Pull back a module isomorphism and identify its endpoints with the chosen composites.

Source context 8 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AffineRigidDescent
attribute [-simp]
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
  Algebra.DescentCofaces.i₁_apply
  Algebra.DescentCofaces.i₂_apply
  Algebra.DescentCofaces.c₁₂_tmul
  Algebra.DescentCofaces.c₂₃_tmul
  Algebra.DescentCofaces.c₁₃_tmul
universe u w
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'

L197 ↗

JacobianVarieties.Picard.Proofs.AffineRigidDescent.ExZar.pullHomIso_hom'

Source context 8 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AffineRigidDescent
attribute [-simp]
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
  Algebra.DescentCofaces.i₁_apply
  Algebra.DescentCofaces.i₂_apply
  Algebra.DescentCofaces.c₁₂_tmul
  Algebra.DescentCofaces.c₂₃_tmul
  Algebra.DescentCofaces.c₁₃_tmul
universe u w
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

L207 ↗

JacobianVarieties.Picard.Proofs.AffineRigidDescent.ExZar.pullHomIso_hom

Source context 9 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AffineRigidDescent
attribute [-simp]
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
  Algebra.DescentCofaces.i₁_apply
  Algebra.DescentCofaces.i₂_apply
  Algebra.DescentCofaces.c₁₂_tmul
  Algebra.DescentCofaces.c₂₃_tmul
  Algebra.DescentCofaces.c₁₃_tmul
universe u w
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

L216 ↗

JacobianVarieties.Picard.Proofs.AffineRigidDescent.ExZar.pullHomMap

Documentation

Pull back a module morphism and identify its endpoints with the chosen composites.

Source context 8 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AffineRigidDescent
attribute [-simp]
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
  Algebra.DescentCofaces.i₁_apply
  Algebra.DescentCofaces.i₂_apply
  Algebra.DescentCofaces.c₁₂_tmul
  Algebra.DescentCofaces.c₂₃_tmul
  Algebra.DescentCofaces.c₁₃_tmul
universe u w
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

L223 ↗

JacobianVarieties.Picard.Proofs.AffineRigidDescent.ExZar.pullHomIso_hom_eq_pullHomMap

Source context 8 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AffineRigidDescent
attribute [-simp]
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
  Algebra.DescentCofaces.i₁_apply
  Algebra.DescentCofaces.i₂_apply
  Algebra.DescentCofaces.c₁₂_tmul
  Algebra.DescentCofaces.c₂₃_tmul
  Algebra.DescentCofaces.c₁₃_tmul
universe u w
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

L231 ↗

JacobianVarieties.Picard.Proofs.AffineRigidDescent.ExZar.toMOD

Documentation

View a module morphism in the category used by the pullback pseudofunctor.

Source context 8 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AffineRigidDescent
attribute [-simp]
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
  Algebra.DescentCofaces.i₁_apply
  Algebra.DescentCofaces.i₂_apply
  Algebra.DescentCofaces.c₁₂_tmul
  Algebra.DescentCofaces.c₂₃_tmul
  Algebra.DescentCofaces.c₁₃_tmul
universe u w
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

L235 ↗

JacobianVarieties.Picard.Proofs.AffineRigidDescent.ExZar.toMOD_eq

Source context 8 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AffineRigidDescent
attribute [-simp]
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
  Algebra.DescentCofaces.i₁_apply
  Algebra.DescentCofaces.i₂_apply
  Algebra.DescentCofaces.c₁₂_tmul
  Algebra.DescentCofaces.c₂₃_tmul
  Algebra.DescentCofaces.c₁₃_tmul
universe u w
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

L241 ↗

JacobianVarieties.Picard.Proofs.AffineRigidDescent.ExZar.pullHom_toMOD

Source context 9 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AffineRigidDescent
attribute [-simp]
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
  Algebra.DescentCofaces.i₁_apply
  Algebra.DescentCofaces.i₂_apply
  Algebra.DescentCofaces.c₁₂_tmul
  Algebra.DescentCofaces.c₂₃_tmul
  Algebra.DescentCofaces.c₁₃_tmul
universe u w
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

L249 ↗

JacobianVarieties.Picard.Proofs.AffineRigidDescent.ExZar.toMOD_comp

Source context 8 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AffineRigidDescent
attribute [-simp]
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
  Algebra.DescentCofaces.i₁_apply
  Algebra.DescentCofaces.i₂_apply
  Algebra.DescentCofaces.c₁₂_tmul
  Algebra.DescentCofaces.c₂₃_tmul
  Algebra.DescentCofaces.c₁₃_tmul
universe u w
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

L256 ↗

JacobianVarieties.Picard.Proofs.AffineRigidDescent.ExZar.toMOD_congr

Source context 8 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AffineRigidDescent
attribute [-simp]
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
  Algebra.DescentCofaces.i₁_apply
  Algebra.DescentCofaces.i₂_apply
  Algebra.DescentCofaces.c₁₂_tmul
  Algebra.DescentCofaces.c₂₃_tmul
  Algebra.DescentCofaces.c₁₃_tmul
universe u w
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

L262 ↗

JacobianVarieties.Picard.Proofs.AffineRigidDescent.ExZar.toMOD_id

Source context 8 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AffineRigidDescent
attribute [-simp]
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
  Algebra.DescentCofaces.i₁_apply
  Algebra.DescentCofaces.i₂_apply
  Algebra.DescentCofaces.c₁₂_tmul
  Algebra.DescentCofaces.c₂₃_tmul
  Algebra.DescentCofaces.c₁₃_tmul
universe u w
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

L267 ↗

JacobianVarieties.Picard.Proofs.AffineRigidDescent.ExZar.isoOfMOD

Documentation

View a pseudofunctor isomorphism as an isomorphism of pulled-back module sheaves.

Source context 8 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AffineRigidDescent
attribute [-simp]
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
  Algebra.DescentCofaces.i₁_apply
  Algebra.DescentCofaces.i₂_apply
  Algebra.DescentCofaces.c₁₂_tmul
  Algebra.DescentCofaces.c₂₃_tmul
  Algebra.DescentCofaces.c₁₃_tmul
universe u w
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

L272 ↗

JacobianVarieties.Picard.Proofs.AffineRigidDescent.ExZar.MOD_pullHom_eq_id_of_iso

Source context 9 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AffineRigidDescent
attribute [-simp]
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
  Algebra.DescentCofaces.i₁_apply
  Algebra.DescentCofaces.i₂_apply
  Algebra.DescentCofaces.c₁₂_tmul
  Algebra.DescentCofaces.c₂₃_tmul
  Algebra.DescentCofaces.c₁₃_tmul
universe u w
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

L284 ↗

JacobianVarieties.Picard.Proofs.AffineRigidDescent.ExZar.pullHomMap_comp_of

Source context 10 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AffineRigidDescent
attribute [-simp]
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
  Algebra.DescentCofaces.i₁_apply
  Algebra.DescentCofaces.i₂_apply
  Algebra.DescentCofaces.c₁₂_tmul
  Algebra.DescentCofaces.c₂₃_tmul
  Algebra.DescentCofaces.c₁₃_tmul
universe u w
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

L310 ↗

JacobianVarieties.Picard.Proofs.AffineRigidDescent.ExZar.homG

Documentation

Express an overlap isomorphism as a morphism in the module pullback pseudofunctor.

Source context 11 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AffineRigidDescent
attribute [-simp]
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
  Algebra.DescentCofaces.i₁_apply
  Algebra.DescentCofaces.i₂_apply
  Algebra.DescentCofaces.c₁₂_tmul
  Algebra.DescentCofaces.c₂₃_tmul
  Algebra.DescentCofaces.c₁₃_tmul
universe u w
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
noncomputable section
namespace ExZar
section PlainDescent
open CategoryTheory.Pseudofunctor CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {ι : Type w} {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

L316 ↗

JacobianVarieties.Picard.Proofs.AffineRigidDescent.ExZar.pullHom_homG

Source context 12 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AffineRigidDescent
attribute [-simp]
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
  Algebra.DescentCofaces.i₁_apply
  Algebra.DescentCofaces.i₂_apply
  Algebra.DescentCofaces.c₁₂_tmul
  Algebra.DescentCofaces.c₂₃_tmul
  Algebra.DescentCofaces.c₁₃_tmul
universe u w
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
noncomputable section
namespace ExZar
section PlainDescent
open CategoryTheory.Pseudofunctor CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {ι : Type w} {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

L338 ↗

JacobianVarieties.Picard.Proofs.AffineRigidDescent.ExZar.dataG

Documentation

Build module descent data from overlap isomorphisms and their diagonal and cocycle laws.

Source context 12 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AffineRigidDescent
attribute [-simp]
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
  Algebra.DescentCofaces.i₁_apply
  Algebra.DescentCofaces.i₂_apply
  Algebra.DescentCofaces.c₁₂_tmul
  Algebra.DescentCofaces.c₂₃_tmul
  Algebra.DescentCofaces.c₁₃_tmul
universe u w
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
noncomputable section
namespace ExZar
section PlainDescent
open CategoryTheory.Pseudofunctor CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {ι : Type w} {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

L358 ↗

JacobianVarieties.Picard.Proofs.AffineRigidDescent.ExZar.dataG_obj

Source context 12 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AffineRigidDescent
attribute [-simp]
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
  Algebra.DescentCofaces.i₁_apply
  Algebra.DescentCofaces.i₂_apply
  Algebra.DescentCofaces.c₁₂_tmul
  Algebra.DescentCofaces.c₂₃_tmul
  Algebra.DescentCofaces.c₁₃_tmul
universe u w
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
noncomputable section
namespace ExZar
section PlainDescent
open CategoryTheory.Pseudofunctor CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {ι : Type w} {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

L361 ↗

JacobianVarieties.Picard.Proofs.AffineRigidDescent.ExZar.exists_iso_of_plainDescent

Source context 13 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AffineRigidDescent
attribute [-simp]
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
  Algebra.DescentCofaces.i₁_apply
  Algebra.DescentCofaces.i₂_apply
  Algebra.DescentCofaces.c₁₂_tmul
  Algebra.DescentCofaces.c₂₃_tmul
  Algebra.DescentCofaces.c₁₃_tmul
universe u w
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
noncomputable section
namespace ExZar
section PlainDescent
open CategoryTheory.Pseudofunctor CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {ι : Type w} {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)

theorem

exists_iso_of_plainDescent_ff

L381 ↗

JacobianVarieties.Picard.Proofs.AffineRigidDescent.ExZar.exists_iso_of_plainDescent_ff

Source context 11 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AffineRigidDescent
attribute [-simp]
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
  Algebra.DescentCofaces.i₁_apply
  Algebra.DescentCofaces.i₂_apply
  Algebra.DescentCofaces.c₁₂_tmul
  Algebra.DescentCofaces.c₂₃_tmul
  Algebra.DescentCofaces.c₁₃_tmul
universe u w
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
noncomputable section
namespace ExZar
section PlainDescentFF
open CategoryTheory.Pseudofunctor
open _root_.AlgebraicGeometry.Scheme.Modules.IsInvertible in

Lean source · statement

theorem exists_iso_of_plainDescent_ff {Y Y' : Scheme.{u}} (q : Y' ⟶ Y) [IsAffineHom q] [Flat q]
    [Surjective q]
    (sq : ∀ _ _ : Unit, ChosenPullback q q) (sq₃ : ∀ i j k : Unit, ChosenPullback₃ (sq i j) (sq j
      k) (sq i k))
    (obj : Unit → Y'.Modules) (hobj : ∀ i, Scheme.Modules.IsInvertible (obj i))
    (φ : ∀ i j, (Scheme.Modules.pullback (sq i j).p₁).obj (obj i) ≅ (Scheme.Modules.pullback (sq i
      j).p₂).obj (obj j))
    (δ : ∀ i, Y' ⟶ (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₆) :
    ∃ L : Y.Modules, Scheme.Modules.IsInvertible L ∧
      ∀ i, Nonempty ((Scheme.Modules.pullback q).obj L ≅ obj i)

lemma

isPullback_baseChangeSnd_snd

L428 ↗

JacobianVarieties.Picard.Proofs.AffineRigidDescent.ExZar.isPullback_baseChangeSnd_snd

Source context 10 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AffineRigidDescent
attribute [-simp]
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
  Algebra.DescentCofaces.i₁_apply
  Algebra.DescentCofaces.i₂_apply
  Algebra.DescentCofaces.c₁₂_tmul
  Algebra.DescentCofaces.c₂₃_tmul
  Algebra.DescentCofaces.c₁₃_tmul
universe u w
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

L437 ↗

JacobianVarieties.Picard.Proofs.AffineRigidDescent.ExZar.isPullback_baseChangeSnd

Source context 10 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AffineRigidDescent
attribute [-simp]
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
  Algebra.DescentCofaces.i₁_apply
  Algebra.DescentCofaces.i₂_apply
  Algebra.DescentCofaces.c₁₂_tmul
  Algebra.DescentCofaces.c₂₃_tmul
  Algebra.DescentCofaces.c₁₃_tmul
universe u w
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₁₂

L460 ↗

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

Documentation

The structure morphism to the base of the fiber product of two schemes over the target.

Source context 10 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AffineRigidDescent
attribute [-simp]
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
  Algebra.DescentCofaces.i₁_apply
  Algebra.DescentCofaces.i₂_apply
  Algebra.DescentCofaces.c₁₂_tmul
  Algebra.DescentCofaces.c₂₃_tmul
  Algebra.DescentCofaces.c₁₃_tmul
universe u w
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₁

L467 ↗

JacobianVarieties.Picard.Proofs.AffineRigidDescent.ExZar.pr₁

Documentation

The first fiber-product projection as a morphism over the base.

Source context 10 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AffineRigidDescent
attribute [-simp]
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
  Algebra.DescentCofaces.i₁_apply
  Algebra.DescentCofaces.i₂_apply
  Algebra.DescentCofaces.c₁₂_tmul
  Algebra.DescentCofaces.c₂₃_tmul
  Algebra.DescentCofaces.c₁₃_tmul
universe u w
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₂

L473 ↗

JacobianVarieties.Picard.Proofs.AffineRigidDescent.ExZar.pr₂

Documentation

The second fiber-product projection as a morphism over the base.

Source context 10 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AffineRigidDescent
attribute [-simp]
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
  Algebra.DescentCofaces.i₁_apply
  Algebra.DescentCofaces.i₂_apply
  Algebra.DescentCofaces.c₁₂_tmul
  Algebra.DescentCofaces.c₂₃_tmul
  Algebra.DescentCofaces.c₁₃_tmul
universe u w
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

L482 ↗

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

Source context 10 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AffineRigidDescent
attribute [-simp]
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
  Algebra.DescentCofaces.i₁_apply
  Algebra.DescentCofaces.i₂_apply
  Algebra.DescentCofaces.c₁₂_tmul
  Algebra.DescentCofaces.c₂₃_tmul
  Algebra.DescentCofaces.c₁₃_tmul
universe u w
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

L487 ↗

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

Source context 10 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AffineRigidDescent
attribute [-simp]
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
  Algebra.DescentCofaces.i₁_apply
  Algebra.DescentCofaces.i₂_apply
  Algebra.DescentCofaces.c₁₂_tmul
  Algebra.DescentCofaces.c₂₃_tmul
  Algebra.DescentCofaces.c₁₃_tmul
universe u w
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₂

L492 ↗

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

Source context 10 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AffineRigidDescent
attribute [-simp]
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
  Algebra.DescentCofaces.i₁_apply
  Algebra.DescentCofaces.i₂_apply
  Algebra.DescentCofaces.c₁₂_tmul
  Algebra.DescentCofaces.c₂₃_tmul
  Algebra.DescentCofaces.c₁₃_tmul
universe u w
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

L499 ↗

JacobianVarieties.Picard.Proofs.AffineRigidDescent.ExZar.chosenPullback

Documentation

The chosen pullback of the two induced maps between base-changed curves.

Source context 10 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AffineRigidDescent
attribute [-simp]
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
  Algebra.DescentCofaces.i₁_apply
  Algebra.DescentCofaces.i₂_apply
  Algebra.DescentCofaces.c₁₂_tmul
  Algebra.DescentCofaces.c₂₃_tmul
  Algebra.DescentCofaces.c₁₃_tmul
universe u w
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

ρ₁₂

L520 ↗

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

Documentation

Project the triple overlap to the overlap of its first two factors.

Source context 12 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AffineRigidDescent
attribute [-simp]
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
  Algebra.DescentCofaces.i₁_apply
  Algebra.DescentCofaces.i₂_apply
  Algebra.DescentCofaces.c₁₂_tmul
  Algebra.DescentCofaces.c₂₃_tmul
  Algebra.DescentCofaces.c₁₃_tmul
universe u w
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

ρ₂₃

L524 ↗

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

Documentation

Project the triple overlap to the overlap of its last two factors.

Source context 12 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AffineRigidDescent
attribute [-simp]
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
  Algebra.DescentCofaces.i₁_apply
  Algebra.DescentCofaces.i₂_apply
  Algebra.DescentCofaces.c₁₂_tmul
  Algebra.DescentCofaces.c₂₃_tmul
  Algebra.DescentCofaces.c₁₃_tmul
universe u w
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

ρ₁₃

L528 ↗

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

Documentation

Project the triple overlap to the overlap of its first and third factors.

Source context 12 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AffineRigidDescent
attribute [-simp]
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
  Algebra.DescentCofaces.i₁_apply
  Algebra.DescentCofaces.i₂_apply
  Algebra.DescentCofaces.c₁₂_tmul
  Algebra.DescentCofaces.c₂₃_tmul
  Algebra.DescentCofaces.c₁₃_tmul
universe u w
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₁

L547 ↗

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

Source context 12 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AffineRigidDescent
attribute [-simp]
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
  Algebra.DescentCofaces.i₁_apply
  Algebra.DescentCofaces.i₂_apply
  Algebra.DescentCofaces.c₁₂_tmul
  Algebra.DescentCofaces.c₂₃_tmul
  Algebra.DescentCofaces.c₁₃_tmul
universe u w
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₂

L550 ↗

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

Source context 12 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AffineRigidDescent
attribute [-simp]
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
  Algebra.DescentCofaces.i₁_apply
  Algebra.DescentCofaces.i₂_apply
  Algebra.DescentCofaces.c₁₂_tmul
  Algebra.DescentCofaces.c₂₃_tmul
  Algebra.DescentCofaces.c₁₃_tmul
universe u w
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₁

L553 ↗

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

Source context 12 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AffineRigidDescent
attribute [-simp]
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
  Algebra.DescentCofaces.i₁_apply
  Algebra.DescentCofaces.i₂_apply
  Algebra.DescentCofaces.c₁₂_tmul
  Algebra.DescentCofaces.c₂₃_tmul
  Algebra.DescentCofaces.c₁₃_tmul
universe u w
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₃

L557 ↗

JacobianVarieties.Picard.Proofs.AffineRigidDescent.ExZar.chosenPullback₃

Documentation

The chosen triple pullback of the maps between base-changed curves.

Source context 12 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AffineRigidDescent
attribute [-simp]
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
  Algebra.DescentCofaces.i₁_apply
  Algebra.DescentCofaces.i₂_apply
  Algebra.DescentCofaces.c₁₂_tmul
  Algebra.DescentCofaces.c₂₃_tmul
  Algebra.DescentCofaces.c₁₃_tmul
universe u w
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

L608 ↗

JacobianVarieties.Picard.Proofs.AffineRigidDescent.ExZar.isInvertible_of_iso

Source context 12 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AffineRigidDescent
attribute [-simp]
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
  Algebra.DescentCofaces.i₁_apply
  Algebra.DescentCofaces.i₂_apply
  Algebra.DescentCofaces.c₁₂_tmul
  Algebra.DescentCofaces.c₂₃_tmul
  Algebra.DescentCofaces.c₁₃_tmul
universe u w
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
noncomputable section
namespace ExZar
open  NeronModelInfra AlgebraicGeometry.RelPicard CategoryTheory.Pseudofunctor
  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

L614 ↗

JacobianVarieties.Picard.Proofs.AffineRigidDescent.ExZar.isInvertible_of_openCover

Source context 12 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AffineRigidDescent
attribute [-simp]
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
  Algebra.DescentCofaces.i₁_apply
  Algebra.DescentCofaces.i₂_apply
  Algebra.DescentCofaces.c₁₂_tmul
  Algebra.DescentCofaces.c₂₃_tmul
  Algebra.DescentCofaces.c₁₃_tmul
universe u w
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
noncomputable section
namespace ExZar
open  NeronModelInfra AlgebraicGeometry.RelPicard CategoryTheory.Pseudofunctor
  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 w} {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

abbrev

EE

L636 ↗

JacobianVarieties.Picard.Proofs.AffineRigidDescent.ExZar.EE

Documentation

The unit module sheaf on the given scheme.

Source context 14 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AffineRigidDescent
attribute [-simp]
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
  Algebra.DescentCofaces.i₁_apply
  Algebra.DescentCofaces.i₂_apply
  Algebra.DescentCofaces.c₁₂_tmul
  Algebra.DescentCofaces.c₂₃_tmul
  Algebra.DescentCofaces.c₁₃_tmul
universe u w
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
noncomputable section
namespace ExZar
open  NeronModelInfra AlgebraicGeometry.RelPicard CategoryTheory.Pseudofunctor
  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 w} {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

β

L639 ↗

JacobianVarieties.Picard.Proofs.AffineRigidDescent.ExZar.β

Documentation

Identify the module along its rigidifying section with the pulled-back unit on the target.

Source context 14 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AffineRigidDescent
attribute [-simp]
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
  Algebra.DescentCofaces.i₁_apply
  Algebra.DescentCofaces.i₂_apply
  Algebra.DescentCofaces.c₁₂_tmul
  Algebra.DescentCofaces.c₂₃_tmul
  Algebra.DescentCofaces.c₁₃_tmul
universe u w
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
noncomputable section
namespace ExZar
open  NeronModelInfra AlgebraicGeometry.RelPicard CategoryTheory.Pseudofunctor
  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 w} {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

Θ

L645 ↗

JacobianVarieties.Picard.Proofs.AffineRigidDescent.ExZar.Θ

Documentation

Transport a rigidification through a commuting square to a pulled-back unit sheaf.

Source context 14 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AffineRigidDescent
attribute [-simp]
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
  Algebra.DescentCofaces.i₁_apply
  Algebra.DescentCofaces.i₂_apply
  Algebra.DescentCofaces.c₁₂_tmul
  Algebra.DescentCofaces.c₂₃_tmul
  Algebra.DescentCofaces.c₁₃_tmul
universe u w
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
noncomputable section
namespace ExZar
open  NeronModelInfra AlgebraicGeometry.RelPicard CategoryTheory.Pseudofunctor
  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 w} {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

L662 ↗

JacobianVarieties.Picard.Proofs.AffineRigidDescent.ExZar.iso_eq_of_map_rigSection_eq

Source context 17 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AffineRigidDescent
attribute [-simp]
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
  Algebra.DescentCofaces.i₁_apply
  Algebra.DescentCofaces.i₂_apply
  Algebra.DescentCofaces.c₁₂_tmul
  Algebra.DescentCofaces.c₂₃_tmul
  Algebra.DescentCofaces.c₁₃_tmul
universe u w
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
noncomputable section
namespace ExZar
open  NeronModelInfra AlgebraicGeometry.RelPicard CategoryTheory.Pseudofunctor
  CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
section Rigidity
variable {Z : Scheme.{u}} (z : Z ⟶ Spec (CommRingCat.of R))
open _root_.AlgebraicGeometry.RelPicard.RigidifiedLineBundle in

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 := 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

L691 ↗

JacobianVarieties.Picard.Proofs.AffineRigidDescent.ExZar.hom_eq_of_map_rigSection_eq

Source context 16 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AffineRigidDescent
attribute [-simp]
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
  Algebra.DescentCofaces.i₁_apply
  Algebra.DescentCofaces.i₂_apply
  Algebra.DescentCofaces.c₁₂_tmul
  Algebra.DescentCofaces.c₂₃_tmul
  Algebra.DescentCofaces.c₁₃_tmul
universe u w
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
noncomputable section
namespace ExZar
open  NeronModelInfra AlgebraicGeometry.RelPicard CategoryTheory.Pseudofunctor
  CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
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

L708 ↗

JacobianVarieties.Picard.Proofs.AffineRigidDescent.ExZar.exists_iso_map_rigSection_eq

Source context 16 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AffineRigidDescent
attribute [-simp]
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
  Algebra.DescentCofaces.i₁_apply
  Algebra.DescentCofaces.i₂_apply
  Algebra.DescentCofaces.c₁₂_tmul
  Algebra.DescentCofaces.c₂₃_tmul
  Algebra.DescentCofaces.c₁₃_tmul
universe u w
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
noncomputable section
namespace ExZar
open  NeronModelInfra AlgebraicGeometry.RelPicard CategoryTheory.Pseudofunctor
  CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
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

L744 ↗

JacobianVarieties.Picard.Proofs.AffineRigidDescent.ExZar.fF

Documentation

The map between base-changed curves induced by a member of the covering family.

Source context 18 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AffineRigidDescent
attribute [-simp]
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
  Algebra.DescentCofaces.i₁_apply
  Algebra.DescentCofaces.i₂_apply
  Algebra.DescentCofaces.c₁₂_tmul
  Algebra.DescentCofaces.c₂₃_tmul
  Algebra.DescentCofaces.c₁₃_tmul
universe u w
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
noncomputable section
namespace ExZar
open  NeronModelInfra AlgebraicGeometry.RelPicard CategoryTheory.Pseudofunctor
  CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
section Datum
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type w} {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

L747 ↗

JacobianVarieties.Picard.Proofs.AffineRigidDescent.ExZar.sqF

Documentation

The chosen double overlap for the induced maps between base-changed curves.

Source context 18 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AffineRigidDescent
attribute [-simp]
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
  Algebra.DescentCofaces.i₁_apply
  Algebra.DescentCofaces.i₂_apply
  Algebra.DescentCofaces.c₁₂_tmul
  Algebra.DescentCofaces.c₂₃_tmul
  Algebra.DescentCofaces.c₁₃_tmul
universe u w
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
noncomputable section
namespace ExZar
open  NeronModelInfra AlgebraicGeometry.RelPicard CategoryTheory.Pseudofunctor
  CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
section Datum
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type w} {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

L750 ↗

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

Documentation

The chosen triple overlap for the induced maps between base-changed curves.

Source context 18 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AffineRigidDescent
attribute [-simp]
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
  Algebra.DescentCofaces.i₁_apply
  Algebra.DescentCofaces.i₂_apply
  Algebra.DescentCofaces.c₁₂_tmul
  Algebra.DescentCofaces.c₂₃_tmul
  Algebra.DescentCofaces.c₁₃_tmul
universe u w
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
noncomputable section
namespace ExZar
open  NeronModelInfra AlgebraicGeometry.RelPicard CategoryTheory.Pseudofunctor
  CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
section Datum
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type w} {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

L754 ↗

JacobianVarieties.Picard.Proofs.AffineRigidDescent.ExZar.wT

Documentation

The structure morphism from a double overlap to the target of the covering family.

Source context 18 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AffineRigidDescent
attribute [-simp]
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
  Algebra.DescentCofaces.i₁_apply
  Algebra.DescentCofaces.i₂_apply
  Algebra.DescentCofaces.c₁₂_tmul
  Algebra.DescentCofaces.c₂₃_tmul
  Algebra.DescentCofaces.c₁₃_tmul
universe u w
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
noncomputable section
namespace ExZar
open  NeronModelInfra AlgebraicGeometry.RelPicard CategoryTheory.Pseudofunctor
  CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
section Datum
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type w} {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

L756 ↗

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

Source context 18 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AffineRigidDescent
attribute [-simp]
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
  Algebra.DescentCofaces.i₁_apply
  Algebra.DescentCofaces.i₂_apply
  Algebra.DescentCofaces.c₁₂_tmul
  Algebra.DescentCofaces.c₂₃_tmul
  Algebra.DescentCofaces.c₁₃_tmul
universe u w
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
noncomputable section
namespace ExZar
open  NeronModelInfra AlgebraicGeometry.RelPicard CategoryTheory.Pseudofunctor
  CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
section Datum
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type w} {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

Θ₁

L759 ↗

JacobianVarieties.Picard.Proofs.AffineRigidDescent.ExZar.Θ₁

Documentation

The first bundle rigidification transported to a double overlap.

Source context 18 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AffineRigidDescent
attribute [-simp]
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
  Algebra.DescentCofaces.i₁_apply
  Algebra.DescentCofaces.i₂_apply
  Algebra.DescentCofaces.c₁₂_tmul
  Algebra.DescentCofaces.c₂₃_tmul
  Algebra.DescentCofaces.c₁₃_tmul
universe u w
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
noncomputable section
namespace ExZar
open  NeronModelInfra AlgebraicGeometry.RelPicard CategoryTheory.Pseudofunctor
  CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
section Datum
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type w} {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

Θ₂

L764 ↗

JacobianVarieties.Picard.Proofs.AffineRigidDescent.ExZar.Θ₂

Documentation

The second bundle rigidification transported to a double overlap.

Source context 18 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AffineRigidDescent
attribute [-simp]
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
  Algebra.DescentCofaces.i₁_apply
  Algebra.DescentCofaces.i₂_apply
  Algebra.DescentCofaces.c₁₂_tmul
  Algebra.DescentCofaces.c₂₃_tmul
  Algebra.DescentCofaces.c₁₃_tmul
universe u w
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
noncomputable section
namespace ExZar
open  NeronModelInfra AlgebraicGeometry.RelPicard CategoryTheory.Pseudofunctor
  CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
section Datum
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type w} {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

L769 ↗

JacobianVarieties.Picard.Proofs.AffineRigidDescent.ExZar.exists_homIso

Source context 19 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AffineRigidDescent
attribute [-simp]
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
  Algebra.DescentCofaces.i₁_apply
  Algebra.DescentCofaces.i₂_apply
  Algebra.DescentCofaces.c₁₂_tmul
  Algebra.DescentCofaces.c₂₃_tmul
  Algebra.DescentCofaces.c₁₃_tmul
universe u w
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
noncomputable section
namespace ExZar
open  NeronModelInfra AlgebraicGeometry.RelPicard CategoryTheory.Pseudofunctor
  CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
section Datum
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type w} {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

L780 ↗

JacobianVarieties.Picard.Proofs.AffineRigidDescent.ExZar.homIso

Documentation

Choose the overlap isomorphism normalized to preserve the transported rigidifications.

Source context 19 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AffineRigidDescent
attribute [-simp]
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
  Algebra.DescentCofaces.i₁_apply
  Algebra.DescentCofaces.i₂_apply
  Algebra.DescentCofaces.c₁₂_tmul
  Algebra.DescentCofaces.c₂₃_tmul
  Algebra.DescentCofaces.c₁₃_tmul
universe u w
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
noncomputable section
namespace ExZar
open  NeronModelInfra AlgebraicGeometry.RelPicard CategoryTheory.Pseudofunctor
  CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
section Datum
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type w} {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

L785 ↗

JacobianVarieties.Picard.Proofs.AffineRigidDescent.ExZar.map_homIso

Source context 18 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AffineRigidDescent
attribute [-simp]
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
  Algebra.DescentCofaces.i₁_apply
  Algebra.DescentCofaces.i₂_apply
  Algebra.DescentCofaces.c₁₂_tmul
  Algebra.DescentCofaces.c₂₃_tmul
  Algebra.DescentCofaces.c₁₃_tmul
universe u w
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
noncomputable section
namespace ExZar
open  NeronModelInfra AlgebraicGeometry.RelPicard CategoryTheory.Pseudofunctor
  CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
section Datum
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type w} {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

L801 ↗

JacobianVarieties.Picard.Proofs.AffineRigidDescent.ExZar.half_A

Source context 21 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AffineRigidDescent
attribute [-simp]
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
  Algebra.DescentCofaces.i₁_apply
  Algebra.DescentCofaces.i₂_apply
  Algebra.DescentCofaces.c₁₂_tmul
  Algebra.DescentCofaces.c₂₃_tmul
  Algebra.DescentCofaces.c₁₃_tmul
universe u w
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
noncomputable section
namespace ExZar
open  NeronModelInfra AlgebraicGeometry.RelPicard CategoryTheory.Pseudofunctor
  CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
section Datum
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type w} {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

L820 ↗

JacobianVarieties.Picard.Proofs.AffineRigidDescent.ExZar.half_B

Source context 21 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AffineRigidDescent
attribute [-simp]
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
  Algebra.DescentCofaces.i₁_apply
  Algebra.DescentCofaces.i₂_apply
  Algebra.DescentCofaces.c₁₂_tmul
  Algebra.DescentCofaces.c₂₃_tmul
  Algebra.DescentCofaces.c₁₃_tmul
universe u w
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
noncomputable section
namespace ExZar
open  NeronModelInfra AlgebraicGeometry.RelPicard CategoryTheory.Pseudofunctor
  CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
section Datum
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type w} {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

L828 ↗

JacobianVarieties.Picard.Proofs.AffineRigidDescent.ExZar.half_C

Source context 21 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AffineRigidDescent
attribute [-simp]
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
  Algebra.DescentCofaces.i₁_apply
  Algebra.DescentCofaces.i₂_apply
  Algebra.DescentCofaces.c₁₂_tmul
  Algebra.DescentCofaces.c₂₃_tmul
  Algebra.DescentCofaces.c₁₃_tmul
universe u w
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
noncomputable section
namespace ExZar
open  NeronModelInfra AlgebraicGeometry.RelPicard CategoryTheory.Pseudofunctor
  CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
section Datum
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type w} {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

L837 ↗

JacobianVarieties.Picard.Proofs.AffineRigidDescent.ExZar.half

Source context 21 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AffineRigidDescent
attribute [-simp]
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
  Algebra.DescentCofaces.i₁_apply
  Algebra.DescentCofaces.i₂_apply
  Algebra.DescentCofaces.c₁₂_tmul
  Algebra.DescentCofaces.c₂₃_tmul
  Algebra.DescentCofaces.c₁₃_tmul
universe u w
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
noncomputable section
namespace ExZar
open  NeronModelInfra AlgebraicGeometry.RelPicard CategoryTheory.Pseudofunctor
  CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
section Datum
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type w} {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'

L857 ↗

JacobianVarieties.Picard.Proofs.AffineRigidDescent.ExZar.half'

Source context 21 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AffineRigidDescent
attribute [-simp]
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
  Algebra.DescentCofaces.i₁_apply
  Algebra.DescentCofaces.i₂_apply
  Algebra.DescentCofaces.c₁₂_tmul
  Algebra.DescentCofaces.c₂₃_tmul
  Algebra.DescentCofaces.c₁₃_tmul
universe u w
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
noncomputable section
namespace ExZar
open  NeronModelInfra AlgebraicGeometry.RelPicard CategoryTheory.Pseudofunctor
  CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
section Datum
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type w} {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

L873 ↗

JacobianVarieties.Picard.Proofs.AffineRigidDescent.ExZar.half_inv

Source context 21 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AffineRigidDescent
attribute [-simp]
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
  Algebra.DescentCofaces.i₁_apply
  Algebra.DescentCofaces.i₂_apply
  Algebra.DescentCofaces.c₁₂_tmul
  Algebra.DescentCofaces.c₂₃_tmul
  Algebra.DescentCofaces.c₁₃_tmul
universe u w
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
noncomputable section
namespace ExZar
open  NeronModelInfra AlgebraicGeometry.RelPicard CategoryTheory.Pseudofunctor
  CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
section Datum
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type w} {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

L900 ↗

JacobianVarieties.Picard.Proofs.AffineRigidDescent.ExZar.key

Source context 20 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AffineRigidDescent
attribute [-simp]
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
  Algebra.DescentCofaces.i₁_apply
  Algebra.DescentCofaces.i₂_apply
  Algebra.DescentCofaces.c₁₂_tmul
  Algebra.DescentCofaces.c₂₃_tmul
  Algebra.DescentCofaces.c₁₃_tmul
universe u w
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
noncomputable section
namespace ExZar
open  NeronModelInfra AlgebraicGeometry.RelPicard CategoryTheory.Pseudofunctor
  CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
section Datum
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type w} {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))
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val

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

δ

L948 ↗

JacobianVarieties.Picard.Proofs.AffineRigidDescent.ExZar.δ

Documentation

The diagonal morphism into the self-overlap of a member of the covering family.

Source context 20 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AffineRigidDescent
attribute [-simp]
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
  Algebra.DescentCofaces.i₁_apply
  Algebra.DescentCofaces.i₂_apply
  Algebra.DescentCofaces.c₁₂_tmul
  Algebra.DescentCofaces.c₂₃_tmul
  Algebra.DescentCofaces.c₁₃_tmul
universe u w
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
noncomputable section
namespace ExZar
open  NeronModelInfra AlgebraicGeometry.RelPicard CategoryTheory.Pseudofunctor
  CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
section Datum
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type w} {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))
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val

Lean source · statement

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

lemma

δ_pr₁

L951 ↗

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

Source context 20 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AffineRigidDescent
attribute [-simp]
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
  Algebra.DescentCofaces.i₁_apply
  Algebra.DescentCofaces.i₂_apply
  Algebra.DescentCofaces.c₁₂_tmul
  Algebra.DescentCofaces.c₂₃_tmul
  Algebra.DescentCofaces.c₁₃_tmul
universe u w
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
noncomputable section
namespace ExZar
open  NeronModelInfra AlgebraicGeometry.RelPicard CategoryTheory.Pseudofunctor
  CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
section Datum
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type w} {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))
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val

Lean source · statement

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

lemma

δ_pr₂

L958 ↗

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

Source context 20 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AffineRigidDescent
attribute [-simp]
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
  Algebra.DescentCofaces.i₁_apply
  Algebra.DescentCofaces.i₂_apply
  Algebra.DescentCofaces.c₁₂_tmul
  Algebra.DescentCofaces.c₂₃_tmul
  Algebra.DescentCofaces.c₁₃_tmul
universe u w
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
noncomputable section
namespace ExZar
open  NeronModelInfra AlgebraicGeometry.RelPicard CategoryTheory.Pseudofunctor
  CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
section Datum
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type w} {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))
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val

Lean source · statement

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

lemma

nonempty_rigidification

L965 ↗

JacobianVarieties.Picard.Proofs.AffineRigidDescent.ExZar.nonempty_rigidification

Source context 20 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AffineRigidDescent
attribute [-simp]
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
  Algebra.DescentCofaces.i₁_apply
  Algebra.DescentCofaces.i₂_apply
  Algebra.DescentCofaces.c₁₂_tmul
  Algebra.DescentCofaces.c₂₃_tmul
  Algebra.DescentCofaces.c₁₃_tmul
universe u w
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
noncomputable section
namespace ExZar
open  NeronModelInfra AlgebraicGeometry.RelPicard CategoryTheory.Pseudofunctor
  CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
section Datum
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type w} {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))
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val

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

L973 ↗

JacobianVarieties.Picard.Proofs.AffineRigidDescent.ExZar.pullHomIso_self

Source context 20 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AffineRigidDescent
attribute [-simp]
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
  Algebra.DescentCofaces.i₁_apply
  Algebra.DescentCofaces.i₂_apply
  Algebra.DescentCofaces.c₁₂_tmul
  Algebra.DescentCofaces.c₂₃_tmul
  Algebra.DescentCofaces.c₁₃_tmul
universe u w
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
noncomputable section
namespace ExZar
open  NeronModelInfra AlgebraicGeometry.RelPicard CategoryTheory.Pseudofunctor
  CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
section Datum
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type w} {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))
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val

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) ε :=
    (Category.comp_id _).trans (Category.id_comp _).symm
  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]
      simp only [Iso.refl_hom, Iso.hom_inv_id]
      exact ((Scheme.Modules.pullback (rigSection c (u i) ε)).map_id _).symm)

abbrev

ζT3

L998 ↗

JacobianVarieties.Picard.Proofs.AffineRigidDescent.ExZar.ζT3

Documentation

The structure morphism from a triple overlap to the target of the covering family.

Source context 22 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AffineRigidDescent
attribute [-simp]
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
  Algebra.DescentCofaces.i₁_apply
  Algebra.DescentCofaces.i₂_apply
  Algebra.DescentCofaces.c₁₂_tmul
  Algebra.DescentCofaces.c₂₃_tmul
  Algebra.DescentCofaces.c₁₃_tmul
universe u w
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
noncomputable section
namespace ExZar
open  NeronModelInfra AlgebraicGeometry.RelPicard CategoryTheory.Pseudofunctor
  CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
section Datum
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type w} {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))
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
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

χ₁

L1002 ↗

JacobianVarieties.Picard.Proofs.AffineRigidDescent.ExZar.χ₁

Documentation

Project a triple overlap to its first member of the covering family.

Source context 22 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AffineRigidDescent
attribute [-simp]
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
  Algebra.DescentCofaces.i₁_apply
  Algebra.DescentCofaces.i₂_apply
  Algebra.DescentCofaces.c₁₂_tmul
  Algebra.DescentCofaces.c₂₃_tmul
  Algebra.DescentCofaces.c₁₃_tmul
universe u w
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
noncomputable section
namespace ExZar
open  NeronModelInfra AlgebraicGeometry.RelPicard CategoryTheory.Pseudofunctor
  CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
section Datum
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type w} {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))
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
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

χ₂

L1005 ↗

JacobianVarieties.Picard.Proofs.AffineRigidDescent.ExZar.χ₂

Documentation

Project a triple overlap to its second member of the covering family.

Source context 22 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AffineRigidDescent
attribute [-simp]
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
  Algebra.DescentCofaces.i₁_apply
  Algebra.DescentCofaces.i₂_apply
  Algebra.DescentCofaces.c₁₂_tmul
  Algebra.DescentCofaces.c₂₃_tmul
  Algebra.DescentCofaces.c₁₃_tmul
universe u w
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
noncomputable section
namespace ExZar
open  NeronModelInfra AlgebraicGeometry.RelPicard CategoryTheory.Pseudofunctor
  CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
section Datum
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type w} {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))
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
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

χ₃

L1008 ↗

JacobianVarieties.Picard.Proofs.AffineRigidDescent.ExZar.χ₃

Documentation

Project a triple overlap to its third member of the covering family.

Source context 22 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AffineRigidDescent
attribute [-simp]
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
  Algebra.DescentCofaces.i₁_apply
  Algebra.DescentCofaces.i₂_apply
  Algebra.DescentCofaces.c₁₂_tmul
  Algebra.DescentCofaces.c₂₃_tmul
  Algebra.DescentCofaces.c₁₃_tmul
universe u w
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
noncomputable section
namespace ExZar
open  NeronModelInfra AlgebraicGeometry.RelPicard CategoryTheory.Pseudofunctor
  CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
section Datum
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type w} {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))
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
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χ₁

L1011 ↗

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

Source context 22 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AffineRigidDescent
attribute [-simp]
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
  Algebra.DescentCofaces.i₁_apply
  Algebra.DescentCofaces.i₂_apply
  Algebra.DescentCofaces.c₁₂_tmul
  Algebra.DescentCofaces.c₂₃_tmul
  Algebra.DescentCofaces.c₁₃_tmul
universe u w
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
noncomputable section
namespace ExZar
open  NeronModelInfra AlgebraicGeometry.RelPicard CategoryTheory.Pseudofunctor
  CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
section Datum
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type w} {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))
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
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χ₂

L1012 ↗

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

Source context 22 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AffineRigidDescent
attribute [-simp]
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
  Algebra.DescentCofaces.i₁_apply
  Algebra.DescentCofaces.i₂_apply
  Algebra.DescentCofaces.c₁₂_tmul
  Algebra.DescentCofaces.c₂₃_tmul
  Algebra.DescentCofaces.c₁₃_tmul
universe u w
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
noncomputable section
namespace ExZar
open  NeronModelInfra AlgebraicGeometry.RelPicard CategoryTheory.Pseudofunctor
  CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
section Datum
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type w} {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))
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
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χ₃

L1016 ↗

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

Source context 22 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AffineRigidDescent
attribute [-simp]
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
  Algebra.DescentCofaces.i₁_apply
  Algebra.DescentCofaces.i₂_apply
  Algebra.DescentCofaces.c₁₂_tmul
  Algebra.DescentCofaces.c₂₃_tmul
  Algebra.DescentCofaces.c₁₃_tmul
universe u w
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
noncomputable section
namespace ExZar
open  NeronModelInfra AlgebraicGeometry.RelPicard CategoryTheory.Pseudofunctor
  CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
section Datum
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type w} {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))
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
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₁'

L1025 ↗

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

Source context 22 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AffineRigidDescent
attribute [-simp]
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
  Algebra.DescentCofaces.i₁_apply
  Algebra.DescentCofaces.i₂_apply
  Algebra.DescentCofaces.c₁₂_tmul
  Algebra.DescentCofaces.c₂₃_tmul
  Algebra.DescentCofaces.c₁₃_tmul
universe u w
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
noncomputable section
namespace ExZar
open  NeronModelInfra AlgebraicGeometry.RelPicard CategoryTheory.Pseudofunctor
  CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
section Datum
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type w} {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))
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
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₂'

L1027 ↗

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

Source context 22 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AffineRigidDescent
attribute [-simp]
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
  Algebra.DescentCofaces.i₁_apply
  Algebra.DescentCofaces.i₂_apply
  Algebra.DescentCofaces.c₁₂_tmul
  Algebra.DescentCofaces.c₂₃_tmul
  Algebra.DescentCofaces.c₁₃_tmul
universe u w
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
noncomputable section
namespace ExZar
open  NeronModelInfra AlgebraicGeometry.RelPicard CategoryTheory.Pseudofunctor
  CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
section Datum
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type w} {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))
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
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₃'

L1029 ↗

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

Source context 22 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AffineRigidDescent
attribute [-simp]
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
  Algebra.DescentCofaces.i₁_apply
  Algebra.DescentCofaces.i₂_apply
  Algebra.DescentCofaces.c₁₂_tmul
  Algebra.DescentCofaces.c₂₃_tmul
  Algebra.DescentCofaces.c₁₃_tmul
universe u w
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
noncomputable section
namespace ExZar
open  NeronModelInfra AlgebraicGeometry.RelPicard CategoryTheory.Pseudofunctor
  CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
section Datum
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type w} {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))
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
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

L1032 ↗

JacobianVarieties.Picard.Proofs.AffineRigidDescent.ExZar.pullHomIso_comp

Source context 22 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AffineRigidDescent
attribute [-simp]
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
  Algebra.DescentCofaces.i₁_apply
  Algebra.DescentCofaces.i₂_apply
  Algebra.DescentCofaces.c₁₂_tmul
  Algebra.DescentCofaces.c₂₃_tmul
  Algebra.DescentCofaces.c₁₃_tmul
universe u w
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
noncomputable section
namespace ExZar
open  NeronModelInfra AlgebraicGeometry.RelPicard CategoryTheory.Pseudofunctor
  CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
section Datum
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type w} {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))
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
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])

instance

isAffineHom_q

L1087 ↗

JacobianVarieties.Picard.Proofs.AffineRigidDescent.ExZar.isAffineHom_q

Source context 21 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AffineRigidDescent
attribute [-simp]
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
  Algebra.DescentCofaces.i₁_apply
  Algebra.DescentCofaces.i₂_apply
  Algebra.DescentCofaces.c₁₂_tmul
  Algebra.DescentCofaces.c₂₃_tmul
  Algebra.DescentCofaces.c₁₃_tmul
universe u w
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
noncomputable section
namespace ExZar
open  NeronModelInfra AlgebraicGeometry.RelPicard CategoryTheory.Pseudofunctor
  CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
section FF
open AlgebraicGeometry.SmoothProperCurve
variable {T T' : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)} {t' : T' ⟶ Spec (CommRingCat.of R)}
  (π : SchemeHomOver t' t) [IsAffineHom π.1] [Flat π.1] [Surjective π.1]

Lean source · statement

instance isAffineHom_q : IsAffineHom (baseChangeSnd c π)

instance

flat_q

L1089 ↗

JacobianVarieties.Picard.Proofs.AffineRigidDescent.ExZar.flat_q

Source context 21 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AffineRigidDescent
attribute [-simp]
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
  Algebra.DescentCofaces.i₁_apply
  Algebra.DescentCofaces.i₂_apply
  Algebra.DescentCofaces.c₁₂_tmul
  Algebra.DescentCofaces.c₂₃_tmul
  Algebra.DescentCofaces.c₁₃_tmul
universe u w
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
noncomputable section
namespace ExZar
open  NeronModelInfra AlgebraicGeometry.RelPicard CategoryTheory.Pseudofunctor
  CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
section FF
open AlgebraicGeometry.SmoothProperCurve
variable {T T' : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)} {t' : T' ⟶ Spec (CommRingCat.of R)}
  (π : SchemeHomOver t' t) [IsAffineHom π.1] [Flat π.1] [Surjective π.1]

Lean source · statement

instance flat_q : Flat (baseChangeSnd c π)

instance

surjective_q

L1091 ↗

JacobianVarieties.Picard.Proofs.AffineRigidDescent.ExZar.surjective_q

Source context 21 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AffineRigidDescent
attribute [-simp]
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
  Algebra.DescentCofaces.i₁_apply
  Algebra.DescentCofaces.i₂_apply
  Algebra.DescentCofaces.c₁₂_tmul
  Algebra.DescentCofaces.c₂₃_tmul
  Algebra.DescentCofaces.c₁₃_tmul
universe u w
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
noncomputable section
namespace ExZar
open  NeronModelInfra AlgebraicGeometry.RelPicard CategoryTheory.Pseudofunctor
  CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
section FF
open AlgebraicGeometry.SmoothProperCurve
variable {T T' : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)} {t' : T' ⟶ Spec (CommRingCat.of R)}
  (π : SchemeHomOver t' t) [IsAffineHom π.1] [Flat π.1] [Surjective π.1]

Lean source · statement

instance surjective_q : Surjective (baseChangeSnd c π)

abbrev

fS

L1095 ↗

JacobianVarieties.Picard.Proofs.AffineRigidDescent.ExZar.fS

Documentation

The singleton covering family with the given affine faithfully flat map as its sole member.

Source context 21 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AffineRigidDescent
attribute [-simp]
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
  Algebra.DescentCofaces.i₁_apply
  Algebra.DescentCofaces.i₂_apply
  Algebra.DescentCofaces.c₁₂_tmul
  Algebra.DescentCofaces.c₂₃_tmul
  Algebra.DescentCofaces.c₁₃_tmul
universe u w
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
noncomputable section
namespace ExZar
open  NeronModelInfra AlgebraicGeometry.RelPicard CategoryTheory.Pseudofunctor
  CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
section FF
open AlgebraicGeometry.SmoothProperCurve
variable {T T' : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)} {t' : T' ⟶ Spec (CommRingCat.of R)}
  (π : SchemeHomOver t' t) [IsAffineHom π.1] [Flat π.1] [Surjective π.1]

Lean source · statement

abbrev fS : Unit → SchemeHomOver t' t

theorem

main_ff

L1097 ↗

JacobianVarieties.Picard.Proofs.AffineRigidDescent.ExZar.main_ff

Source context 21 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AffineRigidDescent
attribute [-simp]
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
  Algebra.DescentCofaces.i₁_apply
  Algebra.DescentCofaces.i₂_apply
  Algebra.DescentCofaces.c₁₂_tmul
  Algebra.DescentCofaces.c₂₃_tmul
  Algebra.DescentCofaces.c₁₃_tmul
universe u w
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
noncomputable section
namespace ExZar
open  NeronModelInfra AlgebraicGeometry.RelPicard CategoryTheory.Pseudofunctor
  CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
attribute [local simp] ExZar.pr₁_val
attribute [local simp] ExZar.pr₂_val
section FF
open AlgebraicGeometry.SmoothProperCurve
variable {T T' : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)} {t' : T' ⟶ Spec (CommRingCat.of R)}
  (π : SchemeHomOver t' t) [IsAffineHom π.1] [Flat π.1] [Surjective π.1]

Lean source · full declaration

theorem main_ff (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),
        ⊤)))
    (M' : RigidifiedLineBundle c ε t')
    (hM' : ∀ (Z : Scheme.{u}) (z : Z ⟶ Spec (CommRingCat.of R))
      (p₁ p₂ : SchemeHomOver z t'),
      p₁.1 ≫ π.1 = p₂.1 ≫ π.1 →
        Nonempty ((M'.pullbackAlong p₁).L ≅ (M'.pullbackAlong p₂).L)) :
    ∃ M : RigidifiedLineBundle c ε t, Nonempty ((M.pullbackAlong π).L ≅ M'.L) := by
  have hM : ∀ (i j : Unit) (Z : Scheme.{u}) (z : Z ⟶ Spec (CommRingCat.of R))
      (p₁ : SchemeHomOver z t')
      (p₂ : SchemeHomOver z t'),
      p₁.1 ≫ (fS π i).1 = p₂.1 ≫ (fS π j).1 →
        Nonempty ((((fun _ : Unit => M') i).pullbackAlong p₁).L ≅ (((fun _ : Unit => M')
          j).pullbackAlong p₂).L) :=
    fun _ _ Z z p₁ p₂ h => hM' Z z p₁ p₂ h
  have HH := exists_iso_of_plainDescent_ff (baseChangeSnd c π)
    (sqF c (fS π)) (sq₃F c (fS π)) (fun _ => M'.L) (fun _ => M'.isInvertible)
    (fun i j => homIso c ε (fS π) (fun _ : Unit => M') hM i j)
    (fun i => baseChangeSnd c (δ (fS π) i)) (δ_pr₁ c (fS π)) (δ_pr₂ c (fS π))
    (fun i _ _ => pullHomIso_self c ε (fS π) (fun _ : Unit => M') hM hH0 i)
    (fun i j k _ _ _ _ _ _ => pullHomIso_comp c ε (fS π) (fun _ : Unit => M') hM i j k hH0)
  obtain ⟨L, hL, eL⟩ := HH
  have eᵢ : (Scheme.Modules.pullback (baseChangeSnd c π)).obj L ≅ M'.L := (eL ()).some
  refine ⟨RigidifiedLineBundle.ofInvertible (ε := ε) L hL, ?_⟩
  obtain ⟨a⟩ := RigidifiedLineBundle.nonempty_ofInvertible_pullbackAlong_iso (ε := ε) π hL
  obtain ⟨b⟩ := RigidifiedLineBundle.nonempty_ofInvertible_iso_of_iso (ε := ε) (hL.pullback _)
    M'.isInvertible eᵢ
  obtain ⟨d⟩ := RigidifiedLineBundle.nonempty_ofInvertible_iso_of_rigidified M'
  exact ⟨a ≪≫ b ≪≫ d⟩

theorem

exists_descent_of_isAffineHom_of_flat_of_surjective_of_bijective_sections

L1167 ↗

AlgebraicGeometry.RelPicard.RigidifiedLineBundle.exists_descent_of_isAffineHom_of_flat_of_surjective_of_bijective_sections

Documentation

Descend a rigidified bundle along an affine faithfully flat map using rigidity of sections.

Source context 5 commands

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

open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra AlgebraicGeometry.RelPicard AlgebraicGeometry.SmoothProperCurve
namespace AlgebraicGeometry.RelPicard.RigidifiedLineBundle
universe u
open JacobianVarieties.Picard.Proofs.AffineRigidDescent in

Lean source · full declaration

theorem exists_descent_of_isAffineHom_of_flat_of_surjective_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 T' : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) (t' : T' ⟶ Spec (CommRingCat.of R))
    (π : SchemeHomOver t' t) [IsAffineHom π.1] [Flat π.1] [Surjective π.1]
    (M' : RigidifiedLineBundle c ε t')
    (hM' : ∀ (Z : Scheme.{u}) (z : Z ⟶ Spec (CommRingCat.of R))
      (p₁ p₂ : SchemeHomOver z t'),
      p₁.1 ≫ π.1 = p₂.1 ≫ π.1 →
        Nonempty ((M'.pullbackAlong p₁).L ≅ (M'.pullbackAlong p₂).L)) :
    ∃ M : RigidifiedLineBundle c ε t, Nonempty ((M.pullbackAlong π).L ≅ M'.L) :=
  ExZar.main_ff c ε π hH0 M' hM'

Module documentation

Affine descent of rigidified line bundles

Declarations