refactor(CategoryTheory): introduce ObjectProperty (#22286)

An abbreviation `ObjectProperty C` for predicates on objects of a category `C` is introduced in the file `CategoryTheory.ObjectProperty.Basic`. The file `CategoryTheory.ClosedUnderIsomorphisms` is moved to `ObjectProperty.ClosedUnderIsomorphisms`.



Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>

Author: joelriou

Mathlib.lean

@@ -1821,7 +1821,6 @@ import Mathlib.CategoryTheory.Closed.Ideal
 import Mathlib.CategoryTheory.Closed.Monoidal
 import Mathlib.CategoryTheory.Closed.Types
 import Mathlib.CategoryTheory.Closed.Zero
-import Mathlib.CategoryTheory.ClosedUnderIsomorphisms
 import Mathlib.CategoryTheory.CodiscreteCategory
 import Mathlib.CategoryTheory.CofilteredSystem
 import Mathlib.CategoryTheory.CommSq
@@ -2219,6 +2218,9 @@ import Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
 import Mathlib.CategoryTheory.NatIso
 import Mathlib.CategoryTheory.NatTrans
 import Mathlib.CategoryTheory.Noetherian
+import Mathlib.CategoryTheory.ObjectProperty.Basic
+import Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms
+import Mathlib.CategoryTheory.ObjectProperty.Shift
 import Mathlib.CategoryTheory.Opposites
 import Mathlib.CategoryTheory.PEmpty
 import Mathlib.CategoryTheory.PUnit
@@ -2268,7 +2270,6 @@ import Mathlib.CategoryTheory.Shift.Induced
 import Mathlib.CategoryTheory.Shift.InducedShiftSequence
 import Mathlib.CategoryTheory.Shift.Localization
 import Mathlib.CategoryTheory.Shift.Opposite
-import Mathlib.CategoryTheory.Shift.Predicate
 import Mathlib.CategoryTheory.Shift.Pullback
 import Mathlib.CategoryTheory.Shift.Quotient
 import Mathlib.CategoryTheory.Shift.ShiftSequence

Mathlib/Algebra/Homology/DerivedCategory/Basic.lean

@@ -75,7 +75,7 @@ of acyclic complexes. -/
 def subcategoryAcyclic : Triangulated.Subcategory (HomotopyCategory C (ComplexShape.up ℤ)) :=
   (homologyFunctor C (ComplexShape.up ℤ) 0).homologicalKernel
 
-instance : ClosedUnderIsomorphisms (subcategoryAcyclic C).P := by
+instance : (subcategoryAcyclic C).P.IsClosedUnderIsomorphisms := by
   dsimp [subcategoryAcyclic]
   infer_instance
 

Mathlib/CategoryTheory/ClosedUnderIsomorphisms.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Markus Himmel
 -/
 import Mathlib.CategoryTheory.Limits.Creates
-import Mathlib.CategoryTheory.ClosedUnderIsomorphisms
+import Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms
 
 /-!
 # Limits in full subcategories
@@ -27,32 +27,32 @@ namespace CategoryTheory.Limits
 /-- We say that a property is closed under limits of shape `J` if whenever all objects in a
     `J`-shaped diagram have the property, any limit of this diagram also has the property. -/
 def ClosedUnderLimitsOfShape {C : Type u} [Category.{v} C] (J : Type w) [Category.{w'} J]
-    (P : C → Prop) : Prop :=
+    (P : ObjectProperty C) : Prop :=
   ∀ ⦃F : J ⥤ C⦄ ⦃c : Cone F⦄ (_hc : IsLimit c), (∀ j, P (F.obj j)) → P c.pt
 
 /-- We say that a property is closed under colimits of shape `J` if whenever all objects in a
     `J`-shaped diagram have the property, any colimit of this diagram also has the property. -/
 def ClosedUnderColimitsOfShape {C : Type u} [Category.{v} C] (J : Type w) [Category.{w'} J]
-    (P : C → Prop) : Prop :=
+    (P : ObjectProperty C) : Prop :=
   ∀ ⦃F : J ⥤ C⦄ ⦃c : Cocone F⦄ (_hc : IsColimit c), (∀ j, P (F.obj j)) → P c.pt
 
 section
 
-variable {C : Type u} [Category.{v} C] {J : Type w} [Category.{w'} J] {P : C → Prop}
+variable {C : Type u} [Category.{v} C] {J : Type w} [Category.{w'} J] {P : ObjectProperty C}
 
-theorem closedUnderLimitsOfShape_of_limit [ClosedUnderIsomorphisms P]
+theorem closedUnderLimitsOfShape_of_limit [P.IsClosedUnderIsomorphisms]
     (h : ∀ {F : J ⥤ C} [HasLimit F], (∀ j, P (F.obj j)) → P (limit F)) :
     ClosedUnderLimitsOfShape J P := by
   intros F c hc hF
   have : HasLimit F := ⟨_, hc⟩
-  exact mem_of_iso P ((limit.isLimit _).conePointUniqueUpToIso hc) (h hF)
+  exact P.prop_of_iso ((limit.isLimit _).conePointUniqueUpToIso hc) (h hF)
 
-theorem closedUnderColimitsOfShape_of_colimit [ClosedUnderIsomorphisms P]
+theorem closedUnderColimitsOfShape_of_colimit [P.IsClosedUnderIsomorphisms]
     (h : ∀ {F : J ⥤ C} [HasColimit F], (∀ j, P (F.obj j)) → P (colimit F)) :
     ClosedUnderColimitsOfShape J P := by
   intros F c hc hF
   have : HasColimit F := ⟨_, hc⟩
-  exact mem_of_iso P ((colimit.isColimit _).coconePointUniqueUpToIso hc) (h hF)
+  exact P.prop_of_iso ((colimit.isColimit _).coconePointUniqueUpToIso hc) (h hF)
 
 theorem ClosedUnderLimitsOfShape.limit (h : ClosedUnderLimitsOfShape J P) {F : J ⥤ C} [HasLimit F] :
     (∀ j, P (F.obj j)) → P (limit F) :=

Mathlib/CategoryTheory/Limits/FullSubcategory.lean

@@ -6,7 +6,7 @@ Authors: Markus Himmel
 import Mathlib.CategoryTheory.Limits.FinallySmall
 import Mathlib.CategoryTheory.Limits.Presheaf
 import Mathlib.CategoryTheory.Filtered.Small
-import Mathlib.CategoryTheory.ClosedUnderIsomorphisms
+import Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms
 import Mathlib.CategoryTheory.Limits.Preserves.Finite
 import Mathlib.CategoryTheory.Limits.Preserves.Presheaf
 
@@ -141,7 +141,7 @@ theorem map {A B : Cᵒᵖ ⥤ Type v} (η : A ⟶ B) [IsIso η] : IsIndObject A
 theorem iff_of_iso {A B : Cᵒᵖ ⥤ Type v} (η : A ⟶ B) [IsIso η] : IsIndObject A ↔ IsIndObject B :=
   ⟨.map η, .map (inv η)⟩
 
-instance : ClosedUnderIsomorphisms (IsIndObject (C := C)) where
+instance : ObjectProperty.IsClosedUnderIsomorphisms (IsIndObject (C := C)) where
   of_iso i h := h.map i.hom
 
 /-- Pick a presentation for an ind-object using choice. -/

Mathlib/CategoryTheory/Limits/Indization/IndObject.lean

@@ -3,14 +3,14 @@ Copyright (c) 2024 Joël Riou. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joël Riou
 -/
-import Mathlib.CategoryTheory.ClosedUnderIsomorphisms
+import Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms
 import Mathlib.CategoryTheory.MorphismProperty.Composition
 import Mathlib.CategoryTheory.Localization.Adjunction
 
 /-!
 # Bousfield localization
 
-Given a predicate `P : C → Prop` on the objects of a category `C`,
+Given a predicate `P : ObjectProperty C` on the objects of a category `C`,
 we define `Localization.LeftBousfield.W P : MorphismProperty C`
 as the class of morphisms `f : X ⟶ Y` such that for any `Z : C`
 such that `P Z`, the precomposition with `f` induces a bijection
@@ -42,9 +42,9 @@ namespace LeftBousfield
 
 section
 
-variable (P : C → Prop)
+variable (P : ObjectProperty C)
 
-/-- Given a predicate `P : C → Prop`, this is the class of morphisms `f : X ⟶ Y`
+/-- Given `P : ObjectProperty C`, this is the class of morphisms `f : X ⟶ Y`
 such that for all `Z : C` such that `P Z`, the precomposition with `f` induces
 a bijection `(Y ⟶ Z) ≃ (X ⟶ Z)`. -/
 def W : MorphismProperty C := fun _ _ f =>
@@ -58,11 +58,11 @@ noncomputable def W.homEquiv {X Y : C} {f : X ⟶ Y} (hf : W P f) (Z : C) (hZ :
     (Y ⟶ Z) ≃ (X ⟶ Z) :=
   Equiv.ofBijective _ (hf Z hZ)
 
-lemma W_isoClosure : W (isoClosure P) = W P := by
+lemma W_isoClosure : W P.isoClosure = W P := by
   ext X Y f
   constructor
   · intro hf Z hZ
-    exact hf _ (le_isoClosure _ _ hZ)
+    exact hf _ (P.le_isoClosure _ hZ)
   · rintro hf Z ⟨Z', hZ', ⟨e⟩⟩
     constructor
     · intro g₁ g₂ eq

Mathlib/CategoryTheory/Localization/Bousfield.lean

@@ -0,0 +1,31 @@
+/-
+Copyright (c) 2025 Joël Riou. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joël Riou
+-/
+import Mathlib.CategoryTheory.Category.Basic
+
+/-!
+# Properties of objects in a category
+
+Given a category `C`, we introduce an abbreviation `ObjectProperty C`
+for predicates `C → Prop`.
+
+## TODO
+
+* refactor the file `Limits.FullSubcategory` in order to rename `ClosedUnderLimitsOfShape`
+as `ObjectProperty.IsClosedUnderLimitsOfShape` (and make it a type class)
+* refactor the file `Triangulated.Subcategory` in order to make it a type class
+regarding terms in `ObjectProperty C` when `C` is pretriangulated
+
+-/
+
+universe v u
+
+namespace CategoryTheory
+
+/-- A property of objects in a category `C` is a predicate `C → Prop`. -/
+@[nolint unusedArguments]
+abbrev ObjectProperty (C : Type u) [Category.{v} C] : Type u := C → Prop
+
+end CategoryTheory

Mathlib/CategoryTheory/ObjectProperty/Basic.lean

@@ -0,0 +1,88 @@
+/-
+Copyright (c) 2024 Joël Riou. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joël Riou
+-/
+import Mathlib.CategoryTheory.Iso
+import Mathlib.CategoryTheory.ObjectProperty.Basic
+import Mathlib.Order.Basic
+
+/-! # Properties of objects which are closed under isomorphisms
+
+Given a category `C` and `P : ObjectProperty C` (i.e. `P : C → Prop`),
+this file introduces the type class `P.IsClosedUnderIsomorphisms`.
+
+-/
+
+namespace CategoryTheory
+
+variable {C : Type*} [Category C] (P Q : ObjectProperty C)
+
+namespace ObjectProperty
+
+/-- A predicate `C → Prop` on the objects of a category is closed under isomorphisms
+if whenever `P X`, then all the objects `Y` that are isomorphic to `X` also satisfy `P Y`. -/
+class IsClosedUnderIsomorphisms : Prop where
+  of_iso {X Y : C} (_ : X ≅ Y) (_ : P X) : P Y
+
+@[deprecated (since := "2025-02-25")] alias ClosedUnderIsomorphisms := IsClosedUnderIsomorphisms
+
+lemma prop_of_iso [IsClosedUnderIsomorphisms P] {X Y : C} (e : X ≅ Y) (hX : P X) : P Y :=
+  IsClosedUnderIsomorphisms.of_iso e hX
+
+lemma prop_iff_of_iso [IsClosedUnderIsomorphisms P] {X Y : C} (e : X ≅ Y) : P X ↔ P Y :=
+  ⟨prop_of_iso P e, prop_of_iso P e.symm⟩
+
+lemma prop_of_isIso [IsClosedUnderIsomorphisms P] {X Y : C} (f : X ⟶ Y) [IsIso f] (hX : P X) :
+    P Y :=
+  prop_of_iso P (asIso f) hX
+
+lemma prop_iff_of_isIso [IsClosedUnderIsomorphisms P] {X Y : C} (f : X ⟶ Y) [IsIso f] : P X ↔ P Y :=
+  prop_iff_of_iso P (asIso f)
+
+/-- The closure by isomorphisms of a predicate on objects in a category. -/
+def isoClosure : ObjectProperty C := fun X => ∃ (Y : C) (_ : P Y), Nonempty (X ≅ Y)
+
+lemma prop_isoClosure_iff (X : C) :
+    isoClosure P X ↔ ∃ (Y : C) (_ : P Y), Nonempty (X ≅ Y) := by rfl
+
+variable {P} in
+lemma prop_isoClosure {X Y : C} (h : P X) (e : X ⟶ Y) [IsIso e] : isoClosure P Y :=
+  ⟨X, h, ⟨(asIso e).symm⟩⟩
+
+lemma le_isoClosure : P ≤ isoClosure P :=
+  fun X hX => ⟨X, hX, ⟨Iso.refl X⟩⟩
+
+variable {P Q} in
+lemma monotone_isoClosure (h : P ≤ Q) : isoClosure P ≤ isoClosure Q := by
+  rintro X ⟨X', hX', ⟨e⟩⟩
+  exact ⟨X', h _ hX', ⟨e⟩⟩
+
+lemma isoClosure_eq_self [IsClosedUnderIsomorphisms P] : isoClosure P = P := by
+  apply le_antisymm
+  · intro X ⟨Y, hY, ⟨e⟩⟩
+    exact prop_of_iso P e.symm hY
+  · exact le_isoClosure P
+
+lemma isoClosure_le_iff [IsClosedUnderIsomorphisms Q] : isoClosure P ≤ Q ↔ P ≤ Q :=
+  ⟨(le_isoClosure P).trans,
+    fun h => (monotone_isoClosure h).trans (by rw [isoClosure_eq_self])⟩
+
+instance : IsClosedUnderIsomorphisms (isoClosure P) where
+  of_iso := by
+    rintro X Y e ⟨Z, hZ, ⟨f⟩⟩
+    exact ⟨Z, hZ, ⟨e.symm.trans f⟩⟩
+
+end ObjectProperty
+
+open ObjectProperty
+
+@[deprecated (since := "2025-02-25")] alias mem_of_iso := prop_of_iso
+@[deprecated (since := "2025-02-25")] alias mem_iff_of_iso := prop_iff_of_iso
+@[deprecated (since := "2025-02-25")] alias mem_of_isIso := prop_of_isIso
+@[deprecated (since := "2025-02-25")] alias mem_iff_of_isIso := prop_iff_of_isIso
+@[deprecated (since := "2025-02-25")] alias isoClosure := isoClosure
+@[deprecated (since := "2025-02-25")] alias mem_isoClosure_iff := prop_isoClosure_iff
+@[deprecated (since := "2025-02-25")] alias mem_isoClosure := prop_isoClosure
+
+end CategoryTheory

Mathlib/CategoryTheory/ObjectProperty/ClosedUnderIsomorphisms.lean

@@ -0,0 +1,58 @@
+/-
+Copyright (c) 2024 Joël Riou. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joël Riou
+-/
+import Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms
+import Mathlib.CategoryTheory.Shift.Basic
+
+/-!
+# Properties of objects on categories equipped with shift
+
+Given a predicate `P : ObjectProperty C` on objects of a category equipped with a shift
+by `A`, we define shifted properties of objects `P.shift a` for all `a : A`.
+
+-/
+
+open CategoryTheory Category
+
+namespace CategoryTheory
+
+variable {C : Type*} [Category C] (P : ObjectProperty C)
+  {A : Type*} [AddMonoid A] [HasShift C A]
+
+namespace ObjectProperty
+
+/-- Given a predicate `P : C → Prop` on objects of a category equipped with a shift by `A`,
+this is the predicate which is satisfied by `X` if `P (X⟦a⟧)`. -/
+def shift (a : A) : ObjectProperty C := fun X => P (X⟦a⟧)
+
+lemma prop_shift_iff (a : A) (X : C) : P.shift a X ↔ P (X⟦a⟧) := Iff.rfl
+
+instance (a : A) [P.IsClosedUnderIsomorphisms] :
+    (P.shift a).IsClosedUnderIsomorphisms where
+  of_iso e hX := P.prop_of_iso ((shiftFunctor C a).mapIso e) hX
+
+variable (A)
+
+@[simp]
+lemma shift_zero [P.IsClosedUnderIsomorphisms] : P.shift (0 : A) = P := by
+  ext X
+  exact P.prop_iff_of_iso ((shiftFunctorZero C A).app X)
+
+variable {A}
+
+lemma shift_shift (a b c : A) (h : a + b = c) [P.IsClosedUnderIsomorphisms] :
+    (P.shift b).shift a = P.shift c := by
+  ext X
+  exact P.prop_iff_of_iso ((shiftFunctorAdd' C a b c h).symm.app X)
+
+end ObjectProperty
+
+@[deprecated (since := "2025-02-25")] alias PredicateShift := ObjectProperty.shift
+@[deprecated (since := "2025-02-25")] alias predicateShift_iff := ObjectProperty.prop_shift_iff
+@[deprecated (since := "2025-02-25")] alias predicateShift_zero := ObjectProperty.shift_zero
+@[deprecated (since := "2025-02-25")] alias predicateShift_predicateShift :=
+  ObjectProperty.shift_shift
+
+end CategoryTheory