Theorems · Theorem · category theory

CategoryTheory.Abelian.Ext.comp_hom

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {X Y Z : C} [inst_3 : HasDerivedCategory C] {a b : ℕ}
  (α : CategoryTheory.Abelian.Ext X Y a) (β : CategoryTheory.Abelian.Ext Y Z b) {c : ℕ} (h : a + b = c),
  (α.comp β h).hom = α.hom.comp β.hom ⋯

Defined in

Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Cited by

27 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.AbelianCategoryTheory.HasExtHasDerivedCategory