# Documentation

## Mathlib.CategoryTheory.ConcreteCategory.Elementwise

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

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