(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)