# 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

source
@[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)

Instances For

source
theorem CategoryTheory.ObjectProperty.le_def {C : Type u} [Category.{v, u} C] {P Q : ObjectProperty C} :
P ≤ Q ↔ ∀ (X : C), P X → Q X
source
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)

Instances For

source
@[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)
source
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)

Instances For

source
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)
source
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)
source
inductive CategoryTheory.ObjectProperty.strictMap {C : Type u} {D : Type u'} [Category.{v, u} C] [Category.{v', u'} D] (P : ObjectProperty C) (F : Functor C D) :
ObjectProperty D

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

- mk {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.strictMap F (F.obj X)

Instances For

source
theorem CategoryTheory.ObjectProperty.strictMap_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.strictMap F Y ↔ ∃ (X : C), P X ∧ F.obj X = Y
source
theorem CategoryTheory.ObjectProperty.strictMap_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.strictMap F (F.obj X)
source
class CategoryTheory.ObjectProperty.Is {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) (X : C) :
Prop

The typeclass associated to `P : ObjectProperty C`.

- prop : P X

Instances

source
theorem CategoryTheory.ObjectProperty.is_iff {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) (X : C) :
P.Is X ↔ P X
source
theorem CategoryTheory.ObjectProperty.prop_of_is {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) (X : C) [P.Is X] :
P X
source
theorem CategoryTheory.ObjectProperty.is_of_prop {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) {X : C} (hX : P X) :
P.Is X
source
inductive CategoryTheory.ObjectProperty.ofObj {C : Type u} [Category.{v, u} C] {ι : Type u'} (X : ι → C) :
ObjectProperty C

The property of objects that is satisfied by the `X i` for a family of objects `X : ι : C`.

- mk {C : Type u} [Category.{v, u} C] {ι : Type u'} {X : ι → C} (i : ι) : ofObj X (X i)

Instances For

source
@[simp]
theorem CategoryTheory.ObjectProperty.ofObj_apply {C : Type u} [Category.{v, u} C] {ι : Type u'} (X : ι → C) (i : ι) :
ofObj X (X i)
source
theorem CategoryTheory.ObjectProperty.ofObj_iff {C : Type u} [Category.{v, u} C] {ι : Type u'} (X : ι → C) (Y : C) :
ofObj X Y ↔ ∃ (i : ι), X i = Y
source
theorem CategoryTheory.ObjectProperty.ofObj_le_iff {C : Type u} [Category.{v, u} C] {ι : Type u'} (X : ι → C) (P : ObjectProperty C) :
ofObj X ≤ P ↔ ∀ (i : ι), P (X i)
source
@[simp]
theorem CategoryTheory.ObjectProperty.strictMap_ofObj {C : Type u} {D : Type u'} [Category.{v, u} C] [Category.{v', u'} D] {ι : Type u'} (X : ι → C) (F : Functor C D) :
(ofObj X).strictMap F = ofObj (F.obj ∘ X)
source
@[reducible, inline]
abbrev CategoryTheory.ObjectProperty.singleton {C : Type u} [Category.{v, u} C] (X : C) :
ObjectProperty C

The property of objects in a category that is satisfied by a single object `X : C`.

Equations

- CategoryTheory.ObjectProperty.singleton X = CategoryTheory.ObjectProperty.ofObj fun (x : Unit) => X

Instances For

source
@[simp]
theorem CategoryTheory.ObjectProperty.singleton_iff {C : Type u} [Category.{v, u} C] (X Y : C) :
singleton X Y ↔ X = Y
source
@[simp]
theorem CategoryTheory.ObjectProperty.singleton_le_iff {C : Type u} [Category.{v, u} C] {X : C} {P : ObjectProperty C} :
singleton X ≤ P ↔ P X
source
@[simp]
theorem CategoryTheory.ObjectProperty.strictMap_singleton {C : Type u} {D : Type u'} [Category.{v, u} C] [Category.{v', u'} D] (X : C) (F : Functor C D) :
(singleton X).strictMap F = singleton (F.obj X)
source
def CategoryTheory.ObjectProperty.pair {C : Type u} [Category.{v, u} C] (X Y : C) :
ObjectProperty C

The property of objects in a category that is satisfied by `X : C` and `Y : C`.

Equations

- CategoryTheory.ObjectProperty.pair X Y = CategoryTheory.ObjectProperty.ofObj (Sum.elim (fun (x : Unit) => X) fun (x : Unit) => Y)

Instances For

source
@[simp]
theorem CategoryTheory.ObjectProperty.pair_iff {C : Type u} [Category.{v, u} C] (X Y Z : C) :
pair X Y Z ↔ X = Z ∨ Y = Z