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) AddCommGrpCat (in AddCommGrpCat) carries the structure of an R-module, thereby showing that the forgetful functor forget₂ (ModuleCat R) AddCommGrpCat preserves filtered colimits. In particular, this implies that forget (ModuleCat R) preserves filtered colimits.

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

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

Equations

• ModuleCat.FilteredColimits.M F = AddCommGrpCat.FilteredColimits.colimit (F.comp (CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat))

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

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

Equations

• ModuleCat.FilteredColimits.M.mk F x = (F.comp (CategoryTheory.forget (ModuleCat R))).ιColimitType x.fst x.snd

theorem ModuleCat.FilteredColimits.M.mk_surjective {R : Type u} [Ring R] {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J (ModuleCat R)) (m : ↑(M F)) : ∃ (j : J) (x : ↑(F.obj j)), mk F ⟨j, x⟩ = m

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

theorem ModuleCat.FilteredColimits.M.mk_map {R : Type u} [Ring R] {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J (ModuleCat R)) {j k : J} (f : j ⟶ k) (x : ↑(F.obj j)) : mk F ⟨k, (CategoryTheory.ConcreteCategory.hom (F.map f)) x⟩ = mk F ⟨j, x⟩

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

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

Equations

• ModuleCat.FilteredColimits.colimitSMulAux F r x = ModuleCat.FilteredColimits.M.mk F ⟨x.fst, r • x.snd⟩

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 (ModuleCat R)) (r : R) (x y : (j : J) × ↑(F.obj j)) (h : CategoryTheory.Limits.Types.FilteredColimit.Rel (F.comp (CategoryTheory.forget (ModuleCat R))) x y) : colimitSMulAux F r x = colimitSMulAux F r y

@[implicit_reducible]

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

Scalar multiplication in the colimit. See also colimitSMulAux.

Equations

• ModuleCat.FilteredColimits.colimitHasSMul F = { smul := fun (r : R) (x : ↑(ModuleCat.FilteredColimits.M F)) => Quot.lift (ModuleCat.FilteredColimits.colimitSMulAux F r) ⋯ x }

theorem ModuleCat.FilteredColimits.colimit_zero_eq {R : Type u} [Ring R] {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J (ModuleCat R)) (j : J) : 0 = M.mk F ⟨j, 0⟩

theorem ModuleCat.FilteredColimits.colimit_add_mk_eq {R : Type u} [Ring R] {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J (ModuleCat R)) (x y : (j : J) × ↑(F.obj j)) (k : J) (f : x.fst ⟶ k) (g : y.fst ⟶ k) : M.mk F x + M.mk F y = M.mk F ⟨k, (CategoryTheory.ConcreteCategory.hom (F.map f)) x.snd + (CategoryTheory.ConcreteCategory.hom (F.map g)) y.snd⟩

theorem ModuleCat.FilteredColimits.colimit_add_mk_eq' {R : Type u} [Ring R] {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J (ModuleCat R)) {j : J} (x y : ↑(F.obj j)) : M.mk F ⟨j, x⟩ + M.mk F ⟨j, y⟩ = M.mk F ⟨j, x + y⟩

@[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 (ModuleCat R)) (r : R) (x : (j : J) × ↑(F.obj j)) : r • M.mk F x = M.mk F ⟨x.fst, r • x.snd⟩

@[implicit_reducible]

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

Equations

• ModuleCat.FilteredColimits.colimitMulAction F = { toSMul := ModuleCat.FilteredColimits.colimitHasSMul F, mul_smul := ⋯, one_smul := ⋯ }

@[implicit_reducible]

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

Equations

• ModuleCat.FilteredColimits.colimitSMulWithZero F = { toSMul := (ModuleCat.FilteredColimits.colimitMulAction F).toSMul, smul_zero := ⋯, zero_smul := ⋯ }

@[implicit_reducible]

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

Equations

• ModuleCat.FilteredColimits.colimitModule F = { toMulAction := ModuleCat.FilteredColimits.colimitMulAction F, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯ }

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

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

Equations

• ModuleCat.FilteredColimits.colimit F = ModuleCat.of R ↑(ModuleCat.FilteredColimits.M F)

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

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.

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

The cocone over the proposed colimit module.

Equations

• ModuleCat.FilteredColimits.colimitCocone F = { pt := ModuleCat.FilteredColimits.colimit F, ι := { app := ModuleCat.FilteredColimits.coconeMorphism F, naturality := ⋯ } }

noncomputable def ModuleCat.FilteredColimits.colimitDesc {R : Type u} [Ring R] {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J (ModuleCat R)) (t : CategoryTheory.Limits.Cocone F) : 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.

Equations

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

@[simp]

theorem ModuleCat.FilteredColimits.ι_colimitDesc {R : Type u} [Ring R] {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J (ModuleCat R)) (t : CategoryTheory.Limits.Cocone F) (j : J) : CategoryTheory.CategoryStruct.comp ((colimitCocone F).ι.app j) (colimitDesc F t) = t.ι.app j

@[simp]

theorem ModuleCat.FilteredColimits.ι_colimitDesc_assoc {R : Type u} [Ring R] {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J (ModuleCat R)) (t : CategoryTheory.Limits.Cocone F) (j : J) {Z : ModuleCat R} (h : t.pt ⟶ Z) : CategoryTheory.CategoryStruct.comp ((colimitCocone F).ι.app j) (CategoryTheory.CategoryStruct.comp (colimitDesc F t) h) = CategoryTheory.CategoryStruct.comp (t.ι.app j) h

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

The proposed colimit cocone is a colimit in ModuleCat R.

Equations

• ModuleCat.FilteredColimits.colimitCoconeIsColimit F = { desc := ModuleCat.FilteredColimits.colimitDesc F, fac := ⋯, uniq := ⋯ }

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

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

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