Theorems · Definition · category theory

CategoryTheory.InjectiveResolution.extEquivCohomologyClass

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      [inst_2 : CategoryTheory.HasExt C] →
        {X Y : C} →
          (R : CategoryTheory.InjectiveResolution Y) →
            {n : ℕ} →
              CategoryTheory.Abelian.Ext X Y n ≃
                CochainComplex.HomComplex.CohomologyClass ((CochainComplex.singleFunctor C 0).obj X) R.cochainComplex ↑n

If R is an injective resolution of Y, then Ext X Y n identifies to the type of cohomology classes of degree n from (singleFunctor C 0).obj X to R.cochainComplex.

Defined in

Mathlib.CategoryTheory.Abelian.Injective.Ext

Cited by

19 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.AbelianCategoryTheory.HasExt