Colimits in ModuleCat

Let C be a concrete category and F : J ⥤ C a filtered diagram in C. We discuss some results about colimit F when objects and morphisms in C have some algebraic structures.

Main results

• CategoryTheory.Limits.Concrete.colimit_rep_eq_zero: Let C be a category where its objects have zero elements and morphisms preserve zero. If x : Fⱼ is mapped to 0 in the colimit, then there exists a i ⟶ j such that x restricted to i is already 0.

• CategoryTheory.Limits.Concrete.colimit_no_zero_smul_divisor: Let C be a category where its objects are R-modules and morphisms R-linear maps. Let r : R be an element without zero smul divisors for all small sections, i.e. there exists some j : J such that for all j ⟶ i and x : Fᵢ we have r • x = 0 implies x = 0, then if r • x = 0 for x : colimit F, then x = 0.

Implementation details

For now, we specialize our results to C = ModuleCat R, which is the only place they are used. In the future they might be generalized by assuming a HasForget₂ C (ModuleCat R) instance, plus assertions that the module structures induced by HasForget₂ coincide.

theorem CategoryTheory.Limits.Concrete.colimit_rep_eq_zero (R : Type u_1) [Ring R] {J : Type w} [Category.{r, w} J] (F : Functor J (ModuleCat R)) [PreservesColimit F (forget (ModuleCat R))] [IsFiltered J] [HasColimit F] (j : J) (x : ↑(F.obj j)) (hx : (ConcreteCategory.hom (colimit.ι F j)) x = 0) : ∃ (j' : J) (i : j ⟶ j'), (ModuleCat.Hom.hom (F.map i)) x = 0

theorem CategoryTheory.Limits.Concrete.colimit_no_zero_smul_divisor (R : Type u_1) [Ring R] {J : Type w} [Category.{r, w} J] (F : Functor J (ModuleCat R)) [PreservesColimit F (forget (ModuleCat R))] [IsFiltered J] [HasColimit F] (r : R) (H : ∃ (j' : J), ∀ (j : J) (x : j' ⟶ j) (c : ↑(F.obj j)), r • c = 0 → c = 0) (x : ToType (colimit F)) (hx : r • x = 0) : x = 0

if r has no zero smul divisors for all small-enough sections, then r has no zero smul divisors in the colimit.