Module

RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections.lean

Nyll.AlgebraicCurves.Geometry.Picard.RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections

73 declarations indexed from sourceView source ↗

Module documentation

Descent of rigidified line-bundle isomorphisms

Compatible local isomorphisms of rigidified line bundles descend over an open cover when the structural map has bijective global sections after base change. Chosen fibre products and section pullback isomorphisms track the transition morphisms used by the descent comparison.

Imports12

Mathlib.Util.WithWeakNamespace
Nyll.AlgebraicCurves.Geometry.Schemes.SchemeHomOver
Nyll.AlgebraicCurves.Geometry.Picard.Functor
Nyll.SchemeTheory.Cohomology.Cech.TwoAffineOpenCover
Nyll.AlgebraicCurves.Geometry.Picard.RigidifiedLineBundle_exists_iso_map_pullback_rigSection_comp_eq
Nyll.AlgebraicCurves.Geometry.Picard.RigidifiedLineBundle_iso_eq_of_map_pullback_rigSection_comp_eq
Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_toDescentData_map_bijective_of_openCover
Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_pullbackComp_pullbackCongr_pasteSquares_app
Mathlib.AlgebraicGeometry.OpenImmersion
Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime
Nyll.SchemeTheory.CategoryTheory.DescentComparison
Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_canonical_pullback_leg_relation

Imported by6

theorem

nonempty_iso_of_compatible_local_isos

L58 ↗

AlgebraicCurves.Geometry.Picard.Proofs.RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections.OpenCoverAssembly.nonempty_iso_of_compatible_local_isos

Documentation

Descend the two arrows of an actual compatible local isomorphism family. The cover remains abstract while the existing comparison and hom-descent owners are combined in their common Mdl fibre.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections
universe u v
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
namespace OpenCoverAssembly
open CategoryTheory.Pseudofunctor
open HomZar

Lean source · statement

theorem nonempty_iso_of_compatible_local_isos
    {Y : Scheme.{u}} {ι : Type v} {V : ι → Scheme.{u}}
    (g : ∀ i, V i ⟶ Y) [∀ i, IsOpenImmersion (g i)]
    (hg : ∀ y : Y, ∃ i, y ∈ Set.range (g i).base)
    (sq : ∀ i j, ChosenPullback (g i) (g j))
    (sq₃ : ∀ i j k, ChosenPullback₃ (sq i j) (sq j k) (sq i k))
    (L₁ L₂ : Y.Modules)
    (e : ∀ i, (Scheme.Modules.pullback (g i)).obj L₁ ≅
      (Scheme.Modules.pullback (g i)).obj L₂)
    (comm : ∀ i j,
      (Mdl.map (sq i j).p₁.op.toLoc).toFunctor.map (e i).hom ≫
          ((DescentData'.fromDescentDataFunctor Mdl sq sq₃).obj
            ((Mdl.toDescentData g).obj L₂)).hom i j =
        ((DescentData'.fromDescentDataFunctor Mdl sq sq₃).obj
          ((Mdl.toDescentData g).obj L₁)).hom i j ≫
            (Mdl.map (sq i j).p₂.op.toLoc).toFunctor.map (e j).hom) :
    Nonempty (L₁ ≅ L₂)

def

τ

L109 ↗

AlgebraicCurves.Geometry.Picard.Proofs.RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections.AlgebraicGeometry.Scheme.Modules.τ

Documentation

Identify iterated pullback with pullback along the specified composite morphism.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections
universe u v
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
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

L113 ↗

AlgebraicCurves.Geometry.Picard.Proofs.RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections.AlgebraicGeometry.Scheme.Modules.τ_hom_app

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections
universe u v
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
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 = (pullbackComp f g).hom.app M ≫ eqToHom (by rw [e]) := by
  subst e
  simp [τ, pullbackCongr]

theorem

τ_inv_app

L118 ↗

AlgebraicCurves.Geometry.Picard.Proofs.RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections.AlgebraicGeometry.Scheme.Modules.τ_inv_app

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections
universe u v
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
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]) ≫ (pullbackComp f g).inv.app M := by
  subst e
  simp [τ, pullbackCongr]

def

sqIso

L124 ↗

AlgebraicCurves.Geometry.Picard.Proofs.RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections.AlgebraicGeometry.Scheme.Modules.sqIso

Documentation

The pullback isomorphism associated with a commutative square of scheme morphisms.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections
universe u v
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
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

sqIso_hom_app

L129 ↗

AlgebraicCurves.Geometry.Picard.Proofs.RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections.AlgebraicGeometry.Scheme.Modules.sqIso_hom_app

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections
universe u v
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X₀ X₁ X₂ X₃ : Scheme.{u}}

Lean source · statement

theorem sqIso_hom_app {W X Y Z : Scheme.{u}} {f : W ⟶ X} {g : X ⟶ Z} {h : W ⟶ Y} {k : Y ⟶ Z}
    (e : f ≫ g = h ≫ k) (M : Z.Modules) :
    (sqIso e).hom.app M = (τ f g (h ≫ k) e).hom.app M ≫ (τ h k (h ≫ k) rfl).inv.app M

theorem

route_comm

L143 ↗

AlgebraicCurves.Geometry.Picard.Proofs.RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections.AlgebraicGeometry.Scheme.Modules.route_comm

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections
universe u v
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X₀ X₁ X₂ X₃ : Scheme.{u}}
section Route
variable {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)
include e G E F in

Lean source · statement

theorem route_comm : s₀ ≫ d = m ≫ s

theorem

route

L146 ↗

AlgebraicCurves.Geometry.Picard.Proofs.RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections.AlgebraicGeometry.Scheme.Modules.route

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections
universe u v
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X₀ X₁ X₂ X₃ : Scheme.{u}}
section Route
variable {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)

Lean source · statement

theorem route (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) ≫
        (τ s₀ d (m ≫ s) (route_comm a b d e s₀ s₁ s r p m G E F)).hom.app M ≫
          (τ m s (m ≫ s) rfl).inv.app M

theorem

head

L171 ↗

