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

@[reducible, inline]

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

A property of objects in a category C is a predicate C → Prop.

Equations

• CategoryTheory.ObjectProperty C = (C → Prop)

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

The inverse image of a property of objects by a functor.

Equations

• P.inverseImage F X = P (F.obj X)

@[simp]

theorem CategoryTheory.ObjectProperty.prop_inverseImage_iff {C : Type u} {D : Type u'} [Category.{v, u} C] [Category.{v', u'} D] (P : ObjectProperty D) (F : Functor C D) (X : C) : P.inverseImage F X ↔ P (F.obj X)

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

The essential image of a property of objects by a functor.

Equations

• P.map F Y = ∃ (X : C), P X ∧ Nonempty (F.obj X ≅ Y)

theorem CategoryTheory.ObjectProperty.prop_map_iff {C : Type u} {D : Type u'} [Category.{v, u} C] [Category.{v', u'} D] (P : ObjectProperty C) (F : Functor C D) (Y : D) : P.map F Y ↔ ∃ (X : C), P X ∧ Nonempty (F.obj X ≅ Y)

theorem CategoryTheory.ObjectProperty.prop_map_obj {C : Type u} {D : Type u'} [Category.{v, u} C] [Category.{v', u'} D] (P : ObjectProperty C) (F : Functor C D) {X : C} (hX : P X) : P.map F (F.obj X)