Documentation

Mathlib.CategoryTheory.Limits.ConcreteCategory

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

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