The category of sheaves of modules over a scheme

In this file, we define the abelian category of sheaves of modules X.Modules over a scheme X, and study its basic functoriality.

def AlgebraicGeometry.Scheme.Modules (X : Scheme) : Type (u + 1)

The category of sheaves of modules over a scheme.

def AlgebraicGeometry.Scheme.Modules.Hom {X : Scheme} (M N : X.Modules) : Type u

Morphisms between 𝒪ₓ-modules. Use Hom.app to act on sections.

@[implicit_reducible]

instance AlgebraicGeometry.Scheme.Modules.instCategory {X : Scheme} : CategoryTheory.Category.{u, u + 1} X.Modules

@[implicit_reducible]

noncomputable instance AlgebraicGeometry.Scheme.Modules.instAbelian {X : Scheme} : CategoryTheory.Abelian X.Modules

instance AlgebraicGeometry.Scheme.Modules.instHasLimits {X : Scheme} : CategoryTheory.Limits.HasLimits X.Modules

instance AlgebraicGeometry.Scheme.Modules.instHasColimits {X : Scheme} : CategoryTheory.Limits.HasColimits X.Modules

def AlgebraicGeometry.Scheme.Modules.toPresheafOfModules (X : Scheme) : CategoryTheory.Functor X.Modules X.PresheafOfModules

The forgetful functor from 𝒪ₓ-modules to presheaves of modules. This is mostly useful to transport results from (pre)sheaves of modules to 𝒪ₓ-modules and usually shouldn't be used directly when working with actual 𝒪ₓ-modules.

def AlgebraicGeometry.Scheme.Modules.fullyFaithfulToPresheafOfModules {X : Scheme} : (toPresheafOfModules X).FullyFaithful

The forgetful functor from 𝒪ₓ-modules to presheaves of modules is fully faithful.

instance AlgebraicGeometry.Scheme.Modules.instFullPresheafOfModulesToPresheafOfModules {X : Scheme} : (toPresheafOfModules X).Full

instance AlgebraicGeometry.Scheme.Modules.instFaithfulPresheafOfModulesToPresheafOfModules {X : Scheme} : (toPresheafOfModules X).Faithful

instance AlgebraicGeometry.Scheme.Modules.instIsRightAdjointPresheafOfModulesToPresheafOfModules {X : Scheme} : (toPresheafOfModules X).IsRightAdjoint

noncomputable def AlgebraicGeometry.Scheme.Modules.toPresheaf (X : Scheme) : CategoryTheory.Functor X.Modules (TopCat.Presheaf Ab ↑X.toPresheafedSpace)

The forgetful functor from 𝒪ₓ-modules to presheaves of abelian groups.

instance AlgebraicGeometry.Scheme.Modules.instFaithfulPresheafAbCarrierCommRingCatToPresheaf {X : Scheme} : (toPresheaf X).Faithful

instance AlgebraicGeometry.Scheme.Modules.instPreservesLimitsPresheafAbCarrierCommRingCatToPresheaf {X : Scheme} : CategoryTheory.Limits.PreservesLimits (toPresheaf X)

instance AlgebraicGeometry.Scheme.Modules.instReflectsIsomorphismsPresheafAbCarrierCommRingCatToPresheaf {X : Scheme} : (toPresheaf X).ReflectsIsomorphisms

noncomputable def AlgebraicGeometry.Scheme.Modules.presheaf {X : Scheme} (M : X.Modules) : TopCat.Presheaf Ab ↑X.toPresheafedSpace

The underlying abelian presheaf of an 𝒪ₓ-module.

def AlgebraicGeometry.«termΓ(_,_)_1» : Lean.ParserDescr

Notation for sections of a presheaf of module.

@[implicit_reducible]

instance AlgebraicGeometry.Scheme.Modules.instModuleCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensCarrierAbPresheaf {X : Scheme} {M : X.Modules} {U : X.Opens} : Module ↑(X.presheaf.obj (Opposite.op U)) ↑(M.presheaf.obj (Opposite.op U))

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.map_smul {X : Scheme} (M : X.Modules) {U V : X.Opens} (i : U ⟶ V) (r : ↑(X.presheaf.obj (Opposite.op V))) (x : ↑(M.presheaf.obj (Opposite.op V))) : (CategoryTheory.ConcreteCategory.hom (M.presheaf.map i.op)) (r • x) = (CategoryTheory.ConcreteCategory.hom (X.presheaf.map i.op)) r • (CategoryTheory.ConcreteCategory.hom (M.presheaf.map i.op)) x

