The colimit module of a presheaf of modules on a cofiltered category

Given a colimit cocone cR for a presheaf of rings R on a cofiltered category C, M a presheaf of modules over R, and a colimit cocone cM for the underlying functor Cᵒᵖ ⥤ AddCommGrpCat of M, we define a structure of module over cR.pt on a type-synonym PresheafOfModules.ModuleColimit for cM.pt. This extends to a functor PresheafOfModules.colimitFunctor : PresheafOfModules R ⥤ ModuleCat cR.pt.

TODO (@joelriou)

• Define fiber functors on categories of (pre)sheaves of modules
• Refactor Mathlib/Algebra/Category/ModuleCat/Stalk.lean so that it uses this slightly more general construction.

noncomputable def PresheafOfModules.constFunctor {C : Type u} [CategoryTheory.Category.{v, u} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (cR : CategoryTheory.Limits.Cocone R) : CategoryTheory.Functor (ModuleCat ↑cR.pt) (PresheafOfModules R)

Given a cocone cR for a functor R : Cᵒᵖ ⥤ RingCat, this is the functor ModuleCat cR.pt ⥤ PresheafOfModules R which sends a module M over cR.pt to a presheaf of modules whose underlying presheaf of abelian groups is the constant functor Cᵒᵖ ⥤ AddCommGrpCat with value M.

Equations

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

def PresheafOfModules.ModuleColimit {C : Type u} [CategoryTheory.Category.{v, u} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {cR : CategoryTheory.Limits.Cocone R} {M : PresheafOfModules R} {cM : CategoryTheory.Limits.Cocone M.presheaf} : CategoryTheory.Limits.IsColimit cR → CategoryTheory.Limits.IsColimit cM → Type w

Given a colimit cocone for a presheaf of rings R on a cofiltered category C, M a presheaf of modules over R, and a colimit cocone cM for the underlying functor Cᵒᵖ ⥤ AddCommGrpCat of M, this is the type cM.pt on which we define a module structure below.

Equations

• PresheafOfModules.ModuleColimit x✝¹ x✝ = ↑cM.pt

@[implicit_reducible]

instance PresheafOfModules.instAddCommGroupModuleColimit {C : Type u} [CategoryTheory.Category.{v, u} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {cR : CategoryTheory.Limits.Cocone R} (hcR : CategoryTheory.Limits.IsColimit cR) {M : PresheafOfModules R} {cM : CategoryTheory.Limits.Cocone M.presheaf} (hcM : CategoryTheory.Limits.IsColimit cM) : AddCommGroup (ModuleColimit hcR hcM)

Equations

• PresheafOfModules.instAddCommGroupModuleColimit hcR hcM = PresheafOfModules.instAddCommGroupModuleColimit._aux_1 hcR hcM

noncomputable def PresheafOfModules.ModuleColimit.coconeSMul {C : Type u} [CategoryTheory.Category.{v, u} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {cR : CategoryTheory.Limits.Cocone R} (hcR : CategoryTheory.Limits.IsColimit cR) {M : PresheafOfModules R} {cM : CategoryTheory.Limits.Cocone M.presheaf} (hcM : CategoryTheory.Limits.IsColimit cM) : CategoryTheory.Limits.Cocone (CategoryTheory.MonoidalCategoryStruct.tensorObj (R.comp (CategoryTheory.forget RingCat)) (M.presheaf.comp (CategoryTheory.forget Ab)))

The cocone for R ⋙ forget _ ⊗ M.presheaf ⋙ forget _ with point ModuleColimit hcR hcM which allows to define the scalar multiplication by cR.pt on ModuleColimit hcR hcM.

Equations

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

@[simp]

theorem PresheafOfModules.ModuleColimit.coconeSMul_ι_app {C : Type u} [CategoryTheory.Category.{v, u} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {cR : CategoryTheory.Limits.Cocone R} (hcR : CategoryTheory.Limits.IsColimit cR) {M : PresheafOfModules R} {cM : CategoryTheory.Limits.Cocone M.presheaf} (hcM : CategoryTheory.Limits.IsColimit cM) (U : Cᵒᵖ) (x✝ : (CategoryTheory.MonoidalCategoryStruct.tensorObj (R.comp (CategoryTheory.forget RingCat)) (M.presheaf.comp (CategoryTheory.forget Ab))).obj U) : (coconeSMul hcR hcM).ι.app U x✝ = match x✝ with | (r, m) => (CategoryTheory.ConcreteCategory.hom (cM.ι.app U)) (r • m)

@[simp]

theorem PresheafOfModules.ModuleColimit.coconeSMul_pt {C : Type u} [CategoryTheory.Category.{v, u} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {cR : CategoryTheory.Limits.Cocone R} (hcR : CategoryTheory.Limits.IsColimit cR) {M : PresheafOfModules R} {cM : CategoryTheory.Limits.Cocone M.presheaf} (hcM : CategoryTheory.Limits.IsColimit cM) : (coconeSMul hcR hcM).pt = ModuleColimit hcR hcM

@[implicit_reducible]

noncomputable instance PresheafOfModules.ModuleColimit.instSMulCarrierPtOppositeRingCat {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.IsCofiltered C] [CategoryTheory.InitiallySmall C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {cR : CategoryTheory.Limits.Cocone R} (hcR : CategoryTheory.Limits.IsColimit cR) {M : PresheafOfModules R} {cM : CategoryTheory.Limits.Cocone M.presheaf} (hcM : CategoryTheory.Limits.IsColimit cM) : SMul (↑cR.pt) (ModuleColimit hcR hcM)

Equations

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

@[reducible, inline]

abbrev PresheafOfModules.ModuleColimit.ιR {C : Type u} [CategoryTheory.Category.{v, u} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (cR : CategoryTheory.Limits.Cocone R) {U : Cᵒᵖ} : ↑(R.obj U) →+* ↑cR.pt

The "inclusion" maps to the colimit ring.

Equations

• PresheafOfModules.ModuleColimit.ιR cR = RingCat.Hom.hom (cR.ι.app U)

@[reducible, inline]

noncomputable abbrev PresheafOfModules.ModuleColimit.ιM {C : Type u} [CategoryTheory.Category.{v, u} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {cR : CategoryTheory.Limits.Cocone R} {hcR : CategoryTheory.Limits.IsColimit cR} {M : PresheafOfModules R} {cM : CategoryTheory.Limits.Cocone M.presheaf} {hcM : CategoryTheory.Limits.IsColimit cM} {U : Cᵒᵖ} : ↑(M.obj U) →+ ModuleColimit hcR hcM

The "inclusion" maps to the colimit module, as an additive map.

Equations

• PresheafOfModules.ModuleColimit.ιM = AddCommGrpCat.Hom.hom (cM.ι.app U)

@[simp]

theorem PresheafOfModules.ModuleColimit.smul_eq {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.IsCofiltered C] [CategoryTheory.InitiallySmall C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {cR : CategoryTheory.Limits.Cocone R} (hcR : CategoryTheory.Limits.IsColimit cR) {M : PresheafOfModules R} {cM : CategoryTheory.Limits.Cocone M.presheaf} (hcM : CategoryTheory.Limits.IsColimit cM) {U : Cᵒᵖ} (r : ↑(R.obj U)) (m : ↑(M.obj U)) : (ιR cR) r • ιM m = ιM (r • m)

theorem PresheafOfModules.ModuleColimit.ιM_jointly_surjective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.IsCofiltered C] [CategoryTheory.InitiallySmall C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {cR : CategoryTheory.Limits.Cocone R} {hcR : CategoryTheory.Limits.IsColimit cR} {M : PresheafOfModules R} {cM : CategoryTheory.Limits.Cocone M.presheaf} {hcM : CategoryTheory.Limits.IsColimit cM} (m : ModuleColimit hcR hcM) : ∃ (U : Cᵒᵖ) (x : ↑(M.obj U)), ιM x = m

theorem PresheafOfModules.ModuleColimit.ιM_jointly_surjective₂ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.IsCofiltered C] [CategoryTheory.InitiallySmall C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {cR : CategoryTheory.Limits.Cocone R} {hcR : CategoryTheory.Limits.IsColimit cR} {M : PresheafOfModules R} {cM : CategoryTheory.Limits.Cocone M.presheaf} {hcM : CategoryTheory.Limits.IsColimit cM} {M' : PresheafOfModules R} {cM' : CategoryTheory.Limits.Cocone M'.presheaf} {hcM' : CategoryTheory.Limits.IsColimit cM'} (m : ModuleColimit hcR hcM) (m' : ModuleColimit hcR hcM') : ∃ (U : Cᵒᵖ) (x : ↑(M.obj U)) (x' : ↑(M'.obj U)), ιM x = m ∧ ιM x' = m'

theorem PresheafOfModules.ModuleColimit.ιM_jointly_surjective₃ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.IsCofiltered C] [CategoryTheory.InitiallySmall C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {cR : CategoryTheory.Limits.Cocone R} {hcR : CategoryTheory.Limits.IsColimit cR} {M : PresheafOfModules R} {cM : CategoryTheory.Limits.Cocone M.presheaf} {hcM : CategoryTheory.Limits.IsColimit cM} {M' : PresheafOfModules R} {cM' : CategoryTheory.Limits.Cocone M'.presheaf} {hcM' : CategoryTheory.Limits.IsColimit cM'} {M'' : PresheafOfModules R} {cM'' : CategoryTheory.Limits.Cocone M''.presheaf} {hcM'' : CategoryTheory.Limits.IsColimit cM''} (m : ModuleColimit hcR hcM) (m' : ModuleColimit hcR hcM') (m'' : ModuleColimit hcR hcM'') : ∃ (U : Cᵒᵖ) (x : ↑(M.obj U)) (x' : ↑(M'.obj U)) (x'' : ↑(M''.obj U)), ιM x = m ∧ ιM x' = m' ∧ ιM x'' = m''

theorem PresheafOfModules.ModuleColimit.ιR_jointly_surjective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.IsCofiltered C] [CategoryTheory.InitiallySmall C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {cR : CategoryTheory.Limits.Cocone R} (hcR : CategoryTheory.Limits.IsColimit cR) (r : ↑cR.pt) : ∃ (U : Cᵒᵖ) (a : ↑(R.obj U)), (ιR cR) a = r

theorem PresheafOfModules.ModuleColimit.jointly_surjective₂ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.IsCofiltered C] [CategoryTheory.InitiallySmall C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {cR : CategoryTheory.Limits.Cocone R} {hcR : CategoryTheory.Limits.IsColimit cR} {M : PresheafOfModules R} {cM : CategoryTheory.Limits.Cocone M.presheaf} {hcM : CategoryTheory.Limits.IsColimit cM} (r : ↑cR.pt) (m : ModuleColimit hcR hcM) : ∃ (U : Cᵒᵖ) (a : ↑(R.obj U)) (x : ↑(M.obj U)), (ιR cR) a = r ∧ ιM x = m

theorem PresheafOfModules.ModuleColimit.jointly_surjective₃ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.IsCofiltered C] [CategoryTheory.InitiallySmall C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {cR : CategoryTheory.Limits.Cocone R} {hcR : CategoryTheory.Limits.IsColimit cR} {M : PresheafOfModules R} {cM : CategoryTheory.Limits.Cocone M.presheaf} {hcM : CategoryTheory.Limits.IsColimit cM} (r₁ r₂ : ↑cR.pt) (m : ModuleColimit hcR hcM) : ∃ (U : Cᵒᵖ) (a₁ : ↑(R.obj U)) (a₂ : ↑(R.obj U)) (x : ↑(M.obj U)), (ιR cR) a₁ = r₁ ∧ (ιR cR) a₂ = r₂ ∧ ιM x = m

theorem PresheafOfModules.ModuleColimit.jointly_surjective₃' {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.IsCofiltered C] [CategoryTheory.InitiallySmall C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {cR : CategoryTheory.Limits.Cocone R} {hcR : CategoryTheory.Limits.IsColimit cR} {M : PresheafOfModules R} {cM : CategoryTheory.Limits.Cocone M.presheaf} {hcM : CategoryTheory.Limits.IsColimit cM} {M' : PresheafOfModules R} {cM' : CategoryTheory.Limits.Cocone M'.presheaf} {hcM' : CategoryTheory.Limits.IsColimit cM'} (r : ↑cR.pt) (m₁ : ModuleColimit hcR hcM) (m₂ : ModuleColimit hcR hcM') : ∃ (U : Cᵒᵖ) (a : ↑(R.obj U)) (x₁ : ↑(M.obj U)) (x₂ : ↑(M'.obj U)), (ιR cR) a = r ∧ ιM x₁ = m₁ ∧ ιM x₂ = m₂

@[implicit_reducible]

noncomputable instance PresheafOfModules.ModuleColimit.instModuleCarrierPtOppositeRingCat {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.IsCofiltered C] [CategoryTheory.InitiallySmall C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {cR : CategoryTheory.Limits.Cocone R} (hcR : CategoryTheory.Limits.IsColimit cR) {M : PresheafOfModules R} {cM : CategoryTheory.Limits.Cocone M.presheaf} (hcM : CategoryTheory.Limits.IsColimit cM) : Module (↑cR.pt) (ModuleColimit hcR hcM)

Equations

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

noncomputable def PresheafOfModules.ModuleColimit.homEquiv' {C : Type u} [CategoryTheory.Category.{v, u} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {cR : CategoryTheory.Limits.Cocone R} (hcR : CategoryTheory.Limits.IsColimit cR) {M : PresheafOfModules R} {cM : CategoryTheory.Limits.Cocone M.presheaf} (hcM : CategoryTheory.Limits.IsColimit cM) {N : Type w} [AddCommGroup N] : (ModuleColimit hcR hcM →+ N) ≃+ (M.presheaf ⟶ (CategoryTheory.Functor.const Cᵒᵖ).obj (AddCommGrpCat.of N))

Auxiliary definition for homEquiv. This is the universal property of PresheafOfModules.ModuleColimit, as an abelian group.

Equations

• PresheafOfModules.ModuleColimit.homEquiv' hcR hcM = { toEquiv := CategoryTheory.ConcreteCategory.homEquiv.symm.trans hcM.homEquiv, map_add' := ⋯ }

theorem PresheafOfModules.ModuleColimit.homEquiv'_app_apply {C : Type u} [CategoryTheory.Category.{v, u} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {cR : CategoryTheory.Limits.Cocone R} (hcR : CategoryTheory.Limits.IsColimit cR) {M : PresheafOfModules R} {cM : CategoryTheory.Limits.Cocone M.presheaf} (hcM : CategoryTheory.Limits.IsColimit cM) {N : ModuleCat ↑cR.pt} (α : ModuleColimit hcR hcM →+ ↑N) {X : Cᵒᵖ} (x : ↑(M.obj X)) : (CategoryTheory.ConcreteCategory.hom (((homEquiv' hcR hcM) α).app X)) x = α ((CategoryTheory.ConcreteCategory.hom (cM.ι.app X)) x)

theorem PresheafOfModules.ModuleColimit.homEquiv'_symm_apply {C : Type u} [CategoryTheory.Category.{v, u} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {cR : CategoryTheory.Limits.Cocone R} (hcR : CategoryTheory.Limits.IsColimit cR) {M : PresheafOfModules R} {cM : CategoryTheory.Limits.Cocone M.presheaf} (hcM : CategoryTheory.Limits.IsColimit cM) {N : ModuleCat ↑cR.pt} (β : M.presheaf ⟶ (CategoryTheory.Functor.const Cᵒᵖ).obj (AddCommGrpCat.of ↑N)) {X : Cᵒᵖ} (x : ↑(M.obj X)) : ((homEquiv' hcR hcM).symm β) ((CategoryTheory.ConcreteCategory.hom (cM.ι.app X)) x) = (CategoryTheory.ConcreteCategory.hom (β.app X)) x

theorem PresheafOfModules.ModuleColimit.map_smul_homEquiv'_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.IsCofiltered C] [CategoryTheory.InitiallySmall C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {cR : CategoryTheory.Limits.Cocone R} (hcR : CategoryTheory.Limits.IsColimit cR) {M : PresheafOfModules R} {cM : CategoryTheory.Limits.Cocone M.presheaf} (hcM : CategoryTheory.Limits.IsColimit cM) {N : ModuleCat ↑cR.pt} (α : ModuleColimit hcR hcM →+ ↑N) : (∀ (U : Cᵒᵖ) (r : ↑(R.obj U)) (m : ↑(M.obj U)), (CategoryTheory.ConcreteCategory.hom (((homEquiv' hcR hcM) α).app U)) (r • m) = (CategoryTheory.ConcreteCategory.hom (cR.ι.app U)) r • (CategoryTheory.ConcreteCategory.hom (((homEquiv' hcR hcM) α).app U)) m) ↔ ∀ (r : ↑cR.pt) (m : ModuleColimit hcR hcM), α (r • m) = r • α m

noncomputable def PresheafOfModules.ModuleColimit.homEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.IsCofiltered C] [CategoryTheory.InitiallySmall C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {cR : CategoryTheory.Limits.Cocone R} (hcR : CategoryTheory.Limits.IsColimit cR) {M : PresheafOfModules R} {cM : CategoryTheory.Limits.Cocone M.presheaf} (hcM : CategoryTheory.Limits.IsColimit cM) {N : ModuleCat ↑cR.pt} : (ModuleCat.of (↑cR.pt) (ModuleColimit hcR hcM) ⟶ N) ≃+ (M ⟶ (constFunctor cR).obj N)

This is the universal property of PresheafOfModules.ModuleColimit as a module. See also PresheafOfModules.colimitAdjunction.

Equations

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

@[simp]

theorem PresheafOfModules.ModuleColimit.homEquiv_app_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.IsCofiltered C] [CategoryTheory.InitiallySmall C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {cR : CategoryTheory.Limits.Cocone R} (hcR : CategoryTheory.Limits.IsColimit cR) {M : PresheafOfModules R} {cM : CategoryTheory.Limits.Cocone M.presheaf} (hcM : CategoryTheory.Limits.IsColimit cM) {N : ModuleCat ↑cR.pt} (α : ModuleCat.of (↑cR.pt) (ModuleColimit hcR hcM) ⟶ N) {X : Cᵒᵖ} (x : ↑(M.obj X)) : (CategoryTheory.ConcreteCategory.hom (((homEquiv hcR hcM) α).app X)) x = (CategoryTheory.ConcreteCategory.hom α) ((CategoryTheory.ConcreteCategory.hom (cM.ι.app X)) x)

theorem PresheafOfModules.ModuleColimit.homEquiv_naturality_right {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.IsCofiltered C] [CategoryTheory.InitiallySmall C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {cR : CategoryTheory.Limits.Cocone R} (hcR : CategoryTheory.Limits.IsColimit cR) {M : PresheafOfModules R} {cM : CategoryTheory.Limits.Cocone M.presheaf} (hcM : CategoryTheory.Limits.IsColimit cM) {N N' : ModuleCat ↑cR.pt} (φ : ModuleCat.of (↑cR.pt) (ModuleColimit hcR hcM) ⟶ N) (g : N ⟶ N') : (homEquiv hcR hcM) (CategoryTheory.CategoryStruct.comp φ g) = CategoryTheory.CategoryStruct.comp ((homEquiv hcR hcM) φ) ((constFunctor cR).map g)

@[simp]

theorem PresheafOfModules.ModuleColimit.homEquiv_symm_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.IsCofiltered C] [CategoryTheory.InitiallySmall C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {cR : CategoryTheory.Limits.Cocone R} (hcR : CategoryTheory.Limits.IsColimit cR) {M : PresheafOfModules R} {cM : CategoryTheory.Limits.Cocone M.presheaf} (hcM : CategoryTheory.Limits.IsColimit cM) {N : ModuleCat ↑cR.pt} (β : M ⟶ (constFunctor cR).obj N) {X : Cᵒᵖ} (x : ↑(M.obj X)) : (CategoryTheory.ConcreteCategory.hom ((homEquiv hcR hcM).symm β)) ((CategoryTheory.ConcreteCategory.hom (cM.ι.app X)) x) = (CategoryTheory.ConcreteCategory.hom (β.app X)) x

noncomputable def PresheafOfModules.ModuleColimit.map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.IsCofiltered C] [CategoryTheory.InitiallySmall C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {cR : CategoryTheory.Limits.Cocone R} (hcR : CategoryTheory.Limits.IsColimit cR) {M : PresheafOfModules R} {cM : CategoryTheory.Limits.Cocone M.presheaf} (hcM : CategoryTheory.Limits.IsColimit cM) {M' : PresheafOfModules R} {cM' : CategoryTheory.Limits.Cocone M'.presheaf} (hcM' : CategoryTheory.Limits.IsColimit cM') (f : M ⟶ M') : ModuleColimit hcR hcM →ₗ[↑cR.pt] ModuleColimit hcR hcM'

The linear map between the colimit modules induced by a morphism of modules.

Equations

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

@[simp]

theorem PresheafOfModules.ModuleColimit.map_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.IsCofiltered C] [CategoryTheory.InitiallySmall C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {cR : CategoryTheory.Limits.Cocone R} (hcR : CategoryTheory.Limits.IsColimit cR) {M : PresheafOfModules R} {cM : CategoryTheory.Limits.Cocone M.presheaf} (hcM : CategoryTheory.Limits.IsColimit cM) {M' : PresheafOfModules R} {cM' : CategoryTheory.Limits.Cocone M'.presheaf} (hcM' : CategoryTheory.Limits.IsColimit cM') (f : M ⟶ M') {U : Cᵒᵖ} (m : ↑(M.obj U)) : (map hcR hcM hcM' f) (ιM m) = ιM ((CategoryTheory.ConcreteCategory.hom (f.app U)) m)

@[simp]

theorem PresheafOfModules.ModuleColimit.map_id {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.IsCofiltered C] [CategoryTheory.InitiallySmall C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {cR : CategoryTheory.Limits.Cocone R} (hcR : CategoryTheory.Limits.IsColimit cR) {M : PresheafOfModules R} {cM : CategoryTheory.Limits.Cocone M.presheaf} (hcM : CategoryTheory.Limits.IsColimit cM) : map hcR hcM hcM (CategoryTheory.CategoryStruct.id M) = LinearMap.id

theorem PresheafOfModules.ModuleColimit.comp_map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.IsCofiltered C] [CategoryTheory.InitiallySmall C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {cR : CategoryTheory.Limits.Cocone R} (hcR : CategoryTheory.Limits.IsColimit cR) {M : PresheafOfModules R} {cM : CategoryTheory.Limits.Cocone M.presheaf} (hcM : CategoryTheory.Limits.IsColimit cM) {M' : PresheafOfModules R} {cM' : CategoryTheory.Limits.Cocone M'.presheaf} (hcM' : CategoryTheory.Limits.IsColimit cM') (f : M ⟶ M') {M'' : PresheafOfModules R} {cM'' : CategoryTheory.Limits.Cocone M''.presheaf} (hcM'' : CategoryTheory.Limits.IsColimit cM'') (g : M' ⟶ M'') : map hcR hcM' hcM'' g ∘ₗ map hcR hcM hcM' f = map hcR hcM hcM'' (CategoryTheory.CategoryStruct.comp f g)

theorem PresheafOfModules.ModuleColimit.homEquiv_naturality_left {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.IsCofiltered C] [CategoryTheory.InitiallySmall C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {cR : CategoryTheory.Limits.Cocone R} (hcR : CategoryTheory.Limits.IsColimit cR) {M : PresheafOfModules R} {cM : CategoryTheory.Limits.Cocone M.presheaf} (hcM : CategoryTheory.Limits.IsColimit cM) {M' : PresheafOfModules R} {cM' : CategoryTheory.Limits.Cocone M'.presheaf} (hcM' : CategoryTheory.Limits.IsColimit cM') {N : ModuleCat ↑cR.pt} (φ' : ModuleCat.of (↑cR.pt) (ModuleColimit hcR hcM') ⟶ N) (f : M ⟶ M') : (homEquiv hcR hcM) (CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (map hcR hcM hcM' f)) φ') = CategoryTheory.CategoryStruct.comp f ((homEquiv hcR hcM') φ')

theorem PresheafOfModules.ModuleColimit.homEquiv_naturality_left_symm {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.IsCofiltered C] [CategoryTheory.InitiallySmall C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {cR : CategoryTheory.Limits.Cocone R} (hcR : CategoryTheory.Limits.IsColimit cR) {M : PresheafOfModules R} {cM : CategoryTheory.Limits.Cocone M.presheaf} (hcM : CategoryTheory.Limits.IsColimit cM) {M' : PresheafOfModules R} {cM' : CategoryTheory.Limits.Cocone M'.presheaf} (hcM' : CategoryTheory.Limits.IsColimit cM') {N : ModuleCat ↑cR.pt} (f : M ⟶ M') (g : M' ⟶ (constFunctor cR).obj N) : (homEquiv hcR hcM).symm (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (map hcR hcM hcM' f)) ((homEquiv hcR hcM').symm g)

noncomputable def PresheafOfModules.colimitFunctor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.IsCofiltered C] [CategoryTheory.InitiallySmall C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {cR : CategoryTheory.Limits.Cocone R} (hcR : CategoryTheory.Limits.IsColimit cR) : CategoryTheory.Functor (PresheafOfModules R) (ModuleCat ↑cR.pt)

The colimit module functor from the category of presheaves of modules over a presheaf of rings R on a cofiltered category to the category of modules over a colimit of R.

Equations

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

noncomputable def PresheafOfModules.colimitAdjunction {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.IsCofiltered C] [CategoryTheory.InitiallySmall C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {cR : CategoryTheory.Limits.Cocone R} (hcR : CategoryTheory.Limits.IsColimit cR) : colimitFunctor hcR ⊣ constFunctor cR

Given a presheaf of rings R on a cofiltered category, this is the adjunction between colimitFunctor : PresheafOfModules R ⥤ ModuleCat cR.pt and the constant functor.

Equations

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

theorem PresheafOfModules.colimitAdjunction_homEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.IsCofiltered C] [CategoryTheory.InitiallySmall C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {cR : CategoryTheory.Limits.Cocone R} (hcR : CategoryTheory.Limits.IsColimit cR) (F : PresheafOfModules R) (G : ModuleCat ↑cR.pt) : (colimitAdjunction hcR).homEquiv F G = ↑(ModuleColimit.homEquiv hcR (CategoryTheory.Limits.colimit.isColimit F.presheaf))

theorem PresheafOfModules.colimitAdjunction_homEquiv_symm_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.IsCofiltered C] [CategoryTheory.InitiallySmall C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {cR : CategoryTheory.Limits.Cocone R} (hcR : CategoryTheory.Limits.IsColimit cR) {F : PresheafOfModules R} {G : ModuleCat ↑cR.pt} (β : F ⟶ (constFunctor cR).obj G) {X : Cᵒᵖ} (m : ↑(F.obj X)) : (CategoryTheory.ConcreteCategory.hom (((colimitAdjunction hcR).homEquiv F G).symm β)) (ModuleColimit.ιM m) = (CategoryTheory.ConcreteCategory.hom (β.app X)) m