AlgebraicCurves.Geometry.Picard.Proofs.RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections.AlgebraicGeometry.Scheme.Modules.head

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections
universe u v
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X₀ X₁ X₂ X₃ : Scheme.{u}}
section Head
variable {X X₀' X₁' X₂' Y Y₀ Y₁ Y₂ : Scheme.{u}}
  (a₁ : X₀' ⟶ X₁') (b₁ : X₁' ⟶ X) (a₂ : X₀' ⟶ X₂') (b₂ : X₂' ⟶ X) (d : X₀' ⟶ X)
  (e₁ : a₁ ≫ b₁ = d) (e₂ : a₂ ≫ b₂ = d)
  (s₀ : Y₀ ⟶ X₀') (s₁ : Y₁ ⟶ X₁') (s₂ : Y₂ ⟶ X₂') (s : Y ⟶ X)
  (r₁ : Y₀ ⟶ Y₁) (p₁ : Y₁ ⟶ Y) (r₂ : Y₀ ⟶ Y₂) (p₂ : Y₂ ⟶ Y) (m : Y₀ ⟶ Y)
  (G₁ : r₁ ≫ p₁ = m) (G₂ : r₂ ≫ p₂ = m)
  (E₁ : s₀ ≫ a₁ = r₁ ≫ s₁) (F₁ : s₁ ≫ b₁ = p₁ ≫ s) (E₂ : s₀ ≫ a₂ = r₂ ≫ s₂) (F₂ : s₂ ≫ b₂ = p₂ ≫ s)

Lean source · statement

theorem head (M : X.Modules) :
    (Scheme.Modules.pullback s₀).map ((τ a₁ b₁ d e₁).hom.app M ≫ (τ a₂ b₂ d e₂).inv.app M) ≫
      (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) =
      (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)

theorem

τ_hom_app_comp_τ_inv_app

L194 ↗

AlgebraicCurves.Geometry.Picard.Proofs.RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections.AlgebraicGeometry.Scheme.Modules.τ_hom_app_comp_τ_inv_app

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections
universe u v
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X₀ X₁ X₂ X₃ : Scheme.{u}}
section HeadRaw
variable {X X₀' X₁' X₂' : Scheme.{u}}
  (a₁ : X₀' ⟶ X₁') (b₁ : X₁' ⟶ X) (a₂ : X₀' ⟶ X₂') (b₂ : X₂' ⟶ X) (d : X₀' ⟶ X)
  (e₁ : a₁ ≫ b₁ = d) (e₂ : a₂ ≫ b₂ = d)

Lean source · statement

theorem τ_hom_app_comp_τ_inv_app (M : X.Modules) :
    (τ a₁ b₁ d e₁).hom.app M ≫ (τ a₂ b₂ d e₂).inv.app M =
      (pullbackComp a₁ b₁).hom.app M ≫ (pullbackCongr e₁).hom.app M ≫ (pullbackCongr
          e₂.symm).hom.app M ≫
        (pullbackComp a₂ b₂).inv.app M

theorem

head'

L208 ↗

AlgebraicCurves.Geometry.Picard.Proofs.RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections.AlgebraicGeometry.Scheme.Modules.head'

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections
universe u v
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X₀ X₁ X₂ X₃ : Scheme.{u}}
section HeadRaw
variable {X X₀' X₁' X₂' : Scheme.{u}}
  (a₁ : X₀' ⟶ X₁') (b₁ : X₁' ⟶ X) (a₂ : X₀' ⟶ X₂') (b₂ : X₂' ⟶ X) (d : X₀' ⟶ X)
  (e₁ : a₁ ≫ b₁ = d) (e₂ : a₂ ≫ b₂ = d)
variable {Y Y₀ Y₁ Y₂ : Scheme.{u}}
  (s₀ : Y₀ ⟶ X₀') (s₁ : Y₁ ⟶ X₁') (s₂ : Y₂ ⟶ X₂') (s : Y ⟶ X)
  (r₁ : Y₀ ⟶ Y₁) (p₁ : Y₁ ⟶ Y) (r₂ : Y₀ ⟶ Y₂) (p₂ : Y₂ ⟶ Y) (m : Y₀ ⟶ Y)
  (G₁ : r₁ ≫ p₁ = m) (G₂ : r₂ ≫ p₂ = m)
  (E₁ : s₀ ≫ a₁ = r₁ ≫ s₁) (F₁ : s₁ ≫ b₁ = p₁ ≫ s) (E₂ : s₀ ≫ a₂ = r₂ ≫ s₂) (F₂ : s₂ ≫ b₂ = p₂ ≫ s)

Lean source · statement

theorem head' (M : X.Modules) :
    (Scheme.Modules.pullback s₀).map ((pullbackComp a₁ b₁).hom.app M ≫ (pullbackCongr e₁).hom.app M
        ≫
        (pullbackCongr e₂.symm).hom.app M ≫ (pullbackComp a₂ b₂).inv.app M) ≫
      (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) =
      (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)

lemma

isPullback_baseChangeSnd_snd

L239 ↗

AlgebraicCurves.Geometry.Picard.Proofs.RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections.AlgebraicGeometry.RelPicard.DescentAux.isPullback_baseChangeSnd_snd

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections
universe u v
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace DescentAux
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
open NeronModelInfra
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

L248 ↗

AlgebraicCurves.Geometry.Picard.Proofs.RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections.AlgebraicGeometry.RelPicard.DescentAux.isPullback_baseChangeSnd

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections
universe u v
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace DescentAux
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
open NeronModelInfra
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₁₂

L271 ↗

AlgebraicCurves.Geometry.Picard.Proofs.RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections.AlgebraicGeometry.RelPicard.DescentAux.strMap₁₂

Documentation

The structural map from the overlap of two schemes over the affine base.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections
universe u v
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace DescentAux
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
open NeronModelInfra
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) :
    pullback ψ₁.1 ψ₂.1 ⟶ Spec (CommRingCat.of R)

def

pr₁

L278 ↗

AlgebraicCurves.Geometry.Picard.Proofs.RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections.AlgebraicGeometry.RelPicard.DescentAux.pr₁

Documentation

The first projection from the overlap, as a morphism over the affine base.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections
universe u v
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace DescentAux
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
open NeronModelInfra
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₂

L284 ↗

AlgebraicCurves.Geometry.Picard.Proofs.RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections.AlgebraicGeometry.RelPicard.DescentAux.pr₂

Documentation

The second projection from the overlap, as a morphism over the affine base.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections
universe u v
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace DescentAux
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
open NeronModelInfra
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

L293 ↗

AlgebraicCurves.Geometry.Picard.Proofs.RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections.AlgebraicGeometry.RelPicard.DescentAux.pr₁_val

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections
universe u v
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace DescentAux
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
open NeronModelInfra
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

L298 ↗

AlgebraicCurves.Geometry.Picard.Proofs.RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections.AlgebraicGeometry.RelPicard.DescentAux.pr₂_val

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections
universe u v
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace DescentAux
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
open NeronModelInfra
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₂

L303 ↗

AlgebraicCurves.Geometry.Picard.Proofs.RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections.AlgebraicGeometry.RelPicard.DescentAux.postComp_pr₁_eq_postComp_pr₂

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections
universe u v
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace DescentAux
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
open NeronModelInfra
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

L310 ↗

AlgebraicCurves.Geometry.Picard.Proofs.RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections.AlgebraicGeometry.RelPicard.DescentAux.chosenPullback

Documentation

The chosen overlap square for the two base changes of the structural morphism.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections
universe u v
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace DescentAux
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
open NeronModelInfra
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 _ _

lemma

chosenPullback_p₁

L324 ↗

AlgebraicCurves.Geometry.Picard.Proofs.RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections.AlgebraicGeometry.RelPicard.DescentAux.chosenPullback_p₁

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections
universe u v
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace DescentAux
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
open NeronModelInfra
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))

Lean source · statement

lemma chosenPullback_p₁ {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 c ψ₁ ψ₂).p₁ = baseChangeSnd c (pr₁ ψ₁ ψ₂)

lemma

chosenPullback_p₂

L329 ↗

AlgebraicCurves.Geometry.Picard.Proofs.RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections.AlgebraicGeometry.RelPicard.DescentAux.chosenPullback_p₂

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections
universe u v
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace DescentAux
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
open NeronModelInfra
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))

Lean source · statement

lemma chosenPullback_p₂ {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 c ψ₁ ψ₂).p₂ = baseChangeSnd c (pr₂ ψ₁ ψ₂)

def

chosenPullback₃

L335 ↗

AlgebraicCurves.Geometry.Picard.Proofs.RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections.AlgebraicGeometry.RelPicard.DescentAux.chosenPullback₃

Documentation

The chosen triple-overlap square for three copies of the same base change.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections
universe u v
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace DescentAux
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
open NeronModelInfra
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))

Lean source · full declaration

