Predicates on objects which are closed under isomorphisms

This file introduces the type class ClosedUnderIsomorphisms P for predicates P : C → Prop on the objects of a category C.

class CategoryTheory.ClosedUnderIsomorphisms {C : Type u_1} [Category.{u_2, u_1} C] (P : C → Prop) : 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

theorem CategoryTheory.mem_of_iso {C : Type u_1} [Category.{u_2, u_1} C] (P : C → Prop) [ClosedUnderIsomorphisms P] {X Y : C} (e : X ≅ Y) (hX : P X) : P Y

theorem CategoryTheory.mem_iff_of_iso {C : Type u_1} [Category.{u_2, u_1} C] (P : C → Prop) [ClosedUnderIsomorphisms P] {X Y : C} (e : X ≅ Y) : P X ↔ P Y

theorem CategoryTheory.mem_of_isIso {C : Type u_1} [Category.{u_2, u_1} C] (P : C → Prop) [ClosedUnderIsomorphisms P] {X Y : C} (f : X ⟶ Y) [IsIso f] (hX : P X) : P Y

theorem CategoryTheory.mem_iff_of_isIso {C : Type u_1} [Category.{u_2, u_1} C] (P : C → Prop) [ClosedUnderIsomorphisms P] {X Y : C} (f : X ⟶ Y) [IsIso f] : P X ↔ P Y

def CategoryTheory.isoClosure {C : Type u_1} [Category.{u_2, u_1} C] (P : C → Prop) : C → Prop

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

Equations

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

theorem CategoryTheory.mem_isoClosure_iff {C : Type u_1} [Category.{u_2, u_1} C] (P : C → Prop) (X : C) : isoClosure P X ↔ ∃ (Y : C), ∃ (x : P Y), Nonempty (X ≅ Y)

theorem CategoryTheory.mem_isoClosure {C : Type u_1} [Category.{u_2, u_1} C] {P : C → Prop} {X Y : C} (h : P X) (e : X ⟶ Y) [IsIso e] : isoClosure P Y

theorem CategoryTheory.le_isoClosure {C : Type u_1} [Category.{u_2, u_1} C] (P : C → Prop) : P ≤ isoClosure P

theorem CategoryTheory.monotone_isoClosure {C : Type u_1} [Category.{u_2, u_1} C] {P Q : C → Prop} (h : P ≤ Q) : isoClosure P ≤ isoClosure Q

theorem CategoryTheory.isoClosure_eq_self {C : Type u_1} [Category.{u_2, u_1} C] (P : C → Prop) [ClosedUnderIsomorphisms P] : isoClosure P = P

theorem CategoryTheory.isoClosure_le_iff {C : Type u_1} [Category.{u_2, u_1} C] (P Q : C → Prop) [ClosedUnderIsomorphisms Q] : isoClosure P ≤ Q ↔ P ≤ Q

instance CategoryTheory.instClosedUnderIsomorphismsIsoClosure {C : Type u_1} [Category.{u_2, u_1} C] (P : C → Prop) : ClosedUnderIsomorphisms (isoClosure P)