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 : X ≅ Y), P X → P Y

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

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

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

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

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

@[simp]

theorem CategoryTheory.ObjectProperty.isoClosure_strictMap {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] (P : ObjectProperty C) (F : Functor C D) : (P.strictMap F).isoClosure = P.map F

@[simp]

theorem CategoryTheory.ObjectProperty.map_isoClosure {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] (P : ObjectProperty C) (F : Functor C D) : P.isoClosure.map F = P.map F