In this file we provide various simp lemmas in its elementwise form via Tactic.Elementwise.
@[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')
{F✝ : C → C → Type uF}
{carrier : C → Type w}
{instFunLike : (X Y : C) → FunLike (F✝ X Y) (carrier X) (carrier Y)}
[inst : ConcreteCategory C F✝]
(x : ToType (F.obj j))
:
(ConcreteCategory.hom (ι F j')) ((ConcreteCategory.hom (F.map f)) x) = (ConcreteCategory.hom (ι F j)) x
@[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)
{F✝ : C → C → Type uF}
{carrier : C → Type w}
{instFunLike : (X Y : C) → FunLike (F✝ X Y) (carrier X) (carrier Y)}
[inst : ConcreteCategory C F✝]
(x : ToType c.pt)
:
@[simp]
theorem
CategoryTheory.Limits.kernel.condition_apply
{C : Type u}
[Category.{v, u} C]
[HasZeroMorphisms C]
{X Y : C}
(f : X ⟶ Y)
[HasKernel f]
{F : C → C → Type uF}
{carrier : C → Type w}
{instFunLike : (X Y : C) → FunLike (F X Y) (carrier X) (carrier Y)}
[inst : ConcreteCategory C F]
(x : ToType (kernel f))
:
@[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)
{F : C → C → Type uF}
{carrier : C → Type w}
{instFunLike : (X Y : C) → FunLike (F X Y) (carrier X) (carrier Y)}
[inst : ConcreteCategory C F]
(x : ToType Y)
:
@[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')
{F✝ : C → C → Type uF}
{carrier : C → Type w}
{instFunLike : (X Y : C) → FunLike (F✝ X Y) (carrier X) (carrier Y)}
[inst : ConcreteCategory C F✝]
(x : ToType (((Functor.const J).obj c.pt).obj j))
:
@[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)
{F✝ : C → C → Type uF}
{carrier : C → Type w}
{instFunLike : (X Y : C) → FunLike (F✝ X Y) (carrier X) (carrier Y)}
[inst : ConcreteCategory C F✝]
(x : ToType (F.obj j))
:
@[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)
{F : C → C → Type uF}
{carrier : C → Type w}
{instFunLike : (X Y : C) → FunLike (F X Y) (carrier X) (carrier Y)}
[inst : ConcreteCategory C F]
(x : ToType W)
:
@[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')
{F✝ : C → C → Type uF}
{carrier : C → Type w}
{instFunLike : (X Y : C) → FunLike (F✝ X Y) (carrier X) (carrier Y)}
[inst : ConcreteCategory C F✝]
(x : ToType (limit F))
:
(ConcreteCategory.hom (F.map f)) ((ConcreteCategory.hom (π F j)) x) = (ConcreteCategory.hom (π F j')) x
@[simp]
theorem
CategoryTheory.Limits.cokernel.condition_apply
{C : Type u}
[Category.{v, u} C]
[HasZeroMorphisms C]
{X Y : C}
(f : X ⟶ Y)
[HasCokernel f]
{F : C → C → Type uF}
{carrier : C → Type w}
{instFunLike : (X Y : C) → FunLike (F X Y) (carrier X) (carrier Y)}
[inst : ConcreteCategory C F]
(x : ToType X)
:
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')
{F✝ : C → C → Type uF}
{carrier : C → Type w}
{instFunLike : (X Y : C) → FunLike (F✝ X Y) (carrier X) (carrier Y)}
[inst : ConcreteCategory C F✝]
(x : ToType (F.obj j))
: