Module

RigidifiedLineBundle_exists_descent_finite_faithfullyFlat_of_bijective_sections.lean

Nyll.JacobianVarieties.Picard.RigidifiedLineBundle_exists_descent_finite_faithfullyFlat_of_bijective_sections

103 declarations indexed from sourceView source ↗

Module documentation

Faithfully flat descent of rigidified line bundles

Compatible invertible sheaves on a finite faithfully flat base change descend, with their rigidifications, using the bijectivity of global sections.

Imports13

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

Imported by2

theorem

pullbackComp_paste

L54 ↗

JacobianVarieties.Picard.Proofs.FaithfulDescent.ExZar.pullbackComp_paste

Source context 10 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FaithfulDescent
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

L78 ↗

JacobianVarieties.Picard.Proofs.FaithfulDescent.ExZar.pullbackComp_paste_app

Source context 10 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FaithfulDescent
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

τ

L91 ↗

JacobianVarieties.Picard.Proofs.FaithfulDescent.ExZar.τ

Documentation

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

Source context 10 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FaithfulDescent
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

L95 ↗

JacobianVarieties.Picard.Proofs.FaithfulDescent.ExZar.τ_hom_app

Source context 10 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FaithfulDescent
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
  rfl

theorem

τ_inv_app

L100 ↗

JacobianVarieties.Picard.Proofs.FaithfulDescent.ExZar.τ_inv_app

Source context 10 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FaithfulDescent
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
  rfl

theorem

τ_paste_app

L105 ↗

JacobianVarieties.Picard.Proofs.FaithfulDescent.ExZar.τ_paste_app

Source context 10 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FaithfulDescent
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

L116 ↗

JacobianVarieties.Picard.Proofs.FaithfulDescent.ExZar.sqIso

Documentation

The natural isomorphism between pullback functors around a commutative square.

Source context 10 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FaithfulDescent
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

L123 ↗

JacobianVarieties.Picard.Proofs.FaithfulDescent.ExZar.route

Source context 10 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FaithfulDescent
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

L138 ↗

JacobianVarieties.Picard.Proofs.FaithfulDescent.ExZar.MOD

Documentation

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

Source context 8 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FaithfulDescent
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

L144 ↗

JacobianVarieties.Picard.Proofs.FaithfulDescent.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.FaithfulDescent
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

L150 ↗

JacobianVarieties.Picard.Proofs.FaithfulDescent.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.FaithfulDescent
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

L157 ↗

JacobianVarieties.Picard.Proofs.FaithfulDescent.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.FaithfulDescent
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

L165 ↗

JacobianVarieties.Picard.Proofs.FaithfulDescent.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.FaithfulDescent
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

L176 ↗

JacobianVarieties.Picard.Proofs.FaithfulDescent.ExZar.pullHom_MOD

Source context 9 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FaithfulDescent
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

L187 ↗

JacobianVarieties.Picard.Proofs.FaithfulDescent.ExZar.pullHomIso

Documentation

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

Source context 8 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FaithfulDescent
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'

L195 ↗

JacobianVarieties.Picard.Proofs.FaithfulDescent.ExZar.pullHomIso_hom'

Source context 8 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FaithfulDescent
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

L205 ↗

JacobianVarieties.Picard.Proofs.FaithfulDescent.ExZar.pullHomIso_hom

Source context 9 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FaithfulDescent
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

L214 ↗

JacobianVarieties.Picard.Proofs.FaithfulDescent.ExZar.pullHomMap

Documentation

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

Source context 8 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FaithfulDescent
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

L221 ↗

JacobianVarieties.Picard.Proofs.FaithfulDescent.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.FaithfulDescent
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

L229 ↗

JacobianVarieties.Picard.Proofs.FaithfulDescent.ExZar.toMOD

Documentation

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

Source context 8 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FaithfulDescent
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

L233 ↗