noncomputable def AlgebraicGeometry.Scheme.Modules.Hom.mapPresheaf {X : Scheme} {M N : X.Modules} (φ : M ⟶ N) : M.presheaf ⟶ N.presheaf

The underlying map between abelian presheaves of a morphism of 𝒪ₓ-modules.

def AlgebraicGeometry.Scheme.Modules.Hom.app {X : Scheme} {M N : X.Modules} (φ : M ⟶ N) (U : X.Opens) : M.presheaf.obj (Opposite.op U) ⟶ N.presheaf.obj (Opposite.op U)

The application of a morphism of 𝒪ₓ-modules to sections.

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.mapPresheaf_app {X : Scheme} {M N : X.Modules} (φ : M ⟶ N) (U : (TopologicalSpace.Opens ↥X)ᵒᵖ) : (Hom.mapPresheaf φ).app U = Hom.app φ (Opposite.unop U)

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.Hom.app_smul {X : Scheme} {M N : X.Modules} {U : X.Opens} (φ : M ⟶ N) (r : ↑(X.presheaf.obj (Opposite.op U))) (x : ↑(M.presheaf.obj (Opposite.op U))) : (CategoryTheory.ConcreteCategory.hom (app φ U)) (r • x) = r • (CategoryTheory.ConcreteCategory.hom (app φ U)) x

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.Hom.add_app {X : Scheme} {M N : X.Modules} {U : X.Opens} (φ ψ : M ⟶ N) : app (φ + ψ) U = app φ U + app ψ U

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.Hom.sub_app {X : Scheme} {M N : X.Modules} {U : X.Opens} (φ ψ : M ⟶ N) : app (φ - ψ) U = app φ U - app ψ U

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.Hom.zero_app {X : Scheme} {M N : X.Modules} {U : X.Opens} : app 0 U = 0

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.Hom.id_app {X : Scheme} {U : X.Opens} (M : X.Modules) : app (CategoryTheory.CategoryStruct.id M) U = CategoryTheory.CategoryStruct.id (M.presheaf.obj (Opposite.op U))

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.Hom.comp_app {X : Scheme} {M N K : X.Modules} {U : X.Opens} (φ : M ⟶ N) (ψ : N ⟶ K) : app (CategoryTheory.CategoryStruct.comp φ ψ) U = CategoryTheory.CategoryStruct.comp (app φ U) (app ψ U)

theorem AlgebraicGeometry.Scheme.Modules.hom_ext {X : Scheme} {M N : X.Modules} (f g : M ⟶ N) (H : ∀ (U : X.Opens), Hom.app f U = Hom.app g U) : f = g

theorem AlgebraicGeometry.Scheme.Modules.hom_ext_iff {X : Scheme} {M N : X.Modules} {f g : M ⟶ N} : f = g ↔ ∀ (U : X.Opens), Hom.app f U = Hom.app g U

theorem AlgebraicGeometry.Scheme.Modules.isSheaf {X : Scheme} (M : X.Modules) : M.presheaf.IsSheaf

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.toPresheaf_obj {X : Scheme} {M : X.Modules} : (toPresheaf X).obj M = M.presheaf

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.toPresheaf_map {X : Scheme} {M N : X.Modules} {φ : M ⟶ N} : (toPresheaf X).map φ = Hom.mapPresheaf φ

theorem AlgebraicGeometry.Scheme.Modules.Hom.isIso_iff_isIso_app {X : Scheme} {M N : X.Modules} {φ : M ⟶ N} : CategoryTheory.IsIso φ ↔ ∀ (U : X.Opens), CategoryTheory.IsIso (app φ U)

instance AlgebraicGeometry.Scheme.Modules.instIsIsoAbApp {X : Scheme} {M N : X.Modules} {φ : M ⟶ N} {U : X.Opens} [CategoryTheory.IsIso φ] : CategoryTheory.IsIso (Hom.app φ U)

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.inv_app {X : Scheme} {M N : X.Modules} {φ : M ⟶ N} {U : X.Opens} [CategoryTheory.IsIso φ] : Hom.app (CategoryTheory.inv φ) U = CategoryTheory.inv (Hom.app φ U)

