NYLL
Module

RestrictOpen.lean

Nyll.SchemeTheory.Sheaves.RestrictOpen
13 declarations indexed from sourceView source ↗

Module documentation

Restriction of module presheaves and sheaves

Compares restriction to open subschemes with the corresponding pullback constructions.

Imports2
Imported by2

Declarations

def

restrictPresheafRingHom

L34 ↗
AlgebraicGeometry.Scheme.Modules.restrictPresheafRingHom
Documentation

The canonical ring-presheaf map identifying restriction to an open subscheme with sections on its image.

Source context 5 commands

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

universe v v₁ v₂ u₁ u₂ u
open CategoryTheory Functor
namespace AlgebraicGeometry.Scheme.Modules
open TopologicalSpace
variable {X : Scheme.{u}} (U : X.Opens)
Lean source · statement
def restrictPresheafRingHom :
    (U : Scheme.{u}).ringCatSheaf.obj ⟶ U.ι.opensFunctor.op ⋙ X.ringCatSheaf.obj
def

restrictPresheaf

L38 ↗
AlgebraicGeometry.Scheme.Modules.restrictPresheaf
Documentation

Restriction of presheaves of modules to the open subscheme.

Source context 5 commands

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

universe v v₁ v₂ u₁ u₂ u
open CategoryTheory Functor
namespace AlgebraicGeometry.Scheme.Modules
open TopologicalSpace
variable {X : Scheme.{u}} (U : X.Opens)
Lean source · statement
def restrictPresheaf : X.PresheafOfModules ⥤ (U : Scheme.{u}).PresheafOfModules
def

restrictPresheaf₀

L42 ↗
AlgebraicGeometry.Scheme.Modules.restrictPresheaf₀
Documentation

Restriction obtained by precomposing with the open-image functor, before scalar restriction.

Source context 5 commands

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

universe v v₁ v₂ u₁ u₂ u
open CategoryTheory Functor
namespace AlgebraicGeometry.Scheme.Modules
open TopologicalSpace
variable {X : Scheme.{u}} (U : X.Opens)
Lean source · statement
def restrictPresheaf₀ : X.PresheafOfModules ⥤ (U : Scheme.{u}).PresheafOfModules
def

restrictPresheafIsoRestrictPresheaf₀

L46 ↗
AlgebraicGeometry.Scheme.Modules.restrictPresheafIsoRestrictPresheaf₀
Documentation

The canonical identification of the two descriptions of presheaf restriction.

Source context 5 commands

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

universe v v₁ v₂ u₁ u₂ u
open CategoryTheory Functor
namespace AlgebraicGeometry.Scheme.Modules
open TopologicalSpace
variable {X : Scheme.{u}} (U : X.Opens)
Lean source · statement
def restrictPresheafIsoRestrictPresheaf₀ : restrictPresheaf U ≅ restrictPresheaf₀
  U
lemma

restrictPresheaf_obj_obj

L49 ↗
AlgebraicGeometry.Scheme.Modules.restrictPresheaf_obj_obj
Source context 5 commands

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

universe v v₁ v₂ u₁ u₂ u
open CategoryTheory Functor
namespace AlgebraicGeometry.Scheme.Modules
open TopologicalSpace
variable {X : Scheme.{u}} (U : X.Opens)
Lean source · statement
lemma restrictPresheaf_obj_obj (P : X.PresheafOfModules) (V : (U : Scheme.{u}).Opensᵒᵖ) :
    (((restrictPresheaf U).obj P).obj V : Type u) = P.obj (Opposite.op (U.ι ''ᵁ V.unop))
def

restrictPresheafAdj

L54 ↗
AlgebraicGeometry.Scheme.Modules.restrictPresheafAdj
Documentation

Restriction to the open subscheme is left adjoint to presheaf pushforward along its inclusion.

Source context 5 commands

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

universe v v₁ v₂ u₁ u₂ u
open CategoryTheory Functor
namespace AlgebraicGeometry.Scheme.Modules
open TopologicalSpace
variable {X : Scheme.{u}} (U : X.Opens)
Lean source · statement
def restrictPresheafAdj :
    restrictPresheaf U ⊣ PresheafOfModules.pushforward.{u} U.ι.toRingCatSheafHom.hom
instance

(anonymous instance)

L74 ↗
Source context 6 commands

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