JacobianVarieties.Picard.Proofs.FaithfulDescent.ExZar.toMOD_eq

Source context 8 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FaithfulDescent
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

L239 ↗

JacobianVarieties.Picard.Proofs.FaithfulDescent.ExZar.pullHom_toMOD

Source context 9 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FaithfulDescent
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

L247 ↗

JacobianVarieties.Picard.Proofs.FaithfulDescent.ExZar.toMOD_comp

Source context 8 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FaithfulDescent
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

L254 ↗

JacobianVarieties.Picard.Proofs.FaithfulDescent.ExZar.toMOD_congr

Source context 8 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FaithfulDescent
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

L260 ↗

JacobianVarieties.Picard.Proofs.FaithfulDescent.ExZar.toMOD_id

Source context 8 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FaithfulDescent
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

L265 ↗

JacobianVarieties.Picard.Proofs.FaithfulDescent.ExZar.isoOfMOD

Documentation

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

Source context 8 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FaithfulDescent
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

L270 ↗

JacobianVarieties.Picard.Proofs.FaithfulDescent.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.FaithfulDescent
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

L282 ↗

JacobianVarieties.Picard.Proofs.FaithfulDescent.ExZar.pullHomMap_comp_of

Source context 10 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FaithfulDescent
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

L308 ↗

JacobianVarieties.Picard.Proofs.FaithfulDescent.ExZar.homG

Documentation

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

Source context 11 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FaithfulDescent
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

L314 ↗

JacobianVarieties.Picard.Proofs.FaithfulDescent.ExZar.pullHom_homG

Source context 12 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FaithfulDescent
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

L336 ↗

JacobianVarieties.Picard.Proofs.FaithfulDescent.ExZar.dataG

Documentation

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

Source context 12 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FaithfulDescent
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

L356 ↗

JacobianVarieties.Picard.Proofs.FaithfulDescent.ExZar.dataG_obj

Source context 12 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FaithfulDescent
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

L359 ↗

JacobianVarieties.Picard.Proofs.FaithfulDescent.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.FaithfulDescent
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

L378 ↗

JacobianVarieties.Picard.Proofs.FaithfulDescent.ExZar.exists_iso_of_plainDescent_ff

Source context 10 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FaithfulDescent
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

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

L425 ↗

JacobianVarieties.Picard.Proofs.FaithfulDescent.ExZar.isPullback_baseChangeSnd_snd

Source context 10 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FaithfulDescent
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

L434 ↗

JacobianVarieties.Picard.Proofs.FaithfulDescent.ExZar.isPullback_baseChangeSnd

Source context 10 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FaithfulDescent
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₁₂

L457 ↗

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

Documentation

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

Source context 10 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FaithfulDescent
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₁

L464 ↗

JacobianVarieties.Picard.Proofs.FaithfulDescent.ExZar.pr₁

Documentation

The first overlap 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.FaithfulDescent
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₂

L470 ↗

JacobianVarieties.Picard.Proofs.FaithfulDescent.ExZar.pr₂

Documentation

The second overlap 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.FaithfulDescent
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

L479 ↗

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

Source context 10 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FaithfulDescent
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

L484 ↗

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

Source context 10 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FaithfulDescent
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₂

L489 ↗

JacobianVarieties.Picard.Proofs.FaithfulDescent.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.FaithfulDescent
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

L496 ↗

JacobianVarieties.Picard.Proofs.FaithfulDescent.ExZar.chosenPullback

Documentation

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

Source context 10 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FaithfulDescent
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

ρ₁₂

L517 ↗

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

Documentation

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

Source context 12 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FaithfulDescent
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

ρ₂₃

L521 ↗

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

Documentation

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

Source context 12 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FaithfulDescent
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

ρ₁₃

L525 ↗

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

Documentation

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

Source context 12 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FaithfulDescent
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₁

L544 ↗

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

Source context 12 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FaithfulDescent
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₂

L547 ↗

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

