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

@[reducible, inline]
abbrev ModuleCat.FilteredColimits.M {R : Type u} [Ring R] {J : Type v} (F : ) :

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.

Equations
Instances For
@[reducible, inline]
abbrev ModuleCat.FilteredColimits.M.mk {R : Type u} [Ring R] {J : Type v} (F : ) :
(j : J) × (F.obj j)

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

Equations
Instances For
theorem ModuleCat.FilteredColimits.M.mk_eq {R : Type u} [Ring R] {J : Type v} (F : ) (x : (j : J) × (F.obj j)) (y : (j : J) × (F.obj j)) (h : ∃ (k : J) (f : x.fst k) (g : y.fst k), (F.map f) x.snd = (F.map g) y.snd) :
def ModuleCat.FilteredColimits.colimitSMulAux {R : Type u} [Ring R] {J : Type v} (F : ) (r : R) (x : (j : J) × (F.obj j)) :

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

Equations
Instances For
theorem ModuleCat.FilteredColimits.colimitSMulAux_eq_of_rel {R : Type u} [Ring R] {J : Type v} (F : ) (r : R) (x : (j : J) × (F.obj j)) (y : (j : J) × (F.obj j)) (h : ) :
instance ModuleCat.FilteredColimits.colimitHasSMul {R : Type u} [Ring R] {J : Type v} (F : ) :

Scalar multiplication in the colimit. See also colimitSMulAux.

Equations
• = { smul := fun (r : R) (x : ) => }
@[simp]
theorem ModuleCat.FilteredColimits.colimit_smul_mk_eq {R : Type u} [Ring R] {J : Type v} (F : ) (r : R) (x : (j : J) × (F.obj j)) :
= ModuleCat.FilteredColimits.M.mk F x.fst, r x.snd
instance ModuleCat.FilteredColimits.colimitMulAction {R : Type u} [Ring R] {J : Type v} (F : ) :
Equations
instance ModuleCat.FilteredColimits.colimitSMulWithZero {R : Type u} [Ring R] {J : Type v} (F : ) :
Equations
instance ModuleCat.FilteredColimits.colimitModule {R : Type u} [Ring R] {J : Type v} (F : ) :
Equations
• = let __src := ; let __src_1 := ;
def ModuleCat.FilteredColimits.colimit {R : Type u} [Ring R] {J : Type v} (F : ) :

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

Equations
Instances For
def ModuleCat.FilteredColimits.coconeMorphism {R : Type u} [Ring R] {J : Type v} (F : ) (j : J) :
F.obj j

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
def ModuleCat.FilteredColimits.colimitCocone {R : Type u} [Ring R] {J : Type v} (F : ) :

The cocone over the proposed colimit module.

Equations
• = { pt := , ι := { app := , naturality := } }
Instances For
def ModuleCat.FilteredColimits.colimitDesc {R : Type u} [Ring R] {J : Type v} (F : ) (t : ) :

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.

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

The proposed colimit cocone is a colimit in ModuleCat R.

Equations
• = { desc := , fac := , uniq := }
Instances For
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.