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 Rwith the structural morphism satisfyingP, and - morphisms are morphisms of
Comma L Rwhere the left morphism satisfiesQand the right morphism satisfiesW.
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 #
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)
:
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)
:
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.
Instances For
@[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)
:
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)
:
The object property on CostructuredArrow L X induced by a morphism property.
Instances For
@[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)
:
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]
:
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)
:
The object property on StructuredArrow X R induced by a morphism property.
Instances For
@[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)
:
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]
:
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.
Instances For
theorem
CategoryTheory.MorphismProperty.over_eq_inverseImage
{T : Type u_3}
[Category.{v_3, u_3} T]
(W : MorphismProperty T)
(X : T)
:
@[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)
:
def
CategoryTheory.MorphismProperty.under
{T : Type u_3}
[Category.{v_3, u_3} T]
(W : MorphismProperty T)
{X : T}
:
The morphism property on Under X induced by a morphism property on C.
Instances For
theorem
CategoryTheory.MorphismProperty.under_eq_inverseImage
{T : Type u_3}
[Category.{v_3, u_3} T]
(W : MorphismProperty T)
(X : T)
:
@[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)
:
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.
Instances For
@[simp]
theorem
CategoryTheory.MorphismProperty.overObj_iff
{T : Type u_3}
[Category.{v_3, u_3} T]
{W : MorphismProperty T}
{X : T}
(Y : Over X)
:
instance
CategoryTheory.MorphismProperty.instIsClosedUnderIsomorphismsOverOverObjOfRespectsIso
{T : Type u_3}
[Category.{v_3, u_3} T]
{W : MorphismProperty T}
{X : T}
[W.RespectsIso]
:
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.
Instances For
@[simp]
theorem
CategoryTheory.MorphismProperty.underObj_iff
{T : Type u_3}
[Category.{v_3, u_3} T]
{W : MorphismProperty T}
{X : T}
(Y : Under X)
:
instance
CategoryTheory.MorphismProperty.instIsClosedUnderIsomorphismsUnderUnderObjOfRespectsIso
{T : Type u_3}
[Category.{v_3, u_3} T]
{W : MorphismProperty T}
{X : T}
[W.RespectsIso]
:
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.
Instances For
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}
:
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)
:
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.
Instances For
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)
:
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}
:
@[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)
:
The underlying morphism of objects in Comma L R.
Instances For
@[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)
:
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)
:
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)
:
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)
:
See Note [custom simps projection]
Instances For
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.
Instances For
@[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)
:
@[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)
:
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.
Instances For
@[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)
:
@[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)
:
@[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]
:
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)
:
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)
:
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}
:
@[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)
:
@[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)
:
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)
:
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)
:
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]
:
If i is an isomorphism in Comma L R, it is also a morphism in P.Comma L R Q W.
Instances For
@[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]
:
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]
:
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)
:
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.
Instances For
@[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)
:
@[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)
:
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)
:
Constructor for isomorphisms in P.Comma L R Q W from isomorphisms of the left and right
components and naturality in the forward direction.
Instances For
@[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)
:
@[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)
:
@[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)
:
@[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)
:
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.
Instances For
@[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✝)
:
@[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)
:
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]
:
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]
:
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)]
:
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]
:
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.
Instances For
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)
:
@[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)
:
@[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)
:
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.
Instances For
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.
Instances For
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.
Instances For
@[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)
:
@[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)
:
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.
Instances For
@[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)
:
@[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)
:
@[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)
:
@[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)
:
@[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)
:
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]
:
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.
Instances For
@[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)
:
@[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)
:
@[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)
:
@[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)
:
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))
:
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.
Instances For
@[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)
:
@[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)
:
@[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)
:
@[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)
:
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))
:
Two equal natural transformations L₁ ⟶ L₂ yield naturally isomorphic functors
P.Comma L₁ R Q W ⥤ P.Comma L₂ R Q W.
Instances For
@[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)
:
@[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)
:
@[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)
:
@[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)
:
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₂)
:
A natural isomorphism L₁ ≅ L₂ induces an equivalence of categories
P.Comma L₁ R Q W ≌ P.Comma L₂ R Q W.
Instances For
@[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)
:
@[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)
:
@[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)
:
@[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)
:
@[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)
:
@[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)
:
@[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)
:
@[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)
:
@[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)
:
@[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)
:
@[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)
:
@[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)
:
@[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)
:
@[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)
:
@[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)
:
@[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)
:
@[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)
:
@[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)
:
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.
Instances For
@[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)
:
@[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)
:
@[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)
:
@[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)
:
@[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)
:
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]
:
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.
Instances For
@[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)
:
@[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)
:
@[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)
:
@[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)
:
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)))
:
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.
Instances For
@[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)
:
@[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)
:
@[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)
:
@[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)
:
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)))
:
Two equal natural transformations R₁ ⟶ R₂ yield naturally isomorphic functors
P.Comma L R₁ Q W ⥤ P.Comma L R₂ Q W.
Instances For
@[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)
:
@[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)
:
@[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)
:
@[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)
:
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₂)
:
A natural isomorphism R₁ ≅ R₂ induces an equivalence of categories
P.Comma L R₁ Q W ≌ P.Comma L R₂ Q W.
Instances For
@[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)
:
@[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)
:
@[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)
:
@[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)
:
@[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)
:
@[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)
:
@[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)
:
@[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)
:
@[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)
:
@[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)
:
@[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)
:
@[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)
:
@[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)
:
@[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)
:
@[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)
:
@[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)
:
@[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)
:
@[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)
:
@[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.
Instances For
@[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]
:
The forgetful functor from the full subcategory of Over X defined by P to Over X.
Instances For
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)
:
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)
:
Construct a morphism in P.Over Q X from a morphism in Over.X.
Instances For
@[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)
:
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.
Instances For
@[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)
:
@[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)
:
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)
:
Make a morphism in P.Over Q X from a morphism in T with compatibilities.
Instances For
@[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)
:
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)
:
Make an isomorphism in P.Over Q X from an isomorphism in T with compatibilities.
Instances For
@[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)
:
@[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)
:
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)
:
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}
:
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)
:
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)
:
@[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')
:
The natural inclusion induced by implications of morphism properties.
Instances For
@[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)
:
@[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)
:
@[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.
Instances For
@[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]
:
The forgetful functor from the full subcategory of Under X defined by P to Under X.
Instances For
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)
:
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)
:
Construct a morphism in P.Under Q X from a morphism in Under.X.
Instances For
@[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)
:
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.
Instances For
@[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)
:
@[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)
:
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)
:
Make a morphism in P.Under Q X from a morphism in T with compatibilities.
Instances For
@[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)
:
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)
:
Make an isomorphism in P.Under Q X from an isomorphism in T with compatibilities.
Instances For
@[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)
:
@[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)
:
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)
:
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}
:
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)
:
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)
:
@[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.
Instances For
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.
Instances For
@[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)
:
@[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)
:
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)
:
Construct a morphism in P.CostructuredArrow Q F X by giving a morphism on the underlying
objects of C.
Instances For
@[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)
:
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)
:
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}
:
@[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.
Instances For
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.
Instances For
@[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)
:
@[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✝)
:
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