Facts about limits of functors into concrete categories
This file doesn't yet attempt to be exhaustive; it just contains lemmas that are useful while comparing categorical limits with existing constructions in concrete categories.
@[simp]
theorem
category_theory.limits.kernel_condition_apply
{C : Type (u+1)}
[category_theory.large_category C]
[category_theory.concrete_category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.limits.has_kernel f]
(x : ↥(category_theory.limits.kernel f)) :
⇑f (⇑(category_theory.limits.kernel.ι f) x) = ⇑0 x
@[simp]
theorem
category_theory.limits.cokernel_condition_apply
{C : Type (u+1)}
[category_theory.large_category C]
[category_theory.concrete_category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.limits.has_cokernel f]
(x : ↥X) :
⇑(category_theory.limits.cokernel.π f) (⇑f x) = ⇑0 x