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.

Equations

• M.Hom N = SheafOfModules.Hom M N

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.

instance AlgebraicGeometry.Scheme.Modules.instPreadditive {X : Scheme} : CategoryTheory.Preadditive X.Modules

Equations

• AlgebraicGeometry.Scheme.Modules.instPreadditive = inferInstanceAs (CategoryTheory.Preadditive (SheafOfModules X.ringCatSheaf))

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

Equations

• AlgebraicGeometry.Scheme.Modules.instAbelian = inferInstanceAs (CategoryTheory.Abelian (SheafOfModules X.ringCatSheaf))

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)

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)

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

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)

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)

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_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_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_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_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_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_τ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_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_τ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_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_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_mapId_inv_τr (x✝ : CategoryTheory.LocallyDiscrete Schemeᵒᵖ) : (pseudofunctor.mapId x✝).inv.τr = CategoryTheory.NatTrans.toCatHom₂ (pushforwardId (Opposite.unop x✝.as)).hom