Theorems · Definition · category theory

CategoryTheory.NonPreadditiveAbelian.r

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.NonPreadditiveAbelian C] →
      (A : C) → A ⟶ CategoryTheory.Limits.cokernel (CategoryTheory.Limits.diag A)

The composite A ⟶ A ⨯ A ⟶ cokernel (Δ A), where the first map is (𝟙 A, 0) and the second map is the canonical projection into the cokernel.

Defined in

Mathlib.CategoryTheory.Abelian.NonPreadditive

Cited by

4 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.NonPreadditiveAbelian