Theorems · Theorem · category theory

CategoryTheory.Abelian.Ext.biprodAddEquiv_symm_apply

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {X₁ X₂ Y : C} {n : ℕ}
  (e : CategoryTheory.Abelian.Ext X₁ Y n × CategoryTheory.Abelian.Ext X₂ Y n),
  CategoryTheory.Abelian.Ext.biprodAddEquiv.symm e =
    (CategoryTheory.Abelian.Ext.mk₀ CategoryTheory.Limits.biprod.fst).comp e.1 ⋯ +
      (CategoryTheory.Abelian.Ext.mk₀ CategoryTheory.Limits.biprod.snd).comp e.2 ⋯

Defined in

Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.AbelianCategoryTheory.HasExt