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.

Equations

• X.Modules = SheafOfModules X.ringCatSheaf

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

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

Equations

• M.Hom N = SheafOfModules.Hom M N

@[implicit_reducible]

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

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

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

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• AlgebraicGeometry.Scheme.Modules.toPresheafOfModules X = SheafOfModules.forget X.ringCatSheaf

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

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

Equations

• AlgebraicGeometry.Scheme.Modules.fullyFaithfulToPresheafOfModules = SheafOfModules.fullyFaithfulForget X.ringCatSheaf

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.

Equations

• AlgebraicGeometry.Scheme.Modules.toPresheaf X = (AlgebraicGeometry.Scheme.Modules.toPresheafOfModules X).comp (PresheafOfModules.toPresheaf X.ringCatSheaf.obj)

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.

Equations

• M.presheaf = M.val.presheaf

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

Notation for sections of a presheaf of module.

Equations

• One or more equations did not get rendered due to their size.

@[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))

Equations

• AlgebraicGeometry.Scheme.Modules.instModuleCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensCarrierAbPresheaf = (M.val.obj (Opposite.op U)).isModule

@[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

def AlgebraicGeometry.Scheme.Modules.smul {X : Scheme} {M : X.Modules} {U : X.Opens} : ↑(X.presheaf.obj (Opposite.op U)) →+* CategoryTheory.End (M.presheaf.obj (Opposite.op U))

Scalar multiplication as an endomorphism of Γ(M, U).

Equations

• AlgebraicGeometry.Scheme.Modules.smul = (M.val.obj (Opposite.op U)).smul

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.smul_apply {X : Scheme} {M : X.Modules} {U : X.Opens} (r : ↑(X.presheaf.obj (Opposite.op U))) (x : ↑(M.presheaf.obj (Opposite.op U))) : (AddCommGrpCat.Hom.hom (smul r)) x = r • x

@[simp]

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

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.map_comp_smul_assoc {X : Scheme} {M : X.Modules} {U V : X.Opens} (i : U ⟶ V) (r : ↑(X.presheaf.obj (Opposite.op V))) {Z : Ab} (h : M.presheaf.obj (Opposite.op U) ⟶ Z) : CategoryTheory.CategoryStruct.comp (smul r) (CategoryTheory.CategoryStruct.comp (M.presheaf.map i.op) h) = CategoryTheory.CategoryStruct.comp (M.presheaf.map i.op) (CategoryTheory.CategoryStruct.comp (smul ((CategoryTheory.ConcreteCategory.hom (X.presheaf.map i.op)) r)) h)

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.

Equations

• AlgebraicGeometry.Scheme.Modules.Hom.mapPresheaf φ = (AlgebraicGeometry.Scheme.Modules.toPresheaf X).map φ

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.

Equations

• AlgebraicGeometry.Scheme.Modules.Hom.app φ U = (CategoryTheory.forget₂ (ModuleCat ↑(X.ringCatSheaf.obj.obj (Opposite.op U))) Ab).map (φ.val.app (Opposite.op U))

@[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.

Equations

• AlgebraicGeometry.Scheme.Modules.pushforward f = SheafOfModules.pushforward (AlgebraicGeometry.Scheme.Hom.toRingCatSheafHom f)

@[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.

Equations

• AlgebraicGeometry.Scheme.Modules.pullback f = SheafOfModules.pullback (AlgebraicGeometry.Scheme.Hom.toRingCatSheafHom f)

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.

Equations

• AlgebraicGeometry.Scheme.Modules.pullbackPushforwardAdjunction f = SheafOfModules.pullbackPushforwardAdjunction (AlgebraicGeometry.Scheme.Hom.toRingCatSheafHom f)

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.

Equations

• AlgebraicGeometry.Scheme.Modules.pushforwardId X = SheafOfModules.pushforwardId X.ringCatSheaf

@[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.

Equations

• AlgebraicGeometry.Scheme.Modules.pullbackId X = SheafOfModules.pullbackId X.ringCatSheaf

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.

Equations

• AlgebraicGeometry.Scheme.Modules.pushforwardComp f g = SheafOfModules.pushforwardComp (AlgebraicGeometry.Scheme.Hom.toRingCatSheafHom g) (AlgebraicGeometry.Scheme.Hom.toRingCatSheafHom f)

@[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.

Equations

• AlgebraicGeometry.Scheme.Modules.pullbackComp f g = SheafOfModules.pullbackComp (AlgebraicGeometry.Scheme.Hom.toRingCatSheafHom g) (AlgebraicGeometry.Scheme.Hom.toRingCatSheafHom f)

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.

Equations

• One or more equations did not get rendered due to their size.

@[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.

Equations

• AlgebraicGeometry.Scheme.Modules.pullbackCongr hf = CategoryTheory.eqToIso ⋯

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.)

Equations

• One or more equations did not get rendered due to their size.

@[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_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_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_obj_obj (b : CategoryTheory.LocallyDiscrete Schemeᵒᵖ) : (pseudofunctor.obj b).obj = CategoryTheory.Cat.of (Opposite.unop b.as).Modules

@[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_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_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_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_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_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_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

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.

Equations

• One or more equations did not get rendered due to their size.

@[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.

Equations

• M.restrict f = (AlgebraicGeometry.Scheme.Modules.restrictFunctor f).obj M

noncomputable def AlgebraicGeometry.Scheme.Modules.restrictAppIso {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] (M : Y.Modules) (U : X.Opens) : (M.restrict f).presheaf.obj (Opposite.op U) ≅ M.presheaf.obj (Opposite.op ((Hom.opensFunctor f).obj U))

The sections of the restriction of M over U are isomorphic to `Γ(M, f ''ᵁ U).

Equations

• AlgebraicGeometry.Scheme.Modules.restrictAppIso f M U = CategoryTheory.Iso.refl ((M.restrict f).presheaf.obj (Opposite.op U))

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.smul_restrictAppIso_hom {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] (M : Y.Modules) (U : X.Opens) (r : ↑(X.presheaf.obj (Opposite.op U))) : CategoryTheory.CategoryStruct.comp (smul r) (restrictAppIso f M U).hom = CategoryTheory.CategoryStruct.comp (restrictAppIso f M U).hom (smul ((CategoryTheory.ConcreteCategory.hom (Hom.appIso f U).inv) r))

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.smul_restrictAppIso_hom_apply {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] (M : Y.Modules) (U : X.Opens) (r : ↑(X.presheaf.obj (Opposite.op U))) (x : ↑((M.restrict f).presheaf.obj (Opposite.op U))) : (CategoryTheory.ConcreteCategory.hom (restrictAppIso f M U).hom) (r • x) = (CategoryTheory.ConcreteCategory.hom (Hom.appIso f U).inv) r • (CategoryTheory.ConcreteCategory.hom (restrictAppIso f M U).hom) x

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.smul_restrictAppIso_hom_assoc {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] (M : Y.Modules) (U : X.Opens) (r : ↑(X.presheaf.obj (Opposite.op U))) {Z : Ab} (h : M.presheaf.obj (Opposite.op ((Hom.opensFunctor f).obj U)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (smul r) (CategoryTheory.CategoryStruct.comp (restrictAppIso f M U).hom h) = CategoryTheory.CategoryStruct.comp (restrictAppIso f M U).hom (CategoryTheory.CategoryStruct.comp (smul ((CategoryTheory.ConcreteCategory.hom (Hom.appIso f U).inv) r)) h)

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.smul_restrictAppIso_inv {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] (M : Y.Modules) (U : X.Opens) (r : ↑(Y.presheaf.obj (Opposite.op ((Hom.opensFunctor f).obj U)))) : CategoryTheory.CategoryStruct.comp (smul r) (restrictAppIso f M U).inv = CategoryTheory.CategoryStruct.comp (restrictAppIso f M U).inv (smul ((CategoryTheory.ConcreteCategory.hom (Hom.appIso f U).hom) r))

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.smul_restrictAppIso_inv_apply {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] (M : Y.Modules) (U : X.Opens) (r : ↑(Y.presheaf.obj (Opposite.op ((Hom.opensFunctor f).obj U)))) (x : ↑(M.presheaf.obj (Opposite.op ((Hom.opensFunctor f).obj U)))) : (CategoryTheory.ConcreteCategory.hom (restrictAppIso f M U).inv) (r • x) = (CategoryTheory.ConcreteCategory.hom (Hom.appIso f U).hom) r • (CategoryTheory.ConcreteCategory.hom (restrictAppIso f M U).inv) x

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.smul_restrictAppIso_inv_assoc {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] (M : Y.Modules) (U : X.Opens) (r : ↑(Y.presheaf.obj (Opposite.op ((Hom.opensFunctor f).obj U)))) {Z : Ab} (h : (M.restrict f).presheaf.obj (Opposite.op U) ⟶ Z) : CategoryTheory.CategoryStruct.comp (smul r) (CategoryTheory.CategoryStruct.comp (restrictAppIso f M U).inv h) = CategoryTheory.CategoryStruct.comp (restrictAppIso f M U).inv (CategoryTheory.CategoryStruct.comp (smul ((CategoryTheory.ConcreteCategory.hom (Hom.appIso f U).hom) r)) h)

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.map_restrictAppIso_hom {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] (M : Y.Modules) {U V : X.Opens} (hUV : Opposite.op V ⟶ Opposite.op U) : CategoryTheory.CategoryStruct.comp ((M.restrict f).presheaf.map hUV) (restrictAppIso f M U).hom = CategoryTheory.CategoryStruct.comp (restrictAppIso f M V).hom (M.presheaf.map (CategoryTheory.homOfLE ⋯).op)

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.map_restrictAppIso_hom_apply {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] (M : Y.Modules) {U V : X.Opens} (hUV : Opposite.op V ⟶ Opposite.op U) (x : ↑((M.restrict f).presheaf.obj (Opposite.op V))) : (CategoryTheory.ConcreteCategory.hom (restrictAppIso f M U).hom) ((CategoryTheory.ConcreteCategory.hom ((M.restrict f).presheaf.map hUV)) x) = (CategoryTheory.ConcreteCategory.hom (M.presheaf.map (CategoryTheory.homOfLE ⋯).op)) ((CategoryTheory.ConcreteCategory.hom (restrictAppIso f M V).hom) x)

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.map_restrictAppIso_hom_assoc {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] (M : Y.Modules) {U V : X.Opens} (hUV : Opposite.op V ⟶ Opposite.op U) {Z : Ab} (h : M.presheaf.obj (Opposite.op ((Hom.opensFunctor f).obj U)) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((M.restrict f).presheaf.map hUV) (CategoryTheory.CategoryStruct.comp (restrictAppIso f M U).hom h) = CategoryTheory.CategoryStruct.comp (restrictAppIso f M V).hom (CategoryTheory.CategoryStruct.comp (M.presheaf.map (CategoryTheory.homOfLE ⋯).op) h)

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.restrictAppIso_inv_map {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] (M : Y.Modules) {U V : X.Opens} (hUV : Opposite.op V ⟶ Opposite.op U) : CategoryTheory.CategoryStruct.comp (restrictAppIso f M V).inv ((M.restrict f).presheaf.map hUV) = CategoryTheory.CategoryStruct.comp (M.presheaf.map (CategoryTheory.homOfLE ⋯).op) (restrictAppIso f M U).inv

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.restrictAppIso_inv_map_apply {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] (M : Y.Modules) {U V : X.Opens} (hUV : Opposite.op V ⟶ Opposite.op U) (x : ↑(M.presheaf.obj (Opposite.op ((Hom.opensFunctor f).obj V)))) : (CategoryTheory.ConcreteCategory.hom ((M.restrict f).presheaf.map hUV)) ((CategoryTheory.ConcreteCategory.hom (restrictAppIso f M V).inv) x) = (CategoryTheory.ConcreteCategory.hom (restrictAppIso f M U).inv) ((CategoryTheory.ConcreteCategory.hom (M.presheaf.map (CategoryTheory.homOfLE ⋯).op)) x)

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.restrictAppIso_inv_map_assoc {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] (M : Y.Modules) {U V : X.Opens} (hUV : Opposite.op V ⟶ Opposite.op U) {Z : Ab} (h : (M.restrict f).presheaf.obj (Opposite.op U) ⟶ Z) : CategoryTheory.CategoryStruct.comp (restrictAppIso f M V).inv (CategoryTheory.CategoryStruct.comp ((M.restrict f).presheaf.map hUV) h) = CategoryTheory.CategoryStruct.comp (M.presheaf.map (CategoryTheory.homOfLE ⋯).op) (CategoryTheory.CategoryStruct.comp (restrictAppIso f M U).inv h)

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))

Avoid using this. Use the isomorphism AlgebraicGeometry.Scheme.Modules.restrictAppIso instead.

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

Avoid using this. Use the isomorphism AlgebraicGeometry.Scheme.Modules.restrictAppIso instead.

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.

Equations

• One or more equations did not get rendered due to their size.

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

Restriction is right adjoint to pushforward.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

@[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.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.restrictFunctorComp_hom_app_app {X Y Z : Scheme} {U : X.Opens} (f : X ⟶ Y) (g : Y ⟶ Z) [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} {U : X.Opens} (f : X ⟶ Y) (g : Y ⟶ Z) [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.

Equations

• One or more equations did not get rendered due to their size.

@[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.

Equations

• One or more equations did not get rendered due to their size.

@[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

noncomputable def AlgebraicGeometry.Scheme.Modules.sheafComposePushforwardComp {R S : CommRingCat} (φ : R ⟶ S) : (CategoryTheory.sheafCompose (Opens.grothendieckTopology ↥(Spec S)) (ModuleCat.restrictScalars (CommRingCat.Hom.hom (Hom.appTop (Spec.map φ))))).comp ((TopCat.Sheaf.pushforward (ModuleCat ↑((Spec R).presheaf.obj (Opposite.op ⊤))) (Spec.map φ).base).comp (CategoryTheory.sheafCompose (Opens.grothendieckTopology ↥(Spec R)) (ModuleCat.restrictScalars (CommRingCat.Hom.hom (ΓSpecIso R).inv)))) ≅ (CategoryTheory.sheafCompose (Opens.grothendieckTopology ↥(Spec S)) (ModuleCat.restrictScalars (CommRingCat.Hom.hom (ΓSpecIso S).inv))).comp ((TopCat.Sheaf.pushforward (ModuleCat ↑S) (Spec.map φ).base).comp (CategoryTheory.sheafCompose (Opens.grothendieckTopology ↥(Spec R)) (ModuleCat.restrictScalars (CommRingCat.Hom.hom φ))))

sheafCompose commutes with pushforward

Equations

• One or more equations did not get rendered due to their size.