Subcategories of comma categories defined by morphism properties

Given functors L : A ⥤ T and R : B ⥤ T and morphism properties P, Q and W on T, A and B respectively, we define the subcategory P.Comma L R Q W of Comma L R where

• objects are objects of Comma L R with the structural morphism satisfying P, and
• morphisms are morphisms of Comma L R where the left morphism satisfies Q and the right morphism satisfies W.

For an object X : T, this specializes to P.Over Q X which is the subcategory of Over X where the structural morphism satisfies P and where the horizontal morphisms satisfy Q. Common examples of the latter are e.g. the category of schemes étale (finite, affine, etc.) over a base X. Here Q = ⊤.

Implementation details

• We provide the general constructor P.Comma L R Q W to obtain Over X and Under X as special cases of the more general setup.

• Most results are developed only in the case where Q = ⊤ and W = ⊤, but the definition is setup in the general case to allow for a later generalization if needed.

theorem CategoryTheory.MorphismProperty.costructuredArrow_iso_iff {A : Type u_1} [Category.{v_1, u_1} A] {T : Type u_3} [Category.{v_3, u_3} T] (P : MorphismProperty T) [P.RespectsIso] {L : Functor A T} {X : T} {f g : CostructuredArrow L X} (e : f ≅ g) : P f.hom ↔ P g.hom

theorem CategoryTheory.MorphismProperty.over_iso_iff {T : Type u_3} [Category.{v_3, u_3} T] (P : MorphismProperty T) [P.RespectsIso] {X : T} {f g : Over X} (e : f ≅ g) : P f.hom ↔ P g.hom

def CategoryTheory.MorphismProperty.commaObj {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] (L : Functor A T) (R : Functor B T) (W : MorphismProperty T) : ObjectProperty (Comma L R)

The object property on Comma L R induced by a morphism property.

@[simp]

theorem CategoryTheory.MorphismProperty.commaObj_iff {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] (L : Functor A T) (R : Functor B T) {W : MorphismProperty T} (Y : Comma L R) : commaObj L R W Y ↔ W Y.hom

instance CategoryTheory.MorphismProperty.instIsClosedUnderIsomorphismsCommaCommaObjOfRespectsIso {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] (L : Functor A T) (R : Functor B T) {W : MorphismProperty T} [W.RespectsIso] : (commaObj L R W).IsClosedUnderIsomorphisms

def CategoryTheory.MorphismProperty.costructuredArrowObj {A : Type u_1} [Category.{v_1, u_1} A] {T : Type u_3} [Category.{v_3, u_3} T] (L : Functor A T) {X : T} (W : MorphismProperty T) : ObjectProperty (CostructuredArrow L X)

The object property on CostructuredArrow L X induced by a morphism property.

@[simp]

theorem CategoryTheory.MorphismProperty.costructuredArrowObj_iff {A : Type u_1} [Category.{v_1, u_1} A] {T : Type u_3} [Category.{v_3, u_3} T] (L : Functor A T) {W : MorphismProperty T} {X : T} (Y : CostructuredArrow L X) : costructuredArrowObj L W Y ↔ W Y.hom

instance CategoryTheory.MorphismProperty.instIsClosedUnderIsomorphismsCostructuredArrowCostructuredArrowObjOfRespectsIso {A : Type u_1} [Category.{v_1, u_1} A] {T : Type u_3} [Category.{v_3, u_3} T] (L : Functor A T) {W : MorphismProperty T} {X : T} [W.RespectsIso] : (costructuredArrowObj L W).IsClosedUnderIsomorphisms

def CategoryTheory.MorphismProperty.structuredArrowObj {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] (R : Functor B T) {X : T} (W : MorphismProperty T) : ObjectProperty (StructuredArrow X R)

The object property on StructuredArrow X R induced by a morphism property.

@[simp]

theorem CategoryTheory.MorphismProperty.structuredArrowObj_iff {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] (R : Functor B T) {W : MorphismProperty T} {X : T} (Y : StructuredArrow X R) : structuredArrowObj R W Y ↔ W Y.hom

instance CategoryTheory.MorphismProperty.instIsClosedUnderIsomorphismsStructuredArrowStructuredArrowObjOfRespectsIso {A : Type u_1} [Category.{v_1, u_1} A] {T : Type u_3} [Category.{v_3, u_3} T] (L : Functor A T) {W : MorphismProperty T} {X : T} [W.RespectsIso] : (structuredArrowObj L W).IsClosedUnderIsomorphisms

def CategoryTheory.MorphismProperty.over {T : Type u_3} [Category.{v_3, u_3} T] (W : MorphismProperty T) {X : T} : MorphismProperty (Over X)

The morphism property on Over X induced by a morphism property on C.

theorem CategoryTheory.MorphismProperty.over_eq_inverseImage {T : Type u_3} [Category.{v_3, u_3} T] (W : MorphismProperty T) (X : T) : W.over = W.inverseImage (CategoryTheory.Over.forget X)

@[simp]

theorem CategoryTheory.MorphismProperty.over_iff {T : Type u_3} [Category.{v_3, u_3} T] {W : MorphismProperty T} {X : T} {Y Z : Over X} (f : Y ⟶ Z) : W.over f ↔ W f.left

def CategoryTheory.MorphismProperty.under {T : Type u_3} [Category.{v_3, u_3} T] (W : MorphismProperty T) {X : T} : MorphismProperty (Under X)

The morphism property on Under X induced by a morphism property on C.

theorem CategoryTheory.MorphismProperty.under_eq_inverseImage {T : Type u_3} [Category.{v_3, u_3} T] (W : MorphismProperty T) (X : T) : W.under = W.inverseImage (CategoryTheory.Under.forget X)

@[simp]

theorem CategoryTheory.MorphismProperty.under_iff {T : Type u_3} [Category.{v_3, u_3} T] {W : MorphismProperty T} {X : T} {Y Z : Under X} (f : Y ⟶ Z) : W.under f ↔ W f.right

def CategoryTheory.MorphismProperty.overObj {T : Type u_3} [Category.{v_3, u_3} T] (W : MorphismProperty T) {X : T} : ObjectProperty (Over X)

The object property on Over X induced by a morphism property.

@[simp]

theorem CategoryTheory.MorphismProperty.overObj_iff {T : Type u_3} [Category.{v_3, u_3} T] {W : MorphismProperty T} {X : T} (Y : Over X) : W.overObj Y ↔ W Y.hom

instance CategoryTheory.MorphismProperty.instIsClosedUnderIsomorphismsOverOverObjOfRespectsIso {T : Type u_3} [Category.{v_3, u_3} T] {W : MorphismProperty T} {X : T} [W.RespectsIso] : W.overObj.IsClosedUnderIsomorphisms

def CategoryTheory.MorphismProperty.underObj {T : Type u_3} [Category.{v_3, u_3} T] (W : MorphismProperty T) {X : T} : ObjectProperty (Under X)

The object property on Under X induced by a morphism property.

@[simp]

theorem CategoryTheory.MorphismProperty.underObj_iff {T : Type u_3} [Category.{v_3, u_3} T] {W : MorphismProperty T} {X : T} (Y : Under X) : W.underObj Y ↔ W Y.hom

instance CategoryTheory.MorphismProperty.instIsClosedUnderIsomorphismsUnderUnderObjOfRespectsIso {T : Type u_3} [Category.{v_3, u_3} T] {W : MorphismProperty T} {X : T} [W.RespectsIso] : W.underObj.IsClosedUnderIsomorphisms

structure CategoryTheory.MorphismProperty.Comma {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] (L : Functor A T) (R : Functor B T) (P : MorphismProperty T) (Q : MorphismProperty A) (W : MorphismProperty B) extends CategoryTheory.Comma L R : Type (max (max u_1 u_2) v_3)

P.Comma L R Q W is the subcategory of Comma L R consisting of objects X : Comma L R where X.hom satisfies P. The morphisms are given by morphisms in Comma L R where the left one satisfies Q and the right one satisfies W.

• left : A
• right : B
• hom : L.obj self.left ⟶ R.obj self.right
• prop : P self.hom

theorem CategoryTheory.MorphismProperty.Comma.ext {A : Type u_1} {inst✝ : Category.{v_1, u_1} A} {B : Type u_2} {inst✝¹ : Category.{v_2, u_2} B} {T : Type u_3} {inst✝² : Category.{v_3, u_3} T} {L : Functor A T} {R : Functor B T} {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} {x y : MorphismProperty.Comma L R P Q W} (left : x.left = y.left) (right : x.right = y.right) (hom : x.hom ≍ y.hom) : x = y

theorem CategoryTheory.MorphismProperty.Comma.ext_iff {A : Type u_1} {inst✝ : Category.{v_1, u_1} A} {B : Type u_2} {inst✝¹ : Category.{v_2, u_2} B} {T : Type u_3} {inst✝² : Category.{v_3, u_3} T} {L : Functor A T} {R : Functor B T} {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} {x y : MorphismProperty.Comma L R P Q W} : x = y ↔ x.left = y.left ∧ x.right = y.right ∧ x.hom ≍ y.hom

structure CategoryTheory.MorphismProperty.Comma.Hom {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] {L : Functor A T} {R : Functor B T} {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} (X Y : MorphismProperty.Comma L R P Q W) extends CategoryTheory.CommaMorphism X.toComma Y.toComma : Type (max v_1 v_2)

A morphism in P.Comma L R Q W is a morphism in Comma L R where the left hom satisfies Q and the right one satisfies W.

• left : X.left ⟶ Y.left
• right : X.right ⟶ Y.right
• w : CategoryStruct.comp (L.map self.left) Y.hom = CategoryStruct.comp X.hom (R.map self.right)
• prop_hom_left : Q self.left
• prop_hom_right : W self.right

theorem CategoryTheory.MorphismProperty.Comma.Hom.ext {A : Type u_1} {inst✝ : Category.{v_1, u_1} A} {B : Type u_2} {inst✝¹ : Category.{v_2, u_2} B} {T : Type u_3} {inst✝² : Category.{v_3, u_3} T} {L : Functor A T} {R : Functor B T} {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} {X Y : MorphismProperty.Comma L R P Q W} {x y : X.Hom Y} (left : x.left = y.left) (right : x.right = y.right) : x = y

theorem CategoryTheory.MorphismProperty.Comma.Hom.ext_iff {A : Type u_1} {inst✝ : Category.{v_1, u_1} A} {B : Type u_2} {inst✝¹ : Category.{v_2, u_2} B} {T : Type u_3} {inst✝² : Category.{v_3, u_3} T} {L : Functor A T} {R : Functor B T} {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} {X Y : MorphismProperty.Comma L R P Q W} {x y : X.Hom Y} : x = y ↔ x.left = y.left ∧ x.right = y.right

@[reducible, inline]

abbrev CategoryTheory.MorphismProperty.Comma.Hom.hom {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] {L : Functor A T} {R : Functor B T} {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} {X Y : MorphismProperty.Comma L R P Q W} (f : X.Hom Y) : X.toComma ⟶ Y.toComma

