Module

Scheme_Modules_toDescentData_essSurj_of_openCover.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_toDescentData_essSurj_of_openCover

104 declarations indexed from sourceView source ↗

Module documentation

Effectivity of descent data for sheaves of scheme modules on an open cover. Compatible local sections form the glued sheaf and recover the prescribed transitions.

Imports52

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_toDescentData_map_bijective_of_openCover
Mathlib.Algebra.Category.Grp.Basic
Mathlib.Algebra.Category.Grp.Limits
Mathlib.Algebra.Category.ModuleCat.Presheaf
Mathlib.Algebra.Category.ModuleCat.Sheaf
Mathlib.Algebra.Group.Hom.Defs
Mathlib.Algebra.Module.Pi
Mathlib.Algebra.Module.Submodule.Defs
Mathlib.Algebra.Notation.Pi.Defs
Mathlib.AlgebraicGeometry.Modules.Presheaf
Mathlib.AlgebraicGeometry.Modules.Sheaf
Mathlib.AlgebraicGeometry.OpenImmersion
Mathlib.AlgebraicGeometry.Restrict
Mathlib.AlgebraicGeometry.Scheme
Mathlib.CategoryTheory.Adjunction.Basic
Mathlib.CategoryTheory.Adjunction.Mates
Mathlib.CategoryTheory.Adjunction.Unique
Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
Mathlib.CategoryTheory.Bicategory.Functor.Cat
Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
Mathlib.CategoryTheory.Bicategory.LocallyDiscrete
Mathlib.CategoryTheory.Category.Basic
Mathlib.CategoryTheory.Category.Cat
Mathlib.CategoryTheory.Category.Preorder
Mathlib.CategoryTheory.ConcreteCategory.Basic
Mathlib.CategoryTheory.ConcreteCategory.Forget
Mathlib.CategoryTheory.EqToHom
Mathlib.CategoryTheory.Equivalence
Mathlib.CategoryTheory.EssentialImage
Mathlib.CategoryTheory.Functor.Basic
Mathlib.CategoryTheory.Functor.Category
Mathlib.CategoryTheory.Functor.ReflectsIso.Basic
Mathlib.CategoryTheory.Iso
Mathlib.CategoryTheory.NatIso
Mathlib.CategoryTheory.NatTrans
Mathlib.CategoryTheory.Opposites
Mathlib.CategoryTheory.Sites.Descent.DescentData
Mathlib.CategoryTheory.Sites.Descent.IsPrestack
Mathlib.CategoryTheory.Sites.Sieves.Basic
Mathlib.CategoryTheory.Sites.Sieves.Presieve
Mathlib.CategoryTheory.Sites.Spaces
Mathlib.CategoryTheory.Types.Basic
Mathlib.Data.Set.Image
Mathlib.Order.BoundedOrder.Lattice
Mathlib.Order.Lattice
Mathlib.Tactic.CategoryTheory.Reassoc
Mathlib.Tactic.Choose
Mathlib.Topology.Category.TopCat.Opens
Mathlib.Topology.Sets.Opens
Mathlib.Topology.Sheaves.Presheaf
Mathlib.Topology.Sheaves.Sheaf
Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing

Imported by2

theorem

pullHom_comp'

L100 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.pullHom_comp'

Source context 20 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace CategoryTheory
open _root_.CategoryTheory
namespace Pseudofunctor
open _root_.CategoryTheory.Pseudofunctor
namespace LocallyDiscreteOpToCat
open _root_.CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
open _root_.CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
open _root_.CategoryTheory.Pseudofunctor
open _root_.CategoryTheory
variable {C : Type*} [Category C] {F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat}

Lean source · statement

theorem pullHom_comp' ⦃X₁ X₂ X₃ : C⦄ ⦃M₁ : F.obj (.mk (op X₁))⦄ ⦃M₂ : F.obj (.mk (op X₂))⦄ ⦃M₃ :
    F.obj (.mk (op X₃))⦄
    ⦃Y : C⦄ ⦃f₁ : Y ⟶ X₁⦄ ⦃f₂ : Y ⟶ X₂⦄ ⦃f₃ : Y ⟶ X₃⦄
    (a : (F.map f₁.op.toLoc).toFunctor.obj M₁ ⟶ (F.map f₂.op.toLoc).toFunctor.obj M₂)
    (b : (F.map f₂.op.toLoc).toFunctor.obj M₂ ⟶ (F.map f₃.op.toLoc).toFunctor.obj M₃)
    ⦃Y' : C⦄ (g : Y' ⟶ Y) (gf₁ : Y' ⟶ X₁) (gf₂ : Y' ⟶ X₂) (gf₃ : Y' ⟶ X₃)
    (h₁ : g ≫ f₁ = gf₁) (h₂ : g ≫ f₂ = gf₂) (h₃ : g ≫ f₃ = gf₃) :
    pullHom (a ≫ b) g gf₁ gf₃ h₁ h₃ = pullHom a g gf₁ gf₂ h₁ h₂ ≫ pullHom b g gf₂ gf₃ h₂ h₃

theorem

map_map_eq_pullHom

L110 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.map_map_eq_pullHom

Source context 20 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace CategoryTheory
open _root_.CategoryTheory
namespace Pseudofunctor
open _root_.CategoryTheory.Pseudofunctor
namespace LocallyDiscreteOpToCat
open _root_.CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
open _root_.CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
open _root_.CategoryTheory.Pseudofunctor
open _root_.CategoryTheory
variable {C : Type*} [Category C] {F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat}

Lean source · statement

theorem map_map_eq_pullHom ⦃X Y : C⦄ (f : Y ⟶ X) ⦃M N : F.obj (.mk (op X))⦄ (ψ : M ⟶ N) ⦃Y' : C⦄
    (g : Y' ⟶ Y) (gf : Y' ⟶ X) (hgf : g ≫ f = gf) :
    (F.map gf.op.toLoc).toFunctor.map ψ = pullHom ((F.map f.op.toLoc).toFunctor.map ψ) g gf gf hgf
      hgf

theorem

comm_of_pullHom

L124 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.comm_of_pullHom

Source context 20 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace CategoryTheory
open _root_.CategoryTheory
namespace Pseudofunctor
open _root_.CategoryTheory.Pseudofunctor
namespace LocallyDiscreteOpToCat
open _root_.CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
open _root_.CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
open _root_.CategoryTheory.Pseudofunctor
open _root_.CategoryTheory
variable {C : Type*} [Category C] {F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat}

Lean source · statement

theorem comm_of_pullHom {ι : Type*} {S : C} {X : ι → C}
    {f : ∀ i, X i ⟶ S} (D₁ D₂ : F.DescentData f) {i j : ι}
    (a : D₁.obj i ⟶ D₂.obj i) (b : D₁.obj j ⟶ D₂.obj j)
    {Z₀ Z : C} (q₀ : Z₀ ⟶ S) (g₁ : Z₀ ⟶ X i) (g₂ : Z₀ ⟶ X j)
    (w₁ : g₁ ≫ f i = q₀) (w₂ : g₂ ≫ f j = q₀)
    (comm : (F.map g₁.op.toLoc).toFunctor.map a ≫ D₂.hom q₀ g₁ g₂ w₁ w₂ =
      D₁.hom q₀ g₁ g₂ w₁ w₂ ≫ (F.map g₂.op.toLoc).toFunctor.map b)
    (q : Z ⟶ S) (f₁ : Z ⟶ X i) (f₂ : Z ⟶ X j)
    (h₁ : f₁ ≫ f i = q) (h₂ : f₂ ≫ f j = q)
    (φ : Z ⟶ Z₀) (hφ : φ ≫ q₀ = q) (hφ₁ : φ ≫ g₁ = f₁) (hφ₂ : φ ≫ g₂ = f₂) :
    (F.map f₁.op.toLoc).toFunctor.map a ≫ D₂.hom q f₁ f₂ h₁ h₂ =
      D₁.hom q f₁ f₂ h₁ h₂ ≫ (F.map f₂.op.toLoc).toFunctor.map b

def

canonical_iso

L142 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.canonical_iso

Source context 20 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace CategoryTheory
open _root_.CategoryTheory
namespace Pseudofunctor
open _root_.CategoryTheory.Pseudofunctor
namespace LocallyDiscreteOpToCat
open _root_.CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
open _root_.CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat
open _root_.CategoryTheory.Pseudofunctor
open _root_.CategoryTheory
variable {C : Type*} [Category C] {F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat}

Lean source · statement

def canonical_iso {ι : Type*} {S : C} {X : ι → C}
    (f : ∀ i, X i ⟶ S) (M : F.obj (.mk (op S))) (D : F.DescentData f)
    (e : ∀ i, (F.map (f i).op.toLoc).toFunctor.obj M ≅ D.obj i)
    (comm : ∀ ⦃Z : C⦄ (q : Z ⟶ S) ⦃i j : ι⦄ (f₁ : Z ⟶ X i) (f₂ : Z ⟶ X j)
      (h₁ : f₁ ≫ f i = q) (h₂ : f₂ ≫ f j = q),
      (F.map f₁.op.toLoc).toFunctor.map (e i).hom ≫ D.hom q f₁ f₂ h₁ h₂ =
        ((F.toDescentData f).obj M).hom q f₁ f₂ h₁ h₂ ≫
          (F.map f₂.op.toLoc).toFunctor.map (e j).hom) : (F.toDescentData f).obj M ≅ D

abbrev

MOD

L166 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.AlgebraicGeometry.Scheme.Modules.ObjGlue.MOD

Documentation

The canonical pseudofunctor of scheme modules used by the descent data.

Source context 20 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ObjGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry

Lean source · statement

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

theorem

keyMC

L169 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.AlgebraicGeometry.Scheme.Modules.ObjGlue.keyMC

Source context 20 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ObjGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry

Lean source · statement

theorem keyMC {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

mapComp'_hom_app_eq

L174 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.AlgebraicGeometry.Scheme.Modules.ObjGlue.mapComp'_hom_app_eq

Source context 20 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ObjGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry

Lean source · full declaration

theorem mapComp'_hom_app_eq {X X' Z : Scheme.{u}} (f : X ⟶ X') (g : X' ⟶ 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 keyMC g.op.toLoc f.op.toLoc L

theorem

crux_MOD

L185 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.AlgebraicGeometry.Scheme.Modules.ObjGlue.crux_MOD

Source context 20 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ObjGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry

Lean source · statement

theorem crux_MOD {Z' Z X₁ X₂ : Scheme.{u}} (e : Z' ⟶ Z) (f₁ : Z ⟶ X₁) (f₂ : Z ⟶ X₂)
    (gf₁ : Z' ⟶ X₁) (gf₂ : Z' ⟶ X₂) [IsOpenImmersion e] [IsOpenImmersion f₁] [IsOpenImmersion f₂]
    [IsOpenImmersion gf₁] [IsOpenImmersion gf₂] (h₁ : e ≫ f₁ = gf₁) (h₂ : e ≫ f₂ = gf₂)
    (M₁ : X₁.Modules) (M₂ : X₂.Modules)
    (φ : (MOD.map f₁.op.toLoc).toFunctor.obj M₁ ⟶ (MOD.map f₂.op.toLoc).toFunctor.obj M₂) :
    (restrictFunctorIsoPullback gf₁).hom.app M₁ ≫
        Pseudofunctor.LocallyDiscreteOpToCat.pullHom (F := MOD) φ e gf₁ gf₂ h₁ h₂ ≫
        (restrictFunctorIsoPullback gf₂).inv.app M₂ =
      (restrictFunctorCongr h₁.symm).hom.app M₁ ≫ (restrictFunctorComp e f₁).hom.app M₁ ≫
        (restrictFunctor e).map ((restrictFunctorIsoPullback f₁).hom.app M₁ ≫ φ ≫
          (restrictFunctorIsoPullback f₂).inv.app M₂) ≫
        (restrictFunctorComp e f₂).inv.app M₂ ≫ (restrictFunctorCongr h₂).hom.app M₂

abbrev

Ranges

L204 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.AlgebraicGeometry.Scheme.Modules.ObjGlue.Ranges

Documentation

The opens occurring as ranges of the given family of open immersions.

Source context 22 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ObjGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section WLOG
variable {Y : Scheme.{u}} {ι : Type v} {V : ι → Scheme.{u}} (g : ∀ i, V i ⟶ Y) [∀ i,
  IsOpenImmersion (g i)]

Lean source · statement

abbrev Ranges : Type u

theorem

sieve_ofArrows_eq_opensRange

L206 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.AlgebraicGeometry.Scheme.Modules.ObjGlue.sieve_ofArrows_eq_opensRange

Source context 22 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ObjGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section WLOG
variable {Y : Scheme.{u}} {ι : Type v} {V : ι → Scheme.{u}} (g : ∀ i, V i ⟶ Y) [∀ i,
  IsOpenImmersion (g i)]

Lean source · full declaration

theorem sieve_ofArrows_eq_opensRange :
    Sieve.ofArrows _ g = Sieve.ofArrows (fun O : Ranges g => ((O.1 : Y.Opens) : Scheme.{u})) (fun
      O => O.1.ι) := by
  apply le_antisymm
  · rw [Sieve.ofArrows, Sieve.generate_le_iff]
    rintro Z _ ⟨i⟩
    exact ⟨_, (g i).isoOpensRange.hom, (⟨(g i).opensRange, i, rfl⟩ : Ranges g).1.ι,
      Presieve.ofArrows.mk (⟨(g i).opensRange, i, rfl⟩ : Ranges g), (g i).isoOpensRange_hom_ι⟩
  · rw [Sieve.ofArrows, Sieve.generate_le_iff]
    rintro Z _ ⟨O⟩
    obtain ⟨O, i, rfl⟩ := O
    exact ⟨_, (g i).isoOpensRange.inv, g i, Presieve.ofArrows.mk i, (g i).isoOpensRange_inv_comp⟩

theorem

essSurj_iff_of_sieve_eq

L219 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.AlgebraicGeometry.Scheme.Modules.ObjGlue.essSurj_iff_of_sieve_eq

Source context 23 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ObjGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section WLOG
variable {Y : Scheme.{u}} {ι : Type v} {V : ι → Scheme.{u}} (g : ∀ i, V i ⟶ Y) [∀ i,
  IsOpenImmersion (g i)]
omit [∀ i, IsOpenImmersion (g i)] in

Lean source · statement

theorem essSurj_iff_of_sieve_eq {ι' : Type v'} {V' : ι' → Scheme.{u}} (g' : ∀ i, V' i ⟶ Y)
    (h : Sieve.ofArrows _ g = Sieve.ofArrows _ g') :
    (MOD.toDescentData g).EssSurj ↔ (MOD.toDescentData g').EssSurj

abbrev

incl

L237 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.AlgebraicGeometry.Scheme.Modules.ObjGlue.incl

Documentation

The inclusion of an open from the covering family into the ambient scheme.

Source context 22 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ObjGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Opens
variable {Y : Scheme.{u}} {ι : Type u} (U : ι → Y.Opens)

Lean source · statement

abbrev incl (i : ι) : (U i : Scheme.{u}) ⟶ Y

abbrev

p₁

L240 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.AlgebraicGeometry.Scheme.Modules.ObjGlue.p₁

Documentation

The inclusion of a pairwise intersection into its first covering open.

Source context 22 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ObjGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Opens
variable {Y : Scheme.{u}} {ι : Type u} (U : ι → Y.Opens)

Lean source · statement

abbrev p₁ (i j : ι) : ((U i ⊓ U j : Y.Opens) : Scheme.{u}) ⟶ (U i : Scheme.{u})

abbrev

p₂

L243 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.AlgebraicGeometry.Scheme.Modules.ObjGlue.p₂

Documentation

The inclusion of a pairwise intersection into its second covering open.

Source context 22 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ObjGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Opens
variable {Y : Scheme.{u}} {ι : Type u} (U : ι → Y.Opens)

Lean source · statement

abbrev p₂ (i j : ι) : ((U i ⊓ U j : Y.Opens) : Scheme.{u}) ⟶ (U j : Scheme.{u})

abbrev

Dobj

L249 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.AlgebraicGeometry.Scheme.Modules.ObjGlue.Dobj

Documentation

The module attached to a covering open by the given descent datum.

Source context 23 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ObjGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Opens
variable {Y : Scheme.{u}} {ι : Type u} (U : ι → Y.Opens)
variable (D : (MOD.{u}).DescentData (incl U))

Lean source · statement

abbrev Dobj (i : ι) : ((U i : Y.Opens) : Scheme.{u}).Modules

theorem

D_pullHom

L251 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.AlgebraicGeometry.Scheme.Modules.ObjGlue.D_pullHom

Source context 23 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ObjGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Opens
variable {Y : Scheme.{u}} {ι : Type u} (U : ι → Y.Opens)
variable (D : (MOD.{u}).DescentData (incl U))

Lean source · statement

theorem D_pullHom ⦃Z Z' : Scheme.{u}⦄ (φ : Z' ⟶ Z) (q : Z ⟶ Y) (q' : Z' ⟶ Y) (hq : φ ≫ q = q') ⦃i
    j : ι⦄
    (f₁ : Z ⟶ (U i : Scheme.{u})) (f₂ : Z ⟶ (U j : Scheme.{u})) (hf₁ : f₁ ≫ incl U i = q) (hf₂ :
      f₂ ≫ incl U j = q)
    (g₁ : Z' ⟶ (U i : Scheme.{u})) (g₂ : Z' ⟶ (U j : Scheme.{u})) (hg₁ : φ ≫ f₁ = g₁) (hg₂ : φ ≫
      f₂ = g₂)
    (hg₁' : g₁ ≫ incl U i = q') (hg₂' : g₂ ≫ incl U j = q') :
    Pseudofunctor.LocallyDiscreteOpToCat.pullHom (D.hom q f₁ f₂ hf₁ hf₂) φ g₁ g₂ hg₁ hg₂ =
      D.hom q' g₁ g₂ hg₁' hg₂'

theorem

ofObj_pullHom

L262 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.AlgebraicGeometry.Scheme.Modules.ObjGlue.ofObj_pullHom

Source context 23 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ObjGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Opens
variable {Y : Scheme.{u}} {ι : Type u} (U : ι → Y.Opens)
variable (D : (MOD.{u}).DescentData (incl U))

Lean source · statement

theorem ofObj_pullHom (M : Y.Modules) ⦃Z Z' : Scheme.{u}⦄ (φ : Z' ⟶ Z) (q : Z ⟶ Y) (q' : Z' ⟶ Y)
    (hq : φ ≫ q = q')
    ⦃i j : ι⦄ (f₁ : Z ⟶ (U i : Scheme.{u})) (f₂ : Z ⟶ (U j : Scheme.{u})) (hf₁ : f₁ ≫ incl U i = q)
    (hf₂ : f₂ ≫ incl U j = q) (g₁ : Z' ⟶ (U i : Scheme.{u})) (g₂ : Z' ⟶ (U j : Scheme.{u})) (hg₁ :
      φ ≫ f₁ = g₁)
    (hg₂ : φ ≫ f₂ = g₂) (hg₁' : g₁ ≫ incl U i = q') (hg₂' : g₂ ≫ incl U j = q') :
    Pseudofunctor.LocallyDiscreteOpToCat.pullHom (((MOD.toDescentData (incl U)).obj M).hom q f₁ f₂
      hf₁ hf₂) φ g₁ g₂
        hg₁ hg₂ = ((MOD.toDescentData (incl U)).obj M).hom q' g₁ g₂ hg₁' hg₂'

theorem

ofObj_hom_eq

L273 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.AlgebraicGeometry.Scheme.Modules.ObjGlue.ofObj_hom_eq

Source context 23 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ObjGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Opens
variable {Y : Scheme.{u}} {ι : Type u} (U : ι → Y.Opens)
variable (D : (MOD.{u}).DescentData (incl U))

Lean source · statement

theorem ofObj_hom_eq (M : Y.Modules) ⦃Z : Scheme.{u}⦄ (q : Z ⟶ Y) ⦃i j : ι⦄
    (f₁ : Z ⟶ (U i : Scheme.{u})) (f₂ : Z ⟶ (U j : Scheme.{u}))
    (hf₁ : f₁ ≫ incl U i = q) (hf₂ : f₂ ≫ incl U j = q) {N : Z.Modules}
    (φ : (Modules.pullback f₂).obj ((Modules.pullback (incl U j)).obj M) ⟶ N) :
    @Eq (_root_.AlgebraicGeometry.Scheme.Modules.Hom
      (X := Z)
      ((Modules.pullback f₁).obj ((Modules.pullback (incl U i)).obj M)) N)
      (((MOD.toDescentData (incl U)).obj M).hom q f₁ f₂ hf₁ hf₂ ≫ φ)
      ((((Scheme.Modules.pullbackComp f₁ (incl U i)).hom.app M ≫
          (Scheme.Modules.pullbackCongr hf₁).hom.app M) ≫
        (Scheme.Modules.pullbackCongr hf₂.symm).hom.app M ≫
        (Scheme.Modules.pullbackComp f₂ (incl U j)).inv.app M) ≫ φ)

abbrev

incO

L289 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.AlgebraicGeometry.Scheme.Modules.ObjGlue.incO

Documentation

The inclusion of a smaller open into a specified covering open.

Source context 23 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ObjGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Opens
variable {Y : Scheme.{u}} {ι : Type u} (U : ι → Y.Opens)
variable (D : (MOD.{u}).DescentData (incl U))

Lean source · statement

abbrev incO (i : ι) (O : Y.Opens) (h : O ≤ U i) : (O : Scheme.{u}) ⟶ (U i :
  Scheme.{u})

theorem

incO_comp

L292 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.AlgebraicGeometry.Scheme.Modules.ObjGlue.incO_comp

Source context 23 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ObjGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Opens
variable {Y : Scheme.{u}} {ι : Type u} (U : ι → Y.Opens)
variable (D : (MOD.{u}).DescentData (incl U))

Lean source · statement

theorem incO_comp (i : ι) {O O' : Y.Opens} (hO' : O' ≤ O) (hi : O ≤ U i) :
    Y.homOfLE hO' ≫ incO U i O hi = incO U i O' (hO'.trans hi)

def

τ

L297 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.AlgebraicGeometry.Scheme.Modules.ObjGlue.τ

Documentation

The descent transition expressed through the restriction--pullback comparisons.

Source context 23 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ObjGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Opens
variable {Y : Scheme.{u}} {ι : Type u} (U : ι → Y.Opens)
variable (D : (MOD.{u}).DescentData (incl U))

Lean source · statement

def τ (i j : ι) (O : Y.Opens) (hi : O ≤ U i) (hj : O ≤ U j) :
    (Dobj U D i).restrict (incO U i O hi) ≅ (Dobj U D j).restrict (incO U j O hj)

abbrev

ρ

L304 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.AlgebraicGeometry.Scheme.Modules.ObjGlue.ρ

Documentation

The descent transition on the intersection of two covering opens.

Source context 23 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ObjGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Opens
variable {Y : Scheme.{u}} {ι : Type u} (U : ι → Y.Opens)
variable (D : (MOD.{u}).DescentData (incl U))

Lean source · statement

abbrev ρ (i j : ι) : (Dobj U D i).restrict (p₁ U i j) ≅ (Dobj U D j).restrict (p₂ U
  i j)

theorem

τ_self

L308 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.AlgebraicGeometry.Scheme.Modules.ObjGlue.τ_self

Source context 23 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ObjGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Opens
variable {Y : Scheme.{u}} {ι : Type u} (U : ι → Y.Opens)
variable (D : (MOD.{u}).DescentData (incl U))

Lean source · statement

theorem τ_self (i : ι) (O : Y.Opens) (hi : O ≤ U i) :
    (τ U D i i O hi hi).hom = 𝟙 ((Dobj U D i).restrict (incO U i O hi))

theorem

ρ_self

L323 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.AlgebraicGeometry.Scheme.Modules.ObjGlue.ρ_self

Source context 23 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ObjGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Opens
variable {Y : Scheme.{u}} {ι : Type u} (U : ι → Y.Opens)
variable (D : (MOD.{u}).DescentData (incl U))

Lean source · statement

theorem ρ_self (i : ι) : (ρ U D i i).hom = 𝟙 ((Dobj U D i).restrict (p₁ U i i))

theorem

τ_comp

L325 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.AlgebraicGeometry.Scheme.Modules.ObjGlue.τ_comp

Source context 23 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ObjGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Opens
variable {Y : Scheme.{u}} {ι : Type u} (U : ι → Y.Opens)
variable (D : (MOD.{u}).DescentData (incl U))

Lean source · statement

theorem τ_comp (i j k : ι) (O : Y.Opens) (hi : O ≤ U i) (hj : O ≤ U j) (hk : O ≤ U k) :
    (τ U D i j O hi hj).hom ≫ (τ U D j k O hj hk).hom = (τ U D i k O hi hk).hom

abbrev

P

L354 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.AlgebraicGeometry.Scheme.Modules.ObjGlue.P

Documentation

Push the module on a covering open forward to the ambient scheme.

Source context 23 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ObjGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Opens
variable {Y : Scheme.{u}} {ι : Type u} (U : ι → Y.Opens)
variable (D : (MOD.{u}).DescentData (incl U))

Lean source · statement

abbrev P (i : ι) : Y.Modules

abbrev

Q

L356 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.AlgebraicGeometry.Scheme.Modules.ObjGlue.Q

Documentation

Push the second module restricted to an overlap forward to the ambient scheme.

Source context 23 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ObjGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Opens
variable {Y : Scheme.{u}} {ι : Type u} (U : ι → Y.Opens)
variable (D : (MOD.{u}).DescentData (incl U))

Lean source · statement

abbrev Q (i j : ι) : Y.Modules

def

β

L360 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.AlgebraicGeometry.Scheme.Modules.ObjGlue.β

Documentation

Restrict the second covering module to the overlap and push it forward.

Source context 23 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ObjGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Opens
variable {Y : Scheme.{u}} {ι : Type u} (U : ι → Y.Opens)
variable (D : (MOD.{u}).DescentData (incl U))

Lean source · statement

def β (i j : ι) : P U D j ⟶ Q U D i j

def

α

L366 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.AlgebraicGeometry.Scheme.Modules.ObjGlue.α

Documentation

Restrict the first covering module and transport it by the overlap transition.

Source context 23 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ObjGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Opens
variable {Y : Scheme.{u}} {ι : Type u} (U : ι → Y.Opens)
variable (D : (MOD.{u}).DescentData (incl U))

Lean source · statement

def α (i j : ι) : P U D i ⟶ Q U D i j

def

compatible

L373 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.AlgebraicGeometry.Scheme.Modules.ObjGlue.compatible

Documentation

The submodule of families of sections satisfying all overlap compatibility equations.

Source context 23 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ObjGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Opens
variable {Y : Scheme.{u}} {ι : Type u} (U : ι → Y.Opens)
variable (D : (MOD.{u}).DescentData (incl U))

Lean source · full declaration

def compatible (W : Y.Opens) : Submodule Γ(Y, W) (∀ i, Γ(P U D i, W)) where
  carrier := {s | ∀ i j, (α U D i j).app W (s i) = (β U D i j).app W (s j)}
  add_mem' := by
    intro s t hs ht i j
    simp only [Pi.add_apply, map_add, hs i j, ht i j]
  zero_mem' := by intro i j; simp only [Pi.zero_apply, map_zero]
  smul_mem' := by
    intro r s hs i j
    simp only [Pi.smul_apply, Hom.app_smul, hs i j]

theorem

app_presheaf_map

L383 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.AlgebraicGeometry.Scheme.Modules.ObjGlue.app_presheaf_map

Source context 23 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ObjGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Opens
variable {Y : Scheme.{u}} {ι : Type u} (U : ι → Y.Opens)
variable (D : (MOD.{u}).DescentData (incl U))

Lean source · statement

theorem app_presheaf_map {X : Scheme.{u}} {M N : X.Modules} (φ : M ⟶ N) {W W' : X.Opens} (h : W' ⟶
    W) (x : Γ(M, W)) :
    φ.app W' (M.presheaf.map h.op x) = N.presheaf.map h.op (φ.app W x)

theorem

compatible_map

L388 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.AlgebraicGeometry.Scheme.Modules.ObjGlue.compatible_map

Source context 23 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ObjGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Opens
variable {Y : Scheme.{u}} {ι : Type u} (U : ι → Y.Opens)
variable (D : (MOD.{u}).DescentData (incl U))

Lean source · full declaration

theorem compatible_map {W W' : Y.Opens} (h : W' ⟶ W) (s : ∀ i, Γ(P U D i, W)) (hs : s ∈ compatible
    U D W) :
    (fun i => (P U D i).presheaf.map h.op (s i)) ∈ compatible U D W' := by
  intro i j
  change (α U D i j).app W' ((P U D i).presheaf.map h.op (s i)) = (β U D i j).app W' ((P U D
    j).presheaf.map h.op (s j))
  rw [app_presheaf_map, app_presheaf_map, hs i j]

def

gluedAb

L397 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.AlgebraicGeometry.Scheme.Modules.ObjGlue.gluedAb

Documentation

The abelian presheaf of compatible families of sections.

Source context 23 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ObjGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Opens
variable {Y : Scheme.{u}} {ι : Type u} (U : ι → Y.Opens)
variable (D : (MOD.{u}).DescentData (incl U))

Lean source · full declaration

def gluedAb : (TopologicalSpace.Opens Y)ᵒᵖ ⥤ Ab where
  obj W := AddCommGrpCat.of (compatible U D W.unop)
  map {W W'} h := AddCommGrpCat.ofHom
    { toFun := fun s => ⟨fun i => (P U D i).presheaf.map h (s.1 i), compatible_map U D h.unop s.1
      s.2⟩
      map_zero' := by apply Subtype.ext; funext i; simp
      map_add' := by intro s t; apply Subtype.ext; funext i; simp }
  map_id W := by
    apply AddCommGrpCat.ext; intro s; apply Subtype.ext; funext i
    simp
  map_comp {W W' W''} h h' := by
    apply AddCommGrpCat.ext; intro s; apply Subtype.ext; funext i
    simp

theorem

gluedAb_map_apply_coe

L411 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.AlgebraicGeometry.Scheme.Modules.ObjGlue.gluedAb_map_apply_coe

Source context 23 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ObjGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Opens
variable {Y : Scheme.{u}} {ι : Type u} (U : ι → Y.Opens)
variable (D : (MOD.{u}).DescentData (incl U))

Lean source · statement

theorem gluedAb_map_apply_coe {W W' : (TopologicalSpace.Opens Y)ᵒᵖ} (h : W ⟶ W') (s : compatible U
    D W.unop) (i : ι) :
    ((gluedAb U D).map h s).1 i = (P U D i).presheaf.map h (s.1 i)

def

gluedPresheaf

L416 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.AlgebraicGeometry.Scheme.Modules.ObjGlue.gluedPresheaf

Documentation

The presheaf of modules whose sections are compatible families.

Source context 23 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ObjGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Opens
variable {Y : Scheme.{u}} {ι : Type u} (U : ι → Y.Opens)
variable (D : (MOD.{u}).DescentData (incl U))

Lean source · statement

def gluedPresheaf : Y.PresheafOfModules

abbrev

abSheaf

L425 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.AlgebraicGeometry.Scheme.Modules.ObjGlue.abSheaf

Documentation

The underlying abelian sheaf of a sheaf of scheme modules.

Source context 23 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ObjGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Opens
variable {Y : Scheme.{u}} {ι : Type u} (U : ι → Y.Opens)
variable (D : (MOD.{u}).DescentData (incl U))

Lean source · statement

abbrev abSheaf (M : Y.Modules) : TopCat.Sheaf Ab Y.toTopCat

theorem

isSheaf_gluedPresheaf

L427 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.AlgebraicGeometry.Scheme.Modules.ObjGlue.isSheaf_gluedPresheaf

Source context 23 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ObjGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Opens
variable {Y : Scheme.{u}} {ι : Type u} (U : ι → Y.Opens)
variable (D : (MOD.{u}).DescentData (incl U))

Lean source · statement

theorem isSheaf_gluedPresheaf :
    Presheaf.IsSheaf (Opens.grothendieckTopology Y) (gluedPresheaf U D).presheaf

def

glued

L451 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.AlgebraicGeometry.Scheme.Modules.ObjGlue.glued

Documentation

The sheaf of modules formed by gluing compatible families of sections.

Source context 23 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ObjGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Opens
variable {Y : Scheme.{u}} {ι : Type u} (U : ι → Y.Opens)
variable (D : (MOD.{u}).DescentData (incl U))

Lean source · statement

def glued : Y.Modules

theorem

glued_presheaf_obj

L453 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.AlgebraicGeometry.Scheme.Modules.ObjGlue.glued_presheaf_obj

Source context 23 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ObjGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Opens
variable {Y : Scheme.{u}} {ι : Type u} (U : ι → Y.Opens)
variable (D : (MOD.{u}).DescentData (incl U))

Lean source · statement

theorem glued_presheaf_obj (W : Y.Opens) : ((glued U D).presheaf.obj (op W) : Type u) = compatible
    U D W

def

projAb

L457 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.AlgebraicGeometry.Scheme.Modules.ObjGlue.projAb

Documentation

The projection from compatible families to one pushed-forward component.

Source context 23 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ObjGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Opens
variable {Y : Scheme.{u}} {ι : Type u} (U : ι → Y.Opens)
variable (D : (MOD.{u}).DescentData (incl U))

Lean source · full declaration

def projAb (k : ι) : gluedAb U D ⟶ (P U D k).presheaf where
  app W := AddCommGrpCat.ofHom
    { toFun := fun s => s.1 k, map_zero' := rfl, map_add' := fun _ _ => rfl }
  naturality {W W'} h := by apply AddCommGrpCat.ext; intro s; rfl

def

proj

L463 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.AlgebraicGeometry.Scheme.Modules.ObjGlue.proj

Documentation

The module morphism projecting the glued sheaf onto a pushed-forward component.

Source context 23 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ObjGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Opens
variable {Y : Scheme.{u}} {ι : Type u} (U : ι → Y.Opens)
variable (D : (MOD.{u}).DescentData (incl U))

Lean source · statement

def proj (k : ι) : glued U D ⟶ P U D k

theorem

proj_app

L467 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.AlgebraicGeometry.Scheme.Modules.ObjGlue.proj_app

Source context 23 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ObjGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Opens
variable {Y : Scheme.{u}} {ι : Type u} (U : ι → Y.Opens)
variable (D : (MOD.{u}).DescentData (incl U))

Lean source · full declaration

theorem proj_app (k : ι) (W : Y.Opens) (s : compatible U D W) :
    (proj U D k).app W (show Γ(glued U D, W) from s) = s.1 k := rfl

theorem

presheaf_map_congr

L470 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.AlgebraicGeometry.Scheme.Modules.ObjGlue.presheaf_map_congr

Source context 23 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ObjGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Opens
variable {Y : Scheme.{u}} {ι : Type u} (U : ι → Y.Opens)
variable (D : (MOD.{u}).DescentData (incl U))

Lean source · statement

theorem presheaf_map_congr {X : Scheme.{u}} (M : X.Modules) {V V' : X.Opens} (f g : V' ⟶ V) (x :
    Γ(M, V)) :
    M.presheaf.map f.op x = M.presheaf.map g.op x

theorem

preimage_comp'

L474 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.AlgebraicGeometry.Scheme.Modules.ObjGlue.preimage_comp'

Source context 23 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ObjGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Opens
variable {Y : Scheme.{u}} {ι : Type u} (U : ι → Y.Opens)
variable (D : (MOD.{u}).DescentData (incl U))

Lean source · statement

theorem preimage_comp' {X X' X'' : Scheme.{u}} (f : X ⟶ X') (g : X' ⟶ X'') (W : X''.Opens) :
    (f ≫ g) ⁻¹ᵁ W = f ⁻¹ᵁ (g ⁻¹ᵁ W)

theorem

preimage_ι_inf_right

L477 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.AlgebraicGeometry.Scheme.Modules.ObjGlue.preimage_ι_inf_right

Source context 23 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ObjGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Opens
variable {Y : Scheme.{u}} {ι : Type u} (U : ι → Y.Opens)
variable (D : (MOD.{u}).DescentData (incl U))

Lean source · statement

theorem preimage_ι_inf_right (i j : ι) (W : Y.Opens) :
    (U i ⊓ U j).ι ⁻¹ᵁ W = (p₂ U i j) ⁻¹ᵁ ((U j).ι ⁻¹ᵁ W)

theorem

preimage_ι_inf_left

L481 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.AlgebraicGeometry.Scheme.Modules.ObjGlue.preimage_ι_inf_left

Source context 23 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ObjGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Opens
variable {Y : Scheme.{u}} {ι : Type u} (U : ι → Y.Opens)
variable (D : (MOD.{u}).DescentData (incl U))

Lean source · statement

theorem preimage_ι_inf_left (i j : ι) (W : Y.Opens) :
    (U i ⊓ U j).ι ⁻¹ᵁ W = (p₁ U i j) ⁻¹ᵁ ((U i).ι ⁻¹ᵁ W)

theorem

β_le

L485 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.AlgebraicGeometry.Scheme.Modules.ObjGlue.β_le

Source context 23 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ObjGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Opens
variable {Y : Scheme.{u}} {ι : Type u} (U : ι → Y.Opens)
variable (D : (MOD.{u}).DescentData (incl U))

Lean source · statement

theorem β_le (i j : ι) (W : Y.Opens) : (p₂ U i j) ''ᵁ ((U i ⊓ U j).ι ⁻¹ᵁ W) ≤ (U j).ι ⁻¹ᵁ W

theorem

α_le

L488 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.AlgebraicGeometry.Scheme.Modules.ObjGlue.α_le

Source context 23 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ObjGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Opens
variable {Y : Scheme.{u}} {ι : Type u} (U : ι → Y.Opens)
variable (D : (MOD.{u}).DescentData (incl U))

Lean source · statement

theorem α_le (i j : ι) (W : Y.Opens) : (p₁ U i j) ''ᵁ ((U i ⊓ U j).ι ⁻¹ᵁ W) ≤ (U i).ι ⁻¹ᵁ W

theorem

β_eq_of_le

L491 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.AlgebraicGeometry.Scheme.Modules.ObjGlue.β_eq_of_le

Source context 23 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ObjGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Opens
variable {Y : Scheme.{u}} {ι : Type u} (U : ι → Y.Opens)
variable (D : (MOD.{u}).DescentData (incl U))

Lean source · statement

theorem β_eq_of_le {i j : ι} {W : Y.Opens} (hW : W ≤ U i) :
    (p₂ U i j) ''ᵁ ((U i ⊓ U j).ι ⁻¹ᵁ W) = (U j).ι ⁻¹ᵁ W

theorem

β_app_hom

L500 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.AlgebraicGeometry.Scheme.Modules.ObjGlue.β_app_hom

Source context 23 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ObjGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Opens
variable {Y : Scheme.{u}} {ι : Type u} (U : ι → Y.Opens)
variable (D : (MOD.{u}).DescentData (incl U))

Lean source · statement

theorem β_app_hom (i j : ι) (W : Y.Opens) :
    (β U D i j).app W = (Dobj U D j).presheaf.map (homOfLE (β_le U i j W)).op

theorem

β_app

L513 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.AlgebraicGeometry.Scheme.Modules.ObjGlue.β_app

Source context 23 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ObjGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Opens
variable {Y : Scheme.{u}} {ι : Type u} (U : ι → Y.Opens)
variable (D : (MOD.{u}).DescentData (incl U))

Lean source · statement

theorem β_app (i j : ι) (W : Y.Opens) (x : Γ(P U D j, W)) :
    (β U D i j).app W x = ((Dobj U D j).presheaf.map (homOfLE (β_le U i j W)).op x :)

theorem

α_app_hom

L517 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.AlgebraicGeometry.Scheme.Modules.ObjGlue.α_app_hom

Source context 23 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ObjGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Opens
variable {Y : Scheme.{u}} {ι : Type u} (U : ι → Y.Opens)
variable (D : (MOD.{u}).DescentData (incl U))

Lean source · statement

theorem α_app_hom (i j : ι) (W : Y.Opens) :
    (α U D i j).app W = (Dobj U D i).presheaf.map (homOfLE (α_le U i j W)).op ≫
      (ρ U D i j).hom.app ((U i ⊓ U j).ι ⁻¹ᵁ W)

theorem

α_app

L533 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.AlgebraicGeometry.Scheme.Modules.ObjGlue.α_app

Source context 23 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ObjGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Opens
variable {Y : Scheme.{u}} {ι : Type u} (U : ι → Y.Opens)
variable (D : (MOD.{u}).DescentData (incl U))

Lean source · statement

theorem α_app (i j : ι) (W : Y.Opens) (x : Γ(P U D i, W)) :
    (α U D i j).app W x =
      (ρ U D i j).hom.app ((U i ⊓ U j).ι ⁻¹ᵁ W) ((Dobj U D i).presheaf.map (homOfLE (α_le U i j
        W)).op x)

theorem

restrictFunctor_map_app

L539 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.AlgebraicGeometry.Scheme.Modules.ObjGlue.restrictFunctor_map_app

Source context 23 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ObjGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Opens
variable {Y : Scheme.{u}} {ι : Type u} (U : ι → Y.Opens)
variable (D : (MOD.{u}).DescentData (incl U))

Lean source · statement

theorem restrictFunctor_map_app {X : Scheme.{u}} (f : X ⟶ Y) [IsOpenImmersion f] {M N : Y.Modules}
    (t : M ⟶ N)
    (V : X.Opens) : ((restrictFunctor f).map t).app V = t.app (f ''ᵁ V)

theorem

presheaf_map_injective_of_eq

L543 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.AlgebraicGeometry.Scheme.Modules.ObjGlue.presheaf_map_injective_of_eq

Source context 23 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ObjGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Opens
variable {Y : Scheme.{u}} {ι : Type u} (U : ι → Y.Opens)
variable (D : (MOD.{u}).DescentData (incl U))

Lean source · statement

theorem presheaf_map_injective_of_eq {X : Scheme.{u}} (M : X.Modules) {V V' : X.Opens} (e : V' =
    V) (h : V' ≤ V) :
    Function.Injective (M.presheaf.map (homOfLE h).op)

theorem

compatible_ext_of_le

L550 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.AlgebraicGeometry.Scheme.Modules.ObjGlue.compatible_ext_of_le

Source context 23 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ObjGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Opens
variable {Y : Scheme.{u}} {ι : Type u} (U : ι → Y.Opens)
variable (D : (MOD.{u}).DescentData (incl U))

Lean source · statement

theorem compatible_ext_of_le {k : ι} {W : Y.Opens} (hW : W ≤ U k) {s s' : compatible U D W}
    (h : s.1 k = s'.1 k) : s = s'

theorem

map_map

L559 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.AlgebraicGeometry.Scheme.Modules.ObjGlue.map_map

Source context 23 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ObjGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Opens
variable {Y : Scheme.{u}} {ι : Type u} (U : ι → Y.Opens)
variable (D : (MOD.{u}).DescentData (incl U))

Lean source · statement

theorem map_map {X : Scheme.{u}} (M : X.Modules) {V₁ V₂ V₃ : X.Opens} (f : V₂ ⟶ V₁) (g : V₃ ⟶ V₂)
    (x : Γ(M, V₁)) :
    M.presheaf.map g.op (M.presheaf.map f.op x) = M.presheaf.map (g ≫ f).op x

theorem

map_self

L564 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.AlgebraicGeometry.Scheme.Modules.ObjGlue.map_self

Source context 23 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ObjGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Opens
variable {Y : Scheme.{u}} {ι : Type u} (U : ι → Y.Opens)
variable (D : (MOD.{u}).DescentData (incl U))

Lean source · statement

theorem map_self {X : Scheme.{u}} (M : X.Modules) {V : X.Opens} (f : V ⟶ V) (x : Γ(M, V)) :
    M.presheaf.map f.op x = x

theorem

map_map_self

L569 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.AlgebraicGeometry.Scheme.Modules.ObjGlue.map_map_self

Source context 23 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ObjGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Opens
variable {Y : Scheme.{u}} {ι : Type u} (U : ι → Y.Opens)
variable (D : (MOD.{u}).DescentData (incl U))

Lean source · statement

theorem map_map_self {X : Scheme.{u}} (M : X.Modules) {V₁ V₂ : X.Opens} (f : V₂ ⟶ V₁) (g : V₁ ⟶
    V₂) (x : Γ(M, V₁)) :
    M.presheaf.map g.op (M.presheaf.map f.op x) = x

theorem

preimage_ι_eq_incO

L574 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.AlgebraicGeometry.Scheme.Modules.ObjGlue.preimage_ι_eq_incO

Source context 23 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ObjGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Opens
variable {Y : Scheme.{u}} {ι : Type u} (U : ι → Y.Opens)
variable (D : (MOD.{u}).DescentData (incl U))

Lean source · statement

theorem preimage_ι_eq_incO (i : ι) (O : Y.Opens) (hi : O ≤ U i) (V : Y.Opens) :
    O.ι ⁻¹ᵁ V = (incO U i O hi) ⁻¹ᵁ ((U i).ι ⁻¹ᵁ V)

theorem

T_le_in

L578 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.AlgebraicGeometry.Scheme.Modules.ObjGlue.T_le_in

Source context 23 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ObjGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Opens
variable {Y : Scheme.{u}} {ι : Type u} (U : ι → Y.Opens)
variable (D : (MOD.{u}).DescentData (incl U))

Lean source · statement

theorem T_le_in (i : ι) (O : Y.Opens) (hi : O ≤ U i) (V : Y.Opens) :
    (incO U i O hi) ''ᵁ (O.ι ⁻¹ᵁ V) ≤ (U i).ι ⁻¹ᵁ V

theorem

T_eq

L582 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.AlgebraicGeometry.Scheme.Modules.ObjGlue.T_eq

Source context 23 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ObjGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Opens
variable {Y : Scheme.{u}} {ι : Type u} (U : ι → Y.Opens)
variable (D : (MOD.{u}).DescentData (incl U))

Lean source · statement

theorem T_eq (i : ι) (O : Y.Opens) (hi : O ≤ U i) (V : Y.Opens) (hV : V ≤ O) :
    (incO U i O hi) ''ᵁ (O.ι ⁻¹ᵁ V) = (U i).ι ⁻¹ᵁ V

theorem

T_le_out

L589 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.AlgebraicGeometry.Scheme.Modules.ObjGlue.T_le_out

Source context 23 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ObjGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Opens
variable {Y : Scheme.{u}} {ι : Type u} (U : ι → Y.Opens)
variable (D : (MOD.{u}).DescentData (incl U))

Lean source · statement

theorem T_le_out (i : ι) (O : Y.Opens) (hi : O ≤ U i) (V : Y.Opens) (hV : V ≤ O) :
    (U i).ι ⁻¹ᵁ V ≤ (incO U i O hi) ''ᵁ (O.ι ⁻¹ᵁ V)

def

T

L594 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.AlgebraicGeometry.Scheme.Modules.ObjGlue.T

Documentation

Transport a section between two covering modules through a smaller common open.

Source context 23 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ObjGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Opens
variable {Y : Scheme.{u}} {ι : Type u} (U : ι → Y.Opens)
variable (D : (MOD.{u}).DescentData (incl U))

Lean source · statement

def T (i j : ι) (O : Y.Opens) (hi : O ≤ U i) (hj : O ≤ U j) (V : Y.Opens) (hV : V ≤ O)
    (x : Γ(Dobj U D i, (U i).ι ⁻¹ᵁ V)) : Γ(Dobj U D j, (U j).ι ⁻¹ᵁ V)

theorem

T_self

L600 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.AlgebraicGeometry.Scheme.Modules.ObjGlue.T_self

Source context 23 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ObjGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Opens
variable {Y : Scheme.{u}} {ι : Type u} (U : ι → Y.Opens)
variable (D : (MOD.{u}).DescentData (incl U))

Lean source · statement

theorem T_self (i : ι) (O : Y.Opens) (hi : O ≤ U i) (V : Y.Opens) (hV : V ≤ O)
    (x : Γ(Dobj U D i, (U i).ι ⁻¹ᵁ V)) : T U D i i O hi hi V hV x = x

theorem

T_comp

L605 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.AlgebraicGeometry.Scheme.Modules.ObjGlue.T_comp

Source context 23 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ObjGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Opens
variable {Y : Scheme.{u}} {ι : Type u} (U : ι → Y.Opens)
variable (D : (MOD.{u}).DescentData (incl U))

Lean source · statement

theorem T_comp (i j k : ι) (O : Y.Opens) (hi : O ≤ U i) (hj : O ≤ U j) (hk : O ≤ U k) (V :
    Y.Opens) (hV : V ≤ O)
    (x : Γ(Dobj U D i, (U i).ι ⁻¹ᵁ V)) :
    T U D j k O hj hk V hV (T U D i j O hi hj V hV x) = T U D i k O hi hk V hV x

theorem

T_res

L635 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.AlgebraicGeometry.Scheme.Modules.ObjGlue.T_res

Source context 23 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ObjGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Opens
variable {Y : Scheme.{u}} {ι : Type u} (U : ι → Y.Opens)
variable (D : (MOD.{u}).DescentData (incl U))

Lean source · statement

theorem T_res (i j : ι) (O : Y.Opens) (hi : O ≤ U i) (hj : O ≤ U j) {V V' : Y.Opens} (hV : V ≤ O)
    (hV' : V' ≤ V)
    (x : Γ(Dobj U D i, (U i).ι ⁻¹ᵁ V)) :
    T U D i j O hi hj V' (hV'.trans hV) ((Dobj U D i).presheaf.map (homOfLE ((U i).ι.preimage_mono
      hV')).op x) =
      (Dobj U D j).presheaf.map (homOfLE ((U j).ι.preimage_mono hV')).op (T U D i j O hi hj V hV
        x)

def

Φ

L675 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.AlgebraicGeometry.Scheme.Modules.ObjGlue.Φ

Documentation

The canonical comparison between restriction along a composite and iterated restriction.

Source context 23 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ObjGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Opens
variable {Y : Scheme.{u}} {ι : Type u} (U : ι → Y.Opens)
variable (D : (MOD.{u}).DescentData (incl U))

Lean source · statement

def Φ {X₀ X₁ X₂ : Scheme.{u}} (e : X₀ ⟶ X₁) (a : X₁ ⟶ X₂) (a' : X₀ ⟶ X₂)
  [IsOpenImmersion e]
    [IsOpenImmersion a] [IsOpenImmersion a'] (w : e ≫ a = a') (M : X₂.Modules) :
    (restrictFunctor a').obj M ⟶ (restrictFunctor e).obj ((restrictFunctor a).obj M)

theorem

Φ_eq_congr_comp

L684 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.AlgebraicGeometry.Scheme.Modules.ObjGlue.Φ_eq_congr_comp

Source context 23 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ObjGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Opens
variable {Y : Scheme.{u}} {ι : Type u} (U : ι → Y.Opens)
variable (D : (MOD.{u}).DescentData (incl U))

Lean source · statement

theorem Φ_eq_congr_comp {X₀ X₁ X₂ : Scheme.{u}} (e : X₀ ⟶ X₁) (a : X₁ ⟶ X₂) (a' : X₀ ⟶ X₂)
    [IsOpenImmersion e]
    [IsOpenImmersion a] [IsOpenImmersion a'] (w : e ≫ a = a') (M : X₂.Modules) :
    Φ e a a' w M = (restrictFunctorCongr w.symm).hom.app M ≫ (restrictFunctorComp e a).hom.app M

theorem

image_comp_of_eq

L711 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.AlgebraicGeometry.Scheme.Modules.ObjGlue.image_comp_of_eq

Source context 23 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ObjGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Opens
variable {Y : Scheme.{u}} {ι : Type u} (U : ι → Y.Opens)
variable (D : (MOD.{u}).DescentData (incl U))

Lean source · statement

theorem image_comp_of_eq {X₀ X₁ X₂ : Scheme.{u}} (e : X₀ ⟶ X₁) (a : X₁ ⟶ X₂) (a' : X₀ ⟶ X₂)
    [IsOpenImmersion e]
    [IsOpenImmersion a] [IsOpenImmersion a'] (w : e ≫ a = a') (V : X₀.Opens) : a ''ᵁ (e ''ᵁ V) =
      a' ''ᵁ V

theorem

Φ_app

L719 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.AlgebraicGeometry.Scheme.Modules.ObjGlue.Φ_app

Source context 23 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ObjGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Opens
variable {Y : Scheme.{u}} {ι : Type u} (U : ι → Y.Opens)
variable (D : (MOD.{u}).DescentData (incl U))

Lean source · statement

theorem Φ_app {X₀ X₁ X₂ : Scheme.{u}} (e : X₀ ⟶ X₁) (a : X₁ ⟶ X₂) (a' : X₀ ⟶ X₂) [IsOpenImmersion e]
    [IsOpenImmersion a] [IsOpenImmersion a'] (w : e ≫ a = a') (M : X₂.Modules) (V : X₀.Opens)
    (x : Γ(M, a' ''ᵁ V)) :
    (Φ e a a' w M).app V x = (M.presheaf.map (eqToHom (image_comp_of_eq e a a' w V)).op x :
      Γ(M, a ''ᵁ (e ''ᵁ V)))

def

castComp

L734 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.AlgebraicGeometry.Scheme.Modules.ObjGlue.castComp

Documentation

The forward comparison from a composite restriction to its iterated restriction.

Source context 23 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ObjGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Opens
variable {Y : Scheme.{u}} {ι : Type u} (U : ι → Y.Opens)
variable (D : (MOD.{u}).DescentData (incl U))

Lean source · statement

def castComp {X₀ X₁ X₂ : Scheme.{u}} (e : X₀ ⟶ X₁) (a : X₁ ⟶ X₂) (a' : X₀ ⟶ X₂)
  [IsOpenImmersion e]
    [IsOpenImmersion a] [IsOpenImmersion a'] (w : e ≫ a = a') (M : X₂.Modules) :
    (restrictFunctor a').obj M ⟶ (restrictFunctor e).obj ((restrictFunctor a).obj M)

def

castComp'

L741 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.AlgebraicGeometry.Scheme.Modules.ObjGlue.castComp'

Documentation

The reverse comparison from an iterated restriction to its composite restriction.

Source context 23 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ObjGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Opens
variable {Y : Scheme.{u}} {ι : Type u} (U : ι → Y.Opens)
variable (D : (MOD.{u}).DescentData (incl U))

Lean source · statement

def castComp' {X₀ X₁ X₂ : Scheme.{u}} (e : X₀ ⟶ X₁) (a : X₁ ⟶ X₂) (a' : X₀ ⟶ X₂)
  [IsOpenImmersion e]
    [IsOpenImmersion a] [IsOpenImmersion a'] (w : e ≫ a = a') (M : X₂.Modules) :
    (restrictFunctor e).obj ((restrictFunctor a).obj M) ⟶ (restrictFunctor a').obj M

theorem

castComp_app

L747 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.AlgebraicGeometry.Scheme.Modules.ObjGlue.castComp_app

Source context 23 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ObjGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Opens
variable {Y : Scheme.{u}} {ι : Type u} (U : ι → Y.Opens)
variable (D : (MOD.{u}).DescentData (incl U))

Lean source · statement

theorem castComp_app {X₀ X₁ X₂ : Scheme.{u}} (e : X₀ ⟶ X₁) (a : X₁ ⟶ X₂) (a' : X₀ ⟶ X₂)
    [IsOpenImmersion e]
    [IsOpenImmersion a] [IsOpenImmersion a'] (w : e ≫ a = a') (M : X₂.Modules) (V : X₀.Opens)
    (x : Γ(M, a' ''ᵁ V)) :
    (castComp e a a' w M).app V x = (M.presheaf.map (eqToHom (image_comp_of_eq e a a' w V)).op x :
      Γ(M, a ''ᵁ (e ''ᵁ V)))

theorem

castComp'_app

L757 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.AlgebraicGeometry.Scheme.Modules.ObjGlue.castComp'_app

Source context 23 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ObjGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Opens
variable {Y : Scheme.{u}} {ι : Type u} (U : ι → Y.Opens)
variable (D : (MOD.{u}).DescentData (incl U))

Lean source · statement

theorem castComp'_app {X₀ X₁ X₂ : Scheme.{u}} (e : X₀ ⟶ X₁) (a : X₁ ⟶ X₂) (a' : X₀ ⟶ X₂)
    [IsOpenImmersion e]
    [IsOpenImmersion a] [IsOpenImmersion a'] (w : e ≫ a = a') (M : X₂.Modules) (V : X₀.Opens)
    (x : Γ(M, a ''ᵁ (e ''ᵁ V))) :
    (castComp' e a a' w M).app V x = (M.presheaf.map (eqToHom (image_comp_of_eq e a a' w
      V).symm).op x :
      Γ(M, a' ''ᵁ V))

theorem

τ_hom_eq

L772 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.AlgebraicGeometry.Scheme.Modules.ObjGlue.τ_hom_eq

Source context 23 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ObjGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Opens
variable {Y : Scheme.{u}} {ι : Type u} (U : ι → Y.Opens)
variable (D : (MOD.{u}).DescentData (incl U))

Lean source · statement

theorem τ_hom_eq (i j : ι) (O : Y.Opens) (hi : O ≤ U i) (hj : O ≤ U j) : (τ U D i j O hi hj).hom =
    (restrictFunctorIsoPullback (incO U i O hi)).hom.app (Dobj U D i) ≫
      D.hom O.ι (incO U i O hi) (incO U j O hj) (Y.homOfLE_ι hi) (Y.homOfLE_ι hj) ≫
      (restrictFunctorIsoPullback (incO U j O hj)).inv.app (Dobj U D j)

theorem

τ_locality

L794 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.AlgebraicGeometry.Scheme.Modules.ObjGlue.τ_locality

Source context 23 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ObjGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Opens
variable {Y : Scheme.{u}} {ι : Type u} (U : ι → Y.Opens)
variable (D : (MOD.{u}).DescentData (incl U))

Lean source · statement

theorem τ_locality (i j : ι) {O O' : Y.Opens} (hO' : O' ≤ O) (hi : O ≤ U i) (hj : O ≤ U j) :
    (restrictFunctorIsoPullback (incO U i O' (hO'.trans hi))).hom.app (D.obj i) ≫
      D.hom O'.ι (incO U i O' (hO'.trans hi)) (incO U j O' (hO'.trans hj))
        (Y.homOfLE_ι (hO'.trans hi)) (Y.homOfLE_ι (hO'.trans hj)) ≫
      (restrictFunctorIsoPullback (incO U j O' (hO'.trans hj))).inv.app (D.obj j) =
    (restrictFunctorCongr (incO_comp U i hO' hi).symm).hom.app (D.obj i) ≫
      (restrictFunctorComp (Y.homOfLE hO') (incO U i O hi)).hom.app (D.obj i) ≫
      (restrictFunctor (Y.homOfLE hO')).map
        ((restrictFunctorIsoPullback (incO U i O hi)).hom.app (D.obj i) ≫
          D.hom O.ι (incO U i O hi) (incO U j O hj) (Y.homOfLE_ι hi) (Y.homOfLE_ι hj) ≫
          (restrictFunctorIsoPullback (incO U j O hj)).inv.app (D.obj j)) ≫
      (restrictFunctorComp (Y.homOfLE hO') (incO U j O hj)).inv.app (D.obj j) ≫
      (restrictFunctorCongr (incO_comp U j hO' hj)).hom.app (D.obj j)

theorem

T_indep

L817 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.AlgebraicGeometry.Scheme.Modules.ObjGlue.T_indep

Source context 23 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ObjGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Opens
variable {Y : Scheme.{u}} {ι : Type u} (U : ι → Y.Opens)
variable (D : (MOD.{u}).DescentData (incl U))

Lean source · statement

theorem T_indep (i j : ι) (O : Y.Opens) (hi : O ≤ U i) (hj : O ≤ U j) (V : Y.Opens) (hV : V ≤ O)
    (x : Γ(Dobj U D i, (U i).ι ⁻¹ᵁ V)) :
    T U D i j O hi hj V hV x = T U D i j V (hV.trans hi) (hV.trans hj) V le_rfl x

theorem

presheaf_map_injective_of_eq'

L865 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.AlgebraicGeometry.Scheme.Modules.ObjGlue.presheaf_map_injective_of_eq'

Source context 23 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ObjGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Opens
variable {Y : Scheme.{u}} {ι : Type u} (U : ι → Y.Opens)
variable (D : (MOD.{u}).DescentData (incl U))

Lean source · statement

theorem presheaf_map_injective_of_eq' {X : Scheme.{u}} (M : X.Modules) {V V' : X.Opens} (e : V' =
    V) (f : V' ⟶ V) :
    Function.Injective (M.presheaf.map f.op)

theorem

preimage_ι_inf_self

L872 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.AlgebraicGeometry.Scheme.Modules.ObjGlue.preimage_ι_inf_self

Source context 23 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ObjGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Opens
variable {Y : Scheme.{u}} {ι : Type u} (U : ι → Y.Opens)
variable (D : (MOD.{u}).DescentData (incl U))

Lean source · statement

theorem preimage_ι_inf_self (O W : Y.Opens) : O.ι ⁻¹ᵁ (W ⊓ O) = O.ι ⁻¹ᵁ W

theorem

compat_of_T

L876 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.AlgebraicGeometry.Scheme.Modules.ObjGlue.compat_of_T

Source context 23 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ObjGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Opens
variable {Y : Scheme.{u}} {ι : Type u} (U : ι → Y.Opens)
variable (D : (MOD.{u}).DescentData (incl U))

Lean source · statement

theorem compat_of_T (W : Y.Opens) (s : ∀ i, Γ(P U D i, W)) (i j : ι)
    (h : T U D i j (U i ⊓ U j) inf_le_left inf_le_right (W ⊓ (U i ⊓ U j)) inf_le_right
        ((Dobj U D i).presheaf.map (homOfLE ((U i).ι.preimage_mono inf_le_left)).op (s i)) =
      (Dobj U D j).presheaf.map (homOfLE ((U j).ι.preimage_mono inf_le_left)).op (s j)) :
    (α U D i j).app W (s i) = (β U D i j).app W (s j)

def

restrictGluedHom

L939 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.AlgebraicGeometry.Scheme.Modules.ObjGlue.restrictGluedHom

Documentation

Restrict the glued sheaf to a covering open and project to its descent component.

Source context 23 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ObjGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Opens
variable {Y : Scheme.{u}} {ι : Type u} (U : ι → Y.Opens)
variable (D : (MOD.{u}).DescentData (incl U))

Lean source · statement

def restrictGluedHom (k : ι) : (glued U D).restrict (incl U k) ⟶ Dobj U D k

theorem

restrictGluedHom_app

L943 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.AlgebraicGeometry.Scheme.Modules.ObjGlue.restrictGluedHom_app

Source context 23 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ObjGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Opens
variable {Y : Scheme.{u}} {ι : Type u} (U : ι → Y.Opens)
variable (D : (MOD.{u}).DescentData (incl U))

Lean source · full declaration

theorem restrictGluedHom_app (k : ι) (V : ((U k : Y.Opens) : Scheme.{u}).Opens)
    (s : compatible U D ((incl U k) ''ᵁ V)) :
    (restrictGluedHom U D k).app V (show Γ((glued U D).restrict (incl U k), V) from s) =
      (Dobj U D k).presheaf.map (eqToHom ((incl U k).preimage_image_eq V).symm).op (s.1 k) := by
  have h := restrictAdjunction_counit_app_app (incl U k) (Dobj U D k) V
  rw [restrictGluedHom, Scheme.Modules.Hom.comp_app]
  erw [h]
  rfl

theorem

restrictGluedHom_app_injective

L952 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.AlgebraicGeometry.Scheme.Modules.ObjGlue.restrictGluedHom_app_injective

Source context 23 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ObjGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Opens
variable {Y : Scheme.{u}} {ι : Type u} (U : ι → Y.Opens)
variable (D : (MOD.{u}).DescentData (incl U))

Lean source · statement

theorem restrictGluedHom_app_injective (k : ι) (V : ((U k : Y.Opens) : Scheme.{u}).Opens) :
    Function.Injective ((restrictGluedHom U D k).app V)

theorem

preimage_incl_inf_self

L964 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.AlgebraicGeometry.Scheme.Modules.ObjGlue.preimage_incl_inf_self

Source context 23 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ObjGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Opens
variable {Y : Scheme.{u}} {ι : Type u} (U : ι → Y.Opens)
variable (D : (MOD.{u}).DescentData (incl U))

Lean source · statement

theorem preimage_incl_inf_self (i : ι) (W : Y.Opens) : (U i).ι ⁻¹ᵁ (W ⊓ U i) = (U i).ι ⁻¹ᵁ W

theorem

restrictGluedHom_app_surjective

L968 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.AlgebraicGeometry.Scheme.Modules.ObjGlue.restrictGluedHom_app_surjective

Source context 23 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ObjGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Opens
variable {Y : Scheme.{u}} {ι : Type u} (U : ι → Y.Opens)
variable (D : (MOD.{u}).DescentData (incl U))

Lean source · statement

theorem restrictGluedHom_app_surjective (k : ι) (V : ((U k : Y.Opens) : Scheme.{u}).Opens) :
    Function.Surjective ((restrictGluedHom U D k).app V)

theorem

isIso_restrictGluedHom

L1011 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.AlgebraicGeometry.Scheme.Modules.ObjGlue.isIso_restrictGluedHom

Source context 23 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ObjGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Opens
variable {Y : Scheme.{u}} {ι : Type u} (U : ι → Y.Opens)
variable (D : (MOD.{u}).DescentData (incl U))

Lean source · statement

theorem isIso_restrictGluedHom (k : ι) : IsIso (restrictGluedHom U D k)

def

gluedIso

L1019 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.AlgebraicGeometry.Scheme.Modules.ObjGlue.gluedIso

Documentation

The isomorphism from the pullback of the glued sheaf to a descent component.

Source context 23 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ObjGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Opens
variable {Y : Scheme.{u}} {ι : Type u} (U : ι → Y.Opens)
variable (D : (MOD.{u}).DescentData (incl U))

Lean source · statement

def gluedIso (k : ι) : (Modules.pullback (incl U k)).obj (glued U D) ≅ Dobj U D k

theorem

image_mono'

L1023 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.AlgebraicGeometry.Scheme.Modules.ObjGlue.image_mono'

Source context 23 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ObjGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Opens
variable {Y : Scheme.{u}} {ι : Type u} (U : ι → Y.Opens)
variable (D : (MOD.{u}).DescentData (incl U))

Lean source · statement

theorem image_mono' {X X' : Scheme.{u}} (f : X ⟶ X') [IsOpenImmersion f] {A B : X.Opens} (h : A ≤
    B) :
    f ''ᵁ A ≤ f ''ᵁ B

theorem

cs_le

L1027 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.AlgebraicGeometry.Scheme.Modules.ObjGlue.cs_le

Source context 23 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ObjGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Opens
variable {Y : Scheme.{u}} {ι : Type u} (U : ι → Y.Opens)
variable (D : (MOD.{u}).DescentData (incl U))

Lean source · statement

theorem cs_le (i j : ι) (V : ((U i ⊓ U j : Y.Opens) : Scheme.{u}).Opens) :
    (p₁ U i j) ''ᵁ V ≤ (U i).ι ⁻¹ᵁ ((U i ⊓ U j).ι ''ᵁ V)

theorem

cs_le'

L1031 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.AlgebraicGeometry.Scheme.Modules.ObjGlue.cs_le'

Source context 23 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ObjGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Opens
variable {Y : Scheme.{u}} {ι : Type u} (U : ι → Y.Opens)
variable (D : (MOD.{u}).DescentData (incl U))

Lean source · statement

theorem cs_le' (i j : ι) (V : ((U i ⊓ U j : Y.Opens) : Scheme.{u}).Opens) :
    (p₂ U i j) ''ᵁ V ≤ (U j).ι ⁻¹ᵁ ((U i ⊓ U j).ι ''ᵁ V)

theorem

comm_sections

L1036 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.AlgebraicGeometry.Scheme.Modules.ObjGlue.comm_sections

Source context 23 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ObjGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Opens
variable {Y : Scheme.{u}} {ι : Type u} (U : ι → Y.Opens)
variable (D : (MOD.{u}).DescentData (incl U))

Lean source · statement

theorem comm_sections (i j : ι) :
    castComp (p₁ U i j) (incl U i) (U i ⊓ U j).ι (Y.homOfLE_ι inf_le_left) (glued U D) ≫
        (restrictFunctor (p₁ U i j)).map (restrictGluedHom U D i) ≫ (ρ U D i j).hom =
      castComp (p₂ U i j) (incl U j) (U i ⊓ U j).ι (Y.homOfLE_ι inf_le_right) (glued U D) ≫
        (restrictFunctor (p₂ U i j)).map (restrictGluedHom U D j)

theorem

pseudo_map_map

L1127 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.AlgebraicGeometry.Scheme.Modules.ObjGlue.pseudo_map_map

Source context 23 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ObjGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Opens
variable {Y : Scheme.{u}} {ι : Type u} (U : ι → Y.Opens)
variable (D : (MOD.{u}).DescentData (incl U))

Lean source · statement

theorem pseudo_map_map {X X' : Scheme.{u}} (f : X ⟶ X')
    {M N : X'.Modules} (ψ : M ⟶ N) {P Q : X.Modules}
    (a : P ⟶ (Modules.pullback f).obj M)
    (b : (Modules.pullback f).obj N ⟶ Q) :
    @Eq (_root_.AlgebraicGeometry.Scheme.Modules.Hom (X := X) P Q)
      (a ≫ (MOD.map f.op.toLoc).toFunctor.map ψ ≫ b)
      (a ≫ (Modules.pullback f).map ψ ≫ b)

theorem

pullback_map_eq

L1135 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.AlgebraicGeometry.Scheme.Modules.ObjGlue.pullback_map_eq

Source context 23 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ObjGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Opens
variable {Y : Scheme.{u}} {ι : Type u} (U : ι → Y.Opens)
variable (D : (MOD.{u}).DescentData (incl U))

Lean source · statement

theorem pullback_map_eq {X X' : Scheme.{u}} (f : X ⟶ X') [IsOpenImmersion f] {M N : X'.Modules} (ψ
    : M ⟶ N) :
    (Modules.pullback f).map ψ = (restrictFunctorIsoPullback f).inv.app M ≫ (restrictFunctor
      f).map ψ ≫
      (restrictFunctorIsoPullback f).hom.app N

theorem

dictM

L1143 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.AlgebraicGeometry.Scheme.Modules.ObjGlue.dictM

Source context 23 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ObjGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Opens
variable {Y : Scheme.{u}} {ι : Type u} (U : ι → Y.Opens)
variable (D : (MOD.{u}).DescentData (incl U))

Lean source · statement

theorem dictM {X₀ X₁ X₂ : Scheme.{u}} (e : X₀ ⟶ X₁) (a : X₁ ⟶ X₂) (a' : X₀ ⟶ X₂) [IsOpenImmersion e]
    [IsOpenImmersion a] [IsOpenImmersion a'] (w : e ≫ a = a') (M : X₂.Modules) :
    (restrictFunctorIsoPullback a').hom.app M ≫
      ((Scheme.Modules.pullbackCongr w.symm).hom.app M ≫ (Scheme.Modules.pullbackComp e a).inv.app
        M) ≫
      (restrictFunctorIsoPullback e).inv.app ((Modules.pullback a).obj M) ≫
      (restrictFunctor e).map ((restrictFunctorIsoPullback a).inv.app M) = castComp e a a' w M

theorem

commZ₀_formal

L1154 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.AlgebraicGeometry.Scheme.Modules.ObjGlue.commZ₀_formal

Source context 23 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ObjGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Opens
variable {Y : Scheme.{u}} {ι : Type u} (U : ι → Y.Opens)
variable (D : (MOD.{u}).DescentData (incl U))

Lean source · statement

theorem commZ₀_formal {X₀ X₁ X₂ S : Scheme.{u}} (p₁ : X₀ ⟶ X₁) (p₂ : X₀ ⟶ X₂) (ι₁ : X₁ ⟶ S) (ι₂ :
    X₂ ⟶ S)
    (q₀ : X₀ ⟶ S) [IsOpenImmersion p₁] [IsOpenImmersion p₂] [IsOpenImmersion ι₁] [IsOpenImmersion
      ι₂]
    [IsOpenImmersion q₀] (w₁ : p₁ ≫ ι₁ = q₀) (w₂ : p₂ ≫ ι₂ = q₀) (G : S.Modules) (M₁ : X₁.Modules)
    (M₂ : X₂.Modules) (r₁ : (restrictFunctor ι₁).obj G ⟶ M₁) (r₂ : (restrictFunctor ι₂).obj G ⟶ M₂)
    (ρ₀ : (restrictFunctor p₁).obj M₁ ⟶ (restrictFunctor p₂).obj M₂)
    (φ₀ : (Modules.pullback p₁).obj M₁ ⟶ (Modules.pullback p₂).obj M₂)
    (hφ₀ : (restrictFunctorIsoPullback p₁).hom.app M₁ ≫ φ₀ ≫ (restrictFunctorIsoPullback
      p₂).inv.app M₂ = ρ₀)
    (cs : castComp p₁ ι₁ q₀ w₁ G ≫ (restrictFunctor p₁).map r₁ ≫ ρ₀ =
      castComp p₂ ι₂ q₀ w₂ G ≫ (restrictFunctor p₂).map r₂) :
    (Modules.pullback p₁).map ((restrictFunctorIsoPullback ι₁).inv.app G ≫ r₁) ≫ φ₀ =
      (((Scheme.Modules.pullbackComp p₁ ι₁).hom.app G ≫ (Scheme.Modules.pullbackCongr w₁).hom.app
        G) ≫
        (Scheme.Modules.pullbackCongr w₂.symm).hom.app G ≫ (Scheme.Modules.pullbackComp p₂
          ι₂).inv.app G) ≫
      (Modules.pullback p₂).map ((restrictFunctorIsoPullback ι₂).inv.app G ≫ r₂)

theorem

gluedIso_hom

L1185 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.AlgebraicGeometry.Scheme.Modules.ObjGlue.gluedIso_hom

Source context 23 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ObjGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Opens
variable {Y : Scheme.{u}} {ι : Type u} (U : ι → Y.Opens)
variable (D : (MOD.{u}).DescentData (incl U))

Lean source · statement

theorem gluedIso_hom (k : ι) : (gluedIso U D k).hom =
    (restrictFunctorIsoPullback (incl U k)).inv.app (glued U D) ≫ restrictGluedHom U D k

theorem

comm_of_restriction_square

L1189 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.AlgebraicGeometry.Scheme.Modules.ObjGlue.comm_of_restriction_square

Source context 23 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ObjGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Opens
variable {Y : Scheme.{u}} {ι : Type u} (U : ι → Y.Opens)
variable (D : (MOD.{u}).DescentData (incl U))

Lean source · statement

theorem comm_of_restriction_square {κ : Type u} {S Z : Scheme.{u}}
    {X : κ → Scheme.{u}} (f : ∀ k, X k ⟶ S) (E : MOD.DescentData f)
    (i j : κ) (q : Z ⟶ S) (a : Z ⟶ X i) (b : Z ⟶ X j)
    [IsOpenImmersion q] [IsOpenImmersion a] [IsOpenImmersion b]
    [IsOpenImmersion (f i)] [IsOpenImmersion (f j)]
    (wa : a ≫ f i = q) (wb : b ≫ f j = q) (G : S.Modules)
    (ei : (Modules.pullback (f i)).obj G ≅ E.obj i)
    (ej : (Modules.pullback (f j)).obj G ≅ E.obj j)
    (ri : (restrictFunctor (f i)).obj G ⟶ E.obj i)
    (rj : (restrictFunctor (f j)).obj G ⟶ E.obj j)
    (hei : ei.hom = (restrictFunctorIsoPullback (f i)).inv.app G ≫ ri)
    (hej : ej.hom = (restrictFunctorIsoPullback (f j)).inv.app G ≫ rj)
    (rho : (restrictFunctor a).obj (E.obj i) ⟶ (restrictFunctor b).obj (E.obj j))
    (htrans : (restrictFunctorIsoPullback a).hom.app (E.obj i) ≫
      E.hom q a b wa wb ≫ (restrictFunctorIsoPullback b).inv.app (E.obj j) = rho)
    (cs : castComp a (f i) q wa G ≫ (restrictFunctor a).map ri ≫ rho =
      castComp b (f j) q wb G ≫ (restrictFunctor b).map rj) :
    @Eq (_root_.AlgebraicGeometry.Scheme.Modules.Hom (X := Z)
      ((Modules.pullback a).obj ((Modules.pullback (f i)).obj G))
      ((Modules.pullback b).obj (E.obj j)))
      ((MOD.map a.op.toLoc).toFunctor.map ei.hom ≫ E.hom q a b wa wb)
      (((MOD.toDescentData f).obj G).hom q a b wa wb ≫
        (MOD.map b.op.toLoc).toFunctor.map ej.hom)

theorem

commZ₀

L1258 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.AlgebraicGeometry.Scheme.Modules.ObjGlue.commZ₀

Source context 23 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ObjGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Opens
variable {Y : Scheme.{u}} {ι : Type u} (U : ι → Y.Opens)
variable (D : (MOD.{u}).DescentData (incl U))

Lean source · statement

theorem commZ₀ (i j : ι) :
    @Eq (_root_.AlgebraicGeometry.Scheme.Modules.Hom
      (X := ((U i ⊓ U j : Y.Opens) : Scheme.{u}))
      ((Modules.pullback (p₁ U i j)).obj
        ((Modules.pullback (incl U i)).obj (glued U D)))
      ((Modules.pullback (p₂ U i j)).obj (Dobj U D j)))
      ((MOD.map (p₁ U i j).op.toLoc).toFunctor.map (gluedIso U D i).hom ≫
        D.hom (U i ⊓ U j).ι (p₁ U i j) (p₂ U i j)
          (Y.homOfLE_ι inf_le_left) (Y.homOfLE_ι inf_le_right))
      (((MOD.toDescentData (incl U)).obj (glued U D)).hom
          (U i ⊓ U j).ι (p₁ U i j) (p₂ U i j)
          (Y.homOfLE_ι inf_le_left) (Y.homOfLE_ι inf_le_right) ≫
        (MOD.map (p₂ U i j).op.toLoc).toFunctor.map (gluedIso U D j).hom)

theorem

gluedIso_comm

L1279 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.AlgebraicGeometry.Scheme.Modules.ObjGlue.gluedIso_comm

Source context 23 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ObjGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Opens
variable {Y : Scheme.{u}} {ι : Type u} (U : ι → Y.Opens)
variable (D : (MOD.{u}).DescentData (incl U))

Lean source · statement

theorem gluedIso_comm ⦃Z : Scheme.{u}⦄ (q : Z ⟶ Y) ⦃i j : ι⦄ (f₁ : Z ⟶ (U i : Scheme.{u})) (f₂ : Z
    ⟶ (U j : Scheme.{u}))
    (h₁ : f₁ ≫ incl U i = q) (h₂ : f₂ ≫ incl U j = q) :
    (MOD.map f₁.op.toLoc).toFunctor.map (gluedIso U D i).hom ≫ D.hom q f₁ f₂ h₁ h₂ =
      ((MOD.toDescentData (incl U)).obj (glued U D)).hom q f₁ f₂ h₁ h₂ ≫
        (MOD.map f₂.op.toLoc).toFunctor.map (gluedIso U D j).hom

def

isoDescentData

L1305 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.AlgebraicGeometry.Scheme.Modules.ObjGlue.isoDescentData

Documentation

The descent-data isomorphism between the glued sheaf and the prescribed datum.

Source context 23 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ObjGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Opens
variable {Y : Scheme.{u}} {ι : Type u} (U : ι → Y.Opens)
variable (D : (MOD.{u}).DescentData (incl U))

Lean source · statement

def isoDescentData : (MOD.toDescentData (incl U)).obj (glued U D) ≅ D

theorem

essSurj_incl

L1310 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.AlgebraicGeometry.Scheme.Modules.ObjGlue.essSurj_incl

Source context 23 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ObjGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Opens
variable {Y : Scheme.{u}} {ι : Type u} (U : ι → Y.Opens)
variable (D : (MOD.{u}).DescentData (incl U))

Lean source · statement

theorem essSurj_incl : (MOD.toDescentData (incl U)).EssSurj

theorem

toDescentData_essSurj_of_openCover'

L1315 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover.AlgebraicGeometry.Scheme.Modules.ObjGlue.toDescentData_essSurj_of_openCover'

Source context 20 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ObjGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry

Lean source · statement

theorem toDescentData_essSurj_of_openCover'
    {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) :
    (MOD.toDescentData g).EssSurj

theorem

toDescentData_essSurj_of_openCover

L1326 ↗

AlgebraicGeometry.Scheme.Modules.toDescentData_essSurj_of_openCover

Source context 11 commands

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

open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_essSurj_of_openCover
universe v v' u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules in

Lean source · statement

theorem _root_.AlgebraicGeometry.Scheme.Modules.toDescentData_essSurj_of_openCover
    {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) :
    (((Scheme.Modules.pseudofunctor.{u}).comp Bicategory.Adj.forget₁).toDescentData g).EssSurj

Module documentation

Declarations