Modules over presheaves of commutative rings

This file provides short names for categories and functors obtained from a presheaf of commutative rings by forgetting to rings. In particular, these names reduce the need for repeatedly writing the relevant forgetful functor.

@[reducible, inline]

abbrev PresheafOfModulesOfCommRing {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (R : CategoryTheory.Functor Cᵒᵖ CommRingCat) : Type (max (max (max u u₁) (v + 1)) v₁)

The category of presheaves of modules over a presheaf of commutative rings.

Equations

• PresheafOfModulesOfCommRing R = PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))

@[reducible, inline]

abbrev PresheafOfModulesOfCommRing.mk {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} (obj : (X : Cᵒᵖ) → ModuleCat ↑(R.obj X)) (map : {X Y : Cᵒᵖ} → (f : X ⟶ Y) → obj X ⟶ (ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map f))).obj (obj Y)) (map_id : ∀ (X : Cᵒᵖ), map (CategoryTheory.CategoryStruct.id X) = (ModuleCat.restrictScalarsId' (CommRingCat.Hom.hom (R.map (CategoryTheory.CategoryStruct.id X))) ⋯).inv.app (obj X) := by cat_disch) (map_comp : ∀ {X Y Z : Cᵒᵖ} (f : X ⟶ Y) (g : Y ⟶ Z), map (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (map f) (CategoryTheory.CategoryStruct.comp ((ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map f))).map (map g)) ((ModuleCat.restrictScalarsComp' (CommRingCat.Hom.hom (R.map f)) (CommRingCat.Hom.hom (R.map g)) (CommRingCat.Hom.hom (R.map (CategoryTheory.CategoryStruct.comp f g))) ⋯).inv.app (obj Z))) := by cat_disch) : PresheafOfModulesOfCommRing R

Construct a presheaf of modules over a presheaf of commutative rings.

Equations

• PresheafOfModulesOfCommRing.mk obj map map_id map_comp = { obj := obj, map := fun {X Y : Cᵒᵖ} => map, map_id := map_id, map_comp := ⋯ }

@[reducible, inline]

abbrev PresheafOfModulesOfCommRing.obj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} (F : PresheafOfModulesOfCommRing R) (X : Cᵒᵖ) : ModuleCat ↑(R.obj X)

Evaluate a presheaf of modules over a presheaf of commutative rings at an object.

Equations

• F.obj X = F.obj X

@[reducible, inline]

abbrev PresheafOfModulesOfCommRing.map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} (F : PresheafOfModulesOfCommRing R) {X Y : Cᵒᵖ} (f : X ⟶ Y) : F.obj X ⟶ (ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map f))).obj (F.obj Y)

The restriction map of a presheaf of modules over a presheaf of commutative rings.

Equations

• F.map f = F.map f

@[reducible, inline]

abbrev PresheafOfModulesOfCommRing.homMk {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} {M₁ M₂ : PresheafOfModulesOfCommRing R} (app : (X : Cᵒᵖ) → M₁.obj X ⟶ M₂.obj X) (naturality : ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y), CategoryTheory.CategoryStruct.comp (M₁.map f) ((ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map f))).map (app Y)) = CategoryTheory.CategoryStruct.comp (app X) (M₂.map f) := by cat_disch) : M₁ ⟶ M₂

Construct a morphism of presheaves of modules over a presheaf of commutative rings.

Equations

• PresheafOfModulesOfCommRing.homMk app naturality = { app := app, naturality := ⋯ }

@[reducible, inline]

abbrev PresheafOfModulesOfCommRing.isoMk {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} {M₁ M₂ : PresheafOfModulesOfCommRing R} (app : (X : Cᵒᵖ) → M₁.obj X ≅ M₂.obj X) (naturality : ∀ ⦃X Y : Cᵒᵖ⦄ (f : X ⟶ Y), CategoryTheory.CategoryStruct.comp (M₁.map f) ((ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map f))).map (app Y).hom) = CategoryTheory.CategoryStruct.comp (app X).hom (M₂.map f) := by cat_disch) : M₁ ≅ M₂

