Finite resolutions by objects satisfying P : ObjectProperty C

Main definitions

Let C be a category, P : ObjectProperty C be a property of objects of C.

• CategoryTheory.ObjectProperty.hasFiniteResolutionOfLength: We say that X : C has a P-resolution of length n if there exists an exact sequence 0 ⟶ Eₙ ⟶ ⋯ ⟶ E₀ ⟶ X ⟶ 0 such that each Eᵢ : C satisfies P.
• CategoryTheory.ObjectProperty.hasFiniteResolution: We say that X : C has a finite P-resolution if it has a P-resolution of some finite length.

Implementation notes

Rather than defining hasFiniteResolutionOfLength in terms of explicit exact sequences, we define it inductively: X has a P-resolution of length 0 if X satisfies P, and it has a P-resolution of length n + 1 if there exists a short exact sequence 0 ⟶ K ⟶ E ⟶ X ⟶ 0 such that E satisfies P and K has a P-resolution of length n.

TODO

• Construct a chain complex K whose terms satisfy P with a quasi-isomorphism from K to the single complex on X when C is abelian and X has a finite P-resolution.

inductive CategoryTheory.ObjectProperty.hasFiniteResolutionOfLength {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] (P : ObjectProperty C) : ℕ → ObjectProperty C

Let C be a category, P : ObjectProperty C be a property of objects of C. We say that X : C has a P-resolution of length n if there exists an exact sequence 0 ⟶ Eₙ ⟶ ⋯ ⟶ E₀ ⟶ X ⟶ 0 such that each Eᵢ : C satisfies P.

Rather than defining hasFiniteResolutionOfLength in terms of explicit exact sequences, we define it inductively: X has a P-resolution of length 0 if X satisfies P, and it has a P-resolution of length n + 1 if there exists a short exact sequence 0 ⟶ K ⟶ E ⟶ X ⟶ 0 such that E satisfies P and K has a P-resolution of length n.

• zero {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {P : ObjectProperty C} (X : C) (hX : P X) : P.hasFiniteResolutionOfLength 0 X
• succ {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {P : ObjectProperty C} (S : ShortComplex C) (n : ℕ) (hS : S.ShortExact) (h₂ : P S.X₂) (h₁ : P.hasFiniteResolutionOfLength n S.X₁) : P.hasFiniteResolutionOfLength (n + 1) S.X₃

def CategoryTheory.ObjectProperty.hasFiniteResolution {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] (P : ObjectProperty C) : ObjectProperty C

Let C be a category, P : ObjectProperty C be a property of objects in C. We say that X : C has a finite P-resolution if it has a P-resolution of some finite length.

Equations

• P.hasFiniteResolution = ⨆ (n : ℕ), P.hasFiniteResolutionOfLength n

@[simp]

theorem CategoryTheory.ObjectProperty.hasFiniteResolution_iff {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {P : ObjectProperty C} {X : C} : P.hasFiniteResolution X ↔ ∃ (n : ℕ), P.hasFiniteResolutionOfLength n X

theorem CategoryTheory.ObjectProperty.hasFiniteResolutionOfLength.property {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {P : ObjectProperty C} : P = P.hasFiniteResolutionOfLength 0

theorem CategoryTheory.ObjectProperty.hasFiniteResolutionOfLength.monotone {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {P Q : ObjectProperty C} {n : ℕ} (hPQ : P ≤ Q) : P.hasFiniteResolutionOfLength n ≤ Q.hasFiniteResolutionOfLength n

theorem CategoryTheory.ObjectProperty.hasFiniteResolutionOfLength.property_of_isClosedUnderQuotients {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {P : ObjectProperty C} {n : ℕ} [P.IsClosedUnderQuotients] : P.hasFiniteResolutionOfLength n ≤ P

instance CategoryTheory.ObjectProperty.hasFiniteResolutionOfLength.instIsClosedUnderIsomorphisms {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {P : ObjectProperty C} {n : ℕ} [P.IsClosedUnderIsomorphisms] : (P.hasFiniteResolutionOfLength n).IsClosedUnderIsomorphisms

theorem CategoryTheory.ObjectProperty.hasFiniteResolutionOfLength.map_exactFunctor {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {P : ObjectProperty C} {n : ℕ} {D : Type u'} [Category.{v', u'} D] [Limits.HasZeroMorphisms D] {Q : ObjectProperty D} (F : Functor C D) [F.PreservesZeroMorphisms] [Limits.PreservesFiniteLimits F] [Limits.PreservesFiniteColimits F] (hF : P ≤ Q.inverseImage F) : P.hasFiniteResolutionOfLength n ≤ (Q.hasFiniteResolutionOfLength n).inverseImage F

theorem CategoryTheory.ObjectProperty.hasFiniteResolutionOfLength.le_hasFiniteResolution {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {P : ObjectProperty C} {n : ℕ} : P.hasFiniteResolutionOfLength n ≤ P.hasFiniteResolution

theorem CategoryTheory.ObjectProperty.hasFiniteResolution.le {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {P : ObjectProperty C} : P ≤ P.hasFiniteResolution

instance CategoryTheory.ObjectProperty.hasFiniteResolution.instIs {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {P : ObjectProperty C} {X : C} [P.Is X] : P.hasFiniteResolution.Is X

theorem CategoryTheory.ObjectProperty.hasFiniteResolution.monotone {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {P Q : ObjectProperty C} (hPQ : P ≤ Q) : P.hasFiniteResolution ≤ Q.hasFiniteResolution

theorem CategoryTheory.ObjectProperty.hasFiniteResolution.eq_of_isClosedUnderQuotients {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {P : ObjectProperty C} [P.IsClosedUnderQuotients] : P.hasFiniteResolution = P

instance CategoryTheory.ObjectProperty.hasFiniteResolution.instIsClosedUnderIsomorphisms {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {P : ObjectProperty C} [P.IsClosedUnderIsomorphisms] : P.hasFiniteResolution.IsClosedUnderIsomorphisms

theorem CategoryTheory.ObjectProperty.hasFiniteResolution.of_shortExact {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {P : ObjectProperty C} {S : ShortComplex C} (hS : S.ShortExact) (h₂ : P S.X₂) (h₁ : P.hasFiniteResolution S.X₁) : P.hasFiniteResolution S.X₃

theorem CategoryTheory.ObjectProperty.hasFiniteResolution.map_exactFunctor {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {P : ObjectProperty C} {D : Type u'} [Category.{v', u'} D] [Limits.HasZeroMorphisms D] {Q : ObjectProperty D} (F : Functor C D) [F.PreservesZeroMorphisms] [Limits.PreservesFiniteLimits F] [Limits.PreservesFiniteColimits F] (hF : P ≤ Q.inverseImage F) : P.hasFiniteResolution ≤ Q.hasFiniteResolution.inverseImage F