Weak kernels in pretriangulated categories

We prove that pretriangulated categories have weak kernels: if f : X ⟶ Y is a morphism in a pretriangulated category and if we complete it to a distinguished triangle Z ⟶ X ⟶ Y ⟶ Z⟦1⟧, then the first morphism Z ⟶ Y of that triangle is a weak kernel of f.

TODO: Weak cokernels.

def CategoryTheory.Pretriangulated.kernelForkOfDistTriangle {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (T : Triangle C) (dT : T ∈ distinguishedTriangles) : Limits.KernelFork T.mor₂

If T is a distinguished triangle, then T.mor₁ defines a kernel fork for T.mor₂.

Equations

• CategoryTheory.Pretriangulated.kernelForkOfDistTriangle T dT = CategoryTheory.Limits.KernelFork.ofι T.mor₁ ⋯

noncomputable def CategoryTheory.Pretriangulated.isWeakLimitKernelForkOfDistTriangle {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (T : Triangle C) (dT : T ∈ distinguishedTriangles) : Limits.IsWeakLimit (kernelForkOfDistTriangle T dT)

If T is a distinguished triangle, then the kernel fork for T.mor₂ defined in kernelForkOfDistTriangle is a weak kernel fork.

Equations

• One or more equations did not get rendered due to their size.

instance CategoryTheory.Pretriangulated.instHasWeakKernels {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] : Limits.HasWeakKernels C

A pretriangulated category has weak kernels.