# mathlibdocumentation

category_theory.concrete_category.elementwise

In this file we provide various simp lemmas in its elementwise form via tactic.elementwise.

@[simp]
theorem category_theory.limits.limit.w_apply {J : Type u₁} {C : Type u} (F : J C) {j j' : J} (f : j j') (x : ) :
(F.map f) x) = x
@[simp]
theorem category_theory.limits.colimit.w_apply {J : Type u₁} {C : Type u} (F : J C) {j j' : J} (f : j j') (x : (F.obj j)) :
((F.map f) x) =
@[simp]
theorem category_theory.limits.cokernel.π_desc_apply {C : Type u} {X Y : C} (f : X Y) {W : C} (k : Y W) (h : f k = 0) (x : Y) :
= k x
@[simp]
theorem category_theory.limits.cocone.w_apply {J : Type u₁} {C : Type u₃} {F : J C} {j j' : J} (f : j j') (x : (F.obj j)) :
(c.ι.app j') ((F.map f) x) = (c.ι.app j) x
@[simp]
theorem category_theory.limits.limit.lift_π_apply {J : Type u₁} {C : Type u} {F : J C} (j : J) (x : (c.X)) :
= (c.π.app j) x
@[simp]
theorem category_theory.limits.kernel.lift_ι_apply {C : Type u} {X Y : C} (f : X Y) {W : C} (k : W X) (h : k f = 0) (x : W) :
= k x
@[simp]
theorem category_theory.limits.kernel.condition_apply {C : Type u} {X Y : C} (f : X Y) (x : ) :
f = 0 x
@[simp]
theorem category_theory.limits.colimit.ι_desc_apply {J : Type u₁} {C : Type u} {F : J C} (j : J) (x : (F.obj j)) :
= (c.ι.app j) x
@[simp]
theorem category_theory.limits.cokernel.condition_apply {C : Type u} {X Y : C} (f : X Y) (x : X) :
(f x) = 0 x
@[simp]
theorem category_theory.limits.cone.w_apply {J : Type u₁} {C : Type u₃} {F : J C} {j j' : J} (f : j j') (x : c.X).obj j)) :
(F.map f) ((c.π.app j) x) = (c.π.app j') x