The underlying morphism of objects in Comma L R.

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.Hom.hom_mk {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] {L : Functor A T} {R : Functor B T} {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} {X Y : MorphismProperty.Comma L R P Q W} (f : CommaMorphism X.toComma Y.toComma) (hf : Q f.left) (hg : W f.right) : { toCommaMorphism := f, prop_hom_left := hf, prop_hom_right := hg }.hom = f

theorem CategoryTheory.MorphismProperty.Comma.Hom.hom_left {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] {L : Functor A T} {R : Functor B T} {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} {X Y : MorphismProperty.Comma L R P Q W} (f : X.Hom Y) : f.hom.left = f.left

theorem CategoryTheory.MorphismProperty.Comma.Hom.hom_right {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] {L : Functor A T} {R : Functor B T} {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} {X Y : MorphismProperty.Comma L R P Q W} (f : X.Hom Y) : f.hom.right = f.right

def CategoryTheory.MorphismProperty.Comma.Hom.Simps.hom {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] {L : Functor A T} {R : Functor B T} {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} {X Y : MorphismProperty.Comma L R P Q W} (f : X.Hom Y) : X.toComma ⟶ Y.toComma

See Note [custom simps projection]

def CategoryTheory.MorphismProperty.Comma.id {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] {L : Functor A T} {R : Functor B T} {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.ContainsIdentities] [W.ContainsIdentities] (X : MorphismProperty.Comma L R P Q W) : X.Hom X

The identity morphism of an object in P.Comma L R Q W.

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.id_right {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] {L : Functor A T} {R : Functor B T} {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.ContainsIdentities] [W.ContainsIdentities] (X : MorphismProperty.Comma L R P Q W) : X.id.right = CategoryStruct.id X.right

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.id_left {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] {L : Functor A T} {R : Functor B T} {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.ContainsIdentities] [W.ContainsIdentities] (X : MorphismProperty.Comma L R P Q W) : X.id.left = CategoryStruct.id X.left

def CategoryTheory.MorphismProperty.Comma.Hom.comp {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] {L : Functor A T} {R : Functor B T} {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsStableUnderComposition] [W.IsStableUnderComposition] {X Y Z : MorphismProperty.Comma L R P Q W} (f : X.Hom Y) (g : Y.Hom Z) : X.Hom Z

Composition of morphisms in P.Comma L R Q W.

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.Hom.comp_left {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] {L : Functor A T} {R : Functor B T} {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsStableUnderComposition] [W.IsStableUnderComposition] {X Y Z : MorphismProperty.Comma L R P Q W} (f : X.Hom Y) (g : Y.Hom Z) : (f.comp g).left = CategoryStruct.comp f.left g.left

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.Hom.comp_right {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] {L : Functor A T} {R : Functor B T} {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsStableUnderComposition] [W.IsStableUnderComposition] {X Y Z : MorphismProperty.Comma L R P Q W} (f : X.Hom Y) (g : Y.Hom Z) : (f.comp g).right = CategoryStruct.comp f.right g.right

@[implicit_reducible]

instance CategoryTheory.MorphismProperty.Comma.instCategory {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] (L : Functor A T) (R : Functor B T) (P : MorphismProperty T) (Q : MorphismProperty A) (W : MorphismProperty B) [Q.IsMultiplicative] [W.IsMultiplicative] : Category.{max v_1 v_2, max (max v_3 u_2) u_1} (MorphismProperty.Comma L R P Q W)

theorem CategoryTheory.MorphismProperty.Comma.toCommaMorphism_eq_hom {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] {L : Functor A T} {R : Functor B T} {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] {X Y : MorphismProperty.Comma L R P Q W} (f : X ⟶ Y) : f.toCommaMorphism = Hom.hom f

theorem CategoryTheory.MorphismProperty.Comma.Hom.ext' {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] {L : Functor A T} {R : Functor B T} {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] {X Y : MorphismProperty.Comma L R P Q W} {f g : X ⟶ Y} (h : hom f = hom g) : f = g

Alternative ext lemma for Comma.Hom.

theorem CategoryTheory.MorphismProperty.Comma.Hom.ext'_iff {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] {L : Functor A T} {R : Functor B T} {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] {X Y : MorphismProperty.Comma L R P Q W} {f g : X ⟶ Y} : f = g ↔ hom f = hom g

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.id_hom {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] {L : Functor A T} {R : Functor B T} {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] (X : MorphismProperty.Comma L R P Q W) : Hom.hom (CategoryStruct.id X) = CategoryStruct.id X.toComma

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.comp_hom {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] {L : Functor A T} {R : Functor B T} {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] {X Y Z : MorphismProperty.Comma L R P Q W} (f : X ⟶ Y) (g : Y ⟶ Z) : Hom.hom (CategoryStruct.comp f g) = CategoryStruct.comp (Hom.hom f) (Hom.hom g)

theorem CategoryTheory.MorphismProperty.Comma.comp_left {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] {L : Functor A T} {R : Functor B T} {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] {X Y Z : MorphismProperty.Comma L R P Q W} (f : X ⟶ Y) (g : Y ⟶ Z) : (CategoryStruct.comp f g).left = CategoryStruct.comp f.left g.left

theorem CategoryTheory.MorphismProperty.Comma.comp_left_assoc {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] {L : Functor A T} {R : Functor B T} {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] {X Y Z : MorphismProperty.Comma L R P Q W} (f : X ⟶ Y) (g : Y ⟶ Z) {Z✝ : A} (h : Z.left ⟶ Z✝) : CategoryStruct.comp (CategoryStruct.comp f g).left h = CategoryStruct.comp f.left (CategoryStruct.comp g.left h)

theorem CategoryTheory.MorphismProperty.Comma.comp_right {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] {L : Functor A T} {R : Functor B T} {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] {X Y Z : MorphismProperty.Comma L R P Q W} (f : X ⟶ Y) (g : Y ⟶ Z) : (CategoryStruct.comp f g).right = CategoryStruct.comp f.right g.right

theorem CategoryTheory.MorphismProperty.Comma.comp_right_assoc {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] {L : Functor A T} {R : Functor B T} {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] {X Y Z : MorphismProperty.Comma L R P Q W} (f : X ⟶ Y) (g : Y ⟶ Z) {Z✝ : B} (h : Z.right ⟶ Z✝) : CategoryStruct.comp (CategoryStruct.comp f g).right h = CategoryStruct.comp f.right (CategoryStruct.comp g.right h)

def CategoryTheory.MorphismProperty.Comma.homFromCommaOfIsIso {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] {L : Functor A T} {R : Functor B T} {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] [Q.RespectsIso] [W.RespectsIso] {X Y : MorphismProperty.Comma L R P Q W} (i : X.toComma ⟶ Y.toComma) [IsIso i] : X ⟶ Y

If i is an isomorphism in Comma L R, it is also a morphism in P.Comma L R Q W.

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.homFromCommaOfIsIso_hom {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] {L : Functor A T} {R : Functor B T} {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] [Q.RespectsIso] [W.RespectsIso] {X Y : MorphismProperty.Comma L R P Q W} (i : X.toComma ⟶ Y.toComma) [IsIso i] : Hom.hom (homFromCommaOfIsIso i) = i

instance CategoryTheory.MorphismProperty.Comma.instIsIsoHomFromCommaOfIsIso {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] {L : Functor A T} {R : Functor B T} {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] [Q.RespectsIso] [W.RespectsIso] {X Y : MorphismProperty.Comma L R P Q W} (i : X.toComma ⟶ Y.toComma) [IsIso i] : IsIso (homFromCommaOfIsIso i)

def CategoryTheory.MorphismProperty.Comma.isoFromComma {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] {L : Functor A T} {R : Functor B T} {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] [Q.RespectsIso] [W.RespectsIso] {X Y : MorphismProperty.Comma L R P Q W} (i : X.toComma ≅ Y.toComma) : X ≅ Y

Any isomorphism between objects of P.Comma L R Q W in Comma L R is also an isomorphism in P.Comma L R Q W.

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.isoFromComma_inv {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] {L : Functor A T} {R : Functor B T} {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] [Q.RespectsIso] [W.RespectsIso] {X Y : MorphismProperty.Comma L R P Q W} (i : X.toComma ≅ Y.toComma) : (isoFromComma i).inv = homFromCommaOfIsIso i.inv

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.isoFromComma_hom {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] {L : Functor A T} {R : Functor B T} {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] [Q.RespectsIso] [W.RespectsIso] {X Y : MorphismProperty.Comma L R P Q W} (i : X.toComma ≅ Y.toComma) : (isoFromComma i).hom = homFromCommaOfIsIso i.hom

def CategoryTheory.MorphismProperty.Comma.isoMk {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] {L : Functor A T} {R : Functor B T} {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] [Q.RespectsIso] [W.RespectsIso] {X Y : MorphismProperty.Comma L R P Q W} (l : X.left ≅ Y.left) (r : X.right ≅ Y.right) (h : CategoryStruct.comp (L.map l.hom) Y.hom = CategoryStruct.comp X.hom (R.map r.hom) := by cat_disch) : X ≅ Y

Constructor for isomorphisms in P.Comma L R Q W from isomorphisms of the left and right components and naturality in the forward direction.

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.isoMk_hom_left {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] {L : Functor A T} {R : Functor B T} {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] [Q.RespectsIso] [W.RespectsIso] {X Y : MorphismProperty.Comma L R P Q W} (l : X.left ≅ Y.left) (r : X.right ≅ Y.right) (h : CategoryStruct.comp (L.map l.hom) Y.hom = CategoryStruct.comp X.hom (R.map r.hom) := by cat_disch) : (isoMk l r h).hom.left = l.hom

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.isoMk_inv_right {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] {L : Functor A T} {R : Functor B T} {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] [Q.RespectsIso] [W.RespectsIso] {X Y : MorphismProperty.Comma L R P Q W} (l : X.left ≅ Y.left) (r : X.right ≅ Y.right) (h : CategoryStruct.comp (L.map l.hom) Y.hom = CategoryStruct.comp X.hom (R.map r.hom) := by cat_disch) : (isoMk l r h).inv.right = r.inv

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.isoMk_inv_left {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] {L : Functor A T} {R : Functor B T} {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] [Q.RespectsIso] [W.RespectsIso] {X Y : MorphismProperty.Comma L R P Q W} (l : X.left ≅ Y.left) (r : X.right ≅ Y.right) (h : CategoryStruct.comp (L.map l.hom) Y.hom = CategoryStruct.comp X.hom (R.map r.hom) := by cat_disch) : (isoMk l r h).inv.left = l.inv

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.isoMk_hom_right {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] {L : Functor A T} {R : Functor B T} {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] [Q.RespectsIso] [W.RespectsIso] {X Y : MorphismProperty.Comma L R P Q W} (l : X.left ≅ Y.left) (r : X.right ≅ Y.right) (h : CategoryStruct.comp (L.map l.hom) Y.hom = CategoryStruct.comp X.hom (R.map r.hom) := by cat_disch) : (isoMk l r h).hom.right = r.hom

def CategoryTheory.MorphismProperty.Comma.forget {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] (L : Functor A T) (R : Functor B T) (P : MorphismProperty T) (Q : MorphismProperty A) (W : MorphismProperty B) [Q.IsMultiplicative] [W.IsMultiplicative] : Functor (MorphismProperty.Comma L R P Q W) (Comma L R)

