The forgetful functor from R-modules preserves filtered colimits.

Forgetful functors from algebraic categories usually don't preserve colimits. However, they tend to preserve filtered colimits.

In this file, we start with a ring R, a small filtered category J and a functor F : J ⥤ ModuleCat R. We show that the colimit of F ⋙ forget₂ (ModuleCat R) AddCommGroupCat (in AddCommGroupCat) carries the structure of an R-module, thereby showing that the forgetful functor forget₂ (ModuleCat R) AddCommGroupCat preserves filtered colimits. In particular, this implies that forget (ModuleCat R) preserves filtered colimits.

@[inline, reducible]

abbrev ModuleCat.FilteredColimits.M {R : Type u} [Ring R] {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J (ModuleCatMax R)) : AddCommGroupCat

The colimit of F ⋙ forget₂ (ModuleCat R) AddCommGroupCat in the category AddCommGroupCat. In the following, we will show that this has the structure of an R-module.

@[inline, reducible]

abbrev ModuleCat.FilteredColimits.M.mk {R : Type u} [Ring R] {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J (ModuleCatMax R)) : (j : J) × ↑(F.obj j) → ↑(ModuleCat.FilteredColimits.M F)

The canonical projection into the colimit, as a quotient type.

theorem ModuleCat.FilteredColimits.M.mk_eq {R : Type u} [Ring R] {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J (ModuleCatMax R)) (x : (j : J) × ↑(F.obj j)) (y : (j : J) × ↑(F.obj j)) (h : ∃ k f g, ↑(F.map f) x.snd = ↑(F.map g) y.snd) : ModuleCat.FilteredColimits.M.mk F x = ModuleCat.FilteredColimits.M.mk F y

def ModuleCat.FilteredColimits.colimitSMulAux {R : Type u} [Ring R] {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J (ModuleCatMax R)) (r : R) (x : (j : J) × ↑(F.obj j)) : ↑(ModuleCat.FilteredColimits.M F)

The "unlifted" version of scalar multiplication in the colimit.

theorem ModuleCat.FilteredColimits.colimitSMulAux_eq_of_rel {R : Type u} [Ring R] {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J (ModuleCatMax R)) (r : R) (x : (j : J) × ↑(F.obj j)) (y : (j : J) × ↑(F.obj j)) (h : CategoryTheory.Limits.Types.FilteredColimit.Rel (CategoryTheory.Functor.comp F (CategoryTheory.forget (ModuleCat R))) x y) : ModuleCat.FilteredColimits.colimitSMulAux F r x = ModuleCat.FilteredColimits.colimitSMulAux F r y

instance ModuleCat.FilteredColimits.colimitHasSmul {R : Type u} [Ring R] {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J (ModuleCatMax R)) : SMul R ↑(ModuleCat.FilteredColimits.M F)

Scalar multiplication in the colimit. See also colimitSMulAux.

@[simp]

theorem ModuleCat.FilteredColimits.colimit_smul_mk_eq {R : Type u} [Ring R] {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J (ModuleCatMax R)) (r : R) (x : (j : J) × ↑(F.obj j)) : r • ModuleCat.FilteredColimits.M.mk F x = ModuleCat.FilteredColimits.M.mk F { fst := x.fst, snd := r • x.snd }

instance ModuleCat.FilteredColimits.colimitMulAction {R : Type u} [Ring R] {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J (ModuleCatMax R)) : MulAction R ↑(ModuleCat.FilteredColimits.M F)

instance ModuleCat.FilteredColimits.colimitSMulWithZero {R : Type u} [Ring R] {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J (ModuleCatMax R)) : SMulWithZero R ↑(ModuleCat.FilteredColimits.M F)

instance ModuleCat.FilteredColimits.colimitModule {R : Type u} [Ring R] {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J (ModuleCatMax R)) : Module R ↑(ModuleCat.FilteredColimits.M F)

def ModuleCat.FilteredColimits.colimit {R : Type u} [Ring R] {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J (ModuleCatMax R)) : ModuleCatMax R

The bundled R-module giving the filtered colimit of a diagram.

def ModuleCat.FilteredColimits.coconeMorphism {R : Type u} [Ring R] {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J (ModuleCatMax R)) (j : J) : F.obj j ⟶ ModuleCat.FilteredColimits.colimit F

The linear map from a given R-module in the diagram to the colimit module.

def ModuleCat.FilteredColimits.colimitCocone {R : Type u} [Ring R] {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J (ModuleCatMax R)) : CategoryTheory.Limits.Cocone F

The cocone over the proposed colimit module.

def ModuleCat.FilteredColimits.colimitDesc {R : Type u} [Ring R] {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J (ModuleCatMax R)) (t : CategoryTheory.Limits.Cocone F) : ModuleCat.FilteredColimits.colimit F ⟶ t.pt

Given a cocone t of F, the induced monoid linear map from the colimit to the cocone point. We already know that this is a morphism between additive groups. The only thing left to see is that it is a linear map, i.e. preserves scalar multiplication.

def ModuleCat.FilteredColimits.colimitCoconeIsColimit {R : Type u} [Ring R] {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J (ModuleCatMax R)) : CategoryTheory.Limits.IsColimit (ModuleCat.FilteredColimits.colimitCocone F)

The proposed colimit cocone is a colimit in ModuleCat R.

instance ModuleCat.FilteredColimits.forget₂AddCommGroupPreservesFilteredColimits {R : Type u} [Ring R] : CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget₂ (ModuleCat R) AddCommGroupCat)

instance ModuleCat.FilteredColimits.forgetPreservesFilteredColimits {R : Type u} [Ring R] : CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget (ModuleCat R))