Theorems · Inductive type · category theory

CategoryTheory.ProjectiveResolution

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Limits.HasZeroObject C] → [CategoryTheory.Limits.HasZeroMorphisms C] → C → Type (max u v)

A ProjectiveResolution Z consists of a bundled ℕ-indexed chain complex of projective objects, along with a quasi-isomorphism to the complex consisting of just Z supported in degree 0.

Defined in

Mathlib.CategoryTheory.Preadditive.Projective.Resolution

Cited by

92 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasZeroObjectCategoryTheory.Limits.HasZeroMorphisms