universe v v₁ v₂ u₁ u₂ u
open CategoryTheory Functor
namespace AlgebraicGeometry.Scheme.Modules
open TopologicalSpace
variable {X : Scheme.{u}} (U : X.Opens)
section
Lean source · statement
instance : (PresheafOfModules.pushforward.{u} U.ι.toRingCatSheafHom.hom).IsRightAdjoint
def

pullbackPresheafIsoRestrictPresheaf

L78 ↗
AlgebraicGeometry.Scheme.Modules.pullbackPresheafIsoRestrictPresheaf
Documentation

The identification of presheaf pullback along an open inclusion with restriction.

Source context 7 commands

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

universe v v₁ v₂ u₁ u₂ u
open CategoryTheory Functor
namespace AlgebraicGeometry.Scheme.Modules
open TopologicalSpace
variable {X : Scheme.{u}} (U : X.Opens)
section
local instance : (PresheafOfModules.pushforward.{u} U.ι.toRingCatSheafHom.hom).IsRightAdjoint :=
  (restrictPresheafAdj U).isRightAdjoint
Lean source · statement
def pullbackPresheafIsoRestrictPresheaf :
    PresheafOfModules.pullback.{u} U.ι.toRingCatSheafHom.hom ≅ restrictPresheaf U
def

sheafificationCompPullbackIso

L85 ↗
AlgebraicGeometry.Scheme.Modules.sheafificationCompPullbackIso
Documentation

Sheafification followed by pullback to an open subscheme agrees with restriction followed by sheafification.

Source context 7 commands

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

universe v v₁ v₂ u₁ u₂ u
open CategoryTheory Functor
namespace AlgebraicGeometry.Scheme.Modules
open TopologicalSpace
variable {X : Scheme.{u}} (U : X.Opens)
section
local instance : (PresheafOfModules.pushforward.{u} U.ι.toRingCatSheafHom.hom).IsRightAdjoint :=
  (restrictPresheafAdj U).isRightAdjoint
Lean source · statement
def sheafificationCompPullbackIso :
    PresheafOfModules.sheafification (𝟙 X.ringCatSheaf.obj) ⋙ Modules.pullback U.ι ≅
      restrictPresheaf U ⋙ PresheafOfModules.sheafification (𝟙 (U : Scheme.{u}).ringCatSheaf.obj)
def

restrictOpen

L94 ↗
AlgebraicGeometry.Scheme.Modules.restrictOpen
Documentation

Restriction of sheaves of modules to an open subscheme using the open-image functor.

Source context 5 commands

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

universe v v₁ v₂ u₁ u₂ u
open CategoryTheory Functor
namespace AlgebraicGeometry.Scheme.Modules
open TopologicalSpace
variable {X : Scheme.{u}} (U : X.Opens)
Lean source · statement
def restrictOpen : X.Modules ⥤ (U : Scheme.{u}).Modules
lemma

restrictOpen_obj_val

L97 ↗
AlgebraicGeometry.Scheme.Modules.restrictOpen_obj_val
Source context 5 commands

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

universe v v₁ v₂ u₁ u₂ u
open CategoryTheory Functor
namespace AlgebraicGeometry.Scheme.Modules
open TopologicalSpace
variable {X : Scheme.{u}} (U : X.Opens)
Lean source · statement
lemma restrictOpen_obj_val (M : X.Modules) :
    ((restrictOpen U).obj M).val = (restrictPresheaf U).obj M.val
def

restrictOpenIsoRestrictFunctor

L101 ↗
AlgebraicGeometry.Scheme.Modules.restrictOpenIsoRestrictFunctor
Documentation

The canonical identification of open restriction with the scheme restriction functor.

Source context 5 commands

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

universe v v₁ v₂ u₁ u₂ u
open CategoryTheory Functor
namespace AlgebraicGeometry.Scheme.Modules
open TopologicalSpace
variable {X : Scheme.{u}} (U : X.Opens)
Lean source · statement
def restrictOpenIsoRestrictFunctor : restrictOpen U ≅ Modules.restrictFunctor U.ι
def

restrictOpenIsoPullback

L109 ↗
AlgebraicGeometry.Scheme.Modules.restrictOpenIsoPullback
Documentation

The canonical identification of open restriction with scheme pullback.

Source context 5 commands

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

universe v v₁ v₂ u₁ u₂ u
open CategoryTheory Functor
namespace AlgebraicGeometry.Scheme.Modules
open TopologicalSpace
variable {X : Scheme.{u}} (U : X.Opens)
Lean source · statement
def restrictOpenIsoPullback : restrictOpen U ≅ Modules.pullback U.ι

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