mathlib documentation

category_theory.limits.concrete_category

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

@[simp]
theorem category_theory.limits.cocone.w_apply {J : Type v} [category_theory.small_category J] {C : Type u₁} [category_theory.category C] {F : J C} (c : category_theory.limits.cocone F) {j j' : J} (f : j j') [I : category_theory.concrete_category C] (x : (F.obj j)) :
(c.ι.app j') ((F.map f) x) = (c.ι.app j) x
@[simp]
theorem category_theory.limits.cone.w_apply {J : Type v} [category_theory.small_category J] {C : Type u₁} [category_theory.category C] {F : J C} (c : category_theory.limits.cone F) {j j' : J} (f : j j') [I : category_theory.concrete_category C] (x : (((category_theory.functor.const J).obj c.X).obj j)) :
(F.map f) ((c.π.app j) x) = (c.π.app j') x