Theorems · Theorem · category theory

CategoryTheory.Abelian.Pseudoelement.comp_apply

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {P Q R : C} (f : P ⟶ Q)
  (g : Q ⟶ R) (a : CategoryTheory.Abelian.Pseudoelement P),
  CategoryTheory.Abelian.Pseudoelement.pseudoApply (CategoryTheory.CategoryStruct.comp f g) a =
    CategoryTheory.Abelian.Pseudoelement.pseudoApply g (CategoryTheory.Abelian.Pseudoelement.pseudoApply f a)

Applying a pseudoelement to a composition of morphisms is the same as composing with each morphism. Sadly, this is not a definitional equality, but at least it is true.

Defined in

Mathlib.CategoryTheory.Abelian.Pseudoelements

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Abelian