Theorems · Theorem · category theory

CategoryTheory.ShortComplex.ShortExact.comp_extClass_assoc

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) {Y : C} {n : ℕ}
  (γ : CategoryTheory.Abelian.Ext S.X₁ Y n) {n' : ℕ} (h : 1 + n = n'),
  (CategoryTheory.Abelian.Ext.mk₀ S.g).comp (hS.extClass.comp γ h) ⋯ = 0

Defined in

Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.AbelianCategoryTheory.HasExt