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

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

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

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

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

def CategoryTheory.isoClosure {C : Type u_1} [CategoryTheory.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} [CategoryTheory.Category.{u_2, u_1} C] (P : C → Prop) (X : C) : CategoryTheory.isoClosure P X ↔ ∃ (Y : C), ∃ (x : P Y), Nonempty (X ≅ Y)

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

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

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

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

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

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

Equations

• ⋯ = ⋯