Colimits in concrete categories with algebraic structures

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.

theorem CategoryTheory.Limits.Concrete.colimit_rep_eq_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ConcreteCategory C] {J : Type w} [CategoryTheory.Category.{r, w} J] (F : CategoryTheory.Functor J C) [CategoryTheory.Limits.PreservesColimit F (CategoryTheory.forget C)] [CategoryTheory.IsFiltered J] [(c : C) → Zero ((CategoryTheory.forget C).obj c)] [∀ {c c' : C}, ZeroHomClass (c ⟶ c') ((CategoryTheory.forget C).obj c) ((CategoryTheory.forget C).obj c')] [CategoryTheory.Limits.HasColimit F] (j : J) (x : (CategoryTheory.forget C).obj (F.obj j)) (hx : (CategoryTheory.Limits.colimit.ι F j) x = 0) : ∃ (j' : J) (i : j ⟶ j'), (F.map i) x = 0

theorem CategoryTheory.Limits.Concrete.colimit_no_zero_smul_divisor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ConcreteCategory C] {J : Type w} [CategoryTheory.Category.{r, w} J] (F : CategoryTheory.Functor J C) [CategoryTheory.Limits.PreservesColimit F (CategoryTheory.forget C)] [CategoryTheory.IsFiltered J] [CategoryTheory.Limits.HasColimit F] (R : Type u_1) [Semiring R] [(c : C) → AddCommMonoid ((CategoryTheory.forget C).obj c)] [(c : C) → Module R ((CategoryTheory.forget C).obj c)] [∀ {c c' : C}, LinearMapClass (c ⟶ c') R ((CategoryTheory.forget C).obj c) ((CategoryTheory.forget C).obj c')] (r : R) (H : ∃ (j' : J), ∀ (j : J), (j' ⟶ j) → ∀ (c : (CategoryTheory.forget C).obj (F.obj j)), r • c = 0 → c = 0) (x : (CategoryTheory.forget C).obj (CategoryTheory.Limits.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.