Source context 12 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FaithfulDescent
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.FaithfulDescent.ExZar.ρ₂₃_pr₁

Source context 12 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FaithfulDescent
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₃

L554 ↗

JacobianVarieties.Picard.Proofs.FaithfulDescent.ExZar.chosenPullback₃

Documentation

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

Source context 12 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FaithfulDescent
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

L598 ↗

JacobianVarieties.Picard.Proofs.FaithfulDescent.ExZar.isInvertible_of_iso

Source context 11 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FaithfulDescent
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 CategoryTheory.Pseudofunctor
open CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)

Lean source · statement

theorem isInvertible_of_iso {X : Scheme.{u}} {L L' : X.Modules} (e : L ≅ L')
    (h : Scheme.Modules.IsInvertible L') : Scheme.Modules.IsInvertible L

theorem

isInvertible_of_openCover

L604 ↗

JacobianVarieties.Picard.Proofs.FaithfulDescent.ExZar.isInvertible_of_openCover

Source context 11 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FaithfulDescent
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 CategoryTheory.Pseudofunctor
open CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)

Lean source · statement

theorem isInvertible_of_openCover {Y : Scheme.{u}} {ι : Type 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

L626 ↗

JacobianVarieties.Picard.Proofs.FaithfulDescent.ExZar.EE

Documentation

The unit module sheaf on the base scheme.

Source context 13 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FaithfulDescent
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 CategoryTheory.Pseudofunctor
open CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section Theta
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type 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

β

L629 ↗

JacobianVarieties.Picard.Proofs.FaithfulDescent.ExZar.β

Documentation

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

Source context 13 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FaithfulDescent
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 CategoryTheory.Pseudofunctor
open CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section Theta
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type 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

Θ

L635 ↗

JacobianVarieties.Picard.Proofs.FaithfulDescent.ExZar.Θ

Documentation

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

Source context 13 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FaithfulDescent
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 CategoryTheory.Pseudofunctor
open CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section Theta
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type 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

L649 ↗

JacobianVarieties.Picard.Proofs.FaithfulDescent.ExZar.iso_eq_of_map_rigSection_eq

Source context 13 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FaithfulDescent
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 CategoryTheory.Pseudofunctor
open CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section Rigidity
variable {Z : Scheme.{u}} (z : Z ⟶ Spec (CommRingCat.of R))

Lean source · full declaration

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

theorem

hom_eq_of_map_rigSection_eq

L679 ↗

JacobianVarieties.Picard.Proofs.FaithfulDescent.ExZar.hom_eq_of_map_rigSection_eq

Source context 13 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FaithfulDescent
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 CategoryTheory.Pseudofunctor
open CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section Rigidity
variable {Z : Scheme.{u}} (z : Z ⟶ Spec (CommRingCat.of R))

Lean source · full declaration

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

theorem

exists_iso_map_rigSection_eq

L697 ↗

JacobianVarieties.Picard.Proofs.FaithfulDescent.ExZar.exists_iso_map_rigSection_eq

Source context 13 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FaithfulDescent
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 CategoryTheory.Pseudofunctor
open CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section Rigidity
variable {Z : Scheme.{u}} (z : Z ⟶ Spec (CommRingCat.of R))

Lean source · statement

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

def

fF

L730 ↗

JacobianVarieties.Picard.Proofs.FaithfulDescent.ExZar.fF

Documentation

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

Source context 13 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FaithfulDescent
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 CategoryTheory.Pseudofunctor
open CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section Datum
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type 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

L733 ↗

JacobianVarieties.Picard.Proofs.FaithfulDescent.ExZar.sqF

Documentation

The chosen pullback square of two local curve charts.

Source context 13 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FaithfulDescent
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 CategoryTheory.Pseudofunctor
open CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section Datum
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type 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

L736 ↗

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

Documentation

The chosen threefold pullback data for three local curve charts.

Source context 13 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FaithfulDescent
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 CategoryTheory.Pseudofunctor
open CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section Datum
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type 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

L740 ↗

JacobianVarieties.Picard.Proofs.FaithfulDescent.ExZar.wT

Documentation

The map from a pairwise overlap to the base.

Source context 13 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FaithfulDescent
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 CategoryTheory.Pseudofunctor
open CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section Datum
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type 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

L742 ↗

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

Source context 13 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FaithfulDescent
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 CategoryTheory.Pseudofunctor
open CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section Datum
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type 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

Θ₁

L745 ↗

JacobianVarieties.Picard.Proofs.FaithfulDescent.ExZar.Θ₁

Documentation

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

Source context 13 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FaithfulDescent
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 CategoryTheory.Pseudofunctor
open CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section Datum
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type 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

Θ₂

L750 ↗

JacobianVarieties.Picard.Proofs.FaithfulDescent.ExZar.Θ₂

Documentation

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

Source context 13 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FaithfulDescent
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 CategoryTheory.Pseudofunctor
open CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section Datum
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type 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

L755 ↗

JacobianVarieties.Picard.Proofs.FaithfulDescent.ExZar.exists_homIso

Source context 14 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FaithfulDescent
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 CategoryTheory.Pseudofunctor
open CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section Datum
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type 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

L766 ↗

JacobianVarieties.Picard.Proofs.FaithfulDescent.ExZar.homIso

Documentation

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

Source context 14 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FaithfulDescent
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 CategoryTheory.Pseudofunctor
open CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section Datum
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type 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

L771 ↗

JacobianVarieties.Picard.Proofs.FaithfulDescent.ExZar.map_homIso

Source context 13 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FaithfulDescent
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 CategoryTheory.Pseudofunctor
open CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section Datum
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type 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

L787 ↗

JacobianVarieties.Picard.Proofs.FaithfulDescent.ExZar.half_A

Source context 16 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FaithfulDescent
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 CategoryTheory.Pseudofunctor
open CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section Datum
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type 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

L806 ↗

JacobianVarieties.Picard.Proofs.FaithfulDescent.ExZar.half_B

Source context 16 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FaithfulDescent
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 CategoryTheory.Pseudofunctor
open CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section Datum
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type 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

L814 ↗

JacobianVarieties.Picard.Proofs.FaithfulDescent.ExZar.half_C

Source context 16 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FaithfulDescent
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 CategoryTheory.Pseudofunctor
open CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section Datum
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type 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

L823 ↗

JacobianVarieties.Picard.Proofs.FaithfulDescent.ExZar.half

Source context 16 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FaithfulDescent
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 CategoryTheory.Pseudofunctor
open CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section Datum
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type 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'

L843 ↗

JacobianVarieties.Picard.Proofs.FaithfulDescent.ExZar.half'

Source context 16 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FaithfulDescent
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 CategoryTheory.Pseudofunctor
open CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section Datum
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type 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

L859 ↗

JacobianVarieties.Picard.Proofs.FaithfulDescent.ExZar.half_inv

Source context 16 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FaithfulDescent
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 CategoryTheory.Pseudofunctor
open CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section Datum
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type 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

L883 ↗

JacobianVarieties.Picard.Proofs.FaithfulDescent.ExZar.key

Source context 13 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FaithfulDescent
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 CategoryTheory.Pseudofunctor
open CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section Datum
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type 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 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

δ

L931 ↗

JacobianVarieties.Picard.Proofs.FaithfulDescent.ExZar.δ

Documentation

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

Source context 13 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FaithfulDescent
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 CategoryTheory.Pseudofunctor
open CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section Datum
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type 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 δ (i : ι) : SchemeHomOver (u i) (strMap₁₂ (f i) (f i))

lemma

δ_pr₁

L934 ↗

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

Source context 13 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FaithfulDescent
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 CategoryTheory.Pseudofunctor
open CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section Datum
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type 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₁ (i : ι) : baseChangeSnd c (δ f i) ≫ baseChangeSnd c (pr₁ (f i) (f i)) = 𝟙 _

lemma

δ_pr₂

L941 ↗

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

Source context 13 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FaithfulDescent
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 CategoryTheory.Pseudofunctor
open CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section Datum
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type 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₂ (i : ι) : baseChangeSnd c (δ f i) ≫ baseChangeSnd c (pr₂ (f i) (f i)) = 𝟙 _

lemma

nonempty_rigidification

L948 ↗

JacobianVarieties.Picard.Proofs.FaithfulDescent.ExZar.nonempty_rigidification

Source context 13 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FaithfulDescent
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 CategoryTheory.Pseudofunctor
open CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section Datum
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type 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 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

L957 ↗

JacobianVarieties.Picard.Proofs.FaithfulDescent.ExZar.pullHomIso_self

Source context 13 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FaithfulDescent
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 CategoryTheory.Pseudofunctor
open CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section Datum
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type 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 · full declaration

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

abbrev

ζT3

L982 ↗

JacobianVarieties.Picard.Proofs.FaithfulDescent.ExZar.ζT3

Documentation

The structure map from a triple overlap to the base.

Source context 15 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FaithfulDescent
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 CategoryTheory.Pseudofunctor
open CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section Datum
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type 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 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

χ₁

L986 ↗

JacobianVarieties.Picard.Proofs.FaithfulDescent.ExZar.χ₁

Documentation

The first chart projection from the triple overlap.

Source context 15 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FaithfulDescent
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 CategoryTheory.Pseudofunctor
open CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section Datum
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type 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 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

χ₂

L989 ↗

JacobianVarieties.Picard.Proofs.FaithfulDescent.ExZar.χ₂

Documentation

The second chart projection from the triple overlap.

Source context 15 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FaithfulDescent
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 CategoryTheory.Pseudofunctor
open CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section Datum
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type 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 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

χ₃

L992 ↗

JacobianVarieties.Picard.Proofs.FaithfulDescent.ExZar.χ₃

Documentation

The third chart projection from the triple overlap.

Source context 15 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FaithfulDescent
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 CategoryTheory.Pseudofunctor
open CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section Datum
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type 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 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χ₁

L995 ↗

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

Source context 15 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FaithfulDescent
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 CategoryTheory.Pseudofunctor
open CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section Datum
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type 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 comp
variable (i j k : ι)

Lean source · statement

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

lemma

hχ₂

L996 ↗

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

Source context 15 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FaithfulDescent
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 CategoryTheory.Pseudofunctor
open CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section Datum
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type 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 comp
variable (i j k : ι)

Lean source · statement

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

lemma

hχ₃

L1000 ↗

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

Source context 15 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FaithfulDescent
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 CategoryTheory.Pseudofunctor
open CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section Datum
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type 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 comp
variable (i j k : ι)

Lean source · statement

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

lemma

S₁'

L1009 ↗

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

Source context 15 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FaithfulDescent
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 CategoryTheory.Pseudofunctor
open CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section Datum
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type 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 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₂'

L1011 ↗

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

Source context 15 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FaithfulDescent
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 CategoryTheory.Pseudofunctor
open CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section Datum
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type 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 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₃'

L1013 ↗

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

Source context 15 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FaithfulDescent
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 CategoryTheory.Pseudofunctor
open CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section Datum
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type 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 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

L1017 ↗

JacobianVarieties.Picard.Proofs.FaithfulDescent.ExZar.pullHomIso_comp

Source context 15 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FaithfulDescent
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 CategoryTheory.Pseudofunctor
open CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section Datum
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
  {ι : Type 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 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])

