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.

class CategoryTheory.ObjectProperty.IsClosedUnderIsomorphisms {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) : Prop

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.

• of_iso {X Y : C} : (X ≅ Y) → P X → P Y

@[deprecated CategoryTheory.ObjectProperty.IsClosedUnderIsomorphisms (since := "2025-02-25")]

def CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) : Prop

Alias of CategoryTheory.ObjectProperty.IsClosedUnderIsomorphisms.

---

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.

Equations

• @CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms = @CategoryTheory.ObjectProperty.IsClosedUnderIsomorphisms

theorem CategoryTheory.ObjectProperty.prop_of_iso {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) [P.IsClosedUnderIsomorphisms] {X Y : C} (e : X ≅ Y) (hX : P X) : P Y

theorem CategoryTheory.ObjectProperty.prop_iff_of_iso {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) [P.IsClosedUnderIsomorphisms] {X Y : C} (e : X ≅ Y) : P X ↔ P Y

theorem CategoryTheory.ObjectProperty.prop_of_isIso {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) [P.IsClosedUnderIsomorphisms] {X Y : C} (f : X ⟶ Y) [IsIso f] (hX : P X) : P Y

theorem CategoryTheory.ObjectProperty.prop_iff_of_isIso {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) [P.IsClosedUnderIsomorphisms] {X Y : C} (f : X ⟶ Y) [IsIso f] : P X ↔ P Y

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

The closure by isomorphisms of a predicate on objects in a category.

Equations

• P.isoClosure X = ∃ (Y : C), ∃ (x : P Y), Nonempty (X ≅ Y)

theorem CategoryTheory.ObjectProperty.prop_isoClosure_iff {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) (X : C) : P.isoClosure X ↔ ∃ (Y : C), ∃ (x : P Y), Nonempty (X ≅ Y)

theorem CategoryTheory.ObjectProperty.prop_isoClosure {C : Type u} [Category.{v, u} C] {P : ObjectProperty C} {X Y : C} (h : P X) (e : X ⟶ Y) [IsIso e] : P.isoClosure Y

theorem CategoryTheory.ObjectProperty.le_isoClosure {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) : P ≤ P.isoClosure

theorem CategoryTheory.ObjectProperty.monotone_isoClosure {C : Type u} [Category.{v, u} C] {P Q : ObjectProperty C} (h : P ≤ Q) : P.isoClosure ≤ Q.isoClosure

theorem CategoryTheory.ObjectProperty.isoClosure_eq_self {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) [P.IsClosedUnderIsomorphisms] : P.isoClosure = P

theorem CategoryTheory.ObjectProperty.isoClosure_le_iff {C : Type u} [Category.{v, u} C] (P Q : ObjectProperty C) [Q.IsClosedUnderIsomorphisms] : P.isoClosure ≤ Q ↔ P ≤ Q

instance CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphismsIsoClosure {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) : P.isoClosure.IsClosedUnderIsomorphisms

instance CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphismsMap {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] (P : ObjectProperty C) (F : Functor C D) : (P.map F).IsClosedUnderIsomorphisms

instance CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphismsInverseImage {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] (P : ObjectProperty C) (F : Functor D C) [P.IsClosedUnderIsomorphisms] : (P.inverseImage F).IsClosedUnderIsomorphisms

@[deprecated CategoryTheory.ObjectProperty.prop_of_iso (since := "2025-02-25")]

theorem CategoryTheory.mem_of_iso {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) [P.IsClosedUnderIsomorphisms] {X Y : C} (e : X ≅ Y) (hX : P X) : P Y

Alias of CategoryTheory.ObjectProperty.prop_of_iso.

@[deprecated CategoryTheory.ObjectProperty.prop_iff_of_iso (since := "2025-02-25")]

theorem CategoryTheory.mem_iff_of_iso {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) [P.IsClosedUnderIsomorphisms] {X Y : C} (e : X ≅ Y) : P X ↔ P Y

Alias of CategoryTheory.ObjectProperty.prop_iff_of_iso.

@[deprecated CategoryTheory.ObjectProperty.prop_of_isIso (since := "2025-02-25")]

theorem CategoryTheory.mem_of_isIso {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) [P.IsClosedUnderIsomorphisms] {X Y : C} (f : X ⟶ Y) [IsIso f] (hX : P X) : P Y

Alias of CategoryTheory.ObjectProperty.prop_of_isIso.

@[deprecated CategoryTheory.ObjectProperty.prop_iff_of_isIso (since := "2025-02-25")]

theorem CategoryTheory.mem_iff_of_isIso {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) [P.IsClosedUnderIsomorphisms] {X Y : C} (f : X ⟶ Y) [IsIso f] : P X ↔ P Y

Alias of CategoryTheory.ObjectProperty.prop_iff_of_isIso.

@[deprecated CategoryTheory.ObjectProperty.isoClosure (since := "2025-02-25")]

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

Alias of CategoryTheory.ObjectProperty.isoClosure.

---

The closure by isomorphisms of a predicate on objects in a category.

Equations

• @CategoryTheory.isoClosure = @CategoryTheory.ObjectProperty.isoClosure

@[deprecated CategoryTheory.ObjectProperty.prop_isoClosure_iff (since := "2025-02-25")]

theorem CategoryTheory.mem_isoClosure_iff {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) (X : C) : P.isoClosure X ↔ ∃ (Y : C), ∃ (x : P Y), Nonempty (X ≅ Y)

Alias of CategoryTheory.ObjectProperty.prop_isoClosure_iff.

@[deprecated CategoryTheory.ObjectProperty.prop_isoClosure (since := "2025-02-25")]

theorem CategoryTheory.mem_isoClosure {C : Type u} [Category.{v, u} C] {P : ObjectProperty C} {X Y : C} (h : P X) (e : X ⟶ Y) [IsIso e] : P.isoClosure Y

Alias of CategoryTheory.ObjectProperty.prop_isoClosure.