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, AandBrespectively, we define the subcategoryP.Comma L R Q Wof `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.{u_5, u_1} A] {T : Type u_3} [Category.{u_4, 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.{u_4, u_3} T] (P : MorphismProperty T) [P.RespectsIso] {X : T} {f g : Over X} (e : f ≅ g) : P f.hom ↔ P g.hom

structure CategoryTheory.MorphismProperty.Comma {A : Type u_1} [Category.{u_4, u_1} A] {B : Type u_2} [Category.{u_5, u_2} B] {T : Type u_3} [Category.{u_6, 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) u_6)

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.{u_4, u_1} A} {B : Type u_2} {inst✝¹ : Category.{u_5, u_2} B} {T : Type u_3} {inst✝² : Category.{u_6, 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 : HEq x.hom y.hom) : x = y

structure CategoryTheory.MorphismProperty.Comma.Hom {A : Type u_1} [Category.{u_4, u_1} A] {B : Type u_2} [Category.{u_5, u_2} B] {T : Type u_3} [Category.{u_6, 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 u_4 u_5)

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.{u_4, u_1} A} {B : Type u_2} {inst✝¹ : Category.{u_5, u_2} B} {T : Type u_3} {inst✝² : Category.{u_6, 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

@[reducible, inline]

abbrev CategoryTheory.MorphismProperty.Comma.Hom.hom {A : Type u_1} [Category.{u_4, u_1} A] {B : Type u_2} [Category.{u_5, u_2} B] {T : Type u_3} [Category.{u_6, 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.

Equations

• f.hom = f.toCommaMorphism

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.Hom.hom_mk {A : Type u_1} [Category.{u_4, u_1} A] {B : Type u_2} [Category.{u_5, u_2} B] {T : Type u_3} [Category.{u_6, 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.{u_4, u_1} A] {B : Type u_2} [Category.{u_5, u_2} B] {T : Type u_3} [Category.{u_6, 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.{u_4, u_1} A] {B : Type u_2} [Category.{u_5, u_2} B] {T : Type u_3} [Category.{u_6, 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.{u_4, u_1} A] {B : Type u_2} [Category.{u_5, u_2} B] {T : Type u_3} [Category.{u_6, 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]

Equations

• CategoryTheory.MorphismProperty.Comma.Hom.Simps.hom f = f.hom

def CategoryTheory.MorphismProperty.Comma.id {A : Type u_1} [Category.{u_4, u_1} A] {B : Type u_2} [Category.{u_5, u_2} B] {T : Type u_3} [Category.{u_6, 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.

Equations

• X.id = { left := CategoryTheory.CategoryStruct.id X.left, right := CategoryTheory.CategoryStruct.id X.right, w := ⋯, prop_hom_left := ⋯, prop_hom_right := ⋯ }

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.id_right {A : Type u_1} [Category.{u_4, u_1} A] {B : Type u_2} [Category.{u_5, u_2} B] {T : Type u_3} [Category.{u_6, 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.{u_4, u_1} A] {B : Type u_2} [Category.{u_5, u_2} B] {T : Type u_3} [Category.{u_6, 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.{u_4, u_1} A] {B : Type u_2} [Category.{u_5, u_2} B] {T : Type u_3} [Category.{u_6, 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.

Equations

• f.comp g = { left := CategoryTheory.CategoryStruct.comp f.left g.left, right := CategoryTheory.CategoryStruct.comp f.right g.right, w := ⋯, prop_hom_left := ⋯, prop_hom_right := ⋯ }

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.Hom.comp_left {A : Type u_1} [Category.{u_4, u_1} A] {B : Type u_2} [Category.{u_5, u_2} B] {T : Type u_3} [Category.{u_6, 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.{u_4, u_1} A] {B : Type u_2} [Category.{u_5, u_2} B] {T : Type u_3} [Category.{u_6, 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

instance CategoryTheory.MorphismProperty.Comma.instCategory {A : Type u_1} [Category.{u_4, u_1} A] {B : Type u_2} [Category.{u_5, u_2} B] {T : Type u_3} [Category.{u_6, 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 u_4 u_5, max (max u_6 u_2) u_1} (MorphismProperty.Comma L R P Q W)

Equations

• CategoryTheory.MorphismProperty.Comma.instCategory L R P Q W = CategoryTheory.Category.mk ⋯ ⋯ ⋯

theorem CategoryTheory.MorphismProperty.Comma.toCommaMorphism_eq_hom {A : Type u_1} [Category.{u_4, u_1} A] {B : Type u_2} [Category.{u_5, u_2} B] {T : Type u_3} [Category.{u_6, 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.{u_4, u_1} A] {B : Type u_2} [Category.{u_5, u_2} B] {T : Type u_3} [Category.{u_6, 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.

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.id_hom {A : Type u_1} [Category.{u_4, u_1} A] {B : Type u_2} [Category.{u_5, u_2} B] {T : Type u_3} [Category.{u_6, 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.{u_4, u_1} A] {B : Type u_2} [Category.{u_5, u_2} B] {T : Type u_3} [Category.{u_6, 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.{u_4, u_1} A] {B : Type u_2} [Category.{u_5, u_2} B] {T : Type u_3} [Category.{u_6, 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.{u_4, u_1} A] {B : Type u_2} [Category.{u_5, u_2} B] {T : Type u_3} [Category.{u_6, 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.{u_4, u_1} A] {B : Type u_2} [Category.{u_5, u_2} B] {T : Type u_3} [Category.{u_6, 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.{u_4, u_1} A] {B : Type u_2} [Category.{u_5, u_2} B] {T : Type u_3} [Category.{u_6, 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.{u_4, u_1} A] {B : Type u_2} [Category.{u_5, u_2} B] {T : Type u_3} [Category.{u_6, 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.

Equations

• CategoryTheory.MorphismProperty.Comma.homFromCommaOfIsIso i = { toCommaMorphism := i, prop_hom_left := ⋯, prop_hom_right := ⋯ }

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.homFromCommaOfIsIso_hom {A : Type u_1} [Category.{u_4, u_1} A] {B : Type u_2} [Category.{u_5, u_2} B] {T : Type u_3} [Category.{u_6, 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.{u_4, u_1} A] {B : Type u_2} [Category.{u_5, u_2} B] {T : Type u_3} [Category.{u_6, 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.{u_4, u_1} A] {B : Type u_2} [Category.{u_5, u_2} B] {T : Type u_3} [Category.{u_6, 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.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.isoFromComma_inv {A : Type u_1} [Category.{u_4, u_1} A] {B : Type u_2} [Category.{u_5, u_2} B] {T : Type u_3} [Category.{u_6, 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.{u_4, u_1} A] {B : Type u_2} [Category.{u_5, u_2} B] {T : Type u_3} [Category.{u_6, 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.{u_4, u_1} A] {B : Type u_2} [Category.{u_5, u_2} B] {T : Type u_3} [Category.{u_6, 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 aesop_cat) : 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.

Equations

• CategoryTheory.MorphismProperty.Comma.isoMk l r h = CategoryTheory.MorphismProperty.Comma.isoFromComma (CategoryTheory.Comma.isoMk l r h)

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.isoMk_inv_left {A : Type u_1} [Category.{u_4, u_1} A] {B : Type u_2} [Category.{u_5, u_2} B] {T : Type u_3} [Category.{u_6, 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 aesop_cat) : (isoMk l r h).inv.left = l.inv

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.isoMk_inv_right {A : Type u_1} [Category.{u_4, u_1} A] {B : Type u_2} [Category.{u_5, u_2} B] {T : Type u_3} [Category.{u_6, 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 aesop_cat) : (isoMk l r h).inv.right = r.inv

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.isoMk_hom_right {A : Type u_1} [Category.{u_4, u_1} A] {B : Type u_2} [Category.{u_5, u_2} B] {T : Type u_3} [Category.{u_6, 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 aesop_cat) : (isoMk l r h).hom.right = r.hom

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.isoMk_hom_left {A : Type u_1} [Category.{u_4, u_1} A] {B : Type u_2} [Category.{u_5, u_2} B] {T : Type u_3} [Category.{u_6, 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 aesop_cat) : (isoMk l r h).hom.left = l.hom

def CategoryTheory.MorphismProperty.Comma.forget {A : Type u_1} [Category.{u_4, u_1} A] {B : Type u_2} [Category.{u_5, u_2} B] {T : Type u_3} [Category.{u_6, 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.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.forget_obj {A : Type u_1} [Category.{u_4, u_1} A] {B : Type u_2} [Category.{u_5, u_2} B] {T : Type u_3} [Category.{u_6, 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.{u_4, u_1} A] {B : Type u_2} [Category.{u_5, u_2} B] {T : Type u_3} [Category.{u_6, 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.{u_4, u_1} A] {B : Type u_2} [Category.{u_5, u_2} B] {T : Type u_3} [Category.{u_6, 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.{u_4, u_1} A] {B : Type u_2} [Category.{u_5, u_2} B] {T : Type u_3} [Category.{u_6, 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.{u_4, u_1} A] {B : Type u_2} [Category.{u_5, u_2} B] {T : Type u_3} [Category.{u_6, 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.{u_4, u_1} A] {B : Type u_2} [Category.{u_5, u_2} B] {T : Type u_3} [Category.{u_6, 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.{u_4, u_1} A] {B : Type u_2} [Category.{u_5, u_2} B] {T : Type u_3} [Category.{u_6, 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.{u_4, u_1} A] {B : Type u_2} [Category.{u_5, u_2} B] {T : Type u_3} [Category.{u_6, 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.

Equations

• One or more equations did not get rendered due to their size.

instance CategoryTheory.MorphismProperty.Comma.instFullTopCommaForget {A : Type u_1} [Category.{u_4, u_1} A] {B : Type u_2} [Category.{u_5, u_2} B] {T : Type u_3} [Category.{u_6, 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.{u_4, u_1} A] {B : Type u_2} [Category.{u_5, u_2} B] {T : Type u_3} [Category.{u_6, 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.{u_4, u_1} A] {B : Type u_2} [Category.{u_5, u_2} B] {T : Type u_3} [Category.{u_6, 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.lift {A : Type u_1} [Category.{u_5, u_1} A] {B : Type u_2} [Category.{u_6, u_2} B] {T : Type u_3} [Category.{u_7, 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.{u_8, 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.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.lift_map_hom {A : Type u_1} [Category.{u_5, u_1} A] {B : Type u_2} [Category.{u_6, u_2} B] {T : Type u_3} [Category.{u_7, 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.{u_8, 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

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.lift_obj_toComma {A : Type u_1} [Category.{u_5, u_1} A] {B : Type u_2} [Category.{u_6, u_2} B] {T : Type u_3} [Category.{u_7, 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.{u_8, 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

def CategoryTheory.MorphismProperty.Comma.mapLeft {A : Type u_1} [Category.{u_4, u_1} A] {B : Type u_2} [Category.{u_5, u_2} B] {T : Type u_3} [Category.{u_6, 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.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.mapLeft_map_left {A : Type u_1} [Category.{u_4, u_1} A] {B : Type u_2} [Category.{u_5, u_2} B] {T : Type u_3} [Category.{u_6, 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_right {A : Type u_1} [Category.{u_4, u_1} A] {B : Type u_2} [Category.{u_5, u_2} B] {T : Type u_3} [Category.{u_6, 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

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.mapLeft_map_right {A : Type u_1} [Category.{u_4, u_1} A] {B : Type u_2} [Category.{u_5, u_2} B] {T : Type u_3} [Category.{u_6, 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_hom {A : Type u_1} [Category.{u_4, u_1} A] {B : Type u_2} [Category.{u_5, u_2} B] {T : Type u_3} [Category.{u_6, 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.{u_4, u_1} A] {B : Type u_2} [Category.{u_5, u_2} B] {T : Type u_3} [Category.{u_6, 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

def CategoryTheory.MorphismProperty.Comma.mapRight {A : Type u_1} [Category.{u_4, u_1} A] {B : Type u_2} [Category.{u_5, u_2} B] {T : Type u_3} [Category.{u_6, 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.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.mapRight_map_left {A : Type u_1} [Category.{u_4, u_1} A] {B : Type u_2} [Category.{u_5, u_2} B] {T : Type u_3} [Category.{u_6, 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_map_right {A : Type u_1} [Category.{u_4, u_1} A] {B : Type u_2} [Category.{u_5, u_2} B] {T : Type u_3} [Category.{u_6, 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_hom {A : Type u_1} [Category.{u_4, u_1} A] {B : Type u_2} [Category.{u_5, u_2} B] {T : Type u_3} [Category.{u_6, 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_left {A : Type u_1} [Category.{u_4, u_1} A] {B : Type u_2} [Category.{u_5, u_2} B] {T : Type u_3} [Category.{u_6, 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

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.mapRight_obj_right {A : Type u_1} [Category.{u_4, u_1} A] {B : Type u_2} [Category.{u_5, u_2} B] {T : Type u_3} [Category.{u_6, 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

@[reducible, inline]

abbrev CategoryTheory.MorphismProperty.Over {T : Type u_1} [Category.{u_2, u_1} T] (P Q : MorphismProperty T) (X : T) : Type (max u_2 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.

Equations

• P.Over Q X = CategoryTheory.MorphismProperty.Comma (CategoryTheory.Functor.id T) (CategoryTheory.Functor.fromPUnit X) P Q ⊤

@[reducible, inline]

abbrev CategoryTheory.MorphismProperty.Over.forget {T : Type u_1} [Category.{u_2, 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.

Equations

• CategoryTheory.MorphismProperty.Over.forget P Q X = CategoryTheory.MorphismProperty.Comma.forget (CategoryTheory.Functor.id T) (CategoryTheory.Functor.fromPUnit X) P Q ⊤

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

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

def CategoryTheory.MorphismProperty.Over.Hom.mk {T : Type u_1} [Category.{u_2, 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.

Equations

• CategoryTheory.MorphismProperty.Over.Hom.mk f hf = { toCommaMorphism := f, prop_hom_left := hf, prop_hom_right := trivial }

@[simp]

theorem CategoryTheory.MorphismProperty.Over.Hom.mk_hom {T : Type u_1} [Category.{u_2, 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.{u_2, 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.

Equations

• CategoryTheory.MorphismProperty.Over.mk Q f hf = { left := A, right := { as := PUnit.unit }, hom := f, prop := hf }

@[simp]

theorem CategoryTheory.MorphismProperty.Over.mk_hom {T : Type u_1} [Category.{u_2, 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.{u_2, 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.{u_2, 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 aesop_cat) (hf : Q f := by trivial) : A ⟶ B

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

Equations

• CategoryTheory.MorphismProperty.Over.homMk f w hf = { toCommaMorphism := CategoryTheory.Over.homMk f w, prop_hom_left := hf, prop_hom_right := trivial }

@[simp]

theorem CategoryTheory.MorphismProperty.Over.homMk_hom {T : Type u_1} [Category.{u_2, 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 aesop_cat) (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.{u_2, 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 aesop_cat) : A ≅ B

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

Equations

• CategoryTheory.MorphismProperty.Over.isoMk f w = CategoryTheory.MorphismProperty.Comma.isoMk f (CategoryTheory.Discrete.eqToIso' ⋯) ⋯

@[simp]

theorem CategoryTheory.MorphismProperty.Over.isoMk_inv_left {T : Type u_1} [Category.{u_2, 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 aesop_cat) : (Over.isoMk f w).inv.left = f.inv

@[simp]

theorem CategoryTheory.MorphismProperty.Over.isoMk_hom_left {T : Type u_1} [Category.{u_2, 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 aesop_cat) : (Over.isoMk f w).hom.left = f.hom

theorem CategoryTheory.MorphismProperty.Over.Hom.ext {T : Type u_1} [Category.{u_2, 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.w {T : Type u_1} [Category.{u_2, 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.{u_2, 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.Under {T : Type u_1} [Category.{u_2, u_1} T] (P Q : MorphismProperty T) (X : T) : Type (max u_2 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.

Equations

• P.Under Q X = CategoryTheory.MorphismProperty.Comma (CategoryTheory.Functor.fromPUnit X) (CategoryTheory.Functor.id T) P ⊤ Q

@[reducible, inline]

abbrev CategoryTheory.MorphismProperty.Under.forget {T : Type u_1} [Category.{u_2, 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.

Equations

• CategoryTheory.MorphismProperty.Under.forget P Q X = CategoryTheory.MorphismProperty.Comma.forget (CategoryTheory.Functor.fromPUnit X) (CategoryTheory.Functor.id T) P ⊤ Q

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

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

def CategoryTheory.MorphismProperty.Under.Hom.mk {T : Type u_1} [Category.{u_2, 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.

Equations

• CategoryTheory.MorphismProperty.Under.Hom.mk f hf = { toCommaMorphism := f, prop_hom_left := trivial, prop_hom_right := hf }

@[simp]

theorem CategoryTheory.MorphismProperty.Under.Hom.mk_hom {T : Type u_1} [Category.{u_2, 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.{u_2, 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.

Equations

• CategoryTheory.MorphismProperty.Under.mk Q f hf = { left := { as := PUnit.unit }, right := A, hom := f, prop := hf }

@[simp]

theorem CategoryTheory.MorphismProperty.Under.mk_hom {T : Type u_1} [Category.{u_2, 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.{u_2, 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.{u_2, 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 aesop_cat) (hf : Q f := by trivial) : A ⟶ B

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

Equations

• CategoryTheory.MorphismProperty.Under.homMk f w hf = { toCommaMorphism := CategoryTheory.Under.homMk f w, prop_hom_left := trivial, prop_hom_right := hf }

@[simp]

theorem CategoryTheory.MorphismProperty.Under.homMk_hom {T : Type u_1} [Category.{u_2, 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 aesop_cat) (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.{u_2, 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 aesop_cat) : A ≅ B

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

Equations

• CategoryTheory.MorphismProperty.Under.isoMk f w = CategoryTheory.MorphismProperty.Comma.isoMk (CategoryTheory.Discrete.eqToIso' ⋯) f ⋯

@[simp]

theorem CategoryTheory.MorphismProperty.Under.isoMk_hom_right {T : Type u_1} [Category.{u_2, 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 aesop_cat) : (Under.isoMk f w).hom.right = f.hom

@[simp]

theorem CategoryTheory.MorphismProperty.Under.isoMk_inv_right {T : Type u_1} [Category.{u_2, 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 aesop_cat) : (Under.isoMk f w).inv.right = f.inv

theorem CategoryTheory.MorphismProperty.Under.Hom.ext {T : Type u_1} [Category.{u_2, 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.w {T : Type u_1} [Category.{u_2, 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.{u_2, 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