abbrev

πS

L1069 ↗

JacobianVarieties.Picard.Proofs.FaithfulDescent.ExZar.πS

Documentation

The projection from the faithfully flat base change as a morphism over the base.

Source context 14 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FaithfulDescent
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 CategoryTheory.Pseudofunctor
open CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section FF
open AlgebraicGeometry.SmoothProperCurve
variable (R' : Type u) [CommRing R'] [Algebra R R'] [Module.Finite R R']
  [Module.FaithfullyFlat R R']
  {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R))

Lean source · statement

abbrev πS : SchemeHomOver (pullback.snd t (specMap R R') ≫ specMap R R') t

instance

flat_specMap

L1072 ↗

JacobianVarieties.Picard.Proofs.FaithfulDescent.ExZar.flat_specMap

Source context 14 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FaithfulDescent
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 CategoryTheory.Pseudofunctor
open CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section FF
open AlgebraicGeometry.SmoothProperCurve
variable (R' : Type u) [CommRing R'] [Algebra R R'] [Module.Finite R R']
  [Module.FaithfullyFlat R R']
  {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R))

Lean source · statement

instance flat_specMap : Flat (specMap R R')

instance

surjective_specMap

L1075 ↗

JacobianVarieties.Picard.Proofs.FaithfulDescent.ExZar.surjective_specMap

Source context 14 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FaithfulDescent
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 CategoryTheory.Pseudofunctor
open CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section FF
open AlgebraicGeometry.SmoothProperCurve
variable (R' : Type u) [CommRing R'] [Algebra R R'] [Module.Finite R R']
  [Module.FaithfullyFlat R R']
  {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R))

Lean source · statement

instance surjective_specMap : Surjective (specMap R R')

instance

isAffineHom_πS

L1078 ↗

JacobianVarieties.Picard.Proofs.FaithfulDescent.ExZar.isAffineHom_πS

Source context 14 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FaithfulDescent
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 CategoryTheory.Pseudofunctor
open CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section FF
open AlgebraicGeometry.SmoothProperCurve
variable (R' : Type u) [CommRing R'] [Algebra R R'] [Module.Finite R R']
  [Module.FaithfullyFlat R R']
  {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R))

Lean source · statement

instance isAffineHom_πS : IsAffineHom (πS (R := R) R' t).1

instance

flat_πS

L1082 ↗

JacobianVarieties.Picard.Proofs.FaithfulDescent.ExZar.flat_πS

Source context 14 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FaithfulDescent
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 CategoryTheory.Pseudofunctor
open CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section FF
open AlgebraicGeometry.SmoothProperCurve
variable (R' : Type u) [CommRing R'] [Algebra R R'] [Module.Finite R R']
  [Module.FaithfullyFlat R R']
  {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R))

Lean source · statement

instance flat_πS : Flat (πS (R := R) R' t).1

instance

surjective_πS

L1086 ↗

JacobianVarieties.Picard.Proofs.FaithfulDescent.ExZar.surjective_πS

Source context 14 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FaithfulDescent
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 CategoryTheory.Pseudofunctor
open CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section FF
open AlgebraicGeometry.SmoothProperCurve
variable (R' : Type u) [CommRing R'] [Algebra R R'] [Module.Finite R R']
  [Module.FaithfullyFlat R R']
  {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R))

Lean source · statement

instance surjective_πS : Surjective (πS (R := R) R' t).1

instance

isAffineHom_q

L1091 ↗

JacobianVarieties.Picard.Proofs.FaithfulDescent.ExZar.isAffineHom_q

Source context 14 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FaithfulDescent
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 CategoryTheory.Pseudofunctor
open CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section FF
open AlgebraicGeometry.SmoothProperCurve
variable (R' : Type u) [CommRing R'] [Algebra R R'] [Module.Finite R R']
  [Module.FaithfullyFlat R R']
  {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R))

Lean source · statement

instance isAffineHom_q : IsAffineHom (baseChangeSnd c (πS (R := R) R' t))

instance

flat_q

L1094 ↗

JacobianVarieties.Picard.Proofs.FaithfulDescent.ExZar.flat_q

Source context 14 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FaithfulDescent
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 CategoryTheory.Pseudofunctor
open CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section FF
open AlgebraicGeometry.SmoothProperCurve
variable (R' : Type u) [CommRing R'] [Algebra R R'] [Module.Finite R R']
  [Module.FaithfullyFlat R R']
  {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R))

Lean source · statement

instance flat_q : Flat (baseChangeSnd c (πS (R := R) R' t))

instance

surjective_q

L1097 ↗

JacobianVarieties.Picard.Proofs.FaithfulDescent.ExZar.surjective_q

Source context 14 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FaithfulDescent
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 CategoryTheory.Pseudofunctor
open CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section FF
open AlgebraicGeometry.SmoothProperCurve
variable (R' : Type u) [CommRing R'] [Algebra R R'] [Module.Finite R R']
  [Module.FaithfullyFlat R R']
  {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R))

Lean source · statement

instance surjective_q : Surjective (baseChangeSnd c (πS (R := R) R' t))

abbrev

fS

L1102 ↗

JacobianVarieties.Picard.Proofs.FaithfulDescent.ExZar.fS

Documentation

The singleton family containing the faithfully flat base-change projection.

Source context 14 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FaithfulDescent
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 CategoryTheory.Pseudofunctor
open CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section FF
open AlgebraicGeometry.SmoothProperCurve
variable (R' : Type u) [CommRing R'] [Algebra R R'] [Module.Finite R R']
  [Module.FaithfullyFlat R R']
  {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R))

Lean source · statement

abbrev fS : Unit → SchemeHomOver (pullback.snd t (specMap R R') ≫ specMap R R') t

theorem

main_ff

L1106 ↗

JacobianVarieties.Picard.Proofs.FaithfulDescent.ExZar.main_ff

Source context 15 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FaithfulDescent
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 CategoryTheory.Pseudofunctor
open CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section FF
open AlgebraicGeometry.SmoothProperCurve
variable (R' : Type u) [CommRing R'] [Algebra R R'] [Module.Finite R R']
  [Module.FaithfullyFlat R R']
  {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R))
omit [Module.Finite R R'] in

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

L1154 ↗

AlgebraicGeometry.RelPicard.RigidifiedLineBundle.exists_descent_finite_faithfullyFlat_of_bijective_sections

Source context 9 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FaithfulDescent
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
open NeronModelInfra AlgebraicGeometry.RelPicard AlgebraicGeometry.SmoothProperCurve in
open _root_.JacobianVarieties.Picard.Proofs.FaithfulDescent in
with_weak_namespace _root_.AlgebraicGeometry.RelPicard.RigidifiedLineBundle

Lean source · full declaration

theorem exists_descent_finite_faithfullyFlat_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), ⊤)))
    (R' : Type u) [CommRing R'] [Algebra R R'] [Module.Finite R R'] [Module.FaithfullyFlat R R']
    {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R))
    (M' : RigidifiedLineBundle c ε (pullback.snd t (specMap R R') ≫ specMap R R'))
    (hM' : ∀ (Z : Scheme.{u}) (z : Z ⟶ Spec (CommRingCat.of R))
      (p₁ p₂ : SchemeHomOver z (pullback.snd t (specMap R R') ≫ specMap R R')),
      p₁.1 ≫ pullback.fst t (specMap R R') = p₂.1 ≫ pullback.fst t (specMap R R') →
        Nonempty ((M'.pullbackAlong p₁).L ≅ (M'.pullbackAlong p₂).L)) :
    ∃ M : RigidifiedLineBundle c ε t,
      Nonempty ((M.pullbackAlong ⟨pullback.fst t (specMap R R'), pullback.condition⟩).L ≅ M'.L) :=
  ExZar.main_ff c ε R' t hH0 M' hM'

Module documentation

Faithfully flat descent of rigidified line bundles

Declarations