Mathlib.CategoryTheory.ObjectProperty.Basic

Module docstring

{"# 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

CategoryTheory.ObjectProperty abbrev

(C : Type u) [Category.{v} C] : Type u

Full source

/-- A property of objects in a category `C` is a predicate `C → Prop`. -/
@[nolint unusedArguments]
abbrev ObjectProperty (C : Type u) [Category.{v} C] : Type u := C → Prop

Object Property in a Category

Informal description

An object property in a category $\mathcal{C}$ is a predicate on the objects of $\mathcal{C}$, i.e., a function that assigns to each object $X$ in $\mathcal{C}$ a proposition $P(X)$.

CategoryTheory.ObjectProperty.le_def theorem

{P Q : ObjectProperty C} : P ≤ Q ↔ ∀ (X : C), P X → Q X

Full source

lemma le_def {P Q : ObjectProperty C} :
    P ≤ Q ↔ ∀ (X : C), P X → Q X := Iff.rfl

Order Relation on Object Properties via Implication

Informal description

For any two object properties $P$ and $Q$ in a category $\mathcal{C}$, the relation $P \leq Q$ holds if and only if for every object $X$ in $\mathcal{C}$, $P(X)$ implies $Q(X)$.

CategoryTheory.ObjectProperty.inverseImage definition

(P : ObjectProperty D) (F : C ⥤ D) : ObjectProperty C

Full source

/-- The inverse image of a property of objects by a functor. -/
def inverseImage (P : ObjectProperty D) (F : C ⥤ D) : ObjectProperty C :=
  fun X ↦ P (F.obj X)

Inverse image of an object property under a functor

Informal description

Given a category $\mathcal{D}$ and an object property $P$ on $\mathcal{D}$, the inverse image of $P$ under a functor $F : \mathcal{C} \to \mathcal{D}$ is the object property on $\mathcal{C}$ defined by: an object $X$ in $\mathcal{C}$ satisfies $P.\text{inverseImage} F X$ if and only if $P (F(X))$ holds.

CategoryTheory.ObjectProperty.prop_inverseImage_iff theorem

(P : ObjectProperty D) (F : C ⥤ D) (X : C) : P.inverseImage F X ↔ P (F.obj X)

Full source

@[simp]
lemma prop_inverseImage_iff (P : ObjectProperty D) (F : C ⥤ D) (X : C) :
    P.inverseImage F X ↔ P (F.obj X) := Iff.rfl

Characterization of Inverse Image Property via Functor Application

Informal description

For any object property $P$ on a category $\mathcal{D}$, any functor $F : \mathcal{C} \to \mathcal{D}$, and any object $X$ in $\mathcal{C}$, the inverse image property $P.\text{inverseImage} F$ holds for $X$ if and only if $P$ holds for $F(X)$.

CategoryTheory.ObjectProperty.map definition

(P : ObjectProperty C) (F : C ⥤ D) : ObjectProperty D

Full source

/-- The essential image of a property of objects by a functor. -/
def map (P : ObjectProperty C) (F : C ⥤ D) : ObjectProperty D :=
  fun Y ↦ ∃ (X : C), P X ∧ Nonempty (F.obj X ≅ Y)

Essential image of an object property under a functor

Informal description

Given a category $\mathcal{C}$ and an object property $P$ on $\mathcal{C}$, the essential image of $P$ under a functor $F : \mathcal{C} \to \mathcal{D}$ is the object property on $\mathcal{D}$ defined by: an object $Y$ in $\mathcal{D}$ satisfies $P.map F Y$ if and only if there exists an object $X$ in $\mathcal{C}$ such that $P X$ holds and $F(X)$ is isomorphic to $Y$.

CategoryTheory.ObjectProperty.prop_map_iff theorem

(P : ObjectProperty C) (F : C ⥤ D) (Y : D) : P.map F Y ↔ ∃ (X : C), P X ∧ Nonempty (F.obj X ≅ Y)

Full source

lemma prop_map_iff (P : ObjectProperty C) (F : C ⥤ D) (Y : D) :
    P.map F Y ↔ ∃ (X : C), P X ∧ Nonempty (F.obj X ≅ Y) := Iff.rfl

Characterization of Essential Image Property via Functor and Isomorphism

Informal description

Let $\mathcal{C}$ and $\mathcal{D}$ be categories, $P$ an object property in $\mathcal{C}$, and $F : \mathcal{C} \to \mathcal{D}$ a functor. For any object $Y$ in $\mathcal{D}$, the essential image property $P.map F Y$ holds if and only if there exists an object $X$ in $\mathcal{C}$ such that $P(X)$ holds and $F(X)$ is isomorphic to $Y$ (i.e., $F(X) \cong Y$).

CategoryTheory.ObjectProperty.prop_map_obj theorem

(P : ObjectProperty C) (F : C ⥤ D) {X : C} (hX : P X) : P.map F (F.obj X)

Full source

lemma prop_map_obj (P : ObjectProperty C) (F : C ⥤ D) {X : C} (hX : P X) :
    P.map F (F.obj X) :=
  ⟨X, hX, ⟨Iso.refl _⟩⟩

Functor Image Preserves Object Property

Informal description

Let $\mathcal{C}$ and $\mathcal{D}$ be categories, $P$ an object property in $\mathcal{C}$, and $F : \mathcal{C} \to \mathcal{D}$ a functor. For any object $X$ in $\mathcal{C}$ satisfying $P(X)$, the image $F(X)$ in $\mathcal{D}$ satisfies the essential image property $P.map F (F(X))$.

CategoryTheory.ObjectProperty.Is structure

(P : ObjectProperty C) (X : C)

Full source

/-- The typeclass associated to `P : ObjectProperty C`. -/
@[mk_iff]
class Is (P : ObjectProperty C) (X : C) : Prop where
  prop : P X

Satisfaction of an Object Property in a Category

Informal description

The structure `ObjectProperty.Is P X` represents that the object $X$ in the category $\mathcal{C}$ satisfies the property $P$, where $P$ is an object property in $\mathcal{C}$ (i.e., a predicate on the objects of $\mathcal{C}$).

CategoryTheory.ObjectProperty.prop_of_is theorem

(P : ObjectProperty C) (X : C) [P.Is X] : P X

Full source

lemma prop_of_is (P : ObjectProperty C) (X : C) [P.Is X] : P X := by rwa [← P.is_iff]

Satisfaction of Object Property Implies Predicate Holds

Informal description

For any object property $P$ in a category $\mathcal{C}$ and any object $X$ in $\mathcal{C}$, if $X$ satisfies $P$ (i.e., $P.\text{Is}\ X$ holds), then the proposition $P(X)$ is true.

CategoryTheory.ObjectProperty.is_of_prop theorem

(P : ObjectProperty C) {X : C} (hX : P X) : P.Is X

Full source

lemma is_of_prop (P : ObjectProperty C) {X : C} (hX : P X) : P.Is X := by rwa [P.is_iff]

Implication from Property to Satisfaction in a Category

Informal description

For any object property $P$ in a category $\mathcal{C}$ and any object $X$ in $\mathcal{C}$, if $P(X)$ holds, then $X$ satisfies the property $P$ (i.e., `P.Is X` holds).