Properties of objects in comma categories

def CategoryTheory.ObjectProperty.comma {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} D] (F₁ : Functor C₁ D) (F₂ : Functor C₂ D) (P₁ : ObjectProperty C₁) (P₂ : ObjectProperty C₂) : ObjectProperty (Comma F₁ F₂)

Given functors F₁ : C₁ ⥤ D and F₂ : C₂ ⥤ D, and properties of objects P₁ : ObjectProperty C₁ and P₂ : ObjectProperty C₂, this is the property of objects in Comma F₁ F₂ satisfying by the objects corresponding to morphisms F₁.obj X₁ ⟶ F₂.obj X₂ where P₁ X₁ and P₂ X₂ hold.

Equations

• CategoryTheory.ObjectProperty.comma F₁ F₂ P₁ P₂ = P₁.inverseImage (CategoryTheory.Comma.fst F₁ F₂) ⊓ P₂.inverseImage (CategoryTheory.Comma.snd F₁ F₂)

@[simp]

theorem CategoryTheory.ObjectProperty.comma_iff {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} D] {F₁ : Functor C₁ D} {F₂ : Functor C₂ D} (P₁ : ObjectProperty C₁) (P₂ : ObjectProperty C₂) (X : Comma F₁ F₂) : comma F₁ F₂ P₁ P₂ X ↔ P₁ X.left ∧ P₂ X.right

instance CategoryTheory.ObjectProperty.instIsStableUnderRetractsCommaComma {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} D] (F₁ : Functor C₁ D) (F₂ : Functor C₂ D) (P₁ : ObjectProperty C₁) (P₂ : ObjectProperty C₂) [P₁.IsStableUnderRetracts] [P₂.IsStableUnderRetracts] : (comma F₁ F₂ P₁ P₂).IsStableUnderRetracts

instance CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphismsCommaComma {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} D] (F₁ : Functor C₁ D) (F₂ : Functor C₂ D) (P₁ : ObjectProperty C₁) (P₂ : ObjectProperty C₂) [P₁.IsClosedUnderIsomorphisms] [P₂.IsClosedUnderIsomorphisms] : (comma F₁ F₂ P₁ P₂).IsClosedUnderIsomorphisms

instance CategoryTheory.ObjectProperty.instSmallCommaCommaOfLocallySmall {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} D] (F₁ : Functor C₁ D) (F₂ : Functor C₂ D) (P₁ : ObjectProperty C₁) (P₂ : ObjectProperty C₂) [ObjectProperty.Small.{w, v_1, u_1} P₁] [ObjectProperty.Small.{w, v_2, u_2} P₂] [LocallySmall.{w, v_3, u_3} D] : ObjectProperty.Small.{w, max v_1 v_2, max (max u_1 u_2) v_3} (comma F₁ F₂ P₁ P₂)

instance CategoryTheory.ObjectProperty.instEssentiallySmallCommaCommaOfLocallySmall {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} D] (F₁ : Functor C₁ D) (F₂ : Functor C₂ D) (P₁ : ObjectProperty C₁) (P₂ : ObjectProperty C₂) [ObjectProperty.EssentiallySmall.{w, v_1, u_1} P₁] [ObjectProperty.EssentiallySmall.{w, v_2, u_2} P₂] [LocallySmall.{w, v_3, u_3} D] : ObjectProperty.EssentiallySmall.{w, max v_1 v_2, max (max u_1 u_2) v_3} (comma F₁ F₂ P₁ P₂)