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₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor J C}
[CategoryTheory.Limits.HasLimit F]
(c : CategoryTheory.Limits.Cone F)
(j : J)
[inst : CategoryTheory.ConcreteCategory C]
(x : (CategoryTheory.forget C).toPrefunctor.obj c.pt)
:
(CategoryTheory.Limits.limit.π F j) ((CategoryTheory.Limits.limit.lift F c) x) = (c.π.app j) x
@[simp]
theorem
CategoryTheory.Limits.cokernel.condition_apply
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasCokernel f]
[inst : CategoryTheory.ConcreteCategory C]
(x : (CategoryTheory.forget C).toPrefunctor.obj X)
:
(CategoryTheory.Limits.cokernel.π f) (f x) = 0 x
@[simp]
theorem
CategoryTheory.Limits.limit.w_apply
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(F : CategoryTheory.Functor J C)
[CategoryTheory.Limits.HasLimit F]
{j : J}
{j' : J}
(f : j ⟶ j')
[inst : CategoryTheory.ConcreteCategory C]
(x : (CategoryTheory.forget C).toPrefunctor.obj
(((CategoryTheory.Functor.const J).toPrefunctor.obj (CategoryTheory.Limits.limit.cone F).pt).toPrefunctor.obj j))
:
(F.toPrefunctor.map f) ((CategoryTheory.Limits.limit.π F j) x) = (CategoryTheory.Limits.limit.π F j') x
@[simp]
theorem
CategoryTheory.Limits.colimit.ι_desc_apply
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor J C}
[CategoryTheory.Limits.HasColimit F]
(c : CategoryTheory.Limits.Cocone F)
(j : J)
[inst : CategoryTheory.ConcreteCategory C]
(x : (CategoryTheory.forget C).toPrefunctor.obj (F.toPrefunctor.obj j))
:
(CategoryTheory.Limits.colimit.desc F c) ((CategoryTheory.Limits.colimit.ι F j) x) = (c.ι.app j) x
@[simp]
theorem
CategoryTheory.Limits.Cone.w_apply
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
(c : CategoryTheory.Limits.Cone F)
{j : J}
{j' : J}
(f : j ⟶ j')
[inst : CategoryTheory.ConcreteCategory C]
(x : (CategoryTheory.forget C).toPrefunctor.obj (((CategoryTheory.Functor.const J).toPrefunctor.obj c.pt).toPrefunctor.obj j))
:
(F.toPrefunctor.map f) ((c.π.app j) x) = (c.π.app j') x
@[simp]
theorem
CategoryTheory.Limits.colimit.w_apply
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(F : CategoryTheory.Functor J C)
[CategoryTheory.Limits.HasColimit F]
{j : J}
{j' : J}
(f : j ⟶ j')
[inst : CategoryTheory.ConcreteCategory C]
(x : (CategoryTheory.forget C).toPrefunctor.obj (F.toPrefunctor.obj j))
:
(CategoryTheory.Limits.colimit.ι F j') ((F.toPrefunctor.map f) x) = (CategoryTheory.Limits.colimit.ι F j) x
@[simp]
theorem
CategoryTheory.Limits.cokernel.π_desc_apply
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasCokernel f]
{W : C}
(k : Y ⟶ W)
(h : CategoryTheory.CategoryStruct.comp f k = 0)
[inst : CategoryTheory.ConcreteCategory C]
(x : (CategoryTheory.forget C).toPrefunctor.obj
((CategoryTheory.Limits.parallelPair f 0).toPrefunctor.obj CategoryTheory.Limits.WalkingParallelPair.one))
:
((CategoryTheory.Limits.cokernelIsCokernel f).desc (CategoryTheory.Limits.CokernelCofork.ofπ k h))
((CategoryTheory.Limits.cokernel.π f) x) = k x
@[simp]
theorem
CategoryTheory.Limits.kernel.condition_apply
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasKernel f]
[inst : CategoryTheory.ConcreteCategory C]
(x : (CategoryTheory.forget C).toPrefunctor.obj
(((CategoryTheory.Functor.const CategoryTheory.Limits.WalkingParallelPair).toPrefunctor.obj
(CategoryTheory.Limits.limit.cone (CategoryTheory.Limits.parallelPair f 0)).pt).toPrefunctor.obj
CategoryTheory.Limits.WalkingParallelPair.zero))
:
f ((CategoryTheory.Limits.kernel.ι f) x) = 0 x
@[simp]
theorem
CategoryTheory.Limits.kernel.lift_ι_apply
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasKernel f]
{W : C}
(k : W ⟶ X)
(h : CategoryTheory.CategoryStruct.comp k f = 0)
[inst : CategoryTheory.ConcreteCategory C]
(x : (CategoryTheory.forget C).toPrefunctor.obj (CategoryTheory.Limits.KernelFork.ofι k h).pt)
:
(CategoryTheory.Limits.kernel.ι f)
(((CategoryTheory.Limits.kernelIsKernel f).lift (CategoryTheory.Limits.KernelFork.ofι k h)) x) = k x
theorem
CategoryTheory.Limits.Cocone.w_apply
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{F : CategoryTheory.Functor J C}
(c : CategoryTheory.Limits.Cocone F)
{j : J}
{j' : J}
(f : j ⟶ j')
[inst : CategoryTheory.ConcreteCategory C]
(x : (CategoryTheory.forget C).toPrefunctor.obj (F.toPrefunctor.obj j))
:
(c.ι.app j') ((F.toPrefunctor.map f) x) = (c.ι.app j) x