Theorems · Definition · category theory

CategoryTheory.ProjectiveResolution.isoExt

{R : Type u_1} →
  [inst : Ring R] →
    {C : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_1, u_2} C] →
        [inst_2 : CategoryTheory.Abelian C] →
          [inst_3 : CategoryTheory.Linear R C] →
            [inst_4 : CategoryTheory.EnoughProjectives C] →
              {X : C} →
                (P : CategoryTheory.ProjectiveResolution X) →
                  (n : ℕ) →
                    (Y : C) →
                      ((Ext R C n).obj (Opposite.op X)).obj Y ≅
                        HomologicalComplex.homology (P.complex.linearYonedaObj R Y) n

Ext can be computed using a projective resolution.

Defined in

Mathlib.CategoryTheory.Abelian.Ext

Cited by

1 results in Mathlib

Foundations

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

Assumes

RingCategoryTheory.CategoryCategoryTheory.AbelianCategoryTheory.LinearCategoryTheory.EnoughProjectives