def chosenPullback₃ {T T' : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)} {t' : T' ⟶ Spec
    (CommRingCat.of R)}
    (ψ : SchemeHomOver t' t) :
    ChosenPullback₃ (chosenPullback c ψ ψ) (chosenPullback c ψ ψ) (chosenPullback c ψ ψ) where
  chosenPullback := chosenPullback c (pr₂ ψ ψ) (pr₁ ψ ψ)
  p := baseChangeSnd c (postComp (postComp ψ (pr₁ ψ ψ)) (pr₁ (pr₂ ψ ψ) (pr₁ ψ ψ)))
  p₁ := baseChangeSnd c (postComp (pr₁ ψ ψ) (pr₁ (pr₂ ψ ψ) (pr₁ ψ ψ)))
  p₃ := baseChangeSnd c (postComp (pr₂ ψ ψ) (pr₂ (pr₂ ψ ψ) (pr₁ ψ ψ)))
  l :=
    { f := baseChangeSnd c
        ⟨pullback.lift ((pr₁ (pr₂ ψ ψ) (pr₁ ψ ψ)).1 ≫ (pr₁ ψ ψ).1) ((pr₂ (pr₂ ψ ψ) (pr₁ ψ ψ)).1 ≫
            (pr₂ ψ ψ).1)
          (by
            have hT₂ : pullback.fst ψ.1 ψ.1 ≫ ψ.1 = pullback.snd ψ.1 ψ.1 ≫ ψ.1 := pullback.condition
            have hT₃ : pullback.fst (pullback.snd ψ.1 ψ.1) (pullback.fst ψ.1 ψ.1) ≫ pullback.snd ψ.1
                ψ.1 =
                pullback.snd (pullback.snd ψ.1 ψ.1) (pullback.fst ψ.1 ψ.1) ≫ pullback.fst ψ.1 ψ.1 :=
              pullback.condition
            simp only [pr₁_val, pr₂_val, Category.assoc]
            rw [hT₂, ← Category.assoc, hT₃, Category.assoc, hT₂]),
         by
          simp only [pr₁_val, pr₂_val]
          rw [← Category.assoc, pullback.lift_fst, Category.assoc]
          rfl⟩
      f_p₁ := by
        change baseChangeSnd c _ ≫ baseChangeSnd c (pr₁ ψ ψ) = _
        erw [baseChangeSnd_comp]; congr 1; exact Subtype.ext (pullback.lift_fst _ _ _)
      f_p₂ := by
        change baseChangeSnd c _ ≫ baseChangeSnd c (pr₂ ψ ψ) = _
        erw [baseChangeSnd_comp]; congr 1; exact Subtype.ext (pullback.lift_snd _ _ _)
      f_p := by
        change baseChangeSnd c _ ≫ baseChangeSnd c (postComp ψ (pr₁ ψ ψ)) = _
        erw [baseChangeSnd_comp]; congr 1
        exact Subtype.ext (by
          change pullback.lift _ _ _ ≫ pullback.fst _ _ ≫ ψ.1 = (pullback.fst _ _ ≫ pullback.fst _
              _) ≫ ψ.1
          rw [pullback.lift_fst_assoc, Category.assoc]
          rfl) }
  hp₁ := by
    change baseChangeSnd c (pr₁ (pr₂ ψ ψ) (pr₁ ψ ψ)) ≫ baseChangeSnd c (pr₁ ψ ψ) = _
    erw [baseChangeSnd_comp]
  hp₃ := by
    change baseChangeSnd c (pr₂ (pr₂ ψ ψ) (pr₁ ψ ψ)) ≫ baseChangeSnd c (pr₂ ψ ψ) = _
    erw [baseChangeSnd_comp]

structure

RigData

L408 ↗

AlgebraicCurves.Geometry.Picard.Proofs.RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections.AlgebraicGeometry.RelPicard.DescentAux.RigData

Documentation

An invertible module on the base-changed scheme with a specified rigidification along the section.

Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections
universe u v
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace DescentAux
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.AlgebraicGeometry.Scheme.Modules
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
with_weak_namespace _root_.AlgebraicCurves.Geometry.Picard.Proofs
with_weak_namespace RigidifiedLineBundle_exists_iso_map_pullback_rigSection_comp_eq
with_weak_namespace AlgebraicGeometry.Scheme
open Modules (unitModule) in
with_weak_namespace _root_.AlgebraicCurves.Geometry.Picard.Proofs
with_weak_namespace
  RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections
with_weak_namespace AlgebraicGeometry.RelPicard.DescentAux

Lean source · full declaration

structure RigData {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) where
  /-- The module on the base-changed scheme. -/
  L : (Limits.pullback c t).Modules
  /-- The module is invertible. -/
  isInvertible : Scheme.Modules.IsInvertible L
  /-- The rigidification of the module along the base-changed section. -/
  α : (Scheme.Modules.pullback (rigSection c t ε)).obj L ≅ unitModule T

def

Compat

L421 ↗

AlgebraicCurves.Geometry.Picard.Proofs.RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections.AlgebraicGeometry.RelPicard.DescentAux.RigData.Compat

Documentation

A module morphism is compatible when it preserves the specified rigidifications.

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections
universe u v
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace DescentAux
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.AlgebraicGeometry.Scheme.Modules
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
namespace RigData
variable {c ε} {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}

Lean source · statement

def Compat (A B : RigData c ε t) (φ : A.L ⟶ B.L) : Prop

lemma

id

L424 ↗

AlgebraicCurves.Geometry.Picard.Proofs.RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections.AlgebraicGeometry.RelPicard.DescentAux.RigData.Compat.id

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections
universe u v
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace DescentAux
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.AlgebraicGeometry.Scheme.Modules
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
namespace RigData
variable {c ε} {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}

Lean source · statement

lemma Compat.id (A : RigData c ε t) : Compat A A (𝟙 A.L)

lemma

comp

L428 ↗

AlgebraicCurves.Geometry.Picard.Proofs.RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections.AlgebraicGeometry.RelPicard.DescentAux.RigData.Compat.comp

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections
universe u v
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace DescentAux
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.AlgebraicGeometry.Scheme.Modules
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
namespace RigData
variable {c ε} {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}

Lean source · statement

lemma Compat.comp {A B D : RigData c ε t} {φ : A.L ⟶ B.L} {ψ : B.L ⟶ D.L} (hφ : Compat A B φ)
    (hψ : Compat B D ψ) : Compat A D (φ ≫ ψ)

lemma

compat_iff_mapIso

L433 ↗

AlgebraicCurves.Geometry.Picard.Proofs.RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections.AlgebraicGeometry.RelPicard.DescentAux.RigData.compat_iff_mapIso

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections
universe u v
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace DescentAux
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.AlgebraicGeometry.Scheme.Modules
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
namespace RigData
variable {c ε} {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}

Lean source · statement

lemma compat_iff_mapIso (A B : RigData c ε t) (φ : A.L ≅ B.L) :
    Compat A B φ.hom ↔ (Scheme.Modules.pullback (rigSection c t ε)).mapIso φ ≪≫ B.α = A.α

lemma

inv

L442 ↗

AlgebraicCurves.Geometry.Picard.Proofs.RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections.AlgebraicGeometry.RelPicard.DescentAux.RigData.Compat.inv

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections
universe u v
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace DescentAux
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.AlgebraicGeometry.Scheme.Modules
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
namespace RigData
variable {c ε} {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}

Lean source · statement

lemma Compat.inv {A B : RigData c ε t} {φ : A.L ≅ B.L} (h : Compat A B φ.hom) : Compat B A φ.inv

def

ofIso

L449 ↗

AlgebraicCurves.Geometry.Picard.Proofs.RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections.AlgebraicGeometry.RelPicard.DescentAux.RigData.ofIso

Documentation

Transport the module and its rigidification along an isomorphism of modules.

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections
universe u v
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace DescentAux
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.AlgebraicGeometry.Scheme.Modules
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
namespace RigData
variable {c ε} {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}

Lean source · full declaration

def ofIso (A : RigData c ε t) (L' : (Limits.pullback c t).Modules) (e : L' ≅ A.L)
    (hL' : Scheme.Modules.IsInvertible L') : RigData c ε t where
  L := L'
  isInvertible := hL'
  α := (Scheme.Modules.pullback (rigSection c t ε)).mapIso e ≪≫ A.α

lemma

ofIso_compat_iff

L455 ↗

AlgebraicCurves.Geometry.Picard.Proofs.RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections.AlgebraicGeometry.RelPicard.DescentAux.RigData.ofIso_compat_iff

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections
universe u v
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace DescentAux
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.AlgebraicGeometry.Scheme.Modules
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
namespace RigData
variable {c ε} {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}

Lean source · statement

lemma ofIso_compat_iff {A B : RigData c ε t} {LA LB : (Limits.pullback c t).Modules} (eA : LA ≅ A.L)
    (eB : LB ≅ B.L)
    (hA : Scheme.Modules.IsInvertible LA) (hB : Scheme.Modules.IsInvertible LB) (φ : LA ⟶ LB) :
    Compat (A.ofIso LA eA hA) (B.ofIso LB eB hB) φ ↔ Compat A B (eA.inv ≫ φ ≫ eB.hom)

def

rigNatIso

L470 ↗

AlgebraicCurves.Geometry.Picard.Proofs.RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections.AlgebraicGeometry.RelPicard.DescentAux.RigData.rigNatIso

Documentation

Identify section pullback after base change with base change after section pullback.

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections
universe u v
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace DescentAux
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.AlgebraicGeometry.Scheme.Modules
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
namespace RigData
variable {c ε} {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}

Lean source · statement

def rigNatIso {T' : Scheme.{u}} {t' : T' ⟶ Spec (CommRingCat.of R)} (ψ : SchemeHomOver t' t) :
    Scheme.Modules.pullback (baseChangeSnd c ψ) ⋙ Scheme.Modules.pullback (rigSection c t' ε) ≅
      Scheme.Modules.pullback (rigSection c t ε) ⋙ Scheme.Modules.pullback ψ.1

def

pb

L478 ↗

AlgebraicCurves.Geometry.Picard.Proofs.RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections.AlgebraicGeometry.RelPicard.DescentAux.RigData.pb

Documentation

Pull back the module and its rigidification along a morphism over the base.

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections
universe u v
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace DescentAux
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.AlgebraicGeometry.Scheme.Modules
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
namespace RigData
variable {c ε} {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}

Lean source · full declaration

def pb (A : RigData c ε t) {T' : Scheme.{u}} {t' : T' ⟶ Spec (CommRingCat.of R)} (ψ : SchemeHomOver
    t' t) :
    RigData c ε t' where
  L := (Scheme.Modules.pullback (baseChangeSnd c ψ)).obj A.L
  isInvertible := A.isInvertible.pullback _
  α := (rigNatIso ψ).app A.L ≪≫ (Scheme.Modules.pullback ψ.1).mapIso A.α ≪≫
      Scheme.Modules.pullbackUnitIso ψ.1

lemma

pb_L

L486 ↗

AlgebraicCurves.Geometry.Picard.Proofs.RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections.AlgebraicGeometry.RelPicard.DescentAux.RigData.pb_L

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections
universe u v
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace DescentAux
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.AlgebraicGeometry.Scheme.Modules
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
namespace RigData
variable {c ε} {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}

Lean source · statement

lemma pb_L (A : RigData c ε t) {T' : Scheme.{u}} {t' : T' ⟶ Spec (CommRingCat.of R)}
    (ψ : SchemeHomOver t' t) : (A.pb ψ).L = (Scheme.Modules.pullback (baseChangeSnd c ψ)).obj A.L

lemma

pb

L490 ↗

AlgebraicCurves.Geometry.Picard.Proofs.RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections.AlgebraicGeometry.RelPicard.DescentAux.RigData.Compat.pb

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections
universe u v
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace DescentAux
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.AlgebraicGeometry.Scheme.Modules
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
namespace RigData
variable {c ε} {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}

Lean source · statement

lemma Compat.pb {A B : RigData c ε t} {φ : A.L ⟶ B.L} (h : Compat A B φ) {T' : Scheme.{u}}
    {t' : T' ⟶ Spec (CommRingCat.of R)} (ψ : SchemeHomOver t' t) :
    Compat (A.pb ψ) (B.pb ψ) ((Scheme.Modules.pullback (baseChangeSnd c ψ)).map φ)

def

ofRLB

L549 ↗

AlgebraicCurves.Geometry.Picard.Proofs.RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections.AlgebraicGeometry.RelPicard.DescentAux.RigData.ofRLB

Documentation

View a rigidified line bundle with a chosen rigidification as explicit rigidification data.

Source context 26 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections
universe u v
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace DescentAux
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
open NeronModelInfra CategoryTheory.Pseudofunctor
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
namespace RigData
variable {c ε} {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
with_weak_namespace _root_.AlgebraicCurves.Geometry.Picard.Proofs
with_weak_namespace RigidifiedLineBundle_exists_iso_map_pullback_rigSection_comp_eq
with_weak_namespace AlgebraicGeometry.Scheme
open Modules (unitModule) in
with_weak_namespace _root_.AlgebraicCurves.Geometry.Picard.Proofs
with_weak_namespace
  RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections
with_weak_namespace AlgebraicGeometry.RelPicard.DescentAux.RigData

Lean source · statement

def ofRLB (M : RigidifiedLineBundle c ε t)
    (α : (Scheme.Modules.pullback (rigSection c t ε)).obj M.L ≅ unitModule T) :
    RigData c ε t

def

toRLB

L554 ↗

AlgebraicCurves.Geometry.Picard.Proofs.RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections.AlgebraicGeometry.RelPicard.DescentAux.RigData.toRLB

Documentation

Forget the chosen rigidification and retain the underlying rigidified line bundle.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections
universe u v
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace DescentAux
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
open NeronModelInfra CategoryTheory.Pseudofunctor
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
namespace RigData
variable {c ε} {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}

Lean source · statement

def toRLB (A : RigData c ε t) : RigidifiedLineBundle c ε t

lemma

exists_compat_iso

L556 ↗

AlgebraicCurves.Geometry.Picard.Proofs.RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections.AlgebraicGeometry.RelPicard.DescentAux.RigData.exists_compat_iso

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections
universe u v
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace DescentAux
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
open NeronModelInfra CategoryTheory.Pseudofunctor
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
namespace RigData
variable {c ε} {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}

Lean source · statement

lemma exists_compat_iso (A B : RigData c ε t) (h : Nonempty (A.L ≅ B.L)) :
    ∃ φ : A.L ≅ B.L, Compat A B φ.hom

lemma

compat_iso_unique

L563 ↗

AlgebraicCurves.Geometry.Picard.Proofs.RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections.AlgebraicGeometry.RelPicard.DescentAux.RigData.compat_iso_unique

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections
universe u v
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace DescentAux
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
open NeronModelInfra CategoryTheory.Pseudofunctor
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
namespace RigData
variable {c ε} {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}

Lean source · full declaration

lemma compat_iso_unique
    (hH0 : ∀ (A : Type u) [CommRing A] [Algebra R A],
      letI := Scheme.TwoAffineOpenCover.algebraOfHom
        (Limits.pullback.snd c (Scheme.TwoAffineOpenCover.specMap R A)) ⊤
      Function.Bijective (algebraMap A Γ(Limits.pullback c (Scheme.TwoAffineOpenCover.specMap R A),
          ⊤)))
    (A B : RigData c ε t) (φ ψ : A.L ≅ B.L) (hφ : Compat A B φ.hom) (hψ : Compat A B ψ.hom) : φ = ψ
        :=
  AlgebraicGeometry.RelPicard.RigidifiedLineBundle.iso_eq_of_map_pullback_rigSection_comp_eq R c ε
      hH0 t
    A.toRLB B.toRLB A.α B.α φ ψ ((compat_iff_mapIso A B φ).mp hφ) ((compat_iff_mapIso A B ψ).mp hψ)

lemma

compat_hom_unique

L575 ↗

AlgebraicCurves.Geometry.Picard.Proofs.RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections.AlgebraicGeometry.RelPicard.DescentAux.RigData.compat_hom_unique

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections
universe u v
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace DescentAux
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
open NeronModelInfra CategoryTheory.Pseudofunctor
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
namespace RigData
variable {c ε} {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}

Lean source · full declaration

lemma compat_hom_unique
    (hH0 : ∀ (A : Type u) [CommRing A] [Algebra R A],
      letI := Scheme.TwoAffineOpenCover.algebraOfHom
        (Limits.pullback.snd c (Scheme.TwoAffineOpenCover.specMap R A)) ⊤
      Function.Bijective (algebraMap A Γ(Limits.pullback c (Scheme.TwoAffineOpenCover.specMap R A),
          ⊤)))
    (A B : RigData c ε t) (φ ψ : A.L ⟶ B.L) [IsIso φ] [IsIso ψ] (hφ : Compat A B φ) (hψ : Compat A B
        ψ) :
    φ = ψ :=
  congrArg Iso.hom (compat_iso_unique hH0 A B (asIso φ) (asIso ψ) hφ hψ)

lemma

chosenPullback_p

L588 ↗

AlgebraicCurves.Geometry.Picard.Proofs.RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections.AlgebraicGeometry.RelPicard.DescentAux.chosenPullback_p

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections
universe u v
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace DescentAux
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
open NeronModelInfra CategoryTheory.Pseudofunctor
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)

Lean source · statement

lemma chosenPullback_p {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 c ψ₁ ψ₂).p = baseChangeSnd c (postComp ψ₁ (pr₁ ψ₁ ψ₂))

def

chosenPullback₃'

L594 ↗

AlgebraicCurves.Geometry.Picard.Proofs.RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections.AlgebraicGeometry.RelPicard.DescentAux.chosenPullback₃'

Documentation

The chosen triple-overlap square for three base changes of the structural morphism.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections
universe u v
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace DescentAux
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
open NeronModelInfra CategoryTheory.Pseudofunctor
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)

Lean source · full declaration

def chosenPullback₃' {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) :
    ChosenPullback₃ (chosenPullback c ψ₁ ψ₂) (chosenPullback c ψ₂ ψ₃) (chosenPullback c ψ₁ ψ₃) where
  chosenPullback := chosenPullback c (pr₂ ψ₁ ψ₂) (pr₁ ψ₂ ψ₃)
  p := baseChangeSnd c (postComp (postComp ψ₁ (pr₁ ψ₁ ψ₂)) (pr₁ (pr₂ ψ₁ ψ₂) (pr₁ ψ₂ ψ₃)))
  p₁ := baseChangeSnd c (postComp (pr₁ ψ₁ ψ₂) (pr₁ (pr₂ ψ₁ ψ₂) (pr₁ ψ₂ ψ₃)))
  p₃ := baseChangeSnd c (postComp (pr₂ ψ₂ ψ₃) (pr₂ (pr₂ ψ₁ ψ₂) (pr₁ ψ₂ ψ₃)))
  l :=
    { f := baseChangeSnd c
        ⟨pullback.lift ((pr₁ (pr₂ ψ₁ ψ₂) (pr₁ ψ₂ ψ₃)).1 ≫ (pr₁ ψ₁ ψ₂).1)
            ((pr₂ (pr₂ ψ₁ ψ₂) (pr₁ ψ₂ ψ₃)).1 ≫ (pr₂ ψ₂ ψ₃).1)
          (by
            have h₁₂ : pullback.fst ψ₁.1 ψ₂.1 ≫ ψ₁.1 = pullback.snd ψ₁.1 ψ₂.1 ≫ ψ₂.1 :=
                pullback.condition
            have h₂₃ : pullback.fst ψ₂.1 ψ₃.1 ≫ ψ₂.1 = pullback.snd ψ₂.1 ψ₃.1 ≫ ψ₃.1 :=
                pullback.condition
            have h' : pullback.fst (pullback.snd ψ₁.1 ψ₂.1) (pullback.fst ψ₂.1 ψ₃.1) ≫ pullback.snd
                ψ₁.1 ψ₂.1 =
                pullback.snd (pullback.snd ψ₁.1 ψ₂.1) (pullback.fst ψ₂.1 ψ₃.1) ≫ pullback.fst ψ₂.1
                    ψ₃.1 :=
              pullback.condition
            simp only [pr₁_val, pr₂_val, Category.assoc]
            rw [h₁₂, ← Category.assoc, h', Category.assoc, h₂₃]),
         by
          simp only [pr₁_val, pr₂_val]
          rw [← Category.assoc, pullback.lift_fst, Category.assoc]
          rfl⟩
      f_p₁ := by
        change baseChangeSnd c _ ≫ baseChangeSnd c (pr₁ ψ₁ ψ₃) = _
        erw [baseChangeSnd_comp]; congr 1; exact Subtype.ext (pullback.lift_fst _ _ _)
      f_p₂ := by
        change baseChangeSnd c _ ≫ baseChangeSnd c (pr₂ ψ₁ ψ₃) = _
        erw [baseChangeSnd_comp]; congr 1; exact Subtype.ext (pullback.lift_snd _ _ _)
      f_p := by
        change baseChangeSnd c _ ≫ baseChangeSnd c (postComp ψ₁ (pr₁ ψ₁ ψ₃)) = _
        erw [baseChangeSnd_comp]; congr 1
        exact Subtype.ext (by
          change pullback.lift _ _ _ ≫ pullback.fst _ _ ≫ ψ₁.1 = (pullback.fst _ _ ≫ pullback.fst _
              _) ≫ ψ₁.1
          rw [pullback.lift_fst_assoc, Category.assoc]
          rfl) }
  hp₁ := by
    change baseChangeSnd c (pr₁ (pr₂ ψ₁ ψ₂) (pr₁ ψ₂ ψ₃)) ≫ baseChangeSnd c (pr₁ ψ₁ ψ₂) = _
    erw [baseChangeSnd_comp]
  hp₃ := by
    change baseChangeSnd c (pr₂ (pr₂ ψ₁ ψ₂) (pr₁ ψ₂ ψ₃)) ≫ baseChangeSnd c (pr₂ ψ₂ ψ₃) = _
    erw [baseChangeSnd_comp]

lemma

exists_mem_range_baseChangeSnd

L644 ↗

AlgebraicCurves.Geometry.Picard.Proofs.RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections.AlgebraicGeometry.RelPicard.DescentAux.exists_mem_range_baseChangeSnd

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections
universe u v
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace DescentAux
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
open NeronModelInfra CategoryTheory.Pseudofunctor
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)

Lean source · statement

lemma exists_mem_range_baseChangeSnd {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
    {ι : Type u} {U : ι → Scheme.{u}} {uS : ∀ i, U i ⟶ Spec (CommRingCat.of R)} (f : ∀ i,
        SchemeHomOver (uS i) t)
    (hf : ∀ x : T, ∃ i, x ∈ Set.range (f i).1.base) (y : ↥(Limits.pullback c t)) :
    ∃ i, y ∈ Set.range (baseChangeSnd c (f i)).base

abbrev

MOD

L673 ↗

AlgebraicCurves.Geometry.Picard.Proofs.RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections.AlgebraicGeometry.RelPicard.DescentAux.MOD

Documentation

The existing pseudofunctor of scheme module sheaves used for descent.

Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections
universe u v
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace DescentAux
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
open NeronModelInfra CategoryTheory.Pseudofunctor
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section MODsec
with_weak_namespace _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
with_weak_namespace Scheme_Modules_toDescentData_map_bijective_of_openCover
with_weak_namespace AlgebraicGeometry.Scheme.Modules
open HomZar in
with_weak_namespace _root_.AlgebraicCurves.Geometry.Picard.Proofs
with_weak_namespace
  RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections
with_weak_namespace AlgebraicGeometry.RelPicard.DescentAux

Lean source · statement

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

theorem

modMap_toFunctor

L676 ↗

AlgebraicCurves.Geometry.Picard.Proofs.RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections.AlgebraicGeometry.RelPicard.DescentAux.modMap_toFunctor

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections
universe u v
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace DescentAux
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
open NeronModelInfra CategoryTheory.Pseudofunctor
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section MODsec

Lean source · statement

theorem modMap_toFunctor {X Y : Scheme.{u}} (g : X ⟶ Y) :
    ((MOD).map g.op.toLoc).toFunctor = Scheme.Modules.pullback g

theorem

modMapComp'_eq_mapComp_app

L679 ↗

AlgebraicCurves.Geometry.Picard.Proofs.RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections.AlgebraicGeometry.RelPicard.DescentAux.modMapComp'_eq_mapComp_app

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections
universe u v
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace DescentAux
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
open NeronModelInfra CategoryTheory.Pseudofunctor
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section MODsec

Lean source · statement

theorem modMapComp'_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

modMapComp'_hom_app

L685 ↗

AlgebraicCurves.Geometry.Picard.Proofs.RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections.AlgebraicGeometry.RelPicard.DescentAux.modMapComp'_hom_app

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections
universe u v
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace DescentAux
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
open NeronModelInfra CategoryTheory.Pseudofunctor
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section MODsec

Lean source · full declaration

theorem modMapComp'_hom_app {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z) (L : Z.Modules) (fg : X ⟶
    Z)
    (h : f ≫ g = fg) :
    ((MOD).mapComp' g.op.toLoc f.op.toLoc fg.op.toLoc (by rw [← h]; rfl)).hom.toNatTrans.app L =
      (Scheme.Modules.pullbackCongr h.symm).hom.app L ≫ (Scheme.Modules.pullbackComp f g).inv.app L
          := by
  subst h
  simp only [Scheme.Modules.pullbackCongr, eqToIso_refl, Iso.refl_hom, NatTrans.id_app,
      Category.id_comp]
  exact modMapComp'_eq_mapComp_app g.op.toLoc f.op.toLoc L

theorem

modMapComp'_inv_app

L696 ↗

AlgebraicCurves.Geometry.Picard.Proofs.RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections.AlgebraicGeometry.RelPicard.DescentAux.modMapComp'_inv_app

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections
universe u v
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace DescentAux
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
open NeronModelInfra CategoryTheory.Pseudofunctor
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section MODsec

Lean source · full declaration

theorem modMapComp'_inv_app {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z) (L : Z.Modules) (fg : X ⟶
    Z)
    (h : f ≫ g = fg) :
    ((MOD).mapComp' g.op.toLoc f.op.toLoc fg.op.toLoc (by rw [← h]; rfl)).inv.toNatTrans.app L =
      (Scheme.Modules.pullbackComp f g).hom.app L ≫ (Scheme.Modules.pullbackCongr h).hom.app L := by
  subst h
  simp only [Scheme.Modules.pullbackCongr, eqToIso_refl, Iso.refl_hom, NatTrans.id_app,
      Category.comp_id]
  have h2 : ((MOD).mapComp' g.op.toLoc f.op.toLoc (g.op.toLoc ≫ f.op.toLoc) rfl).inv.toNatTrans.app
      L =
      ((MOD).mapComp g.op.toLoc f.op.toLoc).inv.toNatTrans.app L := by
    rw [Pseudofunctor.mapComp'_eq_mapComp]
  exact h2

def

transHom₂

L711 ↗

AlgebraicCurves.Geometry.Picard.Proofs.RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections.AlgebraicGeometry.RelPicard.DescentAux.transHom₂

Documentation

The canonical transition morphism on a chosen overlap of two pullbacks.

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections
universe u v
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace DescentAux
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
open NeronModelInfra CategoryTheory.Pseudofunctor
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section MODsec

Lean source · statement

def transHom₂ {X₁ X₂ S : Scheme.{u}} (q₁ : X₁ ⟶ S) (q₂ : X₂ ⟶ S) (cp : ChosenPullback q₁ q₂) (L :
    S.Modules) :
    ((MOD).map cp.p₁.op.toLoc).toFunctor.obj (((MOD).map q₁.op.toLoc).toFunctor.obj L) ⟶
      ((MOD).map cp.p₂.op.toLoc).toFunctor.obj (((MOD).map q₂.op.toLoc).toFunctor.obj L)

theorem

transHom₂_eq_fourfold

L718 ↗

AlgebraicCurves.Geometry.Picard.Proofs.RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections.AlgebraicGeometry.RelPicard.DescentAux.transHom₂_eq_fourfold

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections
universe u v
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace DescentAux
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
open NeronModelInfra CategoryTheory.Pseudofunctor
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section MODsec

Lean source · statement

theorem transHom₂_eq_fourfold {X₁ X₂ S : Scheme.{u}}
    (q₁ : X₁ ⟶ S) (q₂ : X₂ ⟶ S) (cp : ChosenPullback q₁ q₂) (L : S.Modules) :
    transHom₂ q₁ q₂ cp L =
      (Scheme.Modules.pullbackComp cp.p₁ q₁).hom.app L ≫
      (Scheme.Modules.pullbackCongr cp.hp₁).hom.app L ≫
      (Scheme.Modules.pullbackCongr cp.hp₂.symm).hom.app L ≫
      (Scheme.Modules.pullbackComp cp.p₂ q₂).inv.app L

instance

isIso_transHom₂

L728 ↗

AlgebraicCurves.Geometry.Picard.Proofs.RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections.AlgebraicGeometry.RelPicard.DescentAux.isIso_transHom₂

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections
universe u v
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace DescentAux
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
open NeronModelInfra CategoryTheory.Pseudofunctor
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section MODsec

Lean source · statement

instance isIso_transHom₂ {X₁ X₂ S : Scheme.{u}} (q₁ : X₁ ⟶ S) (q₂ : X₂ ⟶ S) (cp :
    ChosenPullback q₁ q₂)
    (L : S.Modules) : IsIso (transHom₂ q₁ q₂ cp L)

theorem

fromDescentData_toDescentData_obj

L735 ↗

AlgebraicCurves.Geometry.Picard.Proofs.RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections.AlgebraicGeometry.RelPicard.DescentAux.fromDescentData_toDescentData_obj

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections
universe u v
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace DescentAux
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
open NeronModelInfra CategoryTheory.Pseudofunctor
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section MODsec

Lean source · statement

theorem fromDescentData_toDescentData_obj {S : Scheme.{u}} {ι : Type v} {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))
    (L : S.Modules) (i : ι) :
    ((DescentData'.fromDescentDataFunctor (MOD) sq sq₃).obj (((MOD).toDescentData g).obj L)).obj i =
      ((MOD).map (g i).op.toLoc).toFunctor.obj L

theorem

fromDescentData_toDescentData_hom

L743 ↗

AlgebraicCurves.Geometry.Picard.Proofs.RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections.AlgebraicGeometry.RelPicard.DescentAux.fromDescentData_toDescentData_hom

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections
universe u v
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace DescentAux
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
open NeronModelInfra CategoryTheory.Pseudofunctor
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section MODsec

Lean source · statement

theorem fromDescentData_toDescentData_hom {S : Scheme.{u}} {ι : Type v} {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))
    (L : S.Modules) (i j : ι) :
    ((DescentData'.fromDescentDataFunctor (MOD) sq sq₃).obj (((MOD).toDescentData g).obj L)).hom i j
        =
      transHom₂ (g i) (g j) (sq i j) L

lemma

bc_pr₁_comp

L765 ↗

AlgebraicCurves.Geometry.Picard.Proofs.RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections.AlgebraicGeometry.RelPicard.DescentAux.bc_pr₁_comp

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections
universe u v
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace DescentAux
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
open NeronModelInfra CategoryTheory.Pseudofunctor
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section bridge
variable {c ε}
variable {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)

Lean source · statement

lemma bc_pr₁_comp : baseChangeSnd c (pr₁ ψ₁ ψ₂) ≫ baseChangeSnd c ψ₁ = baseChangeSnd c (postComp ψ₁
    (pr₁ ψ₁ ψ₂))

lemma

bc_pr₂_comp

L769 ↗

AlgebraicCurves.Geometry.Picard.Proofs.RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections.AlgebraicGeometry.RelPicard.DescentAux.bc_pr₂_comp

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections
universe u v
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace DescentAux
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
open NeronModelInfra CategoryTheory.Pseudofunctor
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section bridge
variable {c ε}
variable {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)

Lean source · statement

lemma bc_pr₂_comp : baseChangeSnd c (pr₂ ψ₁ ψ₂) ≫ baseChangeSnd c ψ₂ = baseChangeSnd c (postComp ψ₁
    (pr₁ ψ₁ ψ₂))

lemma

pr₁_comp_val

L773 ↗

AlgebraicCurves.Geometry.Picard.Proofs.RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections.AlgebraicGeometry.RelPicard.DescentAux.pr₁_comp_val

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections
universe u v
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace DescentAux
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
open NeronModelInfra CategoryTheory.Pseudofunctor
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section bridge
variable {c ε}
variable {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)

Lean source · statement

lemma pr₁_comp_val : (pr₁ ψ₁ ψ₂).1 ≫ ψ₁.1 = (postComp ψ₁ (pr₁ ψ₁ ψ₂)).1

lemma

pr₂_comp_val

L775 ↗

AlgebraicCurves.Geometry.Picard.Proofs.RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections.AlgebraicGeometry.RelPicard.DescentAux.pr₂_comp_val

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections
universe u v
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace DescentAux
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
open NeronModelInfra CategoryTheory.Pseudofunctor
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section bridge
variable {c ε}
variable {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)

Lean source · statement

lemma pr₂_comp_val : (pr₂ ψ₁ ψ₂).1 ≫ ψ₂.1 = (postComp ψ₁ (pr₁ ψ₁ ψ₂)).1

def

rawHom

L779 ↗

AlgebraicCurves.Geometry.Picard.Proofs.RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections.AlgebraicGeometry.RelPicard.DescentAux.rawHom

Documentation

The transition morphism on the chosen overlap of two base changes.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections
universe u v
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace DescentAux
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
open NeronModelInfra CategoryTheory.Pseudofunctor
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section bridge
variable {c ε}
variable {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)
variable (c) in

Lean source · statement

def rawHom (L : (Limits.pullback c t).Modules) :
    (Scheme.Modules.pullback (baseChangeSnd c (pr₁ ψ₁ ψ₂))).obj ((Scheme.Modules.pullback
        (baseChangeSnd c ψ₁)).obj L) ⟶
      (Scheme.Modules.pullback (baseChangeSnd c (pr₂ ψ₁ ψ₂))).obj ((Scheme.Modules.pullback
          (baseChangeSnd c ψ₂)).obj L)

theorem

transHom₂_eq_rawHom

L786 ↗

AlgebraicCurves.Geometry.Picard.Proofs.RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections.AlgebraicGeometry.RelPicard.DescentAux.transHom₂_eq_rawHom

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections
universe u v
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace DescentAux
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
open NeronModelInfra CategoryTheory.Pseudofunctor
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section bridge
variable {c ε}
variable {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)
variable (c) in

Lean source · statement

theorem transHom₂_eq_rawHom (L : (Limits.pullback c t).Modules) :
    transHom₂ (baseChangeSnd c ψ₁) (baseChangeSnd c ψ₂) (chosenPullback c ψ₁ ψ₂) L = rawHom c ψ₁ ψ₂
        L

instance

isIso_rawHom

L790 ↗

AlgebraicCurves.Geometry.Picard.Proofs.RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections.AlgebraicGeometry.RelPicard.DescentAux.isIso_rawHom

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections
universe u v
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace DescentAux
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
open NeronModelInfra CategoryTheory.Pseudofunctor
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section bridge
variable {c ε}
variable {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)
variable (c) in

Lean source · statement

instance isIso_rawHom (L : (Limits.pullback c t).Modules) : IsIso (rawHom c ψ₁ ψ₂ L)

def

legIso

L795 ↗

AlgebraicCurves.Geometry.Picard.Proofs.RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections.AlgebraicGeometry.RelPicard.DescentAux.legIso

Documentation

Compare the two routes for restricting a module to the section over an overlap.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections
universe u v
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace DescentAux
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
open NeronModelInfra CategoryTheory.Pseudofunctor
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section bridge
variable {c ε}
variable {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)
variable (c) in

Lean source · statement

def legIso {T' : Scheme.{u}} {t' : T' ⟶ Spec (CommRingCat.of R)} (ψ : SchemeHomOver t' t)
    (ρ : SchemeHomOver (strMap₁₂ ψ₁ ψ₂) t') (G : ρ.1 ≫ ψ.1 = (postComp ψ₁ (pr₁ ψ₁ ψ₂)).1) (L :
        (Limits.pullback c t).Modules) :
    (Scheme.Modules.pullback (rigSection c (strMap₁₂ ψ₁ ψ₂) ε)).obj
        ((Scheme.Modules.pullback (baseChangeSnd c ρ)).obj ((Scheme.Modules.pullback (baseChangeSnd
            c ψ)).obj L)) ≅
      (Scheme.Modules.pullback (postComp ψ₁ (pr₁ ψ₁ ψ₂)).1).obj ((Scheme.Modules.pullback
          (rigSection c t ε)).obj L)

lemma

map_map_eq_legIso_conj

L809 ↗

AlgebraicCurves.Geometry.Picard.Proofs.RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections.AlgebraicGeometry.RelPicard.DescentAux.map_map_eq_legIso_conj

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections
universe u v
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace DescentAux
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
open NeronModelInfra CategoryTheory.Pseudofunctor
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section bridge
variable {c ε}
variable {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)
variable (c) in

Lean source · statement

lemma map_map_eq_legIso_conj {T' : Scheme.{u}} {t' : T' ⟶ Spec (CommRingCat.of R)} (ψ :
    SchemeHomOver t' t)
    (ρ : SchemeHomOver (strMap₁₂ ψ₁ ψ₂) t') (G : ρ.1 ≫ ψ.1 = (postComp ψ₁ (pr₁ ψ₁ ψ₂)).1)
    (A₁ A₂ : RigData c ε t)
    (φ : (Scheme.Modules.pullback (baseChangeSnd c ψ)).obj A₁.L ⟶ (Scheme.Modules.pullback
        (baseChangeSnd c ψ)).obj A₂.L)
    (hφ : RigData.Compat (A₁.pb ψ) (A₂.pb ψ) φ) :
    (Scheme.Modules.pullback (rigSection c (strMap₁₂ ψ₁ ψ₂) ε)).map
        ((Scheme.Modules.pullback (baseChangeSnd c ρ)).map φ) =
      (legIso ψ₁ ψ₂ ψ ρ G A₁.L).hom ≫ (Scheme.Modules.pullback (postComp ψ₁ (pr₁ ψ₁ ψ₂)).1).map
          (A₁.α.hom ≫ A₂.α.inv) ≫
        (legIso ψ₁ ψ₂ ψ ρ G A₂.L).inv

lemma

map_rawHom_comp_legIso

L873 ↗

AlgebraicCurves.Geometry.Picard.Proofs.RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections.AlgebraicGeometry.RelPicard.DescentAux.map_rawHom_comp_legIso

Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections
universe u v
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace DescentAux
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
open NeronModelInfra CategoryTheory.Pseudofunctor
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section bridge
variable {c ε}
variable {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)
variable (c) in
open _root_.AlgebraicCurves.Geometry.Sheaves.DescentComparison
  (canonical_pullback_native_leg_relation) in

Lean source · statement

lemma map_rawHom_comp_legIso (L : (Limits.pullback c t).Modules) :
    (Scheme.Modules.pullback (rigSection c (strMap₁₂ ψ₁ ψ₂) ε)).map (rawHom c ψ₁ ψ₂ L) ≫
        (legIso ψ₁ ψ₂ ψ₂ (pr₂ ψ₁ ψ₂) (pr₂_comp_val ψ₁ ψ₂) L).hom =
      (legIso ψ₁ ψ₂ ψ₁ (pr₁ ψ₁ ψ₂) (pr₁_comp_val ψ₁ ψ₂) L).hom

theorem

map_comp_rawHom_eq

L911 ↗

AlgebraicCurves.Geometry.Picard.Proofs.RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections.AlgebraicGeometry.RelPicard.DescentAux.map_comp_rawHom_eq

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections
universe u v
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace DescentAux
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
open NeronModelInfra CategoryTheory.Pseudofunctor
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section bridge
variable {c ε}
variable {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)
variable (c) in

Lean source · full declaration

theorem map_comp_rawHom_eq
    (hH0 : ∀ (A : Type u) [CommRing A] [Algebra R A],
      letI := Scheme.TwoAffineOpenCover.algebraOfHom
        (Limits.pullback.snd c (Scheme.TwoAffineOpenCover.specMap R A)) ⊤
      Function.Bijective (algebraMap A Γ(Limits.pullback c (Scheme.TwoAffineOpenCover.specMap R A),
          ⊤)))
    (A₁ A₂ : RigData c ε t)
    (φ₁ : (Scheme.Modules.pullback (baseChangeSnd c ψ₁)).obj A₁.L ⟶ (Scheme.Modules.pullback
        (baseChangeSnd c ψ₁)).obj A₂.L)
    (φ₂ : (Scheme.Modules.pullback (baseChangeSnd c ψ₂)).obj A₁.L ⟶ (Scheme.Modules.pullback
        (baseChangeSnd c ψ₂)).obj A₂.L)
    [IsIso φ₁] [IsIso φ₂]
    (h₁ : RigData.Compat (A₁.pb ψ₁) (A₂.pb ψ₁) φ₁) (h₂ : RigData.Compat (A₁.pb ψ₂) (A₂.pb ψ₂) φ₂) :
    (Scheme.Modules.pullback (baseChangeSnd c (pr₁ ψ₁ ψ₂))).map φ₁ ≫ rawHom c ψ₁ ψ₂ A₂.L =
      rawHom c ψ₁ ψ₂ A₁.L ≫ (Scheme.Modules.pullback (baseChangeSnd c (pr₂ ψ₁ ψ₂))).map φ₂ := by
  have key : (Scheme.Modules.pullback (rigSection c (strMap₁₂ ψ₁ ψ₂) ε)).map
      ((Scheme.Modules.pullback (baseChangeSnd c (pr₁ ψ₁ ψ₂))).map φ₁ ≫ rawHom c ψ₁ ψ₂ A₂.L) =
      (Scheme.Modules.pullback (rigSection c (strMap₁₂ ψ₁ ψ₂) ε)).map
      (rawHom c ψ₁ ψ₂ A₁.L ≫ (Scheme.Modules.pullback (baseChangeSnd c (pr₂ ψ₁ ψ₂))).map φ₂) := by
    have H1 := map_rawHom_comp_legIso (c := c) (ε := ε) ψ₁ ψ₂ A₁.L
    have H2 := map_rawHom_comp_legIso (c := c) (ε := ε) ψ₁ ψ₂ A₂.L
    have H2' : (legIso ψ₁ ψ₂ ψ₁ (pr₁ ψ₁ ψ₂) (pr₁_comp_val ψ₁ ψ₂) A₂.L).inv ≫
        (Scheme.Modules.pullback (rigSection c (strMap₁₂ ψ₁ ψ₂) ε)).map (rawHom c ψ₁ ψ₂ A₂.L) =
        (legIso ψ₁ ψ₂ ψ₂ (pr₂ ψ₁ ψ₂) (pr₂_comp_val ψ₁ ψ₂) A₂.L).inv :=
      (Iso.inv_comp_eq _).mpr ((Iso.eq_comp_inv _).mpr H2)
    rw [Functor.map_comp, Functor.map_comp,
      map_map_eq_legIso_conj ψ₁ ψ₂ ψ₁ (pr₁ ψ₁ ψ₂) (pr₁_comp_val ψ₁ ψ₂) A₁ A₂ φ₁ h₁,
      map_map_eq_legIso_conj ψ₁ ψ₂ ψ₂ (pr₂ ψ₁ ψ₂) (pr₂_comp_val ψ₁ ψ₂) A₁ A₂ φ₂ h₂]
    simp only [Category.assoc]
    rw [H2', ← H1, Category.assoc]
  let Φ : ((Scheme.Modules.pullback (baseChangeSnd c (pr₁ ψ₁ ψ₂))).obj ((Scheme.Modules.pullback
      (baseChangeSnd c ψ₁)).obj A₁.L) ≅
          (Scheme.Modules.pullback (baseChangeSnd c (pr₂ ψ₁ ψ₂))).obj ((Scheme.Modules.pullback
              (baseChangeSnd c ψ₂)).obj A₂.L)) :=
    (Scheme.Modules.pullback (baseChangeSnd c (pr₁ ψ₁ ψ₂))).mapIso (asIso φ₁) ≪≫ asIso (rawHom c ψ₁
        ψ₂ A₂.L)
  let Ψ : ((Scheme.Modules.pullback (baseChangeSnd c (pr₁ ψ₁ ψ₂))).obj ((Scheme.Modules.pullback
      (baseChangeSnd c ψ₁)).obj A₁.L) ≅
          (Scheme.Modules.pullback (baseChangeSnd c (pr₂ ψ₁ ψ₂))).obj ((Scheme.Modules.pullback
              (baseChangeSnd c ψ₂)).obj A₂.L)) :=
    asIso (rawHom c ψ₁ ψ₂ A₁.L) ≪≫ (Scheme.Modules.pullback (baseChangeSnd c (pr₂ ψ₁ ψ₂))).mapIso
        (asIso φ₂)
  have hΨ : (Scheme.Modules.pullback (rigSection c (strMap₁₂ ψ₁ ψ₂) ε)).mapIso Ψ ≪≫ ((A₂.pb ψ₂).pb
      (pr₂ ψ₁ ψ₂)).α =
      (Scheme.Modules.pullback (rigSection c (strMap₁₂ ψ₁ ψ₂) ε)).mapIso Φ ≪≫ ((A₂.pb ψ₂).pb (pr₂ ψ₁
          ψ₂)).α :=
    Iso.ext (by
      first
        | simpa only [Φ, Ψ, Iso.trans_hom, Functor.mapIso_hom, asIso_hom, Functor.map_comp,
            Category.assoc] using
            congrArg (· ≫ ((A₂.pb ψ₂).pb (pr₂ ψ₁ ψ₂)).α.hom) key.symm
        | (change (Scheme.Modules.pullback _).map
              (rawHom c ψ₁ ψ₂ A₁.L ≫ (Scheme.Modules.pullback _).map φ₂) ≫ _ =
              (Scheme.Modules.pullback _).map
                ((Scheme.Modules.pullback _).map φ₁ ≫ rawHom c ψ₁ ψ₂ A₂.L) ≫ _
           rw [key]))
  have hΦΨ : Φ = Ψ :=
    AlgebraicGeometry.RelPicard.RigidifiedLineBundle.iso_eq_of_map_pullback_rigSection_comp_eq R c ε
        hH0
      (strMap₁₂ ψ₁ ψ₂) ((A₁.pb ψ₁).pb (pr₁ ψ₁ ψ₂)).toRLB ((A₂.pb ψ₂).pb (pr₂ ψ₁ ψ₂)).toRLB
      ((Scheme.Modules.pullback (rigSection c (strMap₁₂ ψ₁ ψ₂) ε)).mapIso Φ ≪≫ ((A₂.pb ψ₂).pb (pr₂
          ψ₁ ψ₂)).α)
      ((A₂.pb ψ₂).pb (pr₂ ψ₁ ψ₂)).α Φ Ψ rfl hΨ
  exact congrArg Iso.hom hΦΨ

instance

isOpenImmersion_baseChangeSnd

L983 ↗

AlgebraicCurves.Geometry.Picard.Proofs.RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections.AlgebraicGeometry.RelPicard.DescentAux.isOpenImmersion_baseChangeSnd

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections
universe u v
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace DescentAux
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
open NeronModelInfra CategoryTheory.Pseudofunctor
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section asm_bZ
variable {ι : Type u} {U : ι → Scheme.{u}} (uS : ∀ i, U i ⟶ Spec (CommRingCat.of R))
  {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) (f : ∀ i, SchemeHomOver (uS i) t)

Lean source · statement

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

abbrev

sqZ

L988 ↗

AlgebraicCurves.Geometry.Picard.Proofs.RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections.AlgebraicGeometry.RelPicard.DescentAux.sqZ

Documentation

The chosen pairwise overlap squares for the base-changed open-cover family.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections
universe u v
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace DescentAux
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
open NeronModelInfra CategoryTheory.Pseudofunctor
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section asm_bZ
variable {ι : Type u} {U : ι → Scheme.{u}} (uS : ∀ i, U i ⟶ Spec (CommRingCat.of R))
  {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) (f : ∀ i, SchemeHomOver (uS i) t)

Lean source · statement

abbrev sqZ : ∀ (i j : ι), ChosenPullback (baseChangeSnd c (f i)) (baseChangeSnd c (f j))

abbrev

sq₃Z

L991 ↗

AlgebraicCurves.Geometry.Picard.Proofs.RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections.AlgebraicGeometry.RelPicard.DescentAux.sq₃Z

Documentation

The chosen triple-overlap squares for the base-changed open-cover family.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections
universe u v
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace DescentAux
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
open NeronModelInfra CategoryTheory.Pseudofunctor
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section asm_bZ
variable {ι : Type u} {U : ι → Scheme.{u}} (uS : ∀ i, U i ⟶ Spec (CommRingCat.of R))
  {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) (f : ∀ i, SchemeHomOver (uS i) t)

Lean source · statement

abbrev sq₃Z : ∀ (i j k : ι), ChosenPullback₃ (sqZ c uS t f i j) (sqZ c uS t f j k) (sqZ c uS t f i
    k)

lemma

toDDZ_hom

L995 ↗

AlgebraicCurves.Geometry.Picard.Proofs.RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections.AlgebraicGeometry.RelPicard.DescentAux.toDDZ_hom

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections
universe u v
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace DescentAux
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
open NeronModelInfra CategoryTheory.Pseudofunctor
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section asm_bZ
variable {ι : Type u} {U : ι → Scheme.{u}} (uS : ∀ i, U i ⟶ Spec (CommRingCat.of R))
  {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) (f : ∀ i, SchemeHomOver (uS i) t)

Lean source · full declaration

lemma toDDZ_hom (L : (Limits.pullback c t).Modules) (i j : ι) :
    ((DescentData'.fromDescentDataFunctor (MOD)
          (sqZ c uS t f) (sq₃Z c uS t f)).obj
        (((MOD).toDescentData (fun i => baseChangeSnd c (f i))).obj L)).hom i j =
      rawHom c (f i) (f j) L :=
  (fromDescentData_toDescentData_hom (fun i => baseChangeSnd c (f i))
    (sqZ c uS t f) (sq₃Z c uS t f) L i j).trans
    (transHom₂_eq_rawHom (f i) (f j) L)

lemma

toDDZ_obj

L1004 ↗

AlgebraicCurves.Geometry.Picard.Proofs.RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections.AlgebraicGeometry.RelPicard.DescentAux.toDDZ_obj

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections
universe u v
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace DescentAux
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
open NeronModelInfra CategoryTheory.Pseudofunctor
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section asm_bZ
variable {ι : Type u} {U : ι → Scheme.{u}} (uS : ∀ i, U i ⟶ Spec (CommRingCat.of R))
  {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) (f : ∀ i, SchemeHomOver (uS i) t)

Lean source · full declaration

lemma toDDZ_obj (L : (Limits.pullback c t).Modules) (i : ι) :
    ((DescentData'.fromDescentDataFunctor (MOD)
          (sqZ c uS t f) (sq₃Z c uS t f)).obj
        (((MOD).toDescentData (fun i => baseChangeSnd c (f i))).obj L)).obj i = ((MOD).map
            (baseChangeSnd c (f i)).op.toLoc).toFunctor.obj L :=
  fromDescentData_toDescentData_obj (fun i => baseChangeSnd c (f i))
    (sqZ c uS t f) (sq₃Z c uS t f) L i

theorem

nonempty_iso_of_compatible_local_isos_mod

L1014 ↗

AlgebraicCurves.Geometry.Picard.Proofs.RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections.AlgebraicGeometry.RelPicard.DescentAux.nonempty_iso_of_compatible_local_isos_mod

Documentation

Convert the existing MOD overlap proposition while the cover is abstract.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections
universe u v
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace DescentAux
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
open NeronModelInfra CategoryTheory.Pseudofunctor
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section asm_bZ
variable {ι : Type u} {U : ι → Scheme.{u}} (uS : ∀ i, U i ⟶ Spec (CommRingCat.of R))
  {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) (f : ∀ i, SchemeHomOver (uS i) t)

Lean source · statement

theorem nonempty_iso_of_compatible_local_isos_mod
    {Y : Scheme.{u}} {κ : Type v} {V : κ → Scheme.{u}}
    (g : ∀ i, V i ⟶ Y) [∀ i, IsOpenImmersion (g i)]
    (hg : ∀ y : Y, ∃ i, y ∈ Set.range (g i).base)
    (sq : ∀ i j, ChosenPullback (g i) (g j))
    (sq₃ : ∀ i j k, ChosenPullback₃ (sq i j) (sq j k) (sq i k))
    (L₁ L₂ : Y.Modules)
    (e : ∀ i, (Scheme.Modules.pullback (g i)).obj L₁ ≅
      (Scheme.Modules.pullback (g i)).obj L₂)
    (comm : ∀ i j,
      (MOD.map (sq i j).p₁.op.toLoc).toFunctor.map (e i).hom ≫
          ((DescentData'.fromDescentDataFunctor MOD sq sq₃).obj
            ((MOD.toDescentData g).obj L₂)).hom i j =
        ((DescentData'.fromDescentDataFunctor MOD sq sq₃).obj
          ((MOD.toDescentData g).obj L₁)).hom i j ≫
            (MOD.map (sq i j).p₂.op.toLoc).toFunctor.map (e j).hom) :
    Nonempty (L₁ ≅ L₂)

lemma

isoMk_commZ

L1034 ↗

AlgebraicCurves.Geometry.Picard.Proofs.RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections.AlgebraicGeometry.RelPicard.DescentAux.isoMk_commZ

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections
universe u v
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace DescentAux
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
open NeronModelInfra CategoryTheory.Pseudofunctor
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section asm_bZ
variable {ι : Type u} {U : ι → Scheme.{u}} (uS : ∀ i, U i ⟶ Spec (CommRingCat.of R))
  {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) (f : ∀ i, SchemeHomOver (uS i) t)

Lean source · full declaration

lemma isoMk_commZ
    (hH0 : ∀ (A : Type u) [CommRing A] [Algebra R A],
      letI := Scheme.TwoAffineOpenCover.algebraOfHom
        (Limits.pullback.snd c (Scheme.TwoAffineOpenCover.specMap R A)) ⊤
      Function.Bijective (algebraMap A Γ(Limits.pullback c (Scheme.TwoAffineOpenCover.specMap R A),
          ⊤)))
    (A₁ A₂ : RigData c ε t)
    (ι' : ∀ i, (Scheme.Modules.pullback (baseChangeSnd c (f i))).obj A₁.L ≅
      (Scheme.Modules.pullback (baseChangeSnd c (f i))).obj A₂.L)
    (hι' : ∀ i, RigData.Compat (A₁.pb (f i)) (A₂.pb (f i)) (ι' i).hom) (i j : ι) :
    ((MOD).map (sqZ c uS t f i j).p₁.op.toLoc).toFunctor.map (ι' i).hom ≫
        ((DescentData'.fromDescentDataFunctor (MOD)
          (sqZ c uS t f) (sq₃Z c uS t f)).obj
        (((MOD).toDescentData (fun i => baseChangeSnd c (f i))).obj A₂.L)).hom i j =
      ((DescentData'.fromDescentDataFunctor (MOD)
          (sqZ c uS t f) (sq₃Z c uS t f)).obj
        (((MOD).toDescentData (fun i => baseChangeSnd c (f i))).obj A₁.L)).hom i j ≫
        ((MOD).map (sqZ c uS t f i j).p₂.op.toLoc).toFunctor.map (ι' j).hom := by
  let e : ∀ k,
      (Scheme.Modules.pullback (baseChangeSnd c (f k))).obj A₁.L ≅
        (Scheme.Modules.pullback (baseChangeSnd c (f k))).obj A₂.L := fun k => ι' k
  have hi : RigData.Compat (A₁.pb (f i)) (A₂.pb (f i)) (e i).hom := hι' i
  have hj : RigData.Compat (A₁.pb (f j)) (A₂.pb (f j)) (e j).hom := hι' j
  have hcomm := map_comp_rawHom_eq (f i) (f j) hH0 A₁ A₂ (e i).hom (e j).hom hi hj
  rw [toDDZ_hom, toDDZ_hom]
  dsimp only [sqZ, toDDZ_obj, modMap_toFunctor, chosenPullback_p₁, chosenPullback_p₂]
  exact hcomm

theorem

asm_bZ

L1062 ↗

AlgebraicCurves.Geometry.Picard.Proofs.RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections.AlgebraicGeometry.RelPicard.DescentAux.asm_bZ

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections
universe u v
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace DescentAux
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
open NeronModelInfra CategoryTheory.Pseudofunctor
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section asm_bZ
variable {ι : Type u} {U : ι → Scheme.{u}} (uS : ∀ i, U i ⟶ Spec (CommRingCat.of R))
  {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) (f : ∀ i, SchemeHomOver (uS i) t)

Lean source · full declaration

theorem asm_bZ
    (hH0 : ∀ (A : Type u) [CommRing A] [Algebra R A],
      letI := Scheme.TwoAffineOpenCover.algebraOfHom
        (Limits.pullback.snd c (Scheme.TwoAffineOpenCover.specMap R A)) ⊤
      Function.Bijective (algebraMap A Γ(Limits.pullback c (Scheme.TwoAffineOpenCover.specMap R A),
          ⊤)))
    [∀ i, IsOpenImmersion (f i).1] (hf : ∀ x : T, ∃ i, x ∈ Set.range (f i).1.base)
    (M₁ M₂ : RigidifiedLineBundle c ε t)
    (h : ∀ i, Nonempty ((M₁.pullbackAlong (f i)).L ≅ (M₂.pullbackAlong (f i)).L)) :
    Nonempty (M₁.L ≅ M₂.L) := by
  let A₁ : RigData c ε t := RigData.ofRLB M₁ M₁.rigidified.some
  let A₂ : RigData c ε t := RigData.ofRLB M₂ M₂.rigidified.some
  have hι : ∀ i, ∃ φ : (A₁.pb (f i)).L ≅ (A₂.pb (f i)).L,
      RigData.Compat (A₁.pb (f i)) (A₂.pb (f i)) φ.hom :=
    fun i => RigData.exists_compat_iso (A₁.pb (f i)) (A₂.pb (f i)) (h i)
  choose ι' hι' using hι
  let e : ∀ i,
      (Scheme.Modules.pullback (baseChangeSnd c (f i))).obj A₁.L ≅
        (Scheme.Modules.pullback (baseChangeSnd c (f i))).obj A₂.L := fun i => ι' i
  have he : ∀ i, RigData.Compat (A₁.pb (f i)) (A₂.pb (f i)) (e i).hom := hι'
  change Nonempty (A₁.L ≅ A₂.L)
  exact nonempty_iso_of_compatible_local_isos_mod
    (Y := Limits.pullback c t) (κ := ι) (V := fun i => Limits.pullback c (uS i))
    (fun i => baseChangeSnd c (f i)) (exists_mem_range_baseChangeSnd c f hf)
    (sqZ c uS t f) (sq₃Z c uS t f) A₁.L A₂.L
    e (isoMk_commZ c ε uS t f hH0 A₁ A₂ e he)

theorem

nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections

L1103 ↗

AlgebraicGeometry.RelPicard.RigidifiedLineBundle.nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections
universe u v
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
with_weak_namespace AlgebraicGeometry.RelPicard
open DescentAux in
with_weak_namespace _root_.AlgebraicGeometry.RelPicard.RigidifiedLineBundle

Lean source · full declaration

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

Module documentation

Descent of rigidified line-bundle isomorphisms

Declarations