noncomputable def AlgebraicGeometry.Scheme.Modules.pushforward {X Y : Scheme} (f : X ⟶ Y) : CategoryTheory.Functor X.Modules Y.Modules

The pushforward functor for categories of sheaves of modules over schemes.

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.pushforward_obj_obj {X Y : Scheme} (f : X ⟶ Y) (M : X.Modules) (U : Y.Opens) : ((pushforward f).obj M).presheaf.obj (Opposite.op U) = M.presheaf.obj (Opposite.op ((TopologicalSpace.Opens.map f.base).obj U))

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.pushforward_obj_presheaf_map {X Y : Scheme} {M : X.Modules} (f : X ⟶ Y) {U V : Y.Opens} (i : U ⟶ V) : ((pushforward f).obj M).presheaf.map i.op = M.presheaf.map ((TopologicalSpace.Opens.map f.base).map i).op

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.pushforward_map_app {X Y : Scheme} {M N : X.Modules} (f : X ⟶ Y) (φ : M ⟶ N) (U : Y.Opens) : Hom.app ((pushforward f).map φ) U = Hom.app φ ((TopologicalSpace.Opens.map f.base).obj U)

noncomputable def AlgebraicGeometry.Scheme.Modules.pullback {X Y : Scheme} (f : X ⟶ Y) : CategoryTheory.Functor Y.Modules X.Modules

The pullback functor for categories of sheaves of modules over schemes.

noncomputable def AlgebraicGeometry.Scheme.Modules.pullbackPushforwardAdjunction {X Y : Scheme} (f : X ⟶ Y) : pullback f ⊣ pushforward f

The pullback functor for categories of sheaves of modules over schemes is left adjoint to the pushforward functor.

instance AlgebraicGeometry.Scheme.Modules.instIsLeftAdjointPullback {X Y : Scheme} (f : X ⟶ Y) : (pullback f).IsLeftAdjoint

instance AlgebraicGeometry.Scheme.Modules.instIsRightAdjointPushforward {X Y : Scheme} (f : X ⟶ Y) : (pushforward f).IsRightAdjoint

instance AlgebraicGeometry.Scheme.Modules.instAdditivePushforward {X Y : Scheme} (f : X ⟶ Y) : (pushforward f).Additive

instance AlgebraicGeometry.Scheme.Modules.instAdditivePullback {X Y : Scheme} (f : X ⟶ Y) : (pullback f).Additive

noncomputable def AlgebraicGeometry.Scheme.Modules.pushforwardId (X : Scheme) : pushforward (CategoryTheory.CategoryStruct.id X) ≅ CategoryTheory.Functor.id X.Modules

The pushforward of sheaves of modules by the identity morphism identifies to the identity functor.

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.pushforwardId_hom_app_app {X : Scheme} {M : X.Modules} {U : X.Opens} : Hom.app ((pushforwardId X).hom.app M) U = CategoryTheory.CategoryStruct.id (((pushforward (CategoryTheory.CategoryStruct.id X)).obj M).presheaf.obj (Opposite.op U))

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.pushforwardId_inv_app_app {X : Scheme} {M : X.Modules} {U : X.Opens} : Hom.app ((pushforwardId X).inv.app M) U = CategoryTheory.CategoryStruct.id (((CategoryTheory.Functor.id X.Modules).obj M).presheaf.obj (Opposite.op U))

noncomputable def AlgebraicGeometry.Scheme.Modules.pullbackId (X : Scheme) : pullback (CategoryTheory.CategoryStruct.id X) ≅ CategoryTheory.Functor.id X.Modules

The pullback of sheaves of modules by the identity morphism identifies to the identity functor.

theorem AlgebraicGeometry.Scheme.Modules.conjugateEquiv_pullbackId_hom (X : Scheme) : (CategoryTheory.conjugateEquiv CategoryTheory.Adjunction.id (pullbackPushforwardAdjunction (CategoryTheory.CategoryStruct.id X))) (pullbackId X).hom = (pushforwardId X).inv

noncomputable def AlgebraicGeometry.Scheme.Modules.pushforwardComp {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) : (pushforward f).comp (pushforward g) ≅ pushforward (CategoryTheory.CategoryStruct.comp f g)