The forgetful functor.

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.forget_obj {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] (L : Functor A T) (R : Functor B T) (P : MorphismProperty T) (Q : MorphismProperty A) (W : MorphismProperty B) [Q.IsMultiplicative] [W.IsMultiplicative] (X : MorphismProperty.Comma L R P Q W) : (forget L R P Q W).obj X = X.toComma

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.forget_map {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] (L : Functor A T) (R : Functor B T) (P : MorphismProperty T) (Q : MorphismProperty A) (W : MorphismProperty B) [Q.IsMultiplicative] [W.IsMultiplicative] {X✝ Y✝ : MorphismProperty.Comma L R P Q W} (f : X✝ ⟶ Y✝) : (forget L R P Q W).map f = Hom.hom f

instance CategoryTheory.MorphismProperty.Comma.instFaithfulCommaForget {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] (L : Functor A T) (R : Functor B T) (P : MorphismProperty T) (Q : MorphismProperty A) (W : MorphismProperty B) [Q.IsMultiplicative] [W.IsMultiplicative] : (forget L R P Q W).Faithful

instance CategoryTheory.MorphismProperty.Comma.instIsIsoCommaHom {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] {L : Functor A T} {R : Functor B T} {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] {X Y : MorphismProperty.Comma L R P Q W} (f : X ⟶ Y) [IsIso f] : IsIso (Hom.hom f)

theorem CategoryTheory.MorphismProperty.Comma.hom_homFromCommaOfIsIso {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] {L : Functor A T} {R : Functor B T} {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] [Q.RespectsIso] [W.RespectsIso] {X Y : MorphismProperty.Comma L R P Q W} (i : X ⟶ Y) [IsIso (Hom.hom i)] : homFromCommaOfIsIso (Hom.hom i) = i

theorem CategoryTheory.MorphismProperty.Comma.inv_hom {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] {L : Functor A T} {R : Functor B T} {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] {X Y : MorphismProperty.Comma L R P Q W} (f : X ⟶ Y) [IsIso f] : Hom.hom (inv f) = inv (Hom.hom f)

instance CategoryTheory.MorphismProperty.Comma.instReflectsIsomorphismsCommaForgetOfRespectsIso {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] (L : Functor A T) (R : Functor B T) (P : MorphismProperty T) (Q : MorphismProperty A) (W : MorphismProperty B) [Q.IsMultiplicative] [W.IsMultiplicative] [Q.RespectsIso] [W.RespectsIso] : (forget L R P Q W).ReflectsIsomorphisms

def CategoryTheory.MorphismProperty.Comma.forgetFullyFaithful {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] (L : Functor A T) (R : Functor B T) (P : MorphismProperty T) : (forget L R P ⊤ ⊤).FullyFaithful

The forgetful functor from the full subcategory of Comma L R defined by P is fully faithful.

instance CategoryTheory.MorphismProperty.Comma.instFullTopCommaForget {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] (L : Functor A T) (R : Functor B T) (P : MorphismProperty T) : (forget L R P ⊤ ⊤).Full

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.eqToHom_left {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] {L : Functor A T} {R : Functor B T} (P : MorphismProperty T) (Q : MorphismProperty A) (W : MorphismProperty B) [Q.IsMultiplicative] [W.IsMultiplicative] {X Y : MorphismProperty.Comma L R P Q W} (h : X = Y) : (eqToHom h).left = eqToHom ⋯

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.eqToHom_right {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] {L : Functor A T} {R : Functor B T} (P : MorphismProperty T) (Q : MorphismProperty A) (W : MorphismProperty B) [Q.IsMultiplicative] [W.IsMultiplicative] {X Y : MorphismProperty.Comma L R P Q W} (h : X = Y) : (eqToHom h).right = eqToHom ⋯

