Theorems · Theorem · category theory

CategoryTheory.ProjectiveResolution.of_def

∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.EnoughProjectives C] (Z : C),
  CategoryTheory.ProjectiveResolution.of Z =
    { complex := CategoryTheory.ProjectiveResolution.ofComplex Z, projective := ⋯, hasHomology := ⋯,
      π := ((CategoryTheory.ProjectiveResolution.ofComplex Z).toSingle₀Equiv Z).symm ⟨CategoryTheory.Projective.π Z, ⋯⟩,
      quasiIso := ⋯ }

Defined in

Mathlib.CategoryTheory.Abelian.Projective.Resolution

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.AbelianCategoryTheory.EnoughProjectives