Theorems · Definition · category theory

imageToKernel

{V : Type u} →
  [inst : CategoryTheory.Category.{v, u} V] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] →
      {A B C : V} →
        (f : A ⟶ B) →
          [inst_2 : CategoryTheory.Limits.HasImage f] →
            (g : B ⟶ C) →
              [inst_3 : CategoryTheory.Limits.HasKernel g] →
                CategoryTheory.CategoryStruct.comp f g = 0 →
                  (CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.imageSubobject f) ⟶
                    CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.kernelSubobject g))

The canonical morphism imageSubobject f ⟶ kernelSubobject g when f ≫ g = 0.

Defined in

Mathlib.Algebra.Homology.ImageToKernel

Cited by

21 results in Mathlib

Foundations

Depth 44 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasZeroMorphismsCategoryTheory.Limits.HasImageCategoryTheory.Limits.HasKernel