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) [CategoryStruct.{v, u} C] : Type u

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

Equations

• CategoryTheory.ObjectProperty C = (C → Prop)

theorem CategoryTheory.ObjectProperty.le_def {C : Type u} [CategoryStruct.{v, u} C] {P Q : ObjectProperty C} : P ≤ Q ↔ ∀ (X : C), P X → Q X

theorem CategoryTheory.ObjectProperty.not_le_iff_exists {C : Type u} [CategoryStruct.{v, u} C] {P Q : ObjectProperty C} : ¬P ≤ Q ↔ ∃ (X : C), P X ∧ ¬Q X

class CategoryTheory.ObjectProperty.Is {C : Type u} [CategoryStruct.{v, u} C] (P : ObjectProperty C) (X : C) : Prop

The typeclass associated to P : ObjectProperty C.

• prop : P X

theorem CategoryTheory.ObjectProperty.is_iff {C : Type u} [CategoryStruct.{v, u} C] (P : ObjectProperty C) (X : C) : P.Is X ↔ P X

theorem CategoryTheory.ObjectProperty.prop_of_is {C : Type u} [CategoryStruct.{v, u} C] (P : ObjectProperty C) (X : C) [P.Is X] : P X

theorem CategoryTheory.ObjectProperty.is_of_prop {C : Type u} [CategoryStruct.{v, u} C] (P : ObjectProperty C) {X : C} (hX : P X) : P.Is X

class CategoryTheory.ObjectProperty.Nonempty {C : Type u} [CategoryStruct.{v, u} C] (P : ObjectProperty C) : Prop

Nonempty P is a typeclass saying there exists an object X : C that satisfies P.

• exists_prop : ∃ (X : C), P X

theorem CategoryTheory.ObjectProperty.nonempty_iff {C : Type u} [CategoryStruct.{v, u} C] (P : ObjectProperty C) : P.Nonempty ↔ ∃ (X : C), P X

theorem CategoryTheory.ObjectProperty.exists_prop_of_nonempty {C : Type u} [CategoryStruct.{v, u} C] (P : ObjectProperty C) [P.Nonempty] : ∃ (X : C), P X

theorem CategoryTheory.ObjectProperty.nonempty_of_prop {C : Type u} [CategoryStruct.{v, u} C] {P : ObjectProperty C} {X : C} (h : P X) : P.Nonempty

noncomputable def CategoryTheory.ObjectProperty.arbitrary {C : Type u} [CategoryStruct.{v, u} C] (P : ObjectProperty C) [P.Nonempty] : C

Using Classical.choice, extracts an object from a Nonempty object property.

Equations

• P.arbitrary = ⋯.choose

theorem CategoryTheory.ObjectProperty.prop_arbitrary {C : Type u} [CategoryStruct.{v, u} C] (P : ObjectProperty C) [P.Nonempty] : P P.arbitrary

theorem CategoryTheory.ObjectProperty.Nonempty.mono {C : Type u} [CategoryStruct.{v, u} C] {P Q : ObjectProperty C} [P.Nonempty] (hPQ : P ≤ Q) : Q.Nonempty

theorem CategoryTheory.ObjectProperty.nonempty_of_lt {C : Type u} [CategoryStruct.{v, u} C] {P Q : ObjectProperty C} (h : P < Q) : Q.Nonempty

inductive CategoryTheory.ObjectProperty.ofObj {C : Type u} [CategoryStruct.{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} [CategoryStruct.{v, u} C] {ι : Type u'} {X : ι → C} (i : ι) : ofObj X (X i)

@[simp]

theorem CategoryTheory.ObjectProperty.ofObj_apply {C : Type u} [CategoryStruct.{v, u} C] {ι : Type u'} (X : ι → C) (i : ι) : ofObj X (X i)

theorem CategoryTheory.ObjectProperty.ofObj_iff {C : Type u} [CategoryStruct.{v, u} C] {ι : Type u'} (X : ι → C) (Y : C) : ofObj X Y ↔ ∃ (i : ι), X i = Y

theorem CategoryTheory.ObjectProperty.ofObj_le_iff {C : Type u} [CategoryStruct.{v, u} C] {ι : Type u'} (X : ι → C) (P : ObjectProperty C) : ofObj X ≤ P ↔ ∀ (i : ι), P (X i)

instance CategoryTheory.ObjectProperty.instNonemptyOfObjOfNonempty {C : Type u} [CategoryStruct.{v, u} C] {ι : Type u'} (X : ι → C) [Nonempty ι] : (ofObj X).Nonempty

@[simp]

theorem CategoryTheory.ObjectProperty.ofObj_subtypeVal {C : Type u} [CategoryStruct.{v, u} C] (P : ObjectProperty C) : ofObj Subtype.val = P

@[reducible, inline]

abbrev CategoryTheory.ObjectProperty.singleton {C : Type u} [CategoryStruct.{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

@[simp]

theorem CategoryTheory.ObjectProperty.singleton_iff {C : Type u} [CategoryStruct.{v, u} C] (X Y : C) : singleton X Y ↔ X = Y

@[simp]

theorem CategoryTheory.ObjectProperty.singleton_le_iff {C : Type u} [CategoryStruct.{v, u} C] {X : C} {P : ObjectProperty C} : singleton X ≤ P ↔ P X

def CategoryTheory.ObjectProperty.pair {C : Type u} [CategoryStruct.{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)

@[simp]

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

instance CategoryTheory.ObjectProperty.instNonemptyPair {C : Type u} [CategoryStruct.{v, u} C] (X Y : C) : (pair X Y).Nonempty

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)

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

theorem CategoryTheory.ObjectProperty.map_monotone {C : Type u} {D : Type u'} [Category.{v, u} C] [Category.{v', u'} D] {P Q : ObjectProperty C} (h : P ≤ Q) (F : Functor C D) : P.map F ≤ Q.map F

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)

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

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)

instance CategoryTheory.ObjectProperty.instNonemptyStrictMap {C : Type u} {D : Type u'} [Category.{v, u} C] [Category.{v', u'} D] (P : ObjectProperty C) (F : Functor C D) [P.Nonempty] : (P.strictMap F).Nonempty

theorem CategoryTheory.ObjectProperty.strictMap_monotone {C : Type u} {D : Type u'} [Category.{v, u} C] [Category.{v', u'} D] {P Q : ObjectProperty C} (h : P ≤ Q) (F : Functor C D) : P.strictMap F ≤ Q.strictMap F

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

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

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