The composition of two pushforward functors for sheaves of modules on schemes identify to the pushforward for the composition.

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.pushforwardComp_hom_app_app {X Y Z : Scheme} {M : X.Modules} (f : X ⟶ Y) (g : Y ⟶ Z) (U : Z.Opens) : Hom.app ((pushforwardComp f g).hom.app M) U = CategoryTheory.CategoryStruct.id ((((pushforward f).comp (pushforward g)).obj M).presheaf.obj (Opposite.op U))

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.pushforwardComp_inv_app_app {X Y Z : Scheme} {M : X.Modules} (f : X ⟶ Y) (g : Y ⟶ Z) (U : Z.Opens) : Hom.app ((pushforwardComp f g).inv.app M) U = CategoryTheory.CategoryStruct.id (((pushforward (CategoryTheory.CategoryStruct.comp f g)).obj M).presheaf.obj (Opposite.op U))

noncomputable def AlgebraicGeometry.Scheme.Modules.pullbackComp {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) : (pullback g).comp (pullback f) ≅ pullback (CategoryTheory.CategoryStruct.comp f g)

The composition of two pullback functors for sheaves of modules on schemes identify to the pullback for the composition.

noncomputable def AlgebraicGeometry.Scheme.Modules.pushforwardCongr {X Y : Scheme} {f g : X ⟶ Y} (hf : f = g) : pushforward f ≅ pushforward g

Pushforwards along equal morphisms are isomorphic.

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.pushforwardCongr_hom_app_app {X Y : Scheme} {M : X.Modules} {f g : X ⟶ Y} (hf : f = g) (U : Y.Opens) : Hom.app ((pushforwardCongr hf).hom.app M) U = M.presheaf.map (CategoryTheory.eqToHom ⋯).op

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.pushforwardCongr_inv_app_app {X Y : Scheme} {M : X.Modules} {f g : X ⟶ Y} (hf : f = g) (U : Y.Opens) : Hom.app ((pushforwardCongr hf).inv.app M) U = M.presheaf.map (CategoryTheory.eqToHom ⋯).op

noncomputable def AlgebraicGeometry.Scheme.Modules.pullbackCongr {X Y : Scheme} {f g : X ⟶ Y} (hf : f = g) : pullback f ≅ pullback g

Inverse images along equal morphisms are isomorphic.

theorem AlgebraicGeometry.Scheme.Modules.conjugateEquiv_pullbackComp_inv {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) : (CategoryTheory.conjugateEquiv ((pullbackPushforwardAdjunction g).comp (pullbackPushforwardAdjunction f)) (pullbackPushforwardAdjunction (CategoryTheory.CategoryStruct.comp f g))) (pullbackComp f g).inv = (pushforwardComp f g).hom

theorem AlgebraicGeometry.Scheme.Modules.pseudofunctor_associativity {X Y Z T : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) (h : Z ⟶ T) : CategoryTheory.CategoryStruct.comp (pullbackComp f (CategoryTheory.CategoryStruct.comp g h)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (pullbackComp g h).inv (pullback f)) (CategoryTheory.CategoryStruct.comp ((pullback h).associator (pullback g) (pullback f)).hom (CategoryTheory.CategoryStruct.comp ((pullback h).whiskerLeft (pullbackComp f g).hom) (pullbackComp (CategoryTheory.CategoryStruct.comp f g) h).hom))) = CategoryTheory.eqToHom ⋯

theorem AlgebraicGeometry.Scheme.Modules.pseudofunctor_associativity_assoc {X Y Z T : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) (h : Z ⟶ T) {Z✝ : CategoryTheory.Functor T.Modules X.Modules} (h✝ : pullback (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g) h) ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (pullbackComp f (CategoryTheory.CategoryStruct.comp g h)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (pullbackComp g h).inv (pullback f)) (CategoryTheory.CategoryStruct.comp ((pullback h).associator (pullback g) (pullback f)).hom (CategoryTheory.CategoryStruct.comp ((pullback h).whiskerLeft (pullbackComp f g).hom) (CategoryTheory.CategoryStruct.comp (pullbackComp (CategoryTheory.CategoryStruct.comp f g) h).hom h✝)))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h✝

theorem AlgebraicGeometry.Scheme.Modules.pseudofunctor_left_unitality {X Y : Scheme} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (pullbackComp f (CategoryTheory.CategoryStruct.id Y)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (pullbackId Y).hom (pullback f)) (pullback f).leftUnitor.hom) = CategoryTheory.eqToHom ⋯

