(Co)kernels in functor categories #
noncomputable def
CategoryTheory.Limits.kerIsKernel
(C : Type u_2)
[Category.{v_2, u_2} C]
[HasZeroMorphisms C]
[HasKernels C]
:
IsLimit (KernelFork.ofι (ker.ι C) ⋯)
The kernel inclusion is itself a kernel in the functor category.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
CategoryTheory.Limits.cokerIsCokernel
(C : Type u_2)
[Category.{v_2, u_2} C]
[HasZeroMorphisms C]
[HasCokernels C]
:
IsColimit (CokernelCofork.ofπ (coker.π C) ⋯)
The cokernel projection is itself a cokernel in the functor category.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.Limits.hasKernel_of_hasKernel_app
{J : Type u_1}
{C : Type u_2}
[Category.{v_1, u_1} J]
[Category.{v_2, u_2} C]
[HasZeroMorphisms C]
{F₁ F₂ : Functor J C}
(f : F₁ ⟶ F₂)
[∀ (j : J), HasKernel (f.app j)]
:
theorem
CategoryTheory.Limits.hasCokernel_of_hasCokernel_app
{J : Type u_1}
{C : Type u_2}
[Category.{v_1, u_1} J]
[Category.{v_2, u_2} C]
[HasZeroMorphisms C]
{F₁ F₂ : Functor J C}
(f : F₁ ⟶ F₂)
[∀ (j : J), HasCokernel (f.app j)]
:
theorem
CategoryTheory.Limits.evaluation_preservesLimit_of_hasKernel_app
{J : Type u_1}
{C : Type u_2}
[Category.{v_1, u_1} J]
[Category.{v_2, u_2} C]
[HasZeroMorphisms C]
{F₁ F₂ : Functor J C}
(f : F₁ ⟶ F₂)
[∀ (j : J), HasKernel (f.app j)]
(j : J)
:
PreservesLimit (parallelPair f 0) ((evaluation J C).obj j)
theorem
CategoryTheory.Limits.evaluation_preservesColimit_of_hasCokernel_app
{J : Type u_1}
{C : Type u_2}
[Category.{v_1, u_1} J]
[Category.{v_2, u_2} C]
[HasZeroMorphisms C]
{F₁ F₂ : Functor J C}
(f : F₁ ⟶ F₂)
[∀ (j : J), HasCokernel (f.app j)]
(j : J)
:
PreservesColimit (parallelPair f 0) ((evaluation J C).obj j)