Construct an isomorphism of presheaves of modules over a presheaf of commutative rings.

Equations

• PresheafOfModulesOfCommRing.isoMk app naturality = PresheafOfModules.isoMk app naturality

@[reducible, inline]

noncomputable abbrev PresheafOfModulesOfCommRing.unit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (R : CategoryTheory.Functor Cᵒᵖ CommRingCat) : PresheafOfModulesOfCommRing R

The free presheaf of modules of rank one over a presheaf of commutative rings.

Equations

• PresheafOfModulesOfCommRing.unit R = PresheafOfModules.unit (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))

@[reducible, inline]

noncomputable abbrev PresheafOfModulesOfCommRing.restrictScalars {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R S : CategoryTheory.Functor Cᵒᵖ CommRingCat} (φ : R ⟶ S) : CategoryTheory.Functor (PresheafOfModulesOfCommRing S) (PresheafOfModulesOfCommRing R)

Restriction of scalars along a morphism of presheaves of commutative rings.

Equations

• PresheafOfModulesOfCommRing.restrictScalars φ = PresheafOfModules.restrictScalars (CategoryTheory.Functor.whiskerRight φ (CategoryTheory.forget₂ CommRingCat RingCat))

@[reducible, inline]

abbrev PresheafOfModulesOfCommRing.pushforward₀ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (R : CategoryTheory.Functor Dᵒᵖ CommRingCat) : CategoryTheory.Functor (PresheafOfModulesOfCommRing R) (PresheafOfModulesOfCommRing (F.op.comp R))

The pushforward functor along F for modules over a presheaf of commutative rings.

Equations

• PresheafOfModulesOfCommRing.pushforward₀ F R = PresheafOfModules.pushforward₀ F (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))

@[reducible, inline]

noncomputable abbrev PresheafOfModulesOfCommRing.pushforward {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {R : CategoryTheory.Functor Dᵒᵖ CommRingCat} {S : CategoryTheory.Functor Cᵒᵖ CommRingCat} (φ : S ⟶ F.op.comp R) : CategoryTheory.Functor (PresheafOfModulesOfCommRing R) (PresheafOfModulesOfCommRing S)

The pushforward functor induced by a morphism of presheaves of commutative rings.

Equations

• PresheafOfModulesOfCommRing.pushforward φ = PresheafOfModules.pushforward (CategoryTheory.Functor.whiskerRight φ (CategoryTheory.forget₂ CommRingCat RingCat))

@[reducible, inline]

noncomputable abbrev PresheafOfModulesOfCommRing.pullback {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {R : CategoryTheory.Functor Dᵒᵖ CommRingCat} {S : CategoryTheory.Functor Cᵒᵖ CommRingCat} (φ : S ⟶ F.op.comp R) [(pushforward φ).IsRightAdjoint] : CategoryTheory.Functor (PresheafOfModulesOfCommRing S) (PresheafOfModulesOfCommRing R)

The pullback functor induced by a morphism of presheaves of commutative rings.

Equations

• PresheafOfModulesOfCommRing.pullback φ = PresheafOfModules.pullback (CategoryTheory.Functor.whiskerRight φ (CategoryTheory.forget₂ CommRingCat RingCat))

@[reducible, inline]

noncomputable abbrev PresheafOfModulesOfCommRing.pullbackPushforwardAdjunction {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {R : CategoryTheory.Functor Dᵒᵖ CommRingCat} {S : CategoryTheory.Functor Cᵒᵖ CommRingCat} (φ : S ⟶ F.op.comp R) [(pushforward φ).IsRightAdjoint] : pullback φ ⊣ pushforward φ

The adjunction between pullback and pushforward for modules over presheaves of commutative rings.

Equations

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