THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C)
[category_theory.limits.has_limit F]
{j j' : J}
(f : j ⟶ j')
[I : category_theory.concrete_category C]
(x : ↥(category_theory.limits.limit F)) :
⇑(F.map f) (⇑(category_theory.limits.limit.π F j) x) = ⇑(category_theory.limits.limit.π F j') x
@[simp]
theorem
category_theory.limits.colimit.w_apply
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C)
[category_theory.limits.has_colimit F]
{j j' : J}
(f : j ⟶ j')
[I : category_theory.concrete_category C]
(x : ↥(F.obj j)) :
⇑(category_theory.limits.colimit.ι F j') (⇑(F.map f) x) = ⇑(category_theory.limits.colimit.ι F j) x
@[simp]
theorem
category_theory.limits.cokernel.π_desc_apply
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.limits.has_cokernel f]
{W : C}
(k : Y ⟶ W)
(h : f ≫ k = 0)
[I : category_theory.concrete_category C]
(x : ↥Y) :
⇑(category_theory.limits.cokernel.desc f k h) (⇑(category_theory.limits.cokernel.π f) x) = ⇑k x
@[simp]
theorem
category_theory.limits.cocone.w_apply
{J : Type u₁}
[category_theory.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)) :
@[simp]
theorem
category_theory.limits.limit.lift_π_apply
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
[category_theory.limits.has_limit F]
(c : category_theory.limits.cone F)
(j : J)
[I : category_theory.concrete_category C]
(x : ↥(c.X)) :
⇑(category_theory.limits.limit.π F j) (⇑(category_theory.limits.limit.lift F c) x) = ⇑(c.π.app j) x
@[simp]
theorem
category_theory.limits.kernel.lift_ι_apply
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.limits.has_kernel f]
{W : C}
(k : W ⟶ X)
(h : k ≫ f = 0)
[I : category_theory.concrete_category C]
(x : ↥W) :
⇑(category_theory.limits.kernel.ι f) (⇑(category_theory.limits.kernel.lift f k h) x) = ⇑k x
@[simp]
theorem
category_theory.limits.kernel.condition_apply
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.limits.has_kernel f]
[I : category_theory.concrete_category C]
(x : ↥(category_theory.limits.kernel f)) :
⇑f (⇑(category_theory.limits.kernel.ι f) x) = ⇑0 x
@[simp]
theorem
category_theory.limits.colimit.ι_desc_apply
{J : Type u₁}
[category_theory.category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
[category_theory.limits.has_colimit F]
(c : category_theory.limits.cocone F)
(j : J)
[I : category_theory.concrete_category C]
(x : ↥(F.obj j)) :
⇑(category_theory.limits.colimit.desc F c) (⇑(category_theory.limits.colimit.ι F j) x) = ⇑(c.ι.app j) x
@[simp]
theorem
category_theory.limits.cokernel.condition_apply
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.limits.has_cokernel f]
[I : category_theory.concrete_category C]
(x : ↥X) :
⇑(category_theory.limits.cokernel.π f) (⇑f x) = ⇑0 x
@[simp]
theorem
category_theory.limits.cone.w_apply
{J : Type u₁}
[category_theory.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)) :