Documentation

Mathlib.CategoryTheory.ConcreteCategory.Elementwise

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

source
@[simp]
theorem CategoryTheory.Limits.colimit.w_apply {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] (F : Functor J C) [HasColimit F] {j j' : J} (f : j ⟶ j') [inst : HasForget C] (x : (forget C).obj (F.obj j)) :
(ι F j') ((F.map f) x) = (ι F j) x
source
@[simp]
theorem CategoryTheory.Limits.limit.lift_π_apply {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F : Functor J C} [HasLimit F] (c : Cone F) (j : J) [inst : HasForget C] (x : (forget C).obj c.pt) :
(π F j) ((lift F c) x) = (c.π.app j) x
source
@[simp]
theorem CategoryTheory.Limits.kernel.condition_apply {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [HasKernel f] [inst : HasForget C] (x : (forget C).obj (kernel f)) :
f ((ι f) x) = 0 x
source
@[simp]
theorem CategoryTheory.Limits.cokernel.π_desc_apply {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [HasCokernel f] {W : C} (k : Y ⟶ W) (h : CategoryStruct.comp f k = 0) [inst : HasForget C] (x : (forget C).obj Y) :
(desc f k h) ((π f) x) = k x
source
@[simp]
theorem CategoryTheory.Limits.Cone.w_apply {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} (c : Cone F) {j j' : J} (f : j ⟶ j') [inst : HasForget C] (x : (forget C).obj (((Functor.const J).obj c.pt).obj j)) :
(F.map f) ((c.π.app j) x) = (c.π.app j') x
source
@[simp]
theorem CategoryTheory.Limits.colimit.ι_desc_apply {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F : Functor J C} [HasColimit F] (c : Cocone F) (j : J) [inst : HasForget C] (x : (forget C).obj (F.obj j)) :
(desc F c) ((ι F j) x) = (c.ι.app j) x
source
@[simp]
theorem CategoryTheory.Limits.kernel.lift_ι_apply {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [HasKernel f] {W : C} (k : W ⟶ X) (h : CategoryStruct.comp k f = 0) [inst : HasForget C] (x : (forget C).obj W) :
(ι f) ((lift f k h) x) = k x
source
@[simp]
theorem CategoryTheory.Limits.limit.w_apply {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] (F : Functor J C) [HasLimit F] {j j' : J} (f : j ⟶ j') [inst : HasForget C] (x : (forget C).obj (limit F)) :
(F.map f) ((π F j) x) = (π F j') x
source
@[simp]
theorem CategoryTheory.Limits.cokernel.condition_apply {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [HasCokernel f] [inst : HasForget C] (x : (forget C).obj X) :
(π f) (f x) = 0 x
source
theorem CategoryTheory.Limits.Cocone.w_apply {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} (c : Cocone F) {j j' : J} (f : j ⟶ j') [inst : HasForget C] (x : (forget C).obj (F.obj j)) :
(c.ι.app j') ((F.map f) x) = (c.ι.app j) x