Documentation

Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic

Facts about (co)limits of functors into concrete categories #

If a functor G : J ⥤ C to a concrete category has a limit and that forget C is corepresentable, then (G ⋙ forget C).sections is small.

Given surjections ⋯ ⟶ Xₙ₊₁ ⟶ Xₙ ⟶ ⋯ ⟶ X₀ in a concrete category whose forgetful functor preserves sequential limits, the projection map lim Xₙ ⟶ X₀ is surjective.

theorem CategoryTheory.Limits.Concrete.isColimit_rep_eq_of_exists {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ConcreteCategory C] {J : Type w} [CategoryTheory.Category.{r, w} J] (F : CategoryTheory.Functor J C) {D : CategoryTheory.Limits.Cocone F} {i : J} {j : J} (x : (CategoryTheory.forget C).obj (F.obj i)) (y : (CategoryTheory.forget C).obj (F.obj j)) (h : ∃ (k : J) (f : i k) (g : j k), (F.map f) x = (F.map g) y) :
(D.app i) x = (D.app j) y