def CategoryTheory.MorphismProperty.Comma.changeProp {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] (L : Functor A T) (R : Functor B T) {P P' : MorphismProperty T} {Q Q' : MorphismProperty A} {W W' : MorphismProperty B} (hP : P ≤ P') (hQ : Q ≤ Q') (hW : W ≤ W') [Q.IsMultiplicative] [Q'.IsMultiplicative] [W.IsMultiplicative] [W'.IsMultiplicative] : Functor (MorphismProperty.Comma L R P Q W) (MorphismProperty.Comma L R P' Q' W')

Weaken the conditions on all components.

def CategoryTheory.MorphismProperty.Comma.fullyFaithfulChangeProp {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] (L : Functor A T) (R : Functor B T) {P P' : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} (hP : P ≤ P') [Q.IsMultiplicative] [W.IsMultiplicative] : (changeProp L R hP ⋯ ⋯).FullyFaithful

Weakening the condition on the structure morphisms is fully faithful.

instance CategoryTheory.MorphismProperty.Comma.instFaithfulChangeProp {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] (L : Functor A T) (R : Functor B T) {P P' : MorphismProperty T} {Q Q' : MorphismProperty A} {W W' : MorphismProperty B} (hP : P ≤ P') (hQ : Q ≤ Q') (hW : W ≤ W') [Q.IsMultiplicative] [Q'.IsMultiplicative] [W.IsMultiplicative] [W'.IsMultiplicative] : (changeProp L R hP hQ hW).Faithful

instance CategoryTheory.MorphismProperty.Comma.instFullChangeProp {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] (L : Functor A T) (R : Functor B T) {P P' : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} (hP : P ≤ P') [Q.IsMultiplicative] [W.IsMultiplicative] : (changeProp L R hP ⋯ ⋯).Full

def CategoryTheory.MorphismProperty.Comma.lift {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] {L : Functor A T} {R : Functor B T} {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] {C : Type u_4} [Category.{v_4, u_4} C] (F : Functor C (Comma L R)) (hP : ∀ (X : C), P (F.obj X).hom) (hQ : ∀ {X Y : C} (f : X ⟶ Y), Q (F.map f).left) (hW : ∀ {X Y : C} (f : X ⟶ Y), W (F.map f).right) : Functor C (MorphismProperty.Comma L R P Q W)

Lift a functor F : C ⥤ Comma L R to the subcategory P.Comma L R Q W under suitable assumptions on F.

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.lift_obj_toComma {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] {L : Functor A T} {R : Functor B T} {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] {C : Type u_4} [Category.{v_4, u_4} C] (F : Functor C (Comma L R)) (hP : ∀ (X : C), P (F.obj X).hom) (hQ : ∀ {X Y : C} (f : X ⟶ Y), Q (F.map f).left) (hW : ∀ {X Y : C} (f : X ⟶ Y), W (F.map f).right) (X : C) : ((lift F hP hQ hW).obj X).toComma = F.obj X

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.lift_map_hom {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] {L : Functor A T} {R : Functor B T} {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] {C : Type u_4} [Category.{v_4, u_4} C] (F : Functor C (Comma L R)) (hP : ∀ (X : C), P (F.obj X).hom) (hQ : ∀ {X Y : C} (f : X ⟶ Y), Q (F.map f).left) (hW : ∀ {X Y : C} (f : X ⟶ Y), W (F.map f).right) {X Y : C} (f : X ⟶ Y) : Hom.hom ((lift F hP hQ hW).map f) = F.map f

def CategoryTheory.MorphismProperty.Comma.mapLeft {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] (R : Functor B T) {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] {L₁ L₂ : Functor A T} (l : L₁ ⟶ L₂) (hl : ∀ (X : MorphismProperty.Comma L₂ R P Q W), P (CategoryStruct.comp (l.app X.left) X.hom)) : Functor (MorphismProperty.Comma L₂ R P Q W) (MorphismProperty.Comma L₁ R P Q W)

A natural transformation L₁ ⟶ L₂ induces a functor P.Comma L₂ R Q W ⥤ P.Comma L₁ R Q W.

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.mapLeft_map_left {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] (R : Functor B T) {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] {L₁ L₂ : Functor A T} (l : L₁ ⟶ L₂) (hl : ∀ (X : MorphismProperty.Comma L₂ R P Q W), P (CategoryStruct.comp (l.app X.left) X.hom)) {X Y : MorphismProperty.Comma L₂ R P Q W} (f : X ⟶ Y) : ((mapLeft R l hl).map f).left = (Hom.hom f).left

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.mapLeft_obj_hom {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] (R : Functor B T) {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] {L₁ L₂ : Functor A T} (l : L₁ ⟶ L₂) (hl : ∀ (X : MorphismProperty.Comma L₂ R P Q W), P (CategoryStruct.comp (l.app X.left) X.hom)) (X : MorphismProperty.Comma L₂ R P Q W) : ((mapLeft R l hl).obj X).hom = CategoryStruct.comp (l.app X.left) X.hom

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.mapLeft_obj_left {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] (R : Functor B T) {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] {L₁ L₂ : Functor A T} (l : L₁ ⟶ L₂) (hl : ∀ (X : MorphismProperty.Comma L₂ R P Q W), P (CategoryStruct.comp (l.app X.left) X.hom)) (X : MorphismProperty.Comma L₂ R P Q W) : ((mapLeft R l hl).obj X).left = X.left

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.mapLeft_map_right {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] (R : Functor B T) {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] {L₁ L₂ : Functor A T} (l : L₁ ⟶ L₂) (hl : ∀ (X : MorphismProperty.Comma L₂ R P Q W), P (CategoryStruct.comp (l.app X.left) X.hom)) {X Y : MorphismProperty.Comma L₂ R P Q W} (f : X ⟶ Y) : ((mapLeft R l hl).map f).right = (Hom.hom f).right

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.mapLeft_obj_right {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] (R : Functor B T) {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] {L₁ L₂ : Functor A T} (l : L₁ ⟶ L₂) (hl : ∀ (X : MorphismProperty.Comma L₂ R P Q W), P (CategoryStruct.comp (l.app X.left) X.hom)) (X : MorphismProperty.Comma L₂ R P Q W) : ((mapLeft R l hl).obj X).right = X.right

def CategoryTheory.MorphismProperty.Comma.mapLeftId {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] (L : Functor A T) (R : Functor B T) {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] [Q.RespectsIso] [W.RespectsIso] : mapLeft R (CategoryStruct.id L) ⋯ ≅ Functor.id (MorphismProperty.Comma L R P Q W)

The functor P.Comma L R Q W ⥤ P.Comma L R Q W induced by the identity natural transformation on L is naturally isomorphic to the identity functor.

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.mapLeftId_hom_app_left {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] (L : Functor A T) (R : Functor B T) {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] [Q.RespectsIso] [W.RespectsIso] (X : MorphismProperty.Comma L R P Q W) : ((mapLeftId L R).hom.app X).left = CategoryStruct.id X.left

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.mapLeftId_hom_app_right {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] (L : Functor A T) (R : Functor B T) {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] [Q.RespectsIso] [W.RespectsIso] (X : MorphismProperty.Comma L R P Q W) : ((mapLeftId L R).hom.app X).right = CategoryStruct.id X.right

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.mapLeftId_inv_app_left {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] (L : Functor A T) (R : Functor B T) {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] [Q.RespectsIso] [W.RespectsIso] (X : MorphismProperty.Comma L R P Q W) : ((mapLeftId L R).inv.app X).left = CategoryStruct.id X.left

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.mapLeftId_inv_app_right {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] (L : Functor A T) (R : Functor B T) {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] [Q.RespectsIso] [W.RespectsIso] (X : MorphismProperty.Comma L R P Q W) : ((mapLeftId L R).inv.app X).right = CategoryStruct.id X.right

def CategoryTheory.MorphismProperty.Comma.mapLeftComp {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] (R : Functor B T) {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] {L₁ L₂ L₃ : Functor A T} [Q.RespectsIso] [W.RespectsIso] (l : L₁ ⟶ L₂) (l' : L₂ ⟶ L₃) (hl : ∀ (X : MorphismProperty.Comma L₂ R P Q W), P (CategoryStruct.comp (l.app X.left) X.hom)) (hl' : ∀ (X : MorphismProperty.Comma L₃ R P Q W), P (CategoryStruct.comp (l'.app X.left) X.hom)) (hll' : ∀ (X : MorphismProperty.Comma L₃ R P Q W), P (CategoryStruct.comp ((CategoryStruct.comp l l').app X.left) X.hom)) : mapLeft R (CategoryStruct.comp l l') hll' ≅ (mapLeft R l' hl').comp (mapLeft R l hl)

The functor P.Comma L₁ R Q W ⥤ P.Comma L₃ R Q W induced by the composition of two natural transformations l : L₁ ⟶ L₂ and l' : L₂ ⟶ L₃ is naturally isomorphic to the composition of the two functors induced by these natural transformations.

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.mapLeftComp_inv_app_left {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] (R : Functor B T) {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] {L₁ L₂ L₃ : Functor A T} [Q.RespectsIso] [W.RespectsIso] (l : L₁ ⟶ L₂) (l' : L₂ ⟶ L₃) (hl : ∀ (X : MorphismProperty.Comma L₂ R P Q W), P (CategoryStruct.comp (l.app X.left) X.hom)) (hl' : ∀ (X : MorphismProperty.Comma L₃ R P Q W), P (CategoryStruct.comp (l'.app X.left) X.hom)) (hll' : ∀ (X : MorphismProperty.Comma L₃ R P Q W), P (CategoryStruct.comp ((CategoryStruct.comp l l').app X.left) X.hom)) (X : MorphismProperty.Comma L₃ R P Q W) : ((mapLeftComp R l l' hl hl' hll').inv.app X).left = CategoryStruct.id X.left

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.mapLeftComp_hom_app_right {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] (R : Functor B T) {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] {L₁ L₂ L₃ : Functor A T} [Q.RespectsIso] [W.RespectsIso] (l : L₁ ⟶ L₂) (l' : L₂ ⟶ L₃) (hl : ∀ (X : MorphismProperty.Comma L₂ R P Q W), P (CategoryStruct.comp (l.app X.left) X.hom)) (hl' : ∀ (X : MorphismProperty.Comma L₃ R P Q W), P (CategoryStruct.comp (l'.app X.left) X.hom)) (hll' : ∀ (X : MorphismProperty.Comma L₃ R P Q W), P (CategoryStruct.comp ((CategoryStruct.comp l l').app X.left) X.hom)) (X : MorphismProperty.Comma L₃ R P Q W) : ((mapLeftComp R l l' hl hl' hll').hom.app X).right = CategoryStruct.id X.right

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.mapLeftComp_inv_app_right {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] (R : Functor B T) {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] {L₁ L₂ L₃ : Functor A T} [Q.RespectsIso] [W.RespectsIso] (l : L₁ ⟶ L₂) (l' : L₂ ⟶ L₃) (hl : ∀ (X : MorphismProperty.Comma L₂ R P Q W), P (CategoryStruct.comp (l.app X.left) X.hom)) (hl' : ∀ (X : MorphismProperty.Comma L₃ R P Q W), P (CategoryStruct.comp (l'.app X.left) X.hom)) (hll' : ∀ (X : MorphismProperty.Comma L₃ R P Q W), P (CategoryStruct.comp ((CategoryStruct.comp l l').app X.left) X.hom)) (X : MorphismProperty.Comma L₃ R P Q W) : ((mapLeftComp R l l' hl hl' hll').inv.app X).right = CategoryStruct.id X.right

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.mapLeftComp_hom_app_left {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] (R : Functor B T) {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] {L₁ L₂ L₃ : Functor A T} [Q.RespectsIso] [W.RespectsIso] (l : L₁ ⟶ L₂) (l' : L₂ ⟶ L₃) (hl : ∀ (X : MorphismProperty.Comma L₂ R P Q W), P (CategoryStruct.comp (l.app X.left) X.hom)) (hl' : ∀ (X : MorphismProperty.Comma L₃ R P Q W), P (CategoryStruct.comp (l'.app X.left) X.hom)) (hll' : ∀ (X : MorphismProperty.Comma L₃ R P Q W), P (CategoryStruct.comp ((CategoryStruct.comp l l').app X.left) X.hom)) (X : MorphismProperty.Comma L₃ R P Q W) : ((mapLeftComp R l l' hl hl' hll').hom.app X).left = CategoryStruct.id X.left

def CategoryTheory.MorphismProperty.Comma.mapLeftEq {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] (R : Functor B T) {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] {L₁ L₂ : Functor A T} [Q.RespectsIso] [W.RespectsIso] (l l' : L₁ ⟶ L₂) (h : l = l') (hl : ∀ (X : MorphismProperty.Comma L₂ R P Q W), P (CategoryStruct.comp (l.app X.left) X.hom)) : mapLeft R l hl ≅ mapLeft R l' ⋯

Two equal natural transformations L₁ ⟶ L₂ yield naturally isomorphic functors P.Comma L₁ R Q W ⥤ P.Comma L₂ R Q W.

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.mapLeftEq_inv_app_left {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] (R : Functor B T) {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] {L₁ L₂ : Functor A T} [Q.RespectsIso] [W.RespectsIso] (l l' : L₁ ⟶ L₂) (h : l = l') (hl : ∀ (X : MorphismProperty.Comma L₂ R P Q W), P (CategoryStruct.comp (l.app X.left) X.hom)) (X : MorphismProperty.Comma L₂ R P Q W) : ((mapLeftEq R l l' h hl).inv.app X).left = CategoryStruct.id X.left

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.mapLeftEq_hom_app_left {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] (R : Functor B T) {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] {L₁ L₂ : Functor A T} [Q.RespectsIso] [W.RespectsIso] (l l' : L₁ ⟶ L₂) (h : l = l') (hl : ∀ (X : MorphismProperty.Comma L₂ R P Q W), P (CategoryStruct.comp (l.app X.left) X.hom)) (X : MorphismProperty.Comma L₂ R P Q W) : ((mapLeftEq R l l' h hl).hom.app X).left = CategoryStruct.id X.left

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.mapLeftEq_inv_app_right {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] (R : Functor B T) {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] {L₁ L₂ : Functor A T} [Q.RespectsIso] [W.RespectsIso] (l l' : L₁ ⟶ L₂) (h : l = l') (hl : ∀ (X : MorphismProperty.Comma L₂ R P Q W), P (CategoryStruct.comp (l.app X.left) X.hom)) (X : MorphismProperty.Comma L₂ R P Q W) : ((mapLeftEq R l l' h hl).inv.app X).right = CategoryStruct.id X.right

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.mapLeftEq_hom_app_right {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] (R : Functor B T) {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] {L₁ L₂ : Functor A T} [Q.RespectsIso] [W.RespectsIso] (l l' : L₁ ⟶ L₂) (h : l = l') (hl : ∀ (X : MorphismProperty.Comma L₂ R P Q W), P (CategoryStruct.comp (l.app X.left) X.hom)) (X : MorphismProperty.Comma L₂ R P Q W) : ((mapLeftEq R l l' h hl).hom.app X).right = CategoryStruct.id X.right

def CategoryTheory.MorphismProperty.Comma.mapLeftIso {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] (R : Functor B T) {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] {L₁ L₂ : Functor A T} [P.RespectsIso] [Q.RespectsIso] [W.RespectsIso] (e : L₁ ≅ L₂) : MorphismProperty.Comma L₁ R P Q W ≌ MorphismProperty.Comma L₂ R P Q W

A natural isomorphism L₁ ≅ L₂ induces an equivalence of categories P.Comma L₁ R Q W ≌ P.Comma L₂ R Q W.

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.mapLeftIso_counitIso_inv_app_right {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] (R : Functor B T) {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] {L₁ L₂ : Functor A T} [P.RespectsIso] [Q.RespectsIso] [W.RespectsIso] (e : L₁ ≅ L₂) (X : MorphismProperty.Comma L₂ R P Q W) : ((mapLeftIso R e).counitIso.inv.app X).right = CategoryStruct.id X.right

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.mapLeftIso_counitIso_hom_app_right {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] (R : Functor B T) {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] {L₁ L₂ : Functor A T} [P.RespectsIso] [Q.RespectsIso] [W.RespectsIso] (e : L₁ ≅ L₂) (X : MorphismProperty.Comma L₂ R P Q W) : ((mapLeftIso R e).counitIso.hom.app X).right = CategoryStruct.id X.right

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.mapLeftIso_inverse_obj_left {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] (R : Functor B T) {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] {L₁ L₂ : Functor A T} [P.RespectsIso] [Q.RespectsIso] [W.RespectsIso] (e : L₁ ≅ L₂) (X : MorphismProperty.Comma L₂ R P Q W) : ((mapLeftIso R e).inverse.obj X).left = X.left

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.mapLeftIso_inverse_obj_right {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] (R : Functor B T) {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] {L₁ L₂ : Functor A T} [P.RespectsIso] [Q.RespectsIso] [W.RespectsIso] (e : L₁ ≅ L₂) (X : MorphismProperty.Comma L₂ R P Q W) : ((mapLeftIso R e).inverse.obj X).right = X.right

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.mapLeftIso_counitIso_hom_app_left {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] (R : Functor B T) {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] {L₁ L₂ : Functor A T} [P.RespectsIso] [Q.RespectsIso] [W.RespectsIso] (e : L₁ ≅ L₂) (X : MorphismProperty.Comma L₂ R P Q W) : ((mapLeftIso R e).counitIso.hom.app X).left = CategoryStruct.id X.left

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.mapLeftIso_functor_map_left {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] (R : Functor B T) {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] {L₁ L₂ : Functor A T} [P.RespectsIso] [Q.RespectsIso] [W.RespectsIso] (e : L₁ ≅ L₂) {X Y : MorphismProperty.Comma L₁ R P Q W} (f : X ⟶ Y) : ((mapLeftIso R e).functor.map f).left = (Hom.hom f).left

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.mapLeftIso_unitIso_hom_app_left {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] (R : Functor B T) {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] {L₁ L₂ : Functor A T} [P.RespectsIso] [Q.RespectsIso] [W.RespectsIso] (e : L₁ ≅ L₂) (X : MorphismProperty.Comma L₁ R P Q W) : ((mapLeftIso R e).unitIso.hom.app X).left = CategoryStruct.id X.left

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.mapLeftIso_functor_obj_left {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] (R : Functor B T) {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] {L₁ L₂ : Functor A T} [P.RespectsIso] [Q.RespectsIso] [W.RespectsIso] (e : L₁ ≅ L₂) (X : MorphismProperty.Comma L₁ R P Q W) : ((mapLeftIso R e).functor.obj X).left = X.left

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.mapLeftIso_unitIso_hom_app_right {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] (R : Functor B T) {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] {L₁ L₂ : Functor A T} [P.RespectsIso] [Q.RespectsIso] [W.RespectsIso] (e : L₁ ≅ L₂) (X : MorphismProperty.Comma L₁ R P Q W) : ((mapLeftIso R e).unitIso.hom.app X).right = CategoryStruct.id X.right

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.mapLeftIso_inverse_obj_hom {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] (R : Functor B T) {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] {L₁ L₂ : Functor A T} [P.RespectsIso] [Q.RespectsIso] [W.RespectsIso] (e : L₁ ≅ L₂) (X : MorphismProperty.Comma L₂ R P Q W) : ((mapLeftIso R e).inverse.obj X).hom = CategoryStruct.comp (e.hom.app X.left) X.hom

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.mapLeftIso_inverse_map_left {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] (R : Functor B T) {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] {L₁ L₂ : Functor A T} [P.RespectsIso] [Q.RespectsIso] [W.RespectsIso] (e : L₁ ≅ L₂) {X Y : MorphismProperty.Comma L₂ R P Q W} (f : X ⟶ Y) : ((mapLeftIso R e).inverse.map f).left = (Hom.hom f).left

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.mapLeftIso_unitIso_inv_app_left {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] (R : Functor B T) {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] {L₁ L₂ : Functor A T} [P.RespectsIso] [Q.RespectsIso] [W.RespectsIso] (e : L₁ ≅ L₂) (X : MorphismProperty.Comma L₁ R P Q W) : ((mapLeftIso R e).unitIso.inv.app X).left = CategoryStruct.id X.left

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.mapLeftIso_counitIso_inv_app_left {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] (R : Functor B T) {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] {L₁ L₂ : Functor A T} [P.RespectsIso] [Q.RespectsIso] [W.RespectsIso] (e : L₁ ≅ L₂) (X : MorphismProperty.Comma L₂ R P Q W) : ((mapLeftIso R e).counitIso.inv.app X).left = CategoryStruct.id X.left

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.mapLeftIso_unitIso_inv_app_right {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] (R : Functor B T) {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] {L₁ L₂ : Functor A T} [P.RespectsIso] [Q.RespectsIso] [W.RespectsIso] (e : L₁ ≅ L₂) (X : MorphismProperty.Comma L₁ R P Q W) : ((mapLeftIso R e).unitIso.inv.app X).right = CategoryStruct.id X.right

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.mapLeftIso_inverse_map_right {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] (R : Functor B T) {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] {L₁ L₂ : Functor A T} [P.RespectsIso] [Q.RespectsIso] [W.RespectsIso] (e : L₁ ≅ L₂) {X Y : MorphismProperty.Comma L₂ R P Q W} (f : X ⟶ Y) : ((mapLeftIso R e).inverse.map f).right = (Hom.hom f).right

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.mapLeftIso_functor_obj_hom {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] (R : Functor B T) {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] {L₁ L₂ : Functor A T} [P.RespectsIso] [Q.RespectsIso] [W.RespectsIso] (e : L₁ ≅ L₂) (X : MorphismProperty.Comma L₁ R P Q W) : ((mapLeftIso R e).functor.obj X).hom = CategoryStruct.comp (e.inv.app X.left) X.hom

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.mapLeftIso_functor_map_right {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] (R : Functor B T) {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] {L₁ L₂ : Functor A T} [P.RespectsIso] [Q.RespectsIso] [W.RespectsIso] (e : L₁ ≅ L₂) {X Y : MorphismProperty.Comma L₁ R P Q W} (f : X ⟶ Y) : ((mapLeftIso R e).functor.map f).right = (Hom.hom f).right

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.mapLeftIso_functor_obj_right {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] (R : Functor B T) {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] {L₁ L₂ : Functor A T} [P.RespectsIso] [Q.RespectsIso] [W.RespectsIso] (e : L₁ ≅ L₂) (X : MorphismProperty.Comma L₁ R P Q W) : ((mapLeftIso R e).functor.obj X).right = X.right

def CategoryTheory.MorphismProperty.Comma.mapRight {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] (L : Functor A T) {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] {R₁ R₂ : Functor B T} (r : R₁ ⟶ R₂) (hr : ∀ (X : MorphismProperty.Comma L R₁ P Q W), P (CategoryStruct.comp X.hom (r.app X.right))) : Functor (MorphismProperty.Comma L R₁ P Q W) (MorphismProperty.Comma L R₂ P Q W)

A natural transformation R₁ ⟶ R₂ induces a functor P.Comma L R₁ Q W ⥤ P.Comma L R₂ Q W.

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.mapRight_map_left {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] (L : Functor A T) {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] {R₁ R₂ : Functor B T} (r : R₁ ⟶ R₂) (hr : ∀ (X : MorphismProperty.Comma L R₁ P Q W), P (CategoryStruct.comp X.hom (r.app X.right))) {X Y : MorphismProperty.Comma L R₁ P Q W} (f : X ⟶ Y) : ((mapRight L r hr).map f).left = (Hom.hom f).left

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.mapRight_obj_hom {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] (L : Functor A T) {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] {R₁ R₂ : Functor B T} (r : R₁ ⟶ R₂) (hr : ∀ (X : MorphismProperty.Comma L R₁ P Q W), P (CategoryStruct.comp X.hom (r.app X.right))) (X : MorphismProperty.Comma L R₁ P Q W) : ((mapRight L r hr).obj X).hom = CategoryStruct.comp X.hom (r.app X.right)

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.mapRight_obj_right {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] (L : Functor A T) {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] {R₁ R₂ : Functor B T} (r : R₁ ⟶ R₂) (hr : ∀ (X : MorphismProperty.Comma L R₁ P Q W), P (CategoryStruct.comp X.hom (r.app X.right))) (X : MorphismProperty.Comma L R₁ P Q W) : ((mapRight L r hr).obj X).right = X.right

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.mapRight_map_right {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] (L : Functor A T) {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] {R₁ R₂ : Functor B T} (r : R₁ ⟶ R₂) (hr : ∀ (X : MorphismProperty.Comma L R₁ P Q W), P (CategoryStruct.comp X.hom (r.app X.right))) {X Y : MorphismProperty.Comma L R₁ P Q W} (f : X ⟶ Y) : ((mapRight L r hr).map f).right = (Hom.hom f).right

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.mapRight_obj_left {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] (L : Functor A T) {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] {R₁ R₂ : Functor B T} (r : R₁ ⟶ R₂) (hr : ∀ (X : MorphismProperty.Comma L R₁ P Q W), P (CategoryStruct.comp X.hom (r.app X.right))) (X : MorphismProperty.Comma L R₁ P Q W) : ((mapRight L r hr).obj X).left = X.left

def CategoryTheory.MorphismProperty.Comma.mapRightId {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] (L : Functor A T) (R : Functor B T) {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] [Q.RespectsIso] [W.RespectsIso] : mapRight L (CategoryStruct.id R) ⋯ ≅ Functor.id (MorphismProperty.Comma L R P Q W)

The functor P.Comma L R Q W ⥤ P.Comma L R Q W induced by the identity natural transformation on R is naturally isomorphic to the identity functor.

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.mapRightId_inv_app_left {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] (L : Functor A T) (R : Functor B T) {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] [Q.RespectsIso] [W.RespectsIso] (X : MorphismProperty.Comma L R P Q W) : ((mapRightId L R).inv.app X).left = CategoryStruct.id X.left

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.mapRightId_hom_app_right {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] (L : Functor A T) (R : Functor B T) {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] [Q.RespectsIso] [W.RespectsIso] (X : MorphismProperty.Comma L R P Q W) : ((mapRightId L R).hom.app X).right = CategoryStruct.id X.right

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.mapRightId_hom_app_left {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] (L : Functor A T) (R : Functor B T) {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] [Q.RespectsIso] [W.RespectsIso] (X : MorphismProperty.Comma L R P Q W) : ((mapRightId L R).hom.app X).left = CategoryStruct.id X.left

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.mapRightId_inv_app_right {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] (L : Functor A T) (R : Functor B T) {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] [Q.RespectsIso] [W.RespectsIso] (X : MorphismProperty.Comma L R P Q W) : ((mapRightId L R).inv.app X).right = CategoryStruct.id X.right

def CategoryTheory.MorphismProperty.Comma.mapRightComp {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] (L : Functor A T) {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] {R₁ R₂ R₃ : Functor B T} [Q.RespectsIso] [W.RespectsIso] (r : R₁ ⟶ R₂) (r' : R₂ ⟶ R₃) (hr : ∀ (X : MorphismProperty.Comma L R₁ P Q W), P (CategoryStruct.comp X.hom (r.app X.right))) (hr' : ∀ (X : MorphismProperty.Comma L R₂ P Q W), P (CategoryStruct.comp X.hom (r'.app X.right))) (hrr' : ∀ (X : MorphismProperty.Comma L R₁ P Q W), P (CategoryStruct.comp X.hom ((CategoryStruct.comp r r').app X.right))) : mapRight L (CategoryStruct.comp r r') hrr' ≅ (mapRight L r hr).comp (mapRight L r' hr')

The functor P.Comma L R₁ Q W ⥤ P.Comma L R₃ Q W induced by the composition of the natural transformations r : R₁ ⟶ R₂ and r' : R₂ ⟶ R₃ is naturally isomorphic to the composition of the functors induced by these natural transformations.

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.mapRightComp_inv_app_left {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] (L : Functor A T) {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] {R₁ R₂ R₃ : Functor B T} [Q.RespectsIso] [W.RespectsIso] (r : R₁ ⟶ R₂) (r' : R₂ ⟶ R₃) (hr : ∀ (X : MorphismProperty.Comma L R₁ P Q W), P (CategoryStruct.comp X.hom (r.app X.right))) (hr' : ∀ (X : MorphismProperty.Comma L R₂ P Q W), P (CategoryStruct.comp X.hom (r'.app X.right))) (hrr' : ∀ (X : MorphismProperty.Comma L R₁ P Q W), P (CategoryStruct.comp X.hom ((CategoryStruct.comp r r').app X.right))) (X : MorphismProperty.Comma L R₁ P Q W) : ((mapRightComp L r r' hr hr' hrr').inv.app X).left = CategoryStruct.id X.left

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.mapRightComp_inv_app_right {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] (L : Functor A T) {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] {R₁ R₂ R₃ : Functor B T} [Q.RespectsIso] [W.RespectsIso] (r : R₁ ⟶ R₂) (r' : R₂ ⟶ R₃) (hr : ∀ (X : MorphismProperty.Comma L R₁ P Q W), P (CategoryStruct.comp X.hom (r.app X.right))) (hr' : ∀ (X : MorphismProperty.Comma L R₂ P Q W), P (CategoryStruct.comp X.hom (r'.app X.right))) (hrr' : ∀ (X : MorphismProperty.Comma L R₁ P Q W), P (CategoryStruct.comp X.hom ((CategoryStruct.comp r r').app X.right))) (X : MorphismProperty.Comma L R₁ P Q W) : ((mapRightComp L r r' hr hr' hrr').inv.app X).right = CategoryStruct.id X.right

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.mapRightComp_hom_app_left {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] (L : Functor A T) {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] {R₁ R₂ R₃ : Functor B T} [Q.RespectsIso] [W.RespectsIso] (r : R₁ ⟶ R₂) (r' : R₂ ⟶ R₃) (hr : ∀ (X : MorphismProperty.Comma L R₁ P Q W), P (CategoryStruct.comp X.hom (r.app X.right))) (hr' : ∀ (X : MorphismProperty.Comma L R₂ P Q W), P (CategoryStruct.comp X.hom (r'.app X.right))) (hrr' : ∀ (X : MorphismProperty.Comma L R₁ P Q W), P (CategoryStruct.comp X.hom ((CategoryStruct.comp r r').app X.right))) (X : MorphismProperty.Comma L R₁ P Q W) : ((mapRightComp L r r' hr hr' hrr').hom.app X).left = CategoryStruct.id X.left

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.mapRightComp_hom_app_right {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] (L : Functor A T) {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] {R₁ R₂ R₃ : Functor B T} [Q.RespectsIso] [W.RespectsIso] (r : R₁ ⟶ R₂) (r' : R₂ ⟶ R₃) (hr : ∀ (X : MorphismProperty.Comma L R₁ P Q W), P (CategoryStruct.comp X.hom (r.app X.right))) (hr' : ∀ (X : MorphismProperty.Comma L R₂ P Q W), P (CategoryStruct.comp X.hom (r'.app X.right))) (hrr' : ∀ (X : MorphismProperty.Comma L R₁ P Q W), P (CategoryStruct.comp X.hom ((CategoryStruct.comp r r').app X.right))) (X : MorphismProperty.Comma L R₁ P Q W) : ((mapRightComp L r r' hr hr' hrr').hom.app X).right = CategoryStruct.id X.right

def CategoryTheory.MorphismProperty.Comma.mapRightEq {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] (L : Functor A T) {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] {R₁ R₂ : Functor B T} [Q.RespectsIso] [W.RespectsIso] (r r' : R₁ ⟶ R₂) (h : r = r') (hr : ∀ (X : MorphismProperty.Comma L R₁ P Q W), P (CategoryStruct.comp X.hom (r.app X.right))) : mapRight L r hr ≅ mapRight L r' ⋯

Two equal natural transformations R₁ ⟶ R₂ yield naturally isomorphic functors P.Comma L R₁ Q W ⥤ P.Comma L R₂ Q W.

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.mapRightEq_hom_app_left {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] (L : Functor A T) {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] {R₁ R₂ : Functor B T} [Q.RespectsIso] [W.RespectsIso] (r r' : R₁ ⟶ R₂) (h : r = r') (hr : ∀ (X : MorphismProperty.Comma L R₁ P Q W), P (CategoryStruct.comp X.hom (r.app X.right))) (X : MorphismProperty.Comma L R₁ P Q W) : ((mapRightEq L r r' h hr).hom.app X).left = CategoryStruct.id X.left

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.mapRightEq_inv_app_right {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] (L : Functor A T) {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] {R₁ R₂ : Functor B T} [Q.RespectsIso] [W.RespectsIso] (r r' : R₁ ⟶ R₂) (h : r = r') (hr : ∀ (X : MorphismProperty.Comma L R₁ P Q W), P (CategoryStruct.comp X.hom (r.app X.right))) (X : MorphismProperty.Comma L R₁ P Q W) : ((mapRightEq L r r' h hr).inv.app X).right = CategoryStruct.id X.right

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.mapRightEq_hom_app_right {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] (L : Functor A T) {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] {R₁ R₂ : Functor B T} [Q.RespectsIso] [W.RespectsIso] (r r' : R₁ ⟶ R₂) (h : r = r') (hr : ∀ (X : MorphismProperty.Comma L R₁ P Q W), P (CategoryStruct.comp X.hom (r.app X.right))) (X : MorphismProperty.Comma L R₁ P Q W) : ((mapRightEq L r r' h hr).hom.app X).right = CategoryStruct.id X.right

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.mapRightEq_inv_app_left {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] (L : Functor A T) {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] {R₁ R₂ : Functor B T} [Q.RespectsIso] [W.RespectsIso] (r r' : R₁ ⟶ R₂) (h : r = r') (hr : ∀ (X : MorphismProperty.Comma L R₁ P Q W), P (CategoryStruct.comp X.hom (r.app X.right))) (X : MorphismProperty.Comma L R₁ P Q W) : ((mapRightEq L r r' h hr).inv.app X).left = CategoryStruct.id X.left

def CategoryTheory.MorphismProperty.Comma.mapRightIso {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] (L : Functor A T) {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] {R₁ R₂ : Functor B T} [P.RespectsIso] [Q.RespectsIso] [W.RespectsIso] (e : R₁ ≅ R₂) : MorphismProperty.Comma L R₁ P Q W ≌ MorphismProperty.Comma L R₂ P Q W

A natural isomorphism R₁ ≅ R₂ induces an equivalence of categories P.Comma L R₁ Q W ≌ P.Comma L R₂ Q W.

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.mapRightIso_functor_map_right {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] (L : Functor A T) {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] {R₁ R₂ : Functor B T} [P.RespectsIso] [Q.RespectsIso] [W.RespectsIso] (e : R₁ ≅ R₂) {X Y : MorphismProperty.Comma L R₁ P Q W} (f : X ⟶ Y) : ((mapRightIso L e).functor.map f).right = (Hom.hom f).right

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.mapRightIso_functor_map_left {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] (L : Functor A T) {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] {R₁ R₂ : Functor B T} [P.RespectsIso] [Q.RespectsIso] [W.RespectsIso] (e : R₁ ≅ R₂) {X Y : MorphismProperty.Comma L R₁ P Q W} (f : X ⟶ Y) : ((mapRightIso L e).functor.map f).left = (Hom.hom f).left

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.mapRightIso_unitIso_hom_app_left {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] (L : Functor A T) {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] {R₁ R₂ : Functor B T} [P.RespectsIso] [Q.RespectsIso] [W.RespectsIso] (e : R₁ ≅ R₂) (X : MorphismProperty.Comma L R₁ P Q W) : ((mapRightIso L e).unitIso.hom.app X).left = CategoryStruct.id X.left

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.mapRightIso_counitIso_inv_app_right {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] (L : Functor A T) {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] {R₁ R₂ : Functor B T} [P.RespectsIso] [Q.RespectsIso] [W.RespectsIso] (e : R₁ ≅ R₂) (X : MorphismProperty.Comma L R₂ P Q W) : ((mapRightIso L e).counitIso.inv.app X).right = CategoryStruct.id X.right

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.mapRightIso_inverse_obj_right {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] (L : Functor A T) {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] {R₁ R₂ : Functor B T} [P.RespectsIso] [Q.RespectsIso] [W.RespectsIso] (e : R₁ ≅ R₂) (X : MorphismProperty.Comma L R₂ P Q W) : ((mapRightIso L e).inverse.obj X).right = X.right

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.mapRightIso_unitIso_hom_app_right {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] (L : Functor A T) {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] {R₁ R₂ : Functor B T} [P.RespectsIso] [Q.RespectsIso] [W.RespectsIso] (e : R₁ ≅ R₂) (X : MorphismProperty.Comma L R₁ P Q W) : ((mapRightIso L e).unitIso.hom.app X).right = CategoryStruct.id X.right

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.mapRightIso_functor_obj_hom {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] (L : Functor A T) {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] {R₁ R₂ : Functor B T} [P.RespectsIso] [Q.RespectsIso] [W.RespectsIso] (e : R₁ ≅ R₂) (X : MorphismProperty.Comma L R₁ P Q W) : ((mapRightIso L e).functor.obj X).hom = CategoryStruct.comp X.hom (e.hom.app X.right)

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.mapRightIso_inverse_obj_hom {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] (L : Functor A T) {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] {R₁ R₂ : Functor B T} [P.RespectsIso] [Q.RespectsIso] [W.RespectsIso] (e : R₁ ≅ R₂) (X : MorphismProperty.Comma L R₂ P Q W) : ((mapRightIso L e).inverse.obj X).hom = CategoryStruct.comp X.hom (e.inv.app X.right)

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.mapRightIso_counitIso_inv_app_left {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] (L : Functor A T) {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] {R₁ R₂ : Functor B T} [P.RespectsIso] [Q.RespectsIso] [W.RespectsIso] (e : R₁ ≅ R₂) (X : MorphismProperty.Comma L R₂ P Q W) : ((mapRightIso L e).counitIso.inv.app X).left = CategoryStruct.id X.left

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.mapRightIso_counitIso_hom_app_left {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] (L : Functor A T) {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] {R₁ R₂ : Functor B T} [P.RespectsIso] [Q.RespectsIso] [W.RespectsIso] (e : R₁ ≅ R₂) (X : MorphismProperty.Comma L R₂ P Q W) : ((mapRightIso L e).counitIso.hom.app X).left = CategoryStruct.id X.left

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.mapRightIso_functor_obj_left {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] (L : Functor A T) {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] {R₁ R₂ : Functor B T} [P.RespectsIso] [Q.RespectsIso] [W.RespectsIso] (e : R₁ ≅ R₂) (X : MorphismProperty.Comma L R₁ P Q W) : ((mapRightIso L e).functor.obj X).left = X.left

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.mapRightIso_functor_obj_right {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] (L : Functor A T) {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] {R₁ R₂ : Functor B T} [P.RespectsIso] [Q.RespectsIso] [W.RespectsIso] (e : R₁ ≅ R₂) (X : MorphismProperty.Comma L R₁ P Q W) : ((mapRightIso L e).functor.obj X).right = X.right

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.mapRightIso_counitIso_hom_app_right {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] (L : Functor A T) {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] {R₁ R₂ : Functor B T} [P.RespectsIso] [Q.RespectsIso] [W.RespectsIso] (e : R₁ ≅ R₂) (X : MorphismProperty.Comma L R₂ P Q W) : ((mapRightIso L e).counitIso.hom.app X).right = CategoryStruct.id X.right

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.mapRightIso_inverse_obj_left {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] (L : Functor A T) {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] {R₁ R₂ : Functor B T} [P.RespectsIso] [Q.RespectsIso] [W.RespectsIso] (e : R₁ ≅ R₂) (X : MorphismProperty.Comma L R₂ P Q W) : ((mapRightIso L e).inverse.obj X).left = X.left

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.mapRightIso_inverse_map_right {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] (L : Functor A T) {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] {R₁ R₂ : Functor B T} [P.RespectsIso] [Q.RespectsIso] [W.RespectsIso] (e : R₁ ≅ R₂) {X Y : MorphismProperty.Comma L R₂ P Q W} (f : X ⟶ Y) : ((mapRightIso L e).inverse.map f).right = (Hom.hom f).right

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.mapRightIso_unitIso_inv_app_right {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] (L : Functor A T) {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] {R₁ R₂ : Functor B T} [P.RespectsIso] [Q.RespectsIso] [W.RespectsIso] (e : R₁ ≅ R₂) (X : MorphismProperty.Comma L R₁ P Q W) : ((mapRightIso L e).unitIso.inv.app X).right = CategoryStruct.id X.right

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.mapRightIso_unitIso_inv_app_left {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] (L : Functor A T) {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] {R₁ R₂ : Functor B T} [P.RespectsIso] [Q.RespectsIso] [W.RespectsIso] (e : R₁ ≅ R₂) (X : MorphismProperty.Comma L R₁ P Q W) : ((mapRightIso L e).unitIso.inv.app X).left = CategoryStruct.id X.left

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.mapRightIso_inverse_map_left {A : Type u_1} [Category.{v_1, u_1} A] {B : Type u_2} [Category.{v_2, u_2} B] {T : Type u_3} [Category.{v_3, u_3} T] (L : Functor A T) {P : MorphismProperty T} {Q : MorphismProperty A} {W : MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] {R₁ R₂ : Functor B T} [P.RespectsIso] [Q.RespectsIso] [W.RespectsIso] (e : R₁ ≅ R₂) {X Y : MorphismProperty.Comma L R₂ P Q W} (f : X ⟶ Y) : ((mapRightIso L e).inverse.map f).left = (Hom.hom f).left

@[reducible, inline]

abbrev CategoryTheory.MorphismProperty.Over {T : Type u_1} [Category.{v_1, u_1} T] (P Q : MorphismProperty T) (X : T) : Type (max v_1 u_1)

Given a morphism property P on a category C and an object X : C, this is the subcategory of Over X defined by P where morphisms satisfy Q.

@[reducible, inline]

abbrev CategoryTheory.MorphismProperty.Over.forget {T : Type u_1} [Category.{v_1, u_1} T] (P Q : MorphismProperty T) (X : T) [Q.IsMultiplicative] : Functor (P.Over Q X) (Over X)

The forgetful functor from the full subcategory of Over X defined by P to Over X.

instance CategoryTheory.MorphismProperty.instFaithfulOverTopOverForget {T : Type u_1} [Category.{v_1, u_1} T] (P : MorphismProperty T) (X : T) : (Over.forget P ⊤ X).Faithful

instance CategoryTheory.MorphismProperty.instFullOverTopOverForget {T : Type u_1} [Category.{v_1, u_1} T] (P : MorphismProperty T) (X : T) : (Over.forget P ⊤ X).Full

theorem CategoryTheory.MorphismProperty.Over.forget_comp_forget_map {T : Type u_1} [Category.{v_1, u_1} T] (P Q : MorphismProperty T) (X : T) [Q.IsMultiplicative] {A B : P.Over Q X} (f : A ⟶ B) : ((Over.forget P Q X).comp (CategoryTheory.Over.forget X)).map f = f.left

Occasionally useful for rewriting in the backwards direction.

def CategoryTheory.MorphismProperty.Over.Hom.mk {T : Type u_1} [Category.{v_1, u_1} T] {P Q : MorphismProperty T} {X : T} [Q.IsMultiplicative] {A B : P.Over Q X} (f : A.toComma ⟶ B.toComma) (hf : Q f.left) : A ⟶ B

Construct a morphism in P.Over Q X from a morphism in Over.X.

@[simp]

theorem CategoryTheory.MorphismProperty.Over.Hom.mk_hom {T : Type u_1} [Category.{v_1, u_1} T] {P Q : MorphismProperty T} {X : T} [Q.IsMultiplicative] {A B : P.Over Q X} (f : A.toComma ⟶ B.toComma) (hf : Q f.left) : Comma.Hom.hom (mk f hf) = f

def CategoryTheory.MorphismProperty.Over.mk {T : Type u_1} [Category.{v_1, u_1} T] {P : MorphismProperty T} (Q : MorphismProperty T) {X A : T} (f : A ⟶ X) (hf : P f) : P.Over Q X

Make an object of P.Over Q X from a morphism f : A ⟶ X and a proof of P f.

@[simp]

theorem CategoryTheory.MorphismProperty.Over.mk_hom {T : Type u_1} [Category.{v_1, u_1} T] {P : MorphismProperty T} (Q : MorphismProperty T) {X A : T} (f : A ⟶ X) (hf : P f) : (Over.mk Q f hf).hom = f

@[simp]

theorem CategoryTheory.MorphismProperty.Over.mk_left {T : Type u_1} [Category.{v_1, u_1} T] {P : MorphismProperty T} (Q : MorphismProperty T) {X A : T} (f : A ⟶ X) (hf : P f) : (Over.mk Q f hf).left = A

def CategoryTheory.MorphismProperty.Over.homMk {T : Type u_1} [Category.{v_1, u_1} T] {P Q : MorphismProperty T} {X : T} [Q.IsMultiplicative] {A B : P.Over Q X} (f : A.left ⟶ B.left) (w : CategoryStruct.comp f B.hom = A.hom := by cat_disch) (hf : Q f := by trivial) : A ⟶ B

Make a morphism in P.Over Q X from a morphism in T with compatibilities.

@[simp]

theorem CategoryTheory.MorphismProperty.Over.homMk_hom {T : Type u_1} [Category.{v_1, u_1} T] {P Q : MorphismProperty T} {X : T} [Q.IsMultiplicative] {A B : P.Over Q X} (f : A.left ⟶ B.left) (w : CategoryStruct.comp f B.hom = A.hom := by cat_disch) (hf : Q f := by trivial) : Comma.Hom.hom (Over.homMk f w hf) = CategoryTheory.Over.homMk f w

def CategoryTheory.MorphismProperty.Over.isoMk {T : Type u_1} [Category.{v_1, u_1} T] {P Q : MorphismProperty T} {X : T} [Q.IsMultiplicative] [Q.RespectsIso] {A B : P.Over Q X} (f : A.left ≅ B.left) (w : CategoryStruct.comp f.hom B.hom = A.hom := by cat_disch) : A ≅ B

Make an isomorphism in P.Over Q X from an isomorphism in T with compatibilities.

@[simp]

theorem CategoryTheory.MorphismProperty.Over.isoMk_hom_left {T : Type u_1} [Category.{v_1, u_1} T] {P Q : MorphismProperty T} {X : T} [Q.IsMultiplicative] [Q.RespectsIso] {A B : P.Over Q X} (f : A.left ≅ B.left) (w : CategoryStruct.comp f.hom B.hom = A.hom := by cat_disch) : (Over.isoMk f w).hom.left = f.hom

@[simp]

theorem CategoryTheory.MorphismProperty.Over.isoMk_inv_left {T : Type u_1} [Category.{v_1, u_1} T] {P Q : MorphismProperty T} {X : T} [Q.IsMultiplicative] [Q.RespectsIso] {A B : P.Over Q X} (f : A.left ≅ B.left) (w : CategoryStruct.comp f.hom B.hom = A.hom := by cat_disch) : (Over.isoMk f w).inv.left = f.inv

theorem CategoryTheory.MorphismProperty.Over.Hom.ext {T : Type u_1} [Category.{v_1, u_1} T] {P Q : MorphismProperty T} {X : T} [Q.IsMultiplicative] {A B : P.Over Q X} {f g : A ⟶ B} (h : f.left = g.left) : f = g

theorem CategoryTheory.MorphismProperty.Over.Hom.ext_iff {T : Type u_1} [Category.{v_1, u_1} T] {P Q : MorphismProperty T} {X : T} [Q.IsMultiplicative] {A B : P.Over Q X} {f g : A ⟶ B} : f = g ↔ f.left = g.left

theorem CategoryTheory.MorphismProperty.Over.w {T : Type u_1} [Category.{v_1, u_1} T] {P Q : MorphismProperty T} {X : T} [Q.IsMultiplicative] {A B : P.Over Q X} (f : A ⟶ B) : CategoryStruct.comp f.left B.hom = A.hom

theorem CategoryTheory.MorphismProperty.Over.w_assoc {T : Type u_1} [Category.{v_1, u_1} T] {P Q : MorphismProperty T} {X : T} [Q.IsMultiplicative] {A B : P.Over Q X} (f : A ⟶ B) {Z : T} (h : (Functor.fromPUnit X).obj B.right ⟶ Z) : CategoryStruct.comp f.left (CategoryStruct.comp B.hom h) = CategoryStruct.comp A.hom h

@[reducible, inline]

abbrev CategoryTheory.MorphismProperty.Over.changeProp {T : Type u_1} [Category.{v_1, u_1} T] {P Q : MorphismProperty T} (X : T) [Q.IsMultiplicative] {P' Q' : MorphismProperty T} [Q'.IsMultiplicative] (hPP' : P ≤ P') (hQQ' : Q ≤ Q') : Functor (P.Over Q X) (P'.Over Q' X)

The natural inclusion induced by implications of morphism properties.

@[simp]

theorem CategoryTheory.MorphismProperty.Over.changeProp_obj_left {T : Type u_1} [Category.{v_1, u_1} T] {P Q : MorphismProperty T} {X : T} [Q.IsMultiplicative] {P' Q' : MorphismProperty T} [Q'.IsMultiplicative] (hPP' : P ≤ P') (hQQ' : Q ≤ Q') (Y : P.Over Q X) : ((changeProp X hPP' hQQ').obj Y).left = Y.left

@[simp]

theorem CategoryTheory.MorphismProperty.Over.changeProp_obj_hom {T : Type u_1} [Category.{v_1, u_1} T] {P Q : MorphismProperty T} {X : T} [Q.IsMultiplicative] {P' Q' : MorphismProperty T} [Q'.IsMultiplicative] (hPP' : P ≤ P') (hQQ' : Q ≤ Q') (Y : P.Over Q X) : ((changeProp X hPP' hQQ').obj Y).hom = Y.hom

@[reducible, inline]

abbrev CategoryTheory.MorphismProperty.Under {T : Type u_1} [Category.{v_1, u_1} T] (P Q : MorphismProperty T) (X : T) : Type (max v_1 u_1)

Given a morphism property P on a category C and an object X : C, this is the subcategory of Under X defined by P where morphisms satisfy Q.

@[reducible, inline]

abbrev CategoryTheory.MorphismProperty.Under.forget {T : Type u_1} [Category.{v_1, u_1} T] (P Q : MorphismProperty T) (X : T) [Q.IsMultiplicative] : Functor (P.Under Q X) (Under X)

The forgetful functor from the full subcategory of Under X defined by P to Under X.

instance CategoryTheory.MorphismProperty.instFaithfulUnderTopUnderForget {T : Type u_1} [Category.{v_1, u_1} T] (P : MorphismProperty T) (X : T) : (Under.forget P ⊤ X).Faithful

instance CategoryTheory.MorphismProperty.instFullUnderTopUnderForget {T : Type u_1} [Category.{v_1, u_1} T] (P : MorphismProperty T) (X : T) : (Under.forget P ⊤ X).Full

theorem CategoryTheory.MorphismProperty.Under.forget_comp_forget_map {T : Type u_1} [Category.{v_1, u_1} T] (P Q : MorphismProperty T) (X : T) [Q.IsMultiplicative] {A B : P.Under Q X} (f : A ⟶ B) : ((Under.forget P Q X).comp (CategoryTheory.Under.forget X)).map f = f.right

Occasionally useful for rewriting in the backwards direction.

def CategoryTheory.MorphismProperty.Under.Hom.mk {T : Type u_1} [Category.{v_1, u_1} T] {P Q : MorphismProperty T} {X : T} [Q.IsMultiplicative] {A B : P.Under Q X} (f : A.toComma ⟶ B.toComma) (hf : Q f.right) : A ⟶ B

Construct a morphism in P.Under Q X from a morphism in Under.X.

@[simp]

theorem CategoryTheory.MorphismProperty.Under.Hom.mk_hom {T : Type u_1} [Category.{v_1, u_1} T] {P Q : MorphismProperty T} {X : T} [Q.IsMultiplicative] {A B : P.Under Q X} (f : A.toComma ⟶ B.toComma) (hf : Q f.right) : Comma.Hom.hom (mk f hf) = f

def CategoryTheory.MorphismProperty.Under.mk {T : Type u_1} [Category.{v_1, u_1} T] {P : MorphismProperty T} (Q : MorphismProperty T) {X A : T} (f : X ⟶ A) (hf : P f) : P.Under Q X

Make an object of P.Under Q X from a morphism f : A ⟶ X and a proof of P f.

@[simp]

theorem CategoryTheory.MorphismProperty.Under.mk_hom {T : Type u_1} [Category.{v_1, u_1} T] {P : MorphismProperty T} (Q : MorphismProperty T) {X A : T} (f : X ⟶ A) (hf : P f) : (Under.mk Q f hf).hom = f

@[simp]

theorem CategoryTheory.MorphismProperty.Under.mk_left {T : Type u_1} [Category.{v_1, u_1} T] {P : MorphismProperty T} (Q : MorphismProperty T) {X A : T} (f : X ⟶ A) (hf : P f) : (Under.mk Q f hf).left = { as := PUnit.unit }

def CategoryTheory.MorphismProperty.Under.homMk {T : Type u_1} [Category.{v_1, u_1} T] {P Q : MorphismProperty T} {X : T} [Q.IsMultiplicative] {A B : P.Under Q X} (f : A.right ⟶ B.right) (w : CategoryStruct.comp A.hom f = B.hom := by cat_disch) (hf : Q f := by trivial) : A ⟶ B

Make a morphism in P.Under Q X from a morphism in T with compatibilities.

@[simp]

theorem CategoryTheory.MorphismProperty.Under.homMk_hom {T : Type u_1} [Category.{v_1, u_1} T] {P Q : MorphismProperty T} {X : T} [Q.IsMultiplicative] {A B : P.Under Q X} (f : A.right ⟶ B.right) (w : CategoryStruct.comp A.hom f = B.hom := by cat_disch) (hf : Q f := by trivial) : Comma.Hom.hom (Under.homMk f w hf) = CategoryTheory.Under.homMk f w

def CategoryTheory.MorphismProperty.Under.isoMk {T : Type u_1} [Category.{v_1, u_1} T] {P Q : MorphismProperty T} {X : T} [Q.IsMultiplicative] [Q.RespectsIso] {A B : P.Under Q X} (f : A.right ≅ B.right) (w : CategoryStruct.comp A.hom f.hom = B.hom := by cat_disch) : A ≅ B

Make an isomorphism in P.Under Q X from an isomorphism in T with compatibilities.

@[simp]

theorem CategoryTheory.MorphismProperty.Under.isoMk_inv_right {T : Type u_1} [Category.{v_1, u_1} T] {P Q : MorphismProperty T} {X : T} [Q.IsMultiplicative] [Q.RespectsIso] {A B : P.Under Q X} (f : A.right ≅ B.right) (w : CategoryStruct.comp A.hom f.hom = B.hom := by cat_disch) : (Under.isoMk f w).inv.right = f.inv

@[simp]

theorem CategoryTheory.MorphismProperty.Under.isoMk_hom_right {T : Type u_1} [Category.{v_1, u_1} T] {P Q : MorphismProperty T} {X : T} [Q.IsMultiplicative] [Q.RespectsIso] {A B : P.Under Q X} (f : A.right ≅ B.right) (w : CategoryStruct.comp A.hom f.hom = B.hom := by cat_disch) : (Under.isoMk f w).hom.right = f.hom

theorem CategoryTheory.MorphismProperty.Under.Hom.ext {T : Type u_1} [Category.{v_1, u_1} T] {P Q : MorphismProperty T} {X : T} [Q.IsMultiplicative] {A B : P.Under Q X} {f g : A ⟶ B} (h : f.right = g.right) : f = g

theorem CategoryTheory.MorphismProperty.Under.Hom.ext_iff {T : Type u_1} [Category.{v_1, u_1} T] {P Q : MorphismProperty T} {X : T} [Q.IsMultiplicative] {A B : P.Under Q X} {f g : A ⟶ B} : f = g ↔ f.right = g.right

theorem CategoryTheory.MorphismProperty.Under.w {T : Type u_1} [Category.{v_1, u_1} T] {P Q : MorphismProperty T} {X : T} [Q.IsMultiplicative] {A B : P.Under Q X} (f : A ⟶ B) : CategoryStruct.comp A.hom f.right = B.hom

theorem CategoryTheory.MorphismProperty.Under.w_assoc {T : Type u_1} [Category.{v_1, u_1} T] {P Q : MorphismProperty T} {X : T} [Q.IsMultiplicative] {A B : P.Under Q X} (f : A ⟶ B) {Z : T} (h : B.right ⟶ Z) : CategoryStruct.comp A.hom (CategoryStruct.comp f.right h) = CategoryStruct.comp B.hom h

@[reducible, inline]

abbrev CategoryTheory.MorphismProperty.CostructuredArrow {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] (P : MorphismProperty D) (Q : MorphismProperty C) (F : Functor C D) (X : D) : Type (max u_1 u_4)

Given a morphism property P on a category C and an object X : C, this is the subcategory of CostructuredArrow F X defined by P where morphisms satisfy Q.

def CategoryTheory.MorphismProperty.CostructuredArrow.mk {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] {P : MorphismProperty D} (Q : MorphismProperty C) {F : Functor C D} {X : D} {A : C} (f : F.obj A ⟶ X) (hf : P f) : P.CostructuredArrow Q F X

Construct an object of P.CostructuredArrow Q F X from a morphism F.obj A ⟶ X.

@[simp]

theorem CategoryTheory.MorphismProperty.CostructuredArrow.mk_hom {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] {P : MorphismProperty D} (Q : MorphismProperty C) {F : Functor C D} {X : D} {A : C} (f : F.obj A ⟶ X) (hf : P f) : (CostructuredArrow.mk Q f hf).hom = f

@[simp]

theorem CategoryTheory.MorphismProperty.CostructuredArrow.mk_left {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] {P : MorphismProperty D} (Q : MorphismProperty C) {F : Functor C D} {X : D} {A : C} (f : F.obj A ⟶ X) (hf : P f) : (CostructuredArrow.mk Q f hf).left = A

def CategoryTheory.MorphismProperty.CostructuredArrow.homMk {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] {P : MorphismProperty D} {Q : MorphismProperty C} [Q.IsMultiplicative] {F : Functor C D} {X : D} {A B : P.CostructuredArrow Q F X} (f : A.left ⟶ B.left) (hf : Q f) (w : CategoryStruct.comp (F.map f) B.hom = A.hom := by cat_disch) : A ⟶ B

Construct a morphism in P.CostructuredArrow Q F X by giving a morphism on the underlying objects of C.

@[simp]

theorem CategoryTheory.MorphismProperty.CostructuredArrow.homMk_left {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] {P : MorphismProperty D} {Q : MorphismProperty C} [Q.IsMultiplicative] {F : Functor C D} {X : D} {A B : P.CostructuredArrow Q F X} (f : A.left ⟶ B.left) (hf : Q f) (w : CategoryStruct.comp (F.map f) B.hom = A.hom := by cat_disch) : (homMk f hf w).left = f

theorem CategoryTheory.MorphismProperty.CostructuredArrow.Hom.ext {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] {P : MorphismProperty D} {Q : MorphismProperty C} [Q.IsMultiplicative] {F : Functor C D} {X : D} {A B : P.CostructuredArrow Q F X} {f g : A ⟶ B} (h : f.left = g.left) : f = g

theorem CategoryTheory.MorphismProperty.CostructuredArrow.Hom.ext_iff {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] {P : MorphismProperty D} {Q : MorphismProperty C} [Q.IsMultiplicative] {F : Functor C D} {X : D} {A B : P.CostructuredArrow Q F X} {f g : A ⟶ B} : f = g ↔ f.left = g.left

@[reducible, inline]

abbrev CategoryTheory.MorphismProperty.CostructuredArrow.forget {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] (P : MorphismProperty D) (Q : MorphismProperty C) [Q.IsMultiplicative] (F : Functor C D) (X : D) : Functor (P.CostructuredArrow Q F X) (CostructuredArrow F X)

The forgetful functor from the subcategory P.CostructuredArrow Q F X.

def CategoryTheory.MorphismProperty.CostructuredArrow.toOver {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] (P : MorphismProperty D) (F : Functor C D) (X : D) : Functor (P.CostructuredArrow ⊤ F X) (P.Over ⊤ X)

Reinterpreting an F-costructured arrow F.obj A ⟶ X as an arrow over X.

@[simp]

theorem CategoryTheory.MorphismProperty.CostructuredArrow.toOver_obj {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] (P : MorphismProperty D) (F : Functor C D) (X : D) (A : P.CostructuredArrow ⊤ F X) : (CostructuredArrow.toOver P F X).obj A = Over.mk ⊤ A.hom ⋯

@[simp]

theorem CategoryTheory.MorphismProperty.CostructuredArrow.toOver_map {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] (P : MorphismProperty D) (F : Functor C D) (X : D) {X✝ Y✝ : P.CostructuredArrow ⊤ F X} (f : X✝ ⟶ Y✝) : (CostructuredArrow.toOver P F X).map f = Over.homMk (F.map f.left) ⋯ ⋯

instance CategoryTheory.MorphismProperty.instFaithfulCostructuredArrowTopOverToOver {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] (P : MorphismProperty D) (F : Functor C D) (X : D) [F.Faithful] : (CostructuredArrow.toOver P F X).Faithful

instance CategoryTheory.MorphismProperty.instFullCostructuredArrowTopOverToOver {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] (P : MorphismProperty D) (F : Functor C D) (X : D) [F.Full] : (CostructuredArrow.toOver P F X).Full

instance CategoryTheory.MorphismProperty.HasFactorization.over {C : Type u_3} [Category.{v_1, u_3} C] (W₁ W₂ : MorphismProperty C) [W₁.HasFactorization W₂] (S : C) : W₁.over.HasFactorization W₂.over