feat(CategoryTheory/ObjectProperty/HasFiniteResolution): relation with projective dimension

Mathlib.lean

@@ -3221,6 +3221,8 @@ public import Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
 public import Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
 public import Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits
 public import Mathlib.CategoryTheory.ObjectProperty.HasCardinalLT
+public import Mathlib.CategoryTheory.ObjectProperty.HasFiniteResolution.Basic
+public import Mathlib.CategoryTheory.ObjectProperty.HasFiniteResolution.Projective
 public import Mathlib.CategoryTheory.ObjectProperty.Ind
 public import Mathlib.CategoryTheory.ObjectProperty.InheritedFromHom
 public import Mathlib.CategoryTheory.ObjectProperty.Kernels

Mathlib/CategoryTheory/ObjectProperty/HasFiniteResolution/Basic.lean

@@ -0,0 +1,134 @@
+/-
+Copyright (c) 2026 Yongle Hu. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yongle Hu
+-/
+module
+
+public import Mathlib.CategoryTheory.ObjectProperty.EpiMono
+
+/-!
+# Finite resolutions by objects satisfying `P : ObjectProperty A`
+
+## Main definitions
+
+Let `C` be a category, `P : ObjectProperty C` be a property of objects in `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.
+
+## 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.
+-/
+
+public section
+
+universe v' v u' u
+
+namespace CategoryTheory.ObjectProperty
+
+open Limits
+
+variable {C : Type u} [Category.{v} C] [HasZeroMorphisms C]
+
+/-- Let `C` be a category, `P : ObjectProperty C` be a property of objectsin `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`. -/
+inductive HasFiniteResolutionOfLength (P : ObjectProperty C) : C → ℕ → Prop
+  | zero (X : C) (hX : P X) : HasFiniteResolutionOfLength P X 0
+  | succ (S : ShortComplex C) (n : ℕ) (hS : S.ShortExact) (h₂ : P S.X₂)
+      (h₁ : HasFiniteResolutionOfLength P S.X₁ n) : HasFiniteResolutionOfLength P S.X₃ (n + 1)
+
+/-- 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. -/
+class HasFiniteResolution (P : ObjectProperty C) (X : C) : Prop where
+  out (P X) : ∃ n : ℕ, P.HasFiniteResolutionOfLength X n
+
+variable {P Q : ObjectProperty C} {X : C} {n : ℕ}
+
+namespace HasFiniteResolutionOfLength
+
+theorem property (hX : P.HasFiniteResolutionOfLength X 0) : P X := by
+  cases hX with
+  | zero _ hX => exact hX
+
+theorem monotone (hPQ : P ≤ Q) (hX : P.HasFiniteResolutionOfLength X n) :
+    Q.HasFiniteResolutionOfLength X n := by
+  induction hX with
+  | zero X hX => exact HasFiniteResolutionOfLength.zero X (hPQ X hX)
+  | succ S n hS h₂ _ ih => exact HasFiniteResolutionOfLength.succ S n hS (hPQ S.X₂ h₂) ih
+
+theorem property_of_isClosedUnderQuotients [P.IsClosedUnderQuotients]
+    (hX : P.HasFiniteResolutionOfLength X n) : P X := by
+  cases hX with
+  | zero _ hX => exact hX
+  | succ S _ hS h₂ _ => exact P.prop_X₃_of_shortExact hS h₂
+
+theorem of_iso [P.IsClosedUnderIsomorphisms] {Y : C} (e : X ≅ Y)
+    (hX : P.HasFiniteResolutionOfLength X n) : P.HasFiniteResolutionOfLength Y n := by
+  cases hX with
+  | zero _ hX => exact HasFiniteResolutionOfLength.zero Y (P.prop_of_iso e hX)
+  | succ S n hS h₂ h₁ =>
+      let T : ShortComplex C := ShortComplex.mk S.f (S.g ≫ e.hom) (by simp)
+      let eS : S ≅ T := ShortComplex.isoMk (Iso.refl _) (Iso.refl _) e (by simp [T]) (by simp [T])
+      exact HasFiniteResolutionOfLength.succ T n (ShortComplex.shortExact_of_iso eS hS) h₂ h₁
+
+theorem map_exactFunctor {D : Type u'} [Category.{v'} D] [HasZeroMorphisms D]
+    {Q : ObjectProperty D} (F : C ⥤ D) [F.PreservesZeroMorphisms]
+    [PreservesFiniteLimits F] [PreservesFiniteColimits F]
+    (hF : P ≤ Q.inverseImage F) (hX : P.HasFiniteResolutionOfLength X n) :
+    Q.HasFiniteResolutionOfLength (F.obj X) n := by
+  induction hX with
+  | zero X hX =>
+      exact HasFiniteResolutionOfLength.zero (F.obj X) (hF X hX)
+  | succ S n hS h₂ _ ih =>
+      exact HasFiniteResolutionOfLength.succ (S.map F) n (hS.map_of_exact F) (hF S.X₂ h₂) ih
+
+theorem hasFiniteResolution (hX : P.HasFiniteResolutionOfLength X n) : P.HasFiniteResolution X :=
+  ⟨n, hX⟩
+
+end HasFiniteResolutionOfLength
+
+namespace HasFiniteResolution
+
+theorem of_property (hX : P X) : P.HasFiniteResolution X :=
+  ⟨0, HasFiniteResolutionOfLength.zero X hX⟩
+
+instance [P.Is X] : P.HasFiniteResolution X :=
+  of_property (P.prop_of_is X)
+
+theorem monotone (hPQ : P ≤ Q) [P.HasFiniteResolution X] : Q.HasFiniteResolution X := by
+  obtain ⟨_, hX⟩ := HasFiniteResolution.out P X
+  exact (hX.monotone hPQ).hasFiniteResolution
+
+theorem property_of_isClosedUnderQuotients [P.IsClosedUnderQuotients] [P.HasFiniteResolution X] :
+    P X := by
+  obtain ⟨_, hX⟩ := HasFiniteResolution.out P X
+  exact hX.property_of_isClosedUnderQuotients
+
+theorem of_iso [P.IsClosedUnderIsomorphisms] [P.HasFiniteResolution X] {Y : C} (e : X ≅ Y) :
+    P.HasFiniteResolution Y := by
+  obtain ⟨_, hX⟩ := HasFiniteResolution.out P X
+  exact (hX.of_iso e).hasFiniteResolution
+
+theorem of_shortExact {S : ShortComplex C} (hS : S.ShortExact) (h₂ : P S.X₂)
+    [P.HasFiniteResolution S.X₁] : P.HasFiniteResolution S.X₃ := by
+  obtain ⟨n, h₁⟩ := HasFiniteResolution.out P S.X₁
+  exact (HasFiniteResolutionOfLength.succ S n hS h₂ h₁).hasFiniteResolution
+
+theorem map_exactFunctor {D : Type u'} [Category.{v'} D] [HasZeroMorphisms D]
+    {Q : ObjectProperty D} (F : C ⥤ D) [F.PreservesZeroMorphisms]
+    [PreservesFiniteLimits F] [PreservesFiniteColimits F]
+    (hF : P ≤ Q.inverseImage F) [P.HasFiniteResolution X] :
+    Q.HasFiniteResolution (F.obj X) := by
+  obtain ⟨_, hX⟩ := HasFiniteResolution.out P X
+  exact (hX.map_exactFunctor F hF).hasFiniteResolution
+
+end HasFiniteResolution
+
+end CategoryTheory.ObjectProperty

Mathlib/CategoryTheory/ObjectProperty/HasFiniteResolution/Projective.lean

@@ -0,0 +1,45 @@
+/-
+Copyright (c) 2026 Yongle Hu. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yongle Hu
+-/
+module
+
+public import Mathlib.CategoryTheory.Abelian.Projective.Dimension
+public import Mathlib.CategoryTheory.ObjectProperty.HasFiniteResolution.Basic
+
+/-!
+# `X` has a projective resolution of length `n` if and only if `X` has projective dimension `≤ n`
+-/
+
+public section
+
+universe v u
+
+namespace CategoryTheory.ObjectProperty.HasFiniteResolutionOfLength
+
+open Limits
+
+variable {A : Type u} [Category.{v} A] [Abelian A] {X : A} {n : ℕ}
+
+theorem hasProjectiveDimensionLE (hX : (isProjective A).HasFiniteResolutionOfLength X n) :
+    HasProjectiveDimensionLE X n := by
+  induction hX with
+  | zero X hX => infer_instance
+  | succ S n hS h₂ _ ih => exact (hS.hasProjectiveDimensionLT_X₃_iff n h₂).2 ih
+
+theorem iff_hasProjectiveDimensionLE_of_enoughProjectives [EnoughProjectives A] :
+    (isProjective A).HasFiniteResolutionOfLength X n ↔ HasProjectiveDimensionLE X n := by
+  refine ⟨fun hX ↦ hX.hasProjectiveDimensionLE, fun hX ↦ ?_⟩
+  induction n generalizing X with
+  | zero =>
+      rw [← projective_iff_hasProjectiveDimensionLE_zero X] at hX
+      exact HasFiniteResolutionOfLength.zero X hX
+  | succ n ih =>
+      let f : Projective.over X ⟶ X := Projective.π X
+      let S : ShortComplex A := ShortComplex.mk (kernel.ι f) f (kernel.condition f)
+      have hS : S.ShortExact := ShortComplex.ShortExact.mk (ShortComplex.exact_kernel f)
+      exact HasFiniteResolutionOfLength.succ S n hS inferInstance <| ih <|
+        (hS.hasProjectiveDimensionLT_X₃_iff n inferInstance).1 hX
+
+end CategoryTheory.ObjectProperty.HasFiniteResolutionOfLength