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} [CategoryTheory.Category.{u_5, u_1} A] {T : Type u_3} [CategoryTheory.Category.{u_4, u_3} T] (P : CategoryTheory.MorphismProperty T) [P.RespectsIso] {L : CategoryTheory.Functor A T} {X : T} {f g : CategoryTheory.CostructuredArrow L X} (e : f ≅ g) : P f.hom ↔ P g.hom

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

structure CategoryTheory.MorphismProperty.Comma {A : Type u_1} [CategoryTheory.Category.{u_4, u_1} A] {B : Type u_2} [CategoryTheory.Category.{u_5, u_2} B] {T : Type u_3} [CategoryTheory.Category.{u_6, u_3} T] (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) (P : CategoryTheory.MorphismProperty T) (Q : CategoryTheory.MorphismProperty A) (W : CategoryTheory.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✝ : CategoryTheory.Category.{u_4, u_1} A} {B : Type u_2} {inst✝¹ : CategoryTheory.Category.{u_5, u_2} B} {T : Type u_3} {inst✝² : CategoryTheory.Category.{u_6, u_3} T} {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {P : CategoryTheory.MorphismProperty T} {Q : CategoryTheory.MorphismProperty A} {W : CategoryTheory.MorphismProperty B} {x y : CategoryTheory.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} [CategoryTheory.Category.{u_4, u_1} A] {B : Type u_2} [CategoryTheory.Category.{u_5, u_2} B] {T : Type u_3} [CategoryTheory.Category.{u_6, u_3} T] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {P : CategoryTheory.MorphismProperty T} {Q : CategoryTheory.MorphismProperty A} {W : CategoryTheory.MorphismProperty B} (X Y : CategoryTheory.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 : CategoryTheory.CategoryStruct.comp (L.map self.left) Y.hom = CategoryTheory.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✝ : CategoryTheory.Category.{u_4, u_1} A} {B : Type u_2} {inst✝¹ : CategoryTheory.Category.{u_5, u_2} B} {T : Type u_3} {inst✝² : CategoryTheory.Category.{u_6, u_3} T} {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {P : CategoryTheory.MorphismProperty T} {Q : CategoryTheory.MorphismProperty A} {W : CategoryTheory.MorphismProperty B} {X Y : CategoryTheory.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} [CategoryTheory.Category.{u_4, u_1} A] {B : Type u_2} [CategoryTheory.Category.{u_5, u_2} B] {T : Type u_3} [CategoryTheory.Category.{u_6, u_3} T] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {P : CategoryTheory.MorphismProperty T} {Q : CategoryTheory.MorphismProperty A} {W : CategoryTheory.MorphismProperty B} {X Y : CategoryTheory.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} [CategoryTheory.Category.{u_4, u_1} A] {B : Type u_2} [CategoryTheory.Category.{u_5, u_2} B] {T : Type u_3} [CategoryTheory.Category.{u_6, u_3} T] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {P : CategoryTheory.MorphismProperty T} {Q : CategoryTheory.MorphismProperty A} {W : CategoryTheory.MorphismProperty B} {X Y : CategoryTheory.MorphismProperty.Comma L R P Q W} (f : CategoryTheory.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

@[simp]

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

@[simp]

theorem CategoryTheory.MorphismProperty.Comma.Hom.hom_right {A : Type u_1} [CategoryTheory.Category.{u_4, u_1} A] {B : Type u_2} [CategoryTheory.Category.{u_5, u_2} B] {T : Type u_3} [CategoryTheory.Category.{u_6, u_3} T] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {P : CategoryTheory.MorphismProperty T} {Q : CategoryTheory.MorphismProperty A} {W : CategoryTheory.MorphismProperty B} {X Y : CategoryTheory.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} [CategoryTheory.Category.{u_4, u_1} A] {B : Type u_2} [CategoryTheory.Category.{u_5, u_2} B] {T : Type u_3} [CategoryTheory.Category.{u_6, u_3} T] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {P : CategoryTheory.MorphismProperty T} {Q : CategoryTheory.MorphismProperty A} {W : CategoryTheory.MorphismProperty B} {X Y : CategoryTheory.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} [CategoryTheory.Category.{u_4, u_1} A] {B : Type u_2} [CategoryTheory.Category.{u_5, u_2} B] {T : Type u_3} [CategoryTheory.Category.{u_6, u_3} T] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {P : CategoryTheory.MorphismProperty T} {Q : CategoryTheory.MorphismProperty A} {W : CategoryTheory.MorphismProperty B} [Q.ContainsIdentities] [W.ContainsIdentities] (X : CategoryTheory.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} [CategoryTheory.Category.{u_4, u_1} A] {B : Type u_2} [CategoryTheory.Category.{u_5, u_2} B] {T : Type u_3} [CategoryTheory.Category.{u_6, u_3} T] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {P : CategoryTheory.MorphismProperty T} {Q : CategoryTheory.MorphismProperty A} {W : CategoryTheory.MorphismProperty B} [Q.ContainsIdentities] [W.ContainsIdentities] (X : CategoryTheory.MorphismProperty.Comma L R P Q W) : X.id.right = CategoryTheory.CategoryStruct.id X.right

@[simp]

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

def CategoryTheory.MorphismProperty.Comma.Hom.comp {A : Type u_1} [CategoryTheory.Category.{u_4, u_1} A] {B : Type u_2} [CategoryTheory.Category.{u_5, u_2} B] {T : Type u_3} [CategoryTheory.Category.{u_6, u_3} T] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {P : CategoryTheory.MorphismProperty T} {Q : CategoryTheory.MorphismProperty A} {W : CategoryTheory.MorphismProperty B} [Q.IsStableUnderComposition] [W.IsStableUnderComposition] {X Y Z : CategoryTheory.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} [CategoryTheory.Category.{u_4, u_1} A] {B : Type u_2} [CategoryTheory.Category.{u_5, u_2} B] {T : Type u_3} [CategoryTheory.Category.{u_6, u_3} T] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {P : CategoryTheory.MorphismProperty T} {Q : CategoryTheory.MorphismProperty A} {W : CategoryTheory.MorphismProperty B} [Q.IsStableUnderComposition] [W.IsStableUnderComposition] {X Y Z : CategoryTheory.MorphismProperty.Comma L R P Q W} (f : X.Hom Y) (g : Y.Hom Z) : (f.comp g).left = CategoryTheory.CategoryStruct.comp f.left g.left

@[simp]

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

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

Equations

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

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

Alternative ext lemma for Comma.Hom.

@[simp]

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

@[simp]

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

def CategoryTheory.MorphismProperty.Comma.homFromCommaOfIsIso {A : Type u_1} [CategoryTheory.Category.{u_4, u_1} A] {B : Type u_2} [CategoryTheory.Category.{u_5, u_2} B] {T : Type u_3} [CategoryTheory.Category.{u_6, u_3} T] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {P : CategoryTheory.MorphismProperty T} {Q : CategoryTheory.MorphismProperty A} {W : CategoryTheory.MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] [Q.RespectsIso] [W.RespectsIso] {X Y : CategoryTheory.MorphismProperty.Comma L R P Q W} (i : X.toComma ⟶ Y.toComma) [CategoryTheory.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} [CategoryTheory.Category.{u_4, u_1} A] {B : Type u_2} [CategoryTheory.Category.{u_5, u_2} B] {T : Type u_3} [CategoryTheory.Category.{u_6, u_3} T] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {P : CategoryTheory.MorphismProperty T} {Q : CategoryTheory.MorphismProperty A} {W : CategoryTheory.MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] [Q.RespectsIso] [W.RespectsIso] {X Y : CategoryTheory.MorphismProperty.Comma L R P Q W} (i : X.toComma ⟶ Y.toComma) [CategoryTheory.IsIso i] : CategoryTheory.MorphismProperty.Comma.Hom.hom (CategoryTheory.MorphismProperty.Comma.homFromCommaOfIsIso i) = i

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

Equations

• ⋯ = ⋯

def CategoryTheory.MorphismProperty.Comma.isoFromComma {A : Type u_1} [CategoryTheory.Category.{u_4, u_1} A] {B : Type u_2} [CategoryTheory.Category.{u_5, u_2} B] {T : Type u_3} [CategoryTheory.Category.{u_6, u_3} T] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {P : CategoryTheory.MorphismProperty T} {Q : CategoryTheory.MorphismProperty A} {W : CategoryTheory.MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] [Q.RespectsIso] [W.RespectsIso] {X Y : CategoryTheory.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} [CategoryTheory.Category.{u_4, u_1} A] {B : Type u_2} [CategoryTheory.Category.{u_5, u_2} B] {T : Type u_3} [CategoryTheory.Category.{u_6, u_3} T] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {P : CategoryTheory.MorphismProperty T} {Q : CategoryTheory.MorphismProperty A} {W : CategoryTheory.MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] [Q.RespectsIso] [W.RespectsIso] {X Y : CategoryTheory.MorphismProperty.Comma L R P Q W} (i : X.toComma ≅ Y.toComma) : (CategoryTheory.MorphismProperty.Comma.isoFromComma i).inv = CategoryTheory.MorphismProperty.Comma.homFromCommaOfIsIso i.inv

@[simp]

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

def CategoryTheory.MorphismProperty.Comma.isoMk {A : Type u_1} [CategoryTheory.Category.{u_4, u_1} A] {B : Type u_2} [CategoryTheory.Category.{u_5, u_2} B] {T : Type u_3} [CategoryTheory.Category.{u_6, u_3} T] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {P : CategoryTheory.MorphismProperty T} {Q : CategoryTheory.MorphismProperty A} {W : CategoryTheory.MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] [Q.RespectsIso] [W.RespectsIso] {X Y : CategoryTheory.MorphismProperty.Comma L R P Q W} (l : X.left ≅ Y.left) (r : X.right ≅ Y.right) (h : CategoryTheory.CategoryStruct.comp (L.map l.hom) Y.hom = CategoryTheory.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_hom_left {A : Type u_1} [CategoryTheory.Category.{u_4, u_1} A] {B : Type u_2} [CategoryTheory.Category.{u_5, u_2} B] {T : Type u_3} [CategoryTheory.Category.{u_6, u_3} T] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {P : CategoryTheory.MorphismProperty T} {Q : CategoryTheory.MorphismProperty A} {W : CategoryTheory.MorphismProperty B} [Q.IsMultiplicative] [W.IsMultiplicative] [Q.RespectsIso] [W.RespectsIso] {X Y : CategoryTheory.MorphismProperty.Comma L R P Q W} (l : X.left ≅ Y.left) (r : X.right ≅ Y.right) (h : CategoryTheory.CategoryStruct.comp (L.map l.hom) Y.hom = CategoryTheory.CategoryStruct.comp X.hom (R.map r.hom) := by aesop_cat) : (CategoryTheory.MorphismProperty.Comma.isoMk l r h).hom.left = l.hom

@[simp]

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

@[simp]

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

@[simp]

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

def CategoryTheory.MorphismProperty.Comma.forget {A : Type u_1} [CategoryTheory.Category.{u_4, u_1} A] {B : Type u_2} [CategoryTheory.Category.{u_5, u_2} B] {T : Type u_3} [CategoryTheory.Category.{u_6, u_3} T] (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) (P : CategoryTheory.MorphismProperty T) (Q : CategoryTheory.MorphismProperty A) (W : CategoryTheory.MorphismProperty B) [Q.IsMultiplicative] [W.IsMultiplicative] : CategoryTheory.Functor (CategoryTheory.MorphismProperty.Comma L R P Q W) (CategoryTheory.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} [CategoryTheory.Category.{u_4, u_1} A] {B : Type u_2} [CategoryTheory.Category.{u_5, u_2} B] {T : Type u_3} [CategoryTheory.Category.{u_6, u_3} T] (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) (P : CategoryTheory.MorphismProperty T) (Q : CategoryTheory.MorphismProperty A) (W : CategoryTheory.MorphismProperty B) [Q.IsMultiplicative] [W.IsMultiplicative] (X : CategoryTheory.MorphismProperty.Comma L R P Q W) : (CategoryTheory.MorphismProperty.Comma.forget L R P Q W).obj X = X.toComma

@[simp]

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

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

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

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

Equations

• ⋯ = ⋯

def CategoryTheory.MorphismProperty.Comma.forgetFullyFaithful {A : Type u_1} [CategoryTheory.Category.{u_4, u_1} A] {B : Type u_2} [CategoryTheory.Category.{u_5, u_2} B] {T : Type u_3} [CategoryTheory.Category.{u_6, u_3} T] (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) (P : CategoryTheory.MorphismProperty T) : (CategoryTheory.MorphismProperty.Comma.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} [CategoryTheory.Category.{u_4, u_1} A] {B : Type u_2} [CategoryTheory.Category.{u_5, u_2} B] {T : Type u_3} [CategoryTheory.Category.{u_6, u_3} T] (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) (P : CategoryTheory.MorphismProperty T) : (CategoryTheory.MorphismProperty.Comma.forget L R P ⊤ ⊤).Full

Equations

• ⋯ = ⋯

@[reducible, inline]

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

def CategoryTheory.MorphismProperty.Over.Hom.mk {T : Type u_1} [CategoryTheory.Category.{u_2, u_1} T] {P Q : CategoryTheory.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} [CategoryTheory.Category.{u_2, u_1} T] {P Q : CategoryTheory.MorphismProperty T} {X : T} [Q.IsMultiplicative] {A B : P.Over Q X} (f : A.toComma ⟶ B.toComma) (hf : Q f.left) : CategoryTheory.MorphismProperty.Comma.Hom.hom (CategoryTheory.MorphismProperty.Over.Hom.mk f hf) = f

def CategoryTheory.MorphismProperty.Over.mk {T : Type u_1} [CategoryTheory.Category.{u_2, u_1} T] {P : CategoryTheory.MorphismProperty T} (Q : CategoryTheory.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_left {T : Type u_1} [CategoryTheory.Category.{u_2, u_1} T] {P : CategoryTheory.MorphismProperty T} (Q : CategoryTheory.MorphismProperty T) {X A : T} (f : A ⟶ X) (hf : P f) : (CategoryTheory.MorphismProperty.Over.mk Q f hf).left = A

@[simp]

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

def CategoryTheory.MorphismProperty.Over.homMk {T : Type u_1} [CategoryTheory.Category.{u_2, u_1} T] {P Q : CategoryTheory.MorphismProperty T} {X : T} [Q.IsMultiplicative] {A B : P.Over Q X} (f : A.left ⟶ B.left) (w : CategoryTheory.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} [CategoryTheory.Category.{u_2, u_1} T] {P Q : CategoryTheory.MorphismProperty T} {X : T} [Q.IsMultiplicative] {A B : P.Over Q X} (f : A.left ⟶ B.left) (w : CategoryTheory.CategoryStruct.comp f B.hom = A.hom := by aesop_cat) (hf : Q f := by trivial) : CategoryTheory.MorphismProperty.Comma.Hom.hom (CategoryTheory.MorphismProperty.Over.homMk f w hf) = CategoryTheory.Over.homMk f w

@[reducible, inline]

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

def CategoryTheory.MorphismProperty.Under.Hom.mk {T : Type u_1} [CategoryTheory.Category.{u_2, u_1} T] {P Q : CategoryTheory.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} [CategoryTheory.Category.{u_2, u_1} T] {P Q : CategoryTheory.MorphismProperty T} {X : T} [Q.IsMultiplicative] {A B : P.Under Q X} (f : A.toComma ⟶ B.toComma) (hf : Q f.right) : CategoryTheory.MorphismProperty.Comma.Hom.hom (CategoryTheory.MorphismProperty.Under.Hom.mk f hf) = f

def CategoryTheory.MorphismProperty.Under.mk {T : Type u_1} [CategoryTheory.Category.{u_2, u_1} T] {P : CategoryTheory.MorphismProperty T} (Q : CategoryTheory.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_left {T : Type u_1} [CategoryTheory.Category.{u_2, u_1} T] {P : CategoryTheory.MorphismProperty T} (Q : CategoryTheory.MorphismProperty T) {X A : T} (f : X ⟶ A) (hf : P f) : (CategoryTheory.MorphismProperty.Under.mk Q f hf).left = { as := PUnit.unit }

@[simp]

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

def CategoryTheory.MorphismProperty.Under.homMk {T : Type u_1} [CategoryTheory.Category.{u_2, u_1} T] {P Q : CategoryTheory.MorphismProperty T} {X : T} [Q.IsMultiplicative] {A B : P.Under Q X} (f : A.right ⟶ B.right) (w : CategoryTheory.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} [CategoryTheory.Category.{u_2, u_1} T] {P Q : CategoryTheory.MorphismProperty T} {X : T} [Q.IsMultiplicative] {A B : P.Under Q X} (f : A.right ⟶ B.right) (w : CategoryTheory.CategoryStruct.comp A.hom f = B.hom := by aesop_cat) (hf : Q f := by trivial) : CategoryTheory.MorphismProperty.Comma.Hom.hom (CategoryTheory.MorphismProperty.Under.homMk f w hf) = CategoryTheory.Under.homMk f w