theorem AlgebraicGeometry.Scheme.Modules.pseudofunctor_left_unitality_assoc {X Y : Scheme} (f : X ⟶ Y) {Z : CategoryTheory.Functor Y.Modules X.Modules} (h : pullback f ⟶ Z) : CategoryTheory.CategoryStruct.comp (pullbackComp f (CategoryTheory.CategoryStruct.id Y)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (pullbackId Y).hom (pullback f)) (CategoryTheory.CategoryStruct.comp (pullback f).leftUnitor.hom h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h

theorem AlgebraicGeometry.Scheme.Modules.pseudofunctor_right_unitality {X Y : Scheme} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (pullbackComp (CategoryTheory.CategoryStruct.id X) f).inv (CategoryTheory.CategoryStruct.comp ((pullback f).whiskerLeft (pullbackId X).hom) (pullback f).rightUnitor.hom) = CategoryTheory.eqToHom ⋯

theorem AlgebraicGeometry.Scheme.Modules.pseudofunctor_right_unitality_assoc {X Y : Scheme} (f : X ⟶ Y) {Z : CategoryTheory.Functor Y.Modules X.Modules} (h : pullback f ⟶ Z) : CategoryTheory.CategoryStruct.comp (pullbackComp (CategoryTheory.CategoryStruct.id X) f).inv (CategoryTheory.CategoryStruct.comp ((pullback f).whiskerLeft (pullbackId X).hom) (CategoryTheory.CategoryStruct.comp (pullback f).rightUnitor.hom h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h

noncomputable def AlgebraicGeometry.Scheme.Modules.pseudofunctor : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Schemeᵒᵖ) (CategoryTheory.Bicategory.Adj CategoryTheory.Cat)

The pseudofunctor from Schemeᵒᵖ to the bicategory of adjunctions which sends a scheme X to the category X.Modules of sheaves of modules over X. (This contains both the covariant and the contravariant functorialities of these categories.)

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapId_inv_τr (x✝ : CategoryTheory.LocallyDiscrete Schemeᵒᵖ) : (pseudofunctor.mapId x✝).inv.τr = CategoryTheory.NatTrans.toCatHom₂ (pushforwardId (Opposite.unop x✝.as)).hom

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapComp_hom_τl {a✝ b✝ c✝ : CategoryTheory.LocallyDiscrete Schemeᵒᵖ} (x✝ : a✝ ⟶ b✝) (x✝¹ : b✝ ⟶ c✝) : (pseudofunctor.mapComp x✝ x✝¹).hom.τl = CategoryTheory.NatTrans.toCatHom₂ (pullbackComp x✝¹.as.unop x✝.as.unop).inv

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapId_hom_τl (x✝ : CategoryTheory.LocallyDiscrete Schemeᵒᵖ) : (pseudofunctor.mapId x✝).hom.τl = CategoryTheory.NatTrans.toCatHom₂ (pullbackId (Opposite.unop x✝.as)).hom

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapComp_inv_τl {a✝ b✝ c✝ : CategoryTheory.LocallyDiscrete Schemeᵒᵖ} (x✝ : a✝ ⟶ b✝) (x✝¹ : b✝ ⟶ c✝) : (pseudofunctor.mapComp x✝ x✝¹).inv.τl = CategoryTheory.NatTrans.toCatHom₂ (pullbackComp x✝¹.as.unop x✝.as.unop).hom

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapId_inv_τl (x✝ : CategoryTheory.LocallyDiscrete Schemeᵒᵖ) : (pseudofunctor.mapId x✝).inv.τl = CategoryTheory.NatTrans.toCatHom₂ (pullbackId (Opposite.unop x✝.as)).inv

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.pseudofunctor_map_adj {X✝ Y✝ : CategoryTheory.LocallyDiscrete Schemeᵒᵖ} (f : X✝ ⟶ Y✝) : (pseudofunctor.map f).adj = (pullbackPushforwardAdjunction f.as.unop).toCat

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapComp_hom_τr {a✝ b✝ c✝ : CategoryTheory.LocallyDiscrete Schemeᵒᵖ} (x✝ : a✝ ⟶ b✝) (x✝¹ : b✝ ⟶ c✝) : (pseudofunctor.mapComp x✝ x✝¹).hom.τr = CategoryTheory.NatTrans.toCatHom₂ (pushforwardComp x✝¹.as.unop x✝.as.unop).hom

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapComp_inv_τr {a✝ b✝ c✝ : CategoryTheory.LocallyDiscrete Schemeᵒᵖ} (x✝ : a✝ ⟶ b✝) (x✝¹ : b✝ ⟶ c✝) : (pseudofunctor.mapComp x✝ x✝¹).inv.τr = CategoryTheory.NatTrans.toCatHom₂ (pushforwardComp x✝¹.as.unop x✝.as.unop).inv

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.pseudofunctor_map_r {X✝ Y✝ : CategoryTheory.LocallyDiscrete Schemeᵒᵖ} (f : X✝ ⟶ Y✝) : (pseudofunctor.map f).r = (pushforward f.as.unop).toCatHom

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.pseudofunctor_map_l {X✝ Y✝ : CategoryTheory.LocallyDiscrete Schemeᵒᵖ} (f : X✝ ⟶ Y✝) : (pseudofunctor.map f).l = (pullback f.as.unop).toCatHom

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapId_hom_τr (x✝ : CategoryTheory.LocallyDiscrete Schemeᵒᵖ) : (pseudofunctor.mapId x✝).hom.τr = CategoryTheory.NatTrans.toCatHom₂ (pushforwardId (Opposite.unop x✝.as)).inv

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.pseudofunctor_obj_obj (b : CategoryTheory.LocallyDiscrete Schemeᵒᵖ) : (pseudofunctor.obj b).obj = CategoryTheory.Cat.of (Opposite.unop b.as).Modules

noncomputable def AlgebraicGeometry.Scheme.Modules.restrictFunctor {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] : CategoryTheory.Functor Y.Modules X.Modules

Restriction of an 𝒪ₓ-module along an open immersion. This is isomorphic to the pullback functor (see restrictFunctorIsoPullback) but has better defeqs.

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.Scheme.Modules.restrict {X Y : Scheme} (M : Y.Modules) (f : X ⟶ Y) [IsOpenImmersion f] : X.Modules

The restriction of a module along an open immersion.

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.restrict_obj {X Y : Scheme} (M : Y.Modules) (f : X ⟶ Y) [IsOpenImmersion f] (U : TopologicalSpace.Opens ↥X) : (M.restrict f).presheaf.obj (Opposite.op U) = M.presheaf.obj (Opposite.op ((Hom.opensFunctor f).obj U))

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.restrict_map {X Y : Scheme} (M : Y.Modules) (f : X ⟶ Y) [IsOpenImmersion f] {U V : TopologicalSpace.Opens ↥X} (i : U ⟶ V) : (M.restrict f).presheaf.map i.op = M.presheaf.map ((Hom.opensFunctor f).map i).op

noncomputable def AlgebraicGeometry.Scheme.Modules.restrictFunctorAdjCounitIso {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] : (pushforward f).comp (restrictFunctor f) ≅ CategoryTheory.Functor.id X.Modules

The restriction of a module along an open immersion.

noncomputable def AlgebraicGeometry.Scheme.Modules.restrictAdjunction {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] : restrictFunctor f ⊣ pushforward f

Restriction is right adjoint to pushforward.

instance AlgebraicGeometry.Scheme.Modules.instIsIsoFunctorCounitRestrictAdjunction {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] : CategoryTheory.IsIso (restrictAdjunction f).counit

instance AlgebraicGeometry.Scheme.Modules.instIsLeftAdjointRestrictFunctor {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] : (restrictFunctor f).IsLeftAdjoint

instance AlgebraicGeometry.Scheme.Modules.instFullPushforward {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] : (pushforward f).Full

instance AlgebraicGeometry.Scheme.Modules.instFaithfulPushforward {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] : (pushforward f).Faithful

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.restrictAdjunction_unit_app_app {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] (M : Y.Modules) (U : Y.Opens) : Hom.app ((restrictAdjunction f).unit.app M) U = M.presheaf.map (CategoryTheory.homOfLE ⋯).op

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.restrictAdjunction_counit_app_app {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] (M : X.Modules) (U : X.Opens) : Hom.app ((restrictAdjunction f).counit.app M) U = M.presheaf.map (CategoryTheory.eqToHom ⋯).op

noncomputable def AlgebraicGeometry.Scheme.Modules.restrictFunctorIsoPullback {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] : restrictFunctor f ≅ pullback f

Restriction is naturally isomorphic to the inverse image.

noncomputable def AlgebraicGeometry.Scheme.Modules.restrictFunctorId {X : Scheme} : restrictFunctor (CategoryTheory.CategoryStruct.id X) ≅ CategoryTheory.Functor.id X.Modules

Restriction along the identity is isomorphic to the identity.

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.restrictFunctorId_hom_app_app {X : Scheme} {M : X.Modules} {U : X.Opens} : Hom.app (restrictFunctorId.hom.app M) U = M.presheaf.map (CategoryTheory.eqToHom ⋯).op

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.restrictFunctorId_inv_app_app {X : Scheme} {M : X.Modules} {U : X.Opens} : Hom.app (restrictFunctorId.inv.app M) U = M.presheaf.map (CategoryTheory.eqToHom ⋯).op

noncomputable def AlgebraicGeometry.Scheme.Modules.restrictFunctorComp {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [IsOpenImmersion f] [IsOpenImmersion g] : restrictFunctor (CategoryTheory.CategoryStruct.comp f g) ≅ (restrictFunctor g).comp (restrictFunctor f)

Restriction along the composition is isomorphic to the composition of restrictions.

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.restrictFunctorComp_hom_app_app {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) {U : X.Opens} [IsOpenImmersion f] [IsOpenImmersion g] (M : Z.Modules) : Hom.app ((restrictFunctorComp f g).hom.app M) U = M.presheaf.map (CategoryTheory.eqToHom ⋯).op

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.restrictFunctorComp_inv_app_app {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) {U : X.Opens} [IsOpenImmersion f] [IsOpenImmersion g] (M : Z.Modules) : Hom.app ((restrictFunctorComp f g).inv.app M) U = M.presheaf.map (CategoryTheory.eqToHom ⋯).op

noncomputable def AlgebraicGeometry.Scheme.Modules.restrictFunctorCongr {X Y : Scheme} {f g : X ⟶ Y} (hf : f = g) [IsOpenImmersion f] [IsOpenImmersion g] : restrictFunctor f ≅ restrictFunctor g

Restriction along equal morphisms are isomorphic.

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.restrictFunctorCongr_hom_app_app {X Y : Scheme} {U : X.Opens} {f g : X ⟶ Y} (hf : f = g) [IsOpenImmersion f] [IsOpenImmersion g] (M : Y.Modules) : Hom.app ((restrictFunctorCongr hf).hom.app M) U = M.presheaf.map (CategoryTheory.eqToHom ⋯).op

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.restrictFunctorCongr_inv_app_app {X Y : Scheme} {U : X.Opens} {f g : X ⟶ Y} (hf : f = g) [IsOpenImmersion f] [IsOpenImmersion g] (M : Y.Modules) : Hom.app ((restrictFunctorCongr hf).inv.app M) U = M.presheaf.map (CategoryTheory.eqToHom ⋯).op

noncomputable def AlgebraicGeometry.Scheme.Modules.restrictStalkNatIso {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] (x : ↥X) : (restrictFunctor f).comp ((toPresheaf X).comp (TopCat.Presheaf.stalkFunctor Ab x)) ≅ (toPresheaf Y).comp (TopCat.Presheaf.stalkFunctor Ab (f x))

Restriction along open immersions commutes with taking stalks.

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.germ_restrictStalkNatIso_hom_app {X Y : Scheme} {U : X.Opens} (f : X ⟶ Y) [IsOpenImmersion f] (x : ↥X) (M : Y.Modules) (hxU : x ∈ U) : CategoryTheory.CategoryStruct.comp (((restrictFunctor f).obj M).presheaf.germ U x hxU) ((restrictStalkNatIso f x).hom.app M) = M.presheaf.germ ((Hom.opensFunctor f).obj (Opposite.unop (Opposite.op U))) (f x) ⋯

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.germ_restrictStalkNatIso_inv_app {X Y : Scheme} {U : X.Opens} (f : X ⟶ Y) [IsOpenImmersion f] (x : ↥X) (M : Y.Modules) (hxU : x ∈ U) : CategoryTheory.CategoryStruct.comp (M.presheaf.germ ((Hom.opensFunctor f).obj (Opposite.unop (Opposite.op U))) (f x) ⋯) ((restrictStalkNatIso f x).inv.app M) = ((restrictFunctor f).obj M).presheaf.germ U x hxU