NYLL
Module

Scheme_Modules_toDescentData_map_bijective_of_openCover.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_toDescentData_map_bijective_of_openCover
59 declarations indexed from sourceView source ↗

Module documentation

Descent of module morphisms along an open cover

Compatible module morphisms on open charts glue uniquely to a morphism on the scheme. The restriction and pullback comparisons identify this gluing with the module pseudofunctor's descent-data map, which is bijective for an open cover.

Imports43
  • Mathlib.Algebra.Category.Grp.Basic
  • Mathlib.Algebra.Category.Grp.Limits
  • Mathlib.Algebra.Category.ModuleCat.Presheaf
  • Mathlib.Algebra.Category.ModuleCat.Sheaf
  • Mathlib.Algebra.Group.Basic
  • Mathlib.Algebra.Group.Hom.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.Pseudofunctor
  • Mathlib.CategoryTheory.Bicategory.LocallyDiscrete
  • Mathlib.CategoryTheory.Category.Basic
  • Mathlib.CategoryTheory.Category.Cat
  • Mathlib.CategoryTheory.Category.Preorder
  • Mathlib.CategoryTheory.Comma.Over.Basic
  • Mathlib.CategoryTheory.ConcreteCategory.Basic
  • Mathlib.CategoryTheory.ConcreteCategory.Forget
  • Mathlib.CategoryTheory.Elementwise
  • Mathlib.CategoryTheory.EqToHom
  • Mathlib.CategoryTheory.Functor.Basic
  • Mathlib.CategoryTheory.Functor.Category
  • 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.IsSheafFor
  • Mathlib.Data.FunLike.Basic
  • Mathlib.Data.Set.Image
  • Mathlib.Order.Lattice
  • Mathlib.Topology.Category.TopCat.Opens
  • Mathlib.Topology.Defs.Induced
  • Mathlib.Topology.Sets.Opens
  • Mathlib.Topology.Sheaves.Presheaf
  • Mathlib.Topology.Sheaves.Sheaf
  • Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing
Imported by7

Declarations

theorem

presheaf_map_eq

L89 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar.presheaf_map_eq
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_toDescentData_map_bijective_of_openCover
universe 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 HomZar
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
Lean source · statement
theorem presheaf_map_eq {Y : Scheme.{u}} (M : Y.Modules) {A B : Y.Opens} (p q : op A ⟶ op B) :
    M.presheaf.map p = M.presheaf.map q
theorem

app_naturality

L94 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar.app_naturality
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_toDescentData_map_bijective_of_openCover
universe 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 HomZar
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
Lean source · statement
theorem app_naturality {Y : Scheme.{u}} {M N : Y.Modules} (φ : M ⟶ N) {U V : Y.Opens}
  (i : op U ⟶ op V) :
    M.presheaf.map i ≫ φ.app V = φ.app U ≫ N.presheaf.map i
theorem

D3_LA

L104 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar.D3_LA
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_toDescentData_map_bijective_of_openCover
universe 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 HomZar
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section D3
variable {X₀ X₁ Y : Scheme.{u}} (h : X₀ ⟶ X₁) (g : X₁ ⟶ Y) [IsOpenImmersion h]
  [IsOpenImmersion g] (M : Y.Modules)
Lean source · statement
theorem D3_LA (W : Y.Opens) :
    (((((restrictAdjunction g).unit.app M ≫ (pushforward g).map
      ((restrictFunctorIsoPullback g).hom.app M)) ≫
      (pushforward g).map ((restrictAdjunction h).unit.app ((Modules.pullback g).obj M) ≫
        (pushforward h).map ((restrictFunctorIsoPullback h).hom.app
          ((Modules.pullback g).obj M)))) ≫
      (pushforwardComp h g).hom.app _) ≫
      (pushforward (h ≫ g)).map ((pullbackComp h g).hom.app M)).app W =
    (((M.presheaf.map (homOfLE (g.image_preimage_le W)).op ≫
      ((restrictFunctorIsoPullback g).hom.app M).app (g ⁻¹ᵁ W)) ≫
      (((Modules.pullback g).obj M).presheaf.map (homOfLE (h.image_preimage_le (g ⁻¹ᵁ W))).op ≫
        ((restrictFunctorIsoPullback h).hom.app ((Modules.pullback g).obj M)).app (h ⁻¹ᵁ
          (g ⁻¹ᵁ W)))) ≫
      𝟙 _) ≫
      ((pullbackComp h g).hom.app M).app ((h ≫ g) ⁻¹ᵁ W)
theorem

D3_RA

L121 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar.D3_RA
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_toDescentData_map_bijective_of_openCover
universe 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 HomZar
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section D3
variable {X₀ X₁ Y : Scheme.{u}} (h : X₀ ⟶ X₁) (g : X₁ ⟶ Y) [IsOpenImmersion h]
  [IsOpenImmersion g] (M : Y.Modules)
Lean source · statement
theorem D3_RA (W : Y.Opens) :
    ((restrictAdjunction (h ≫ g)).unit.app M ≫ (pushforward (h ≫ g)).map
      ((restrictFunctorComp h g).hom.app M ≫ (restrictFunctor h).map
        ((restrictFunctorIsoPullback g).hom.app M) ≫
        (restrictFunctorIsoPullback h).hom.app ((Modules.pullback g).obj M) ≫
          (pullbackComp h g).hom.app M)).app W =
    M.presheaf.map (homOfLE ((h ≫ g).image_preimage_le W)).op ≫
      (((restrictFunctorComp h g).hom.app M).app ((h ≫ g) ⁻¹ᵁ W) ≫
        ((restrictFunctorIsoPullback g).hom.app M).app (h ''ᵁ ((h ≫ g) ⁻¹ᵁ W)) ≫
        ((restrictFunctorIsoPullback h).hom.app ((Modules.pullback g).obj M)).app ((h ≫ g) ⁻¹ᵁ W) ≫
        ((pullbackComp h g).hom.app M).app ((h ≫ g) ⁻¹ᵁ W))
theorem

D3_core

L135 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar.D3_core
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_toDescentData_map_bijective_of_openCover
universe 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 HomZar
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section D3
variable {X₀ X₁ Y : Scheme.{u}} (h : X₀ ⟶ X₁) (g : X₁ ⟶ Y) [IsOpenImmersion h]
  [IsOpenImmersion g] (M : Y.Modules)
Lean source · statement
theorem D3_core :
    ((((restrictAdjunction g).unit.app M ≫ (pushforward g).map
      ((restrictFunctorIsoPullback g).hom.app M)) ≫
      (pushforward g).map ((restrictAdjunction h).unit.app ((Modules.pullback g).obj M) ≫
        (pushforward h).map ((restrictFunctorIsoPullback h).hom.app
          ((Modules.pullback g).obj M)))) ≫
      (pushforwardComp h g).hom.app _) ≫
      (pushforward (h ≫ g)).map ((pullbackComp h g).hom.app M) =
    (restrictAdjunction (h ≫ g)).unit.app M ≫ (pushforward (h ≫ g)).map
      ((restrictFunctorComp h g).hom.app M ≫ (restrictFunctor h).map
        ((restrictFunctorIsoPullback g).hom.app M) ≫
        (restrictFunctorIsoPullback h).hom.app ((Modules.pullback g).obj M) ≫
          (pullbackComp h g).hom.app M)
theorem

restrictFunctorIsoPullback_comp_hom_app

L182 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar.restrictFunctorIsoPullback_comp_hom_app
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_toDescentData_map_bijective_of_openCover
universe 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 HomZar
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section D3
variable {X₀ X₁ Y : Scheme.{u}} (h : X₀ ⟶ X₁) (g : X₁ ⟶ Y) [IsOpenImmersion h]
  [IsOpenImmersion g] (M : Y.Modules)
Lean source · statement
theorem restrictFunctorIsoPullback_comp_hom_app :
    (restrictFunctorIsoPullback (h ≫ g)).hom.app M =
      (restrictFunctorComp h g).hom.app M ≫ (restrictFunctor h).map
        ((restrictFunctorIsoPullback g).hom.app M) ≫
        (restrictFunctorIsoPullback h).hom.app ((Modules.pullback g).obj M) ≫
          (pullbackComp h g).hom.app M
abbrev

Mdl

L215 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar.Mdl
Documentation

The scheme-module pseudofunctor with its adjunction data forgotten.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_toDescentData_map_bijective_of_openCover
universe 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 HomZar
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
Lean source · statement
abbrev Mdl : Pseudofunctor (LocallyDiscrete Scheme.{u}ᵒᵖ) Cat
theorem

Mdl_keyMC

L218 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar.Mdl_keyMC
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_toDescentData_map_bijective_of_openCover
universe 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 HomZar
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
Lean source · statement
theorem Mdl_keyMC {a b d : LocallyDiscrete Scheme.{u}ᵒᵖ} (u' : a ⟶ b) (v' : b ⟶ d) (M : Mdl.obj a) :
    (Mdl.mapComp' u' v' (u' ≫ v') rfl).hom.toNatTrans.app M =
      (Mdl.mapComp u' v').hom.toNatTrans.app M
theorem

Mdl_keyMC_inv

L223 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar.Mdl_keyMC_inv
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_toDescentData_map_bijective_of_openCover
universe 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 HomZar
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
Lean source · statement
theorem Mdl_keyMC_inv {a b d : LocallyDiscrete Scheme.{u}ᵒᵖ} (u' : a ⟶ b) (v' : b ⟶ d)
  (M : Mdl.obj a) :
    (Mdl.mapComp' u' v' (u' ≫ v') rfl).inv.toNatTrans.app M =
      (Mdl.mapComp u' v').inv.toNatTrans.app M
theorem

Mdl_mapComp'_hom_app

L229 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar.Mdl_mapComp'_hom_app
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_toDescentData_map_bijective_of_openCover
universe 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 HomZar
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
Lean source · full declaration
theorem Mdl_mapComp'_hom_app {X₀ X₁ Y : Scheme.{u}} (f : X₀ ⟶ X₁) (g : X₁ ⟶ Y) (L : Y.Modules)
    (fg : X₀ ⟶ Y) (hfg : f ≫ g = fg) :
    (Mdl.mapComp' g.op.toLoc f.op.toLoc fg.op.toLoc (by rw [← hfg]; rfl)).hom.toNatTrans.app L =
    (Scheme.Modules.pullbackCongr hfg.symm).hom.app L ≫ (Scheme.Modules.pullbackComp f
      g).inv.app L := by
  subst hfg
  simp only [Scheme.Modules.pullbackCongr, eqToIso_refl, Iso.refl_hom, NatTrans.id_app,
    Category.id_comp]
  exact Mdl_keyMC g.op.toLoc f.op.toLoc L
theorem

Mdl_mapComp'_inv_app

L239 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar.Mdl_mapComp'_inv_app
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_toDescentData_map_bijective_of_openCover
universe 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 HomZar
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
Lean source · full declaration
theorem Mdl_mapComp'_inv_app {X₀ X₁ Y : Scheme.{u}} (f : X₀ ⟶ X₁) (g : X₁ ⟶ Y) (L : Y.Modules)
    (fg : X₀ ⟶ Y) (hfg : f ≫ g = fg) :
    (Mdl.mapComp' g.op.toLoc f.op.toLoc fg.op.toLoc (by rw [← hfg]; rfl)).inv.toNatTrans.app L =
    (Scheme.Modules.pullbackComp f g).hom.app L ≫ (Scheme.Modules.pullbackCongr hfg).hom.app L := by
  subst hfg
  simp only [Scheme.Modules.pullbackCongr, eqToIso_refl, Iso.refl_hom, NatTrans.id_app,
    Category.comp_id]
  exact Mdl_keyMC_inv g.op.toLoc f.op.toLoc L
theorem

pullHom_eq

L248 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar.pullHom_eq
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_toDescentData_map_bijective_of_openCover
universe 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 HomZar
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
Lean source · statement
theorem pullHom_eq {Z' Z X₁ X₂ : Scheme.{u}} (e : Z' ⟶ Z) (f₁ : Z ⟶ X₁) (f₂ : Z ⟶ X₂)
    (M₁ : X₁.Modules) (M₂ : X₂.Modules) (φ : (Modules.pullback f₁).obj M₁ ⟶
      (Modules.pullback f₂).obj M₂) :
    Pseudofunctor.LocallyDiscreteOpToCat.pullHom (F := Mdl)
        (X₁ := X₁) (X₂ := X₂) (M₁ := M₁) (M₂ := M₂) (f₁ := f₁) (f₂ := f₂) φ e (e ≫ f₁) (e ≫
          f₂) rfl rfl =
      (pullbackComp e f₁).inv.app M₁ ≫ (Modules.pullback e).map φ ≫
        (pullbackComp e f₂).hom.app M₂
theorem

restrictFunctorCongr_rfl_hom_app

L263 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar.restrictFunctorCongr_rfl_hom_app
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_toDescentData_map_bijective_of_openCover
universe 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 HomZar
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
Lean source · statement
theorem restrictFunctorCongr_rfl_hom_app {X' Y : Scheme.{u}} (f : X' ⟶ Y) [IsOpenImmersion f]
  (M : Y.Modules) :
    (restrictFunctorCongr (rfl : f = f)).hom.app M = 𝟙 _
theorem

restrictFunctorCongr_rfl_inv_app

L272 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar.restrictFunctorCongr_rfl_inv_app
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_toDescentData_map_bijective_of_openCover
universe 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 HomZar
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
Lean source · statement
theorem restrictFunctorCongr_rfl_inv_app {X' Y : Scheme.{u}} (f : X' ⟶ Y) [IsOpenImmersion f]
  (M : Y.Modules) :
    (restrictFunctorCongr (rfl : f = f)).inv.app M = 𝟙 _
theorem

CRUX_LA

L288 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar.CRUX_LA
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_toDescentData_map_bijective_of_openCover
universe 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 HomZar
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section CruxApp
variable {Z' Z X₁ X₂ : Scheme.{u}} (e : Z' ⟶ Z) (f₁ : Z ⟶ X₁) (f₂ : Z ⟶ X₂)
    [IsOpenImmersion e] [IsOpenImmersion f₁] [IsOpenImmersion f₂]
    (M₁ : X₁.Modules) (M₂ : X₂.Modules) (φ : (Modules.pullback f₁).obj M₁ ⟶
      (Modules.pullback f₂).obj M₂)
Lean source · statement
theorem CRUX_LA (U : Z'.Opens) :
    (((restrictFunctorComp e f₁).hom.app M₁ ≫ (restrictFunctor e).map
      ((restrictFunctorIsoPullback f₁).hom.app M₁) ≫
        (restrictFunctorIsoPullback e).hom.app ((Modules.pullback f₁).obj M₁) ≫
          (pullbackComp e f₁).hom.app M₁) ≫
      ((pullbackComp e f₁).inv.app M₁ ≫ (Modules.pullback e).map φ ≫
        (pullbackComp e f₂).hom.app M₂) ≫
      ((pullbackComp e f₂).inv.app M₂ ≫ (restrictFunctorIsoPullback e).inv.app
        ((Modules.pullback f₂).obj M₂) ≫
        (restrictFunctor e).map ((restrictFunctorIsoPullback f₂).inv.app M₂) ≫
          (restrictFunctorComp e f₂).inv.app M₂)).app U =
    ((restrictFunctorComp e f₁).hom.app M₁).app U ≫
      ((restrictFunctorIsoPullback f₁).hom.app M₁).app (e ''ᵁ U) ≫
      ((restrictFunctorIsoPullback e).hom.app ((Modules.pullback f₁).obj M₁)).app U ≫
      (((pullbackComp e f₁).hom.app M₁).app U ≫ ((pullbackComp e f₁).inv.app M₁).app U) ≫
      ((Modules.pullback e).map φ).app U ≫ ((pullbackComp e f₂).hom.app M₂).app U ≫
      ((pullbackComp e f₂).inv.app M₂).app U ≫
      ((restrictFunctorIsoPullback e).inv.app ((Modules.pullback f₂).obj M₂)).app U ≫
      ((restrictFunctorIsoPullback f₂).inv.app M₂).app (e ''ᵁ U) ≫
      ((restrictFunctorComp e f₂).inv.app M₂).app U
theorem

CRUX_RA

L334 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar.CRUX_RA
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_toDescentData_map_bijective_of_openCover
universe 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 HomZar
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section CruxApp
variable {Z' Z X₁ X₂ : Scheme.{u}} (e : Z' ⟶ Z) (f₁ : Z ⟶ X₁) (f₂ : Z ⟶ X₂)
    [IsOpenImmersion e] [IsOpenImmersion f₁] [IsOpenImmersion f₂]
    (M₁ : X₁.Modules) (M₂ : X₂.Modules) (φ : (Modules.pullback f₁).obj M₁ ⟶
      (Modules.pullback f₂).obj M₂)
Lean source · statement
theorem CRUX_RA (U : Z'.Opens) :
    ((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₂).app U =
    ((restrictFunctorComp e f₁).hom.app M₁).app U ≫
      ((restrictFunctorIsoPullback f₁).hom.app M₁).app (e ''ᵁ U) ≫ φ.app (e ''ᵁ U) ≫
      ((restrictFunctorIsoPullback f₂).inv.app M₂).app (e ''ᵁ U) ≫
      ((restrictFunctorComp e f₂).inv.app M₂).app U
theorem

restrictFunctorIsoPullback_conj_pullHom

L347 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar.restrictFunctorIsoPullback_conj_pullHom
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_toDescentData_map_bijective_of_openCover
universe 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 HomZar
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
Lean source · statement
theorem restrictFunctorIsoPullback_conj_pullHom {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) (φ : (Modules.pullback f₁).obj M₁ ⟶
      (Modules.pullback f₂).obj M₂) :
    (restrictFunctorIsoPullback gf₁).hom.app M₁ ≫
      (Pseudofunctor.LocallyDiscreteOpToCat.pullHom (F := Mdl)
        (X₁ := X₁) (X₂ := X₂) (M₁ := M₁) (M₂ := M₂) (f₁ := f₁) (f₂ := f₂) φ e gf₁ gf₂ h₁ h₂ :
        (Modules.pullback gf₁).obj M₁ ⟶ (Modules.pullback gf₂).obj M₂) ≫
      (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₂
def

toRestrict

L419 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar.toRestrict
Documentation

Transport a pullback-module morphism to the corresponding restrictions.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_toDescentData_map_bijective_of_openCover
universe 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 HomZar
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
Lean source · statement
def toRestrict {Y : Scheme.{u}} (L₁ L₂ : Y.Modules) {X' : Scheme.{u}}
  (g : X' ⟶ Y) [IsOpenImmersion g]
    (θ : (Modules.pullback g).obj L₁ ⟶ (Modules.pullback g).obj L₂) : L₁.restrict g ⟶
      L₂.restrict g
theorem

toRestrict_injective

L425 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar.toRestrict_injective
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_toDescentData_map_bijective_of_openCover
universe 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 HomZar
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
Lean source · statement
theorem toRestrict_injective {Y : Scheme.{u}} (L₁ L₂ : Y.Modules) {X' : Scheme.{u}}
  (g : X' ⟶ Y) [IsOpenImmersion g] :
    Function.Injective (toRestrict L₁ L₂ g)
theorem

toRestrict_map

L431 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar.toRestrict_map
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_toDescentData_map_bijective_of_openCover
universe 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 HomZar
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
Lean source · statement
theorem toRestrict_map {Y : Scheme.{u}} (L₁ L₂ : Y.Modules) {X' : Scheme.{u}} (g : X' ⟶ Y)
  [IsOpenImmersion g]
    (t : L₁ ⟶ L₂) : toRestrict L₁ L₂ g ((Modules.pullback g).map t) =
      (restrictFunctor g).map t
theorem

toRestrict_pullHom

L437 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar.toRestrict_pullHom
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_toDescentData_map_bijective_of_openCover
universe 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 HomZar
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
Lean source · statement
theorem toRestrict_pullHom {Y : Scheme.{u}} (L₁ L₂ : Y.Modules) {X₀ X₁ : Scheme.{u}}
  (h : X₀ ⟶ X₁) (g : X₁ ⟶ Y)
    (k : X₀ ⟶ Y) [IsOpenImmersion h] [IsOpenImmersion g] [IsOpenImmersion k] (hk : h ≫ g = k)
    (θ : (Modules.pullback g).obj L₁ ⟶ (Modules.pullback g).obj L₂) :
    toRestrict L₁ L₂ k (Pseudofunctor.LocallyDiscreteOpToCat.pullHom (F := Mdl)
        (X₁ := Y) (X₂ := Y) (M₁ := L₁) (M₂ := L₂) (f₁ := g) (f₂ := g) θ h k k hk hk) =
      (restrictFunctorCongr hk.symm).hom.app L₁ ≫ (restrictFunctorComp h g).hom.app L₁ ≫
        (restrictFunctor h).map (toRestrict L₁ L₂ g θ) ≫
          (restrictFunctorComp h g).inv.app L₂ ≫ (restrictFunctorCongr hk).hom.app L₂
theorem

mapEq

L453 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar.mapEq
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_toDescentData_map_bijective_of_openCover
universe 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 HomZar
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Elementwise
variable {Y : Scheme.{u}}
Lean source · statement
theorem mapEq (L : Y.Modules) {A B : Y.Opens} (p q : op A ⟶ op B) (x : Γ(L, A)) :
    L.presheaf.map p x = L.presheaf.map q x
theorem

map_map

L457 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar.map_map
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_toDescentData_map_bijective_of_openCover
universe 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 HomZar
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Elementwise
variable {Y : Scheme.{u}}
Lean source · statement
theorem map_map (L : Y.Modules) {A B C : Y.Opens} (p : op A ⟶ op B) (q : op B ⟶ op C)
  (x : Γ(L, A)) :
    L.presheaf.map q (L.presheaf.map p x) = L.presheaf.map (p ≫ q) x
theorem

map_id'

L462 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar.map_id'
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_toDescentData_map_bijective_of_openCover
universe 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 HomZar
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Elementwise
variable {Y : Scheme.{u}}
Lean source · statement
theorem map_id' (L : Y.Modules) {A : Y.Opens} (p : op A ⟶ op A) (x : Γ(L,
  A)) : L.presheaf.map p x = x
theorem

app_naturality_apply

L466 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar.app_naturality_apply
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_toDescentData_map_bijective_of_openCover
universe 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 HomZar
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Elementwise
variable {Y : Scheme.{u}}
Lean source · statement
theorem app_naturality_apply {M N : Y.Modules} (φ : M ⟶ N) {U V : Y.Opens} (i : op U ⟶ op V)
  (x : Γ(M, U)) :
    φ.app V (M.presheaf.map i x) = N.presheaf.map i (φ.app U x)
theorem

restrict_naturality_apply

L472 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar.restrict_naturality_apply
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_toDescentData_map_bijective_of_openCover
universe 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 HomZar
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Elementwise
variable {Y : Scheme.{u}}
Lean source · statement
theorem restrict_naturality_apply {X' : Scheme.{u}} (f : X' ⟶ Y) [IsOpenImmersion f]
  {M N : Y.Modules}
    (φ : M.restrict f ⟶ N.restrict f) {V V' : X'.Opens} (ρ : V' ⟶ V) (m : Γ(M, f ''ᵁ V)) :
    φ.app V' (M.presheaf.map (f.opensFunctor.map ρ).op m) = N.presheaf.map
      (f.opensFunctor.map ρ).op (φ.app V m)
theorem

restrict_app_smul

L479 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar.restrict_app_smul
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_toDescentData_map_bijective_of_openCover
universe 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 HomZar
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Elementwise
variable {Y : Scheme.{u}}
Lean source · statement
theorem restrict_app_smul {X' : Scheme.{u}} (f : X' ⟶ Y) [IsOpenImmersion f] {M N : Y.Modules}
    (φ : M.restrict f ⟶ N.restrict f) (V : X'.Opens) (r : Γ(Y, f ''ᵁ V)) (m : Γ(M, f ''ᵁ V)) :
    φ.app V (r • m) = HSMul.hSMul (α := Γ(Y, f ''ᵁ V)) (β := Γ(N, f ''ᵁ V)) r (φ.app V m)
def

Compatible

L497 ↗
AlgebraicGeometry.Scheme.Modules.HomZar.Compatible
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_toDescentData_map_bijective_of_openCover
universe 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 HomZar
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Glue
variable {Y : Scheme.{u}} {ι : Type v} {X : ι → Scheme.{u}} (f : ∀ i, X i ⟶ Y) [∀ i,
  IsOpenImmersion (f i)]
  (L₁ L₂ : Y.Modules)
Lean source · statement
def _root_.AlgebraicGeometry.Scheme.Modules.HomZar.Compatible (ψ : ∀ i, L₁.restrict
  (f i) ⟶ L₂.restrict (f i)) : Prop
theorem

image_preimage_eq_of_le

L503 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar.image_preimage_eq_of_le
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_toDescentData_map_bijective_of_openCover
universe 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 HomZar
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Glue
variable {Y : Scheme.{u}} {ι : Type v} {X : ι → Scheme.{u}} (f : ∀ i, X i ⟶ Y) [∀ i,
  IsOpenImmersion (f i)]
  (L₁ L₂ : Y.Modules)
open _root_.AlgebraicGeometry.Scheme.Modules.HomZar
Lean source · statement
theorem image_preimage_eq_of_le (i : ι) (O : Y.Opens) (hO : O ≤ (f i).opensRange) : (f i) ''ᵁ
  (f i) ⁻¹ᵁ O = O
def

Ψ

L508 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar.Ψ
Documentation

The local morphism on an open contained in the image of a cover member.

Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_toDescentData_map_bijective_of_openCover
universe 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 HomZar
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Glue
variable {Y : Scheme.{u}} {ι : Type v} {X : ι → Scheme.{u}} (f : ∀ i, X i ⟶ Y) [∀ i,
  IsOpenImmersion (f i)]
  (L₁ L₂ : Y.Modules)
open _root_.AlgebraicGeometry.Scheme.Modules.HomZar
Lean source · statement
def Ψ (ψ : ∀ i, L₁.restrict (f i) ⟶ L₂.restrict (f i)) (i : ι) (O : Y.Opens)
    (hO : O ≤ (f i).opensRange) : Γ(L₁, O) ⟶ Γ(L₂, O)
theorem

Ψ_apply

L515 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar.Ψ_apply
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_toDescentData_map_bijective_of_openCover
universe 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 HomZar
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Glue
variable {Y : Scheme.{u}} {ι : Type v} {X : ι → Scheme.{u}} (f : ∀ i, X i ⟶ Y) [∀ i,
  IsOpenImmersion (f i)]
  (L₁ L₂ : Y.Modules)
open _root_.AlgebraicGeometry.Scheme.Modules.HomZar
variable {f L₁ L₂}
Lean source · statement
theorem Ψ_apply (ψ : ∀ i, L₁.restrict (f i) ⟶ L₂.restrict (f i)) (i : ι) (O : Y.Opens)
    (hO : O ≤ (f i).opensRange) (s : Γ(L₁, O)) :
    Ψ f L₁ L₂ ψ i O hO s = L₂.presheaf.map (eqToHom (image_preimage_eq_of_le f i O hO).symm).op
      ((ψ i).app ((f i) ⁻¹ᵁ O) (L₁.presheaf.map (eqToHom
        (image_preimage_eq_of_le f i O hO)).op s))
theorem

Ψ_res

L523 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar.Ψ_res
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_toDescentData_map_bijective_of_openCover
universe 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 HomZar
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Glue
variable {Y : Scheme.{u}} {ι : Type v} {X : ι → Scheme.{u}} (f : ∀ i, X i ⟶ Y) [∀ i,
  IsOpenImmersion (f i)]
  (L₁ L₂ : Y.Modules)
open _root_.AlgebraicGeometry.Scheme.Modules.HomZar
variable {f L₁ L₂}
Lean source · statement
theorem Ψ_res (ψ : ∀ i, L₁.restrict (f i) ⟶ L₂.restrict (f i)) (i : ι) (O O' : Y.Opens)
    (hO : O ≤ (f i).opensRange) (hO' : O' ≤ (f i).opensRange) (hle : O' ≤ O) (s : Γ(L₁, O)) :
    L₂.presheaf.map (homOfLE hle).op (Ψ f L₁ L₂ ψ i O hO s) = Ψ f L₁ L₂ ψ i O' hO'
      (L₁.presheaf.map (homOfLE hle).op s)
theorem

Ψ_compat

L560 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar.Ψ_compat
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_toDescentData_map_bijective_of_openCover
universe 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 HomZar
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Glue
variable {Y : Scheme.{u}} {ι : Type v} {X : ι → Scheme.{u}} (f : ∀ i, X i ⟶ Y) [∀ i,
  IsOpenImmersion (f i)]
  (L₁ L₂ : Y.Modules)
open _root_.AlgebraicGeometry.Scheme.Modules.HomZar
variable {f L₁ L₂}
Lean source · statement
theorem Ψ_compat (ψ : ∀ i, L₁.restrict (f i) ⟶ L₂.restrict (f i)) (hψ : Compatible f L₁ L₂ ψ)
  (i j : ι)
    (O : Y.Opens) (hOi : O ≤ (f i).opensRange) (hOj : O ≤ (f j).opensRange) (s : Γ(L₁, O)) :
    Ψ f L₁ L₂ ψ i O hOi s = Ψ f L₁ L₂ ψ j O hOj s
theorem

Ψ_smul

L580 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar.Ψ_smul
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_toDescentData_map_bijective_of_openCover
universe 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 HomZar
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Glue
variable {Y : Scheme.{u}} {ι : Type v} {X : ι → Scheme.{u}} (f : ∀ i, X i ⟶ Y) [∀ i,
  IsOpenImmersion (f i)]
  (L₁ L₂ : Y.Modules)
open _root_.AlgebraicGeometry.Scheme.Modules.HomZar
variable {f L₁ L₂}
Lean source · statement
theorem Ψ_smul (ψ : ∀ i, L₁.restrict (f i) ⟶ L₂.restrict (f i)) (i : ι) (O : Y.Opens)
    (hO : O ≤ (f i).opensRange) (r : Γ(Y, O)) (s : Γ(L₁, O)) :
    Ψ f L₁ L₂ ψ i O hO (r • s) = r • Ψ f L₁ L₂ ψ i O hO s
theorem

restrictFunctor_map_injective

L607 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar.restrictFunctor_map_injective
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_toDescentData_map_bijective_of_openCover
universe 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 HomZar
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Glue
variable {Y : Scheme.{u}} {ι : Type v} {X : ι → Scheme.{u}} (f : ∀ i, X i ⟶ Y) [∀ i,
  IsOpenImmersion (f i)]
  (L₁ L₂ : Y.Modules)
open _root_.AlgebraicGeometry.Scheme.Modules.HomZar
variable {f L₁ L₂}
variable (f L₁ L₂)
Lean source · statement
theorem restrictFunctor_map_injective (hf : ∀ y : Y, ∃ i, y ∈ Set.range (f i).base)
    (t t' : L₁ ⟶ L₂) (h : ∀ i, (restrictFunctor (f i)).map t = (restrictFunctor
      (f i)).map t') : t = t'
abbrev

F₂

L632 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar.F₂
Documentation

The underlying sheaf of abelian groups of the target module.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_toDescentData_map_bijective_of_openCover
universe 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 HomZar
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Glue2
variable {Y : Scheme.{u}} {ι : Type v} {X : ι → Scheme.{u}} (f : ∀ i, X i ⟶ Y) [∀ i,
  IsOpenImmersion (f i)]
  (L₁ L₂ : Y.Modules)
Lean source · statement
abbrev F₂ : TopCat.Sheaf Ab Y.carrier
theorem

cover_le_iSup

L634 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar.cover_le_iSup
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_toDescentData_map_bijective_of_openCover
universe 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 HomZar
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Glue2
variable {Y : Scheme.{u}} {ι : Type v} {X : ι → Scheme.{u}} (f : ∀ i, X i ⟶ Y) [∀ i,
  IsOpenImmersion (f i)]
  (L₁ L₂ : Y.Modules)
Lean source · statement
theorem cover_le_iSup (hf : ∀ y : Y, ∃ i, y ∈ Set.range (f i).base) (W : Y.Opens) :
    W ≤ ⨆ i, (f i) ''ᵁ (f i) ⁻¹ᵁ W
theorem

image_preimage_le_opensRange

L640 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar.image_preimage_le_opensRange
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_toDescentData_map_bijective_of_openCover
universe 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 HomZar
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Glue2
variable {Y : Scheme.{u}} {ι : Type v} {X : ι → Scheme.{u}} (f : ∀ i, X i ⟶ Y) [∀ i,
  IsOpenImmersion (f i)]
  (L₁ L₂ : Y.Modules)
Lean source · statement
theorem image_preimage_le_opensRange (i : ι) (W : Y.Opens) : (f i) ''ᵁ (f i) ⁻¹ᵁ W ≤
  (f i).opensRange
def

locSec

L650 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar.locSec
Documentation

The local image of a section on a member of the induced open cover.

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_toDescentData_map_bijective_of_openCover
universe 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 HomZar
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Glue2
variable {Y : Scheme.{u}} {ι : Type v} {X : ι → Scheme.{u}} (f : ∀ i, X i ⟶ Y) [∀ i,
  IsOpenImmersion (f i)]
  (L₁ L₂ : Y.Modules)
variable {f L₁ L₂}
variable (ψ : ∀ i, L₁.restrict (f i) ⟶ L₂.restrict (f i))
  (hψ : _root_.AlgebraicGeometry.Scheme.Modules.HomZar.Compatible f L₁ L₂ ψ)
  (hf : ∀ y : Y, ∃ i, y ∈ Set.range (f i).base)
Lean source · statement
def locSec (W : Y.Opens) (s : Γ(L₁, W)) (i : ι) : Γ(L₂, (f i) ''ᵁ (f i) ⁻¹ᵁ W)
theorem

locSec_compatible

L654 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar.locSec_compatible
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_toDescentData_map_bijective_of_openCover
universe 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 HomZar
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Glue2
variable {Y : Scheme.{u}} {ι : Type v} {X : ι → Scheme.{u}} (f : ∀ i, X i ⟶ Y) [∀ i,
  IsOpenImmersion (f i)]
  (L₁ L₂ : Y.Modules)
variable {f L₁ L₂}
variable (ψ : ∀ i, L₁.restrict (f i) ⟶ L₂.restrict (f i))
  (hψ : _root_.AlgebraicGeometry.Scheme.Modules.HomZar.Compatible f L₁ L₂ ψ)
  (hf : ∀ y : Y, ∃ i, y ∈ Set.range (f i).base)
include hψ in
Lean source · full declaration
theorem locSec_compatible (W : Y.Opens) (s : Γ(L₁, W)) :
    L₂.presheaf.IsCompatible (fun i => (f i) ''ᵁ (f i) ⁻¹ᵁ W) (locSec ψ W s) := by
  intro i j
  change L₂.presheaf.map _ (locSec ψ W s i) = L₂.presheaf.map _ (locSec ψ W s j)
  simp only [locSec]
  have hi : (f i) ''ᵁ (f i) ⁻¹ᵁ W ⊓ (f j) ''ᵁ (f j) ⁻¹ᵁ W ≤ (f i).opensRange :=
    inf_le_left.trans (image_preimage_le_opensRange f i W)
  have hj : (f i) ''ᵁ (f i) ⁻¹ᵁ W ⊓ (f j) ''ᵁ (f j) ⁻¹ᵁ W ≤ (f j).opensRange :=
    inf_le_right.trans (image_preimage_le_opensRange f j W)
  rw [mapEq L₂ _ (homOfLE inf_le_left).op, Ψ_res ψ i _ _ _ hi inf_le_left, map_map,
    mapEq L₂ _ (homOfLE inf_le_right).op (Ψ f L₁ L₂ ψ j _ _ _),
      Ψ_res ψ j _ _ _ hj inf_le_right, map_map,
    Ψ_compat ψ hψ i j _ hi hj]
  try exact congrArg (fun y => Ψ f L₁ L₂ ψ j _ hj y) (mapEq L₁ _ _ s)
def

glue

L670 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar.glue
Documentation

The section obtained by gluing the compatible local images.

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_toDescentData_map_bijective_of_openCover
universe 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 HomZar
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Glue2
variable {Y : Scheme.{u}} {ι : Type v} {X : ι → Scheme.{u}} (f : ∀ i, X i ⟶ Y) [∀ i,
  IsOpenImmersion (f i)]
  (L₁ L₂ : Y.Modules)
variable {f L₁ L₂}
variable (ψ : ∀ i, L₁.restrict (f i) ⟶ L₂.restrict (f i))
  (hψ : _root_.AlgebraicGeometry.Scheme.Modules.HomZar.Compatible f L₁ L₂ ψ)
  (hf : ∀ y : Y, ∃ i, y ∈ Set.range (f i).base)
Lean source · statement
def glue (W : Y.Opens) (s : Γ(L₁, W)) : Γ(L₂, W)
theorem

glue_spec

L675 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar.glue_spec
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_toDescentData_map_bijective_of_openCover
universe 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 HomZar
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Glue2
variable {Y : Scheme.{u}} {ι : Type v} {X : ι → Scheme.{u}} (f : ∀ i, X i ⟶ Y) [∀ i,
  IsOpenImmersion (f i)]
  (L₁ L₂ : Y.Modules)
variable {f L₁ L₂}
variable (ψ : ∀ i, L₁.restrict (f i) ⟶ L₂.restrict (f i))
  (hψ : _root_.AlgebraicGeometry.Scheme.Modules.HomZar.Compatible f L₁ L₂ ψ)
  (hf : ∀ y : Y, ∃ i, y ∈ Set.range (f i).base)
Lean source · statement
theorem glue_spec (W : Y.Opens) (s : Γ(L₁, W)) (i : ι) :
    L₂.presheaf.map (homOfLE ((f i).image_preimage_le W)).op (glue ψ hψ hf W s) = locSec ψ W s i
theorem

glue_unique

L681 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar.glue_unique
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_toDescentData_map_bijective_of_openCover
universe 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 HomZar
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Glue2
variable {Y : Scheme.{u}} {ι : Type v} {X : ι → Scheme.{u}} (f : ∀ i, X i ⟶ Y) [∀ i,
  IsOpenImmersion (f i)]
  (L₁ L₂ : Y.Modules)
variable {f L₁ L₂}
variable (ψ : ∀ i, L₁.restrict (f i) ⟶ L₂.restrict (f i))
  (hψ : _root_.AlgebraicGeometry.Scheme.Modules.HomZar.Compatible f L₁ L₂ ψ)
  (hf : ∀ y : Y, ∃ i, y ∈ Set.range (f i).base)
Lean source · statement
theorem glue_unique (W : Y.Opens) (s : Γ(L₁, W)) (y : Γ(L₂, W))
    (hy : ∀ i, L₂.presheaf.map (homOfLE ((f i).image_preimage_le W)).op y = locSec ψ W s i) :
    y = glue ψ hψ hf W s
theorem

glue_add

L688 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar.glue_add
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_toDescentData_map_bijective_of_openCover
universe 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 HomZar
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Glue2
variable {Y : Scheme.{u}} {ι : Type v} {X : ι → Scheme.{u}} (f : ∀ i, X i ⟶ Y) [∀ i,
  IsOpenImmersion (f i)]
  (L₁ L₂ : Y.Modules)
variable {f L₁ L₂}
variable (ψ : ∀ i, L₁.restrict (f i) ⟶ L₂.restrict (f i))
  (hψ : _root_.AlgebraicGeometry.Scheme.Modules.HomZar.Compatible f L₁ L₂ ψ)
  (hf : ∀ y : Y, ∃ i, y ∈ Set.range (f i).base)
Lean source · statement
theorem glue_add (W : Y.Opens) (s s' : Γ(L₁, W)) :
    glue ψ hψ hf W (s + s') = glue ψ hψ hf W s + glue ψ hψ hf W s'
theorem

glue_smul

L694 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar.glue_smul
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_toDescentData_map_bijective_of_openCover
universe 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 HomZar
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Glue2
variable {Y : Scheme.{u}} {ι : Type v} {X : ι → Scheme.{u}} (f : ∀ i, X i ⟶ Y) [∀ i,
  IsOpenImmersion (f i)]
  (L₁ L₂ : Y.Modules)
variable {f L₁ L₂}
variable (ψ : ∀ i, L₁.restrict (f i) ⟶ L₂.restrict (f i))
  (hψ : _root_.AlgebraicGeometry.Scheme.Modules.HomZar.Compatible f L₁ L₂ ψ)
  (hf : ∀ y : Y, ∃ i, y ∈ Set.range (f i).base)
Lean source · statement
theorem glue_smul (W : Y.Opens) (r : Γ(Y, W)) (s : Γ(L₁, W)) :
    glue ψ hψ hf W (r • s) = r • glue ψ hψ hf W s
theorem

glue_res

L700 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar.glue_res
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_toDescentData_map_bijective_of_openCover
universe 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 HomZar
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Glue2
variable {Y : Scheme.{u}} {ι : Type v} {X : ι → Scheme.{u}} (f : ∀ i, X i ⟶ Y) [∀ i,
  IsOpenImmersion (f i)]
  (L₁ L₂ : Y.Modules)
variable {f L₁ L₂}
variable (ψ : ∀ i, L₁.restrict (f i) ⟶ L₂.restrict (f i))
  (hψ : _root_.AlgebraicGeometry.Scheme.Modules.HomZar.Compatible f L₁ L₂ ψ)
  (hf : ∀ y : Y, ∃ i, y ∈ Set.range (f i).base)
Lean source · statement
theorem glue_res {W W' : Y.Opens} (hle : W' ≤ W) (s : Γ(L₁, W)) :
    L₂.presheaf.map (homOfLE hle).op (glue ψ hψ hf W s) = glue ψ hψ hf W' (L₁.presheaf.map
      (homOfLE hle).op s)
def

gluePresheafHom

L715 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar.gluePresheafHom
Documentation

The presheaf morphism obtained by gluing local module morphisms.

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_toDescentData_map_bijective_of_openCover
universe 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 HomZar
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Glue2
variable {Y : Scheme.{u}} {ι : Type v} {X : ι → Scheme.{u}} (f : ∀ i, X i ⟶ Y) [∀ i,
  IsOpenImmersion (f i)]
  (L₁ L₂ : Y.Modules)
variable {f L₁ L₂}
variable (ψ : ∀ i, L₁.restrict (f i) ⟶ L₂.restrict (f i))
  (hψ : _root_.AlgebraicGeometry.Scheme.Modules.HomZar.Compatible f L₁ L₂ ψ)
  (hf : ∀ y : Y, ∃ i, y ∈ Set.range (f i).base)
Lean source · full declaration
def gluePresheafHom : L₁.presheaf ⟶ L₂.presheaf where
  app W := AddCommGrpCat.ofHom
    { toFun := glue ψ hψ hf W.unop
      map_zero' := by
        have h0 := glue_add ψ hψ hf W.unop 0 0
        rw [add_zero] at h0
        exact left_eq_add.mp h0
      map_add' := glue_add ψ hψ hf W.unop }
  naturality {W W'} i := by
    ext s
    change glue ψ hψ hf W'.unop (L₁.presheaf.map i s) = L₂.presheaf.map i (glue ψ hψ hf W.unop s)
    rw [mapEq L₁ i (homOfLE i.unop.le).op, mapEq L₂ i (homOfLE i.unop.le).op, glue_res]
def

glueHom

L729 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar.glueHom
Documentation

The module morphism obtained by gluing compatible morphisms on the cover.

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_toDescentData_map_bijective_of_openCover
universe 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 HomZar
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Glue2
variable {Y : Scheme.{u}} {ι : Type v} {X : ι → Scheme.{u}} (f : ∀ i, X i ⟶ Y) [∀ i,
  IsOpenImmersion (f i)]
  (L₁ L₂ : Y.Modules)
variable {f L₁ L₂}
variable (ψ : ∀ i, L₁.restrict (f i) ⟶ L₂.restrict (f i))
  (hψ : _root_.AlgebraicGeometry.Scheme.Modules.HomZar.Compatible f L₁ L₂ ψ)
  (hf : ∀ y : Y, ∃ i, y ∈ Set.range (f i).base)
Lean source · statement
def glueHom : L₁ ⟶ L₂
theorem

glueHom_app

L732 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar.glueHom_app
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_toDescentData_map_bijective_of_openCover
universe 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 HomZar
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Glue2
variable {Y : Scheme.{u}} {ι : Type v} {X : ι → Scheme.{u}} (f : ∀ i, X i ⟶ Y) [∀ i,
  IsOpenImmersion (f i)]
  (L₁ L₂ : Y.Modules)
variable {f L₁ L₂}
variable (ψ : ∀ i, L₁.restrict (f i) ⟶ L₂.restrict (f i))
  (hψ : _root_.AlgebraicGeometry.Scheme.Modules.HomZar.Compatible f L₁ L₂ ψ)
  (hf : ∀ y : Y, ∃ i, y ∈ Set.range (f i).base)
Lean source · statement
theorem glueHom_app (W : Y.Opens) (s : Γ(L₁, W)) : (glueHom ψ hψ hf).app W s =
  glue ψ hψ hf W s
theorem

glue_image

L735 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar.glue_image
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_toDescentData_map_bijective_of_openCover
universe 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 HomZar
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Glue2
variable {Y : Scheme.{u}} {ι : Type v} {X : ι → Scheme.{u}} (f : ∀ i, X i ⟶ Y) [∀ i,
  IsOpenImmersion (f i)]
  (L₁ L₂ : Y.Modules)
variable {f L₁ L₂}
variable (ψ : ∀ i, L₁.restrict (f i) ⟶ L₂.restrict (f i))
  (hψ : _root_.AlgebraicGeometry.Scheme.Modules.HomZar.Compatible f L₁ L₂ ψ)
  (hf : ∀ y : Y, ∃ i, y ∈ Set.range (f i).base)
include hψ in
Lean source · statement
theorem glue_image (i : ι) (V : (X i).Opens) (m : Γ(L₁, (f i) ''ᵁ V)) :
    glue ψ hψ hf ((f i) ''ᵁ V) m = (ψ i).app V m
theorem

exists_restrictFunctor_map_eq

L755 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar.exists_restrictFunctor_map_eq
Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_toDescentData_map_bijective_of_openCover
universe 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 HomZar
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Glue2
variable {Y : Scheme.{u}} {ι : Type v} {X : ι → Scheme.{u}} (f : ∀ i, X i ⟶ Y) [∀ i,
  IsOpenImmersion (f i)]
  (L₁ L₂ : Y.Modules)
variable {f L₁ L₂}
variable (ψ : ∀ i, L₁.restrict (f i) ⟶ L₂.restrict (f i))
  (hψ : _root_.AlgebraicGeometry.Scheme.Modules.HomZar.Compatible f L₁ L₂ ψ)
  (hf : ∀ y : Y, ∃ i, y ∈ Set.range (f i).base)
variable (f L₁ L₂)
include hψ hf in
Lean source · statement
theorem exists_restrictFunctor_map_eq :
    ∃ t : L₁ ⟶ L₂, ∀ i, (restrictFunctor (f i)).map t = ψ i
theorem

presheafHom_map_homMk

L770 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar.presheafHom_map_homMk
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_toDescentData_map_bijective_of_openCover
universe 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 HomZar
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Assembly
variable {Y : Scheme.{u}} {ι : Type v} {V : ι → Scheme.{u}} (g : ∀ i, V i ⟶ Y) [∀ i,
  IsOpenImmersion (g i)]
  (L₁ L₂ : Y.Modules)
omit [∀ i, IsOpenImmersion (g i)] in
Lean source · statement
theorem presheafHom_map_homMk (t : L₁ ⟶ L₂) (i : ι) :
    (Mdl.presheafHom L₁ L₂).map (Over.homMk (g i) : Over.mk (g i) ⟶ Over.mk (𝟙 Y)).op
        (Mdl.presheafHomObjHomEquiv t) = (Modules.pullback (g i)).map t
theorem

image_top_lift

L778 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar.image_top_lift
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_toDescentData_map_bijective_of_openCover
universe 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 HomZar
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Assembly
variable {Y : Scheme.{u}} {ι : Type v} {V : ι → Scheme.{u}} (g : ∀ i, V i ⟶ Y) [∀ i,
  IsOpenImmersion (g i)]
  (L₁ L₂ : Y.Modules)
Lean source · statement
theorem image_top_lift {U Y : Scheme.{u}} (f : U ⟶ Y) [IsOpenImmersion f] (A : U.Opens)
  (O : Y.Opens)
    (hO : O = f ''ᵁ A) (H : Set.range ⇑O.ι ⊆ Set.range ⇑f) : IsOpenImmersion.lift f O.ι H ''ᵁ
      ⊤ = A
theorem

conj_apply

L802 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar.conj_apply
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_toDescentData_map_bijective_of_openCover
universe 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 HomZar
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Assembly
variable {Y : Scheme.{u}} {ι : Type v} {V : ι → Scheme.{u}} (g : ∀ i, V i ⟶ Y) [∀ i,
  IsOpenImmersion (g i)]
  (L₁ L₂ : Y.Modules)
Lean source · full declaration
theorem conj_apply {X₀ X₁ : Scheme.{u}} (h : X₀ ⟶ X₁) (g' : X₁ ⟶ Y) (k : X₀ ⟶ Y)
    [IsOpenImmersion h] [IsOpenImmersion g'] [IsOpenImmersion k] (hk : h ≫ g' = k)
    (ψ : L₁.restrict g' ⟶ L₂.restrict g') (U : X₀.Opens) (m : Γ(L₁, k ''ᵁ U)) :
    ((restrictFunctorCongr hk.symm).hom.app L₁ ≫ (restrictFunctorComp h g').hom.app L₁ ≫
        (restrictFunctor h).map ψ ≫ (restrictFunctorComp h g').inv.app L₂ ≫
          (restrictFunctorCongr hk).hom.app L₂).app U m =
      L₂.presheaf.map (eqToHom (show k ''ᵁ U = (h ≫ g') ''ᵁ U by subst hk; rfl)).op
        (L₂.presheaf.map (eqToHom (Scheme.Hom.comp_image h g' U)).op
          (ψ.app (h ''ᵁ U) (L₁.presheaf.map (eqToHom (Scheme.Hom.comp_image h g' U).symm).op
            (L₁.presheaf.map (eqToHom (show (h ≫ g') ''ᵁ U = k ''ᵁ U by subst hk; rfl)).op
              m)))) := by
  rfl
theorem

conjugation_app_image

L816 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar.conjugation_app_image
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_toDescentData_map_bijective_of_openCover
universe 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 HomZar
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Assembly
variable {Y : Scheme.{u}} {ι : Type v} {V : ι → Scheme.{u}} (g : ∀ i, V i ⟶ Y) [∀ i,
  IsOpenImmersion (g i)]
  (L₁ L₂ : Y.Modules)
Lean source · statement
theorem conjugation_app_image
    {Y X₀ X₁ : Scheme.{u}} (L₁ L₂ : Y.Modules)
    (h : X₀ ⟶ X₁) (g : X₁ ⟶ Y) (k : X₀ ⟶ Y)
    [IsOpenImmersion h] [IsOpenImmersion g] [IsOpenImmersion k] (hk : h ≫ g = k)
    (ψ : L₁.restrict g ⟶ L₂.restrict g) (U : X₀.Opens) (A : X₁.Opens) (B : Y.Opens)
    (ha : h ''ᵁ U = A) (hb : g ''ᵁ A = B) (hc : k ''ᵁ U = B) (m : Γ(L₁, B)) :
    ((restrictFunctorCongr hk.symm).hom.app L₁ ≫ (restrictFunctorComp h g).hom.app L₁ ≫
        (restrictFunctor h).map ψ ≫ (restrictFunctorComp h g).inv.app L₂ ≫
          (restrictFunctorCongr hk).hom.app L₂).app U (L₁.presheaf.map (eqToHom hc).op m) =
      L₂.presheaf.map (eqToHom hc).op
        (L₂.presheaf.map (eqToHom hb.symm).op (ψ.app A (L₁.presheaf.map (eqToHom hb).op m)))
theorem

compatible_restrict_lifts

L857 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar.compatible_restrict_lifts
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_toDescentData_map_bijective_of_openCover
universe 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 HomZar
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Assembly
variable {Y : Scheme.{u}} {ι : Type v} {V : ι → Scheme.{u}} (g : ∀ i, V i ⟶ Y) [∀ i,
  IsOpenImmersion (g i)]
  (L₁ L₂ : Y.Modules)
Lean source · full declaration
theorem compatible_restrict_lifts
    (x : ∀ i, (Mdl.presheafHom L₁ L₂).obj (op (Over.mk (g i))))
    (hx : Presieve.Arrows.Compatible (Mdl.presheafHom L₁ L₂) (B := Over.mk (𝟙 Y))
      (X := fun i => Over.mk (g i)) (fun i => Over.homMk (g i)) x)
    (i j : ι) (O : Y.Opens) (a : (O : Scheme.{u}) ⟶ V i) (b : (O : Scheme.{u}) ⟶ V j)
    [IsOpenImmersion a] [IsOpenImmersion b] (ha : a ≫ g i = O.ι) (hb : b ≫ g j = O.ι) :
    (restrictFunctorCongr ha.symm).hom.app L₁ ≫ (restrictFunctorComp a (g i)).hom.app L₁ ≫
        (restrictFunctor a).map (toRestrict L₁ L₂ (g i) (x i)) ≫
          (restrictFunctorComp a (g i)).inv.app L₂ ≫ (restrictFunctorCongr ha).hom.app L₂ =
      (restrictFunctorCongr hb.symm).hom.app L₁ ≫ (restrictFunctorComp b (g j)).hom.app L₁ ≫
        (restrictFunctor b).map (toRestrict L₁ L₂ (g j) (x j)) ≫
          (restrictFunctorComp b (g j)).inv.app L₂ ≫ (restrictFunctorCongr hb).hom.app L₂ := by
  have H := hx i j (Over.mk O.ι) (Over.homMk a ha) (Over.homMk b hb) (by
    ext
    simp only [Over.homMk_left, Over.comp_left, Over.homMk_left, ha, hb])
  dsimp only [Pseudofunctor.presheafHom] at H
  have H' := congrArg (toRestrict L₁ L₂ O.ι) H
  have H₁ := toRestrict_pullHom L₁ L₂ a (g i) O.ι ha (x i)
  have H₂ := toRestrict_pullHom L₁ L₂ b (g j) O.ι hb (x j)
  exact H₁.symm.trans (H'.trans H₂)
theorem

compatible_of_arrowsCompatible

L878 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar.compatible_of_arrowsCompatible
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_toDescentData_map_bijective_of_openCover
universe 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 HomZar
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Assembly
variable {Y : Scheme.{u}} {ι : Type v} {V : ι → Scheme.{u}} (g : ∀ i, V i ⟶ Y) [∀ i,
  IsOpenImmersion (g i)]
  (L₁ L₂ : Y.Modules)
Lean source · full declaration
theorem compatible_of_arrowsCompatible
    (x : ∀ i, (Mdl.presheafHom L₁ L₂).obj (op (Over.mk (g i))))
    (hx : Presieve.Arrows.Compatible (Mdl.presheafHom L₁ L₂) (B := Over.mk (𝟙 Y))
      (X := fun i => Over.mk (g i)) (fun i => Over.homMk (g i)) x) :
    _root_.AlgebraicGeometry.Scheme.Modules.HomZar.Compatible g L₁ L₂
      (fun i => toRestrict L₁ L₂ (g i) (x i)) := by
  intro i j A B hAB
  have hOi : Set.range ⇑((g i) ''ᵁ A).ι ⊆ Set.range ⇑(g i) := by
    rw [Scheme.Opens.range_ι]; rintro _ ⟨a, -, rfl⟩; exact ⟨a, rfl⟩
  have hOj : Set.range ⇑((g i) ''ᵁ A).ι ⊆ Set.range ⇑(g j) := by
    rw [Scheme.Opens.range_ι, hAB]; rintro _ ⟨b, -, rfl⟩; exact ⟨b, rfl⟩
  have he₁ : IsOpenImmersion.lift (g i) ((g i) ''ᵁ A).ι hOi ≫ g i = ((g i) ''ᵁ A).ι :=
    IsOpenImmersion.lift_fac _ _ _
  have he₂ : IsOpenImmersion.lift (g j) ((g i) ''ᵁ A).ι hOj ≫ g j = ((g i) ''ᵁ A).ι :=
    IsOpenImmersion.lift_fac _ _ _
  have hE₀ : ((g i) ''ᵁ A).ι ''ᵁ ⊤ = (g i) ''ᵁ A := by
    rw [Scheme.Hom.image_top_eq_opensRange, Scheme.Opens.opensRange_ι]
  have EA : IsOpenImmersion.lift (g i) ((g i) ''ᵁ A).ι hOi ''ᵁ ⊤ = A :=
    image_top_lift (g i) A ((g i) ''ᵁ A) rfl hOi
  have EB : IsOpenImmersion.lift (g j) ((g i) ''ᵁ A).ι hOj ''ᵁ ⊤ = B :=
    image_top_lift (g j) B ((g i) ''ᵁ A) hAB hOj
  have Hc := compatible_restrict_lifts g L₁ L₂ x hx i j ((g i) ''ᵁ A)
    (IsOpenImmersion.lift (g i) ((g i) ''ᵁ A).ι hOi)
    (IsOpenImmersion.lift (g j) ((g i) ''ᵁ A).ι hOj) he₁ he₂
  ext m
  change (toRestrict L₁ L₂ (g i) (x i)).app A (L₁.presheaf.map (eqToHom hAB).op m) =
    L₂.presheaf.map (eqToHom hAB).op ((toRestrict L₁ L₂ (g j) (x j)).app B m)
  let ψA : Γ(L₁, (g i) ''ᵁ A) → Γ(L₂, (g i) ''ᵁ A) :=
    fun z => (toRestrict L₁ L₂ (g i) (x i)).app A z
  let ψB : Γ(L₁, (g j) ''ᵁ B) → Γ(L₂, (g j) ''ᵁ B) :=
    fun z => (toRestrict L₁ L₂ (g j) (x j)).app B z
  let z : Γ(L₁, (g i) ''ᵁ A) := L₁.presheaf.map (eqToHom hAB).op m
  let input : Γ(L₁, ((g i) ''ᵁ A).ι ''ᵁ ⊤) := L₁.presheaf.map (eqToHom hE₀).op z
  let out : Γ(L₂, ((g i) ''ᵁ A).ι ''ᵁ ⊤) → Γ(L₂, (g i) ''ᵁ A) :=
    fun y => L₂.presheaf.map (eqToHom hE₀.symm).op y
  have Hpoint := congrArg
    (fun χ : L₁.restrict ((g i) ''ᵁ A).ι ⟶ L₂.restrict ((g i) ''ᵁ A).ι =>
      (show Γ(L₂, ((g i) ''ᵁ A).ι ''ᵁ ⊤) from χ.app ⊤ input)) Hc
  have HL := conjugation_app_image L₁ L₂
    (IsOpenImmersion.lift (g i) ((g i) ''ᵁ A).ι hOi) (g i) ((g i) ''ᵁ A).ι he₁
    (toRestrict L₁ L₂ (g i) (x i)) ⊤ A ((g i) ''ᵁ A) EA rfl hE₀ z
  simp only [map_id'] at HL
  have HR := conjugation_app_image L₁ L₂
    (IsOpenImmersion.lift (g j) ((g i) ''ᵁ A).ι hOj) (g j) ((g i) ''ᵁ A).ι he₂
    (toRestrict L₁ L₂ (g j) (x j)) ⊤ B ((g i) ''ᵁ A) EB hAB.symm hE₀ z
  have hm : L₁.presheaf.map (eqToHom hAB.symm).op z = m := by
    dsimp only [z]
    rw [map_map, map_id']
  have hLeft : out (L₂.presheaf.map (eqToHom hE₀).op
      (L₂.presheaf.map (eqToHom (rfl : (g i) ''ᵁ A = (g i) ''ᵁ A)).op (ψA z))) = ψA z := by
    dsimp only [out]
    rw [map_map, map_id', map_id']
  have hRight : out (L₂.presheaf.map (eqToHom hE₀).op
      (L₂.presheaf.map (eqToHom hAB).op (ψB (L₁.presheaf.map (eqToHom hAB.symm).op z)))) =
      L₂.presheaf.map (eqToHom hAB).op (ψB m) := by
    rw [hm]
    dsimp only [out]
    rw [map_map, map_id']
  have hfin := congrArg out (HL.symm.trans (Hpoint.trans HR))
  exact hLeft.symm.trans (hfin.trans hRight)
theorem

main

L939 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_toDescentData_map_bijective_of_openCover.AlgebraicGeometry.Scheme.Modules.HomZar.main
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_toDescentData_map_bijective_of_openCover
universe 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 HomZar
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Assembly
variable {Y : Scheme.{u}} {ι : Type v} {V : ι → Scheme.{u}} (g : ∀ i, V i ⟶ Y) [∀ i,
  IsOpenImmersion (g i)]
  (L₁ L₂ : Y.Modules)
Lean source · statement
theorem main (hg : ∀ y : Y, ∃ i, y ∈ Set.range (g i).base) :
    Function.Bijective ((Mdl.toDescentData g).map : (L₁ ⟶ L₂) → _)
theorem

toDescentData_map_bijective_of_openCover

L962 ↗
AlgebraicGeometry.Scheme.Modules.toDescentData_map_bijective_of_openCover
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_toDescentData_map_bijective_of_openCover
universe v u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
Lean source · statement
theorem _root_.AlgebraicGeometry.Scheme.Modules.toDescentData_map_bijective_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) (L₁ L₂ : Y.Modules) :
    Function.Bijective
      ((((Scheme.Modules.pseudofunctor.{u}).comp Bicategory.Adj.forget₁).toDescentData g).map
        : (L₁ ⟶ L₂) → _)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.