Structured arrow categories on Comma.map #
We characterize structured arrow categories on arbitrary instances of Comma.map as a
comma category itself.
def
CategoryTheory.StructuredArrow.commaMapEquivalenceFunctor
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : Type u₃}
[Category.{v₃, u₃} T]
{L : Functor C T}
{R : Functor D T}
{C' : Type u₄}
[Category.{v₄, u₄} C']
{D' : Type u₅}
[Category.{v₅, u₅} D']
{T' : Type u₆}
[Category.{u₆, u₆} T']
{L' : Functor C' T'}
{R' : Functor D' T'}
{F₁ : Functor C C'}
{F₂ : Functor D D'}
{F : Functor T T'}
(α : F₁.comp L' ⟶ L.comp F)
(β : R.comp F ⟶ F₂.comp R')
[IsIso β]
(X : Comma L' R')
:
Functor (StructuredArrow X (Comma.map α β)) (Comma (map₂ (CategoryStruct.id (L'.obj X.left)) α) (map₂ X.hom (inv β)))
The functor establishing the equivalence StructuredArrow.commaMapEquivalence.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.StructuredArrow.commaMapEquivalenceFunctor_map_right
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : Type u₃}
[Category.{v₃, u₃} T]
{L : Functor C T}
{R : Functor D T}
{C' : Type u₄}
[Category.{v₄, u₄} C']
{D' : Type u₅}
[Category.{v₅, u₅} D']
{T' : Type u₆}
[Category.{u₆, u₆} T']
{L' : Functor C' T'}
{R' : Functor D' T'}
{F₁ : Functor C C'}
{F₂ : Functor D D'}
{F : Functor T T'}
(α : F₁.comp L' ⟶ L.comp F)
(β : R.comp F ⟶ F₂.comp R')
[IsIso β]
(X : Comma L' R')
{Y Z : StructuredArrow X (Comma.map α β)}
(f : Y ⟶ Z)
:
((commaMapEquivalenceFunctor α β X).map f).right = homMk f.right.right ⋯
@[simp]
theorem
CategoryTheory.StructuredArrow.commaMapEquivalenceFunctor_map_left
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : Type u₃}
[Category.{v₃, u₃} T]
{L : Functor C T}
{R : Functor D T}
{C' : Type u₄}
[Category.{v₄, u₄} C']
{D' : Type u₅}
[Category.{v₅, u₅} D']
{T' : Type u₆}
[Category.{u₆, u₆} T']
{L' : Functor C' T'}
{R' : Functor D' T'}
{F₁ : Functor C C'}
{F₂ : Functor D D'}
{F : Functor T T'}
(α : F₁.comp L' ⟶ L.comp F)
(β : R.comp F ⟶ F₂.comp R')
[IsIso β]
(X : Comma L' R')
{Y Z : StructuredArrow X (Comma.map α β)}
(f : Y ⟶ Z)
:
((commaMapEquivalenceFunctor α β X).map f).left = homMk f.right.left ⋯
@[simp]
theorem
CategoryTheory.StructuredArrow.commaMapEquivalenceFunctor_obj_right
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : Type u₃}
[Category.{v₃, u₃} T]
{L : Functor C T}
{R : Functor D T}
{C' : Type u₄}
[Category.{v₄, u₄} C']
{D' : Type u₅}
[Category.{v₅, u₅} D']
{T' : Type u₆}
[Category.{u₆, u₆} T']
{L' : Functor C' T'}
{R' : Functor D' T'}
{F₁ : Functor C C'}
{F₂ : Functor D D'}
{F : Functor T T'}
(α : F₁.comp L' ⟶ L.comp F)
(β : R.comp F ⟶ F₂.comp R')
[IsIso β]
(X : Comma L' R')
(Y : StructuredArrow X (Comma.map α β))
:
((commaMapEquivalenceFunctor α β X).obj Y).right = mk Y.hom.right
@[simp]
theorem
CategoryTheory.StructuredArrow.commaMapEquivalenceFunctor_obj_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : Type u₃}
[Category.{v₃, u₃} T]
{L : Functor C T}
{R : Functor D T}
{C' : Type u₄}
[Category.{v₄, u₄} C']
{D' : Type u₅}
[Category.{v₅, u₅} D']
{T' : Type u₆}
[Category.{u₆, u₆} T']
{L' : Functor C' T'}
{R' : Functor D' T'}
{F₁ : Functor C C'}
{F₂ : Functor D D'}
{F : Functor T T'}
(α : F₁.comp L' ⟶ L.comp F)
(β : R.comp F ⟶ F₂.comp R')
[IsIso β]
(X : Comma L' R')
(Y : StructuredArrow X (Comma.map α β))
:
((commaMapEquivalenceFunctor α β X).obj Y).hom = homMk Y.right.hom ⋯
@[simp]
theorem
CategoryTheory.StructuredArrow.commaMapEquivalenceFunctor_obj_left
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : Type u₃}
[Category.{v₃, u₃} T]
{L : Functor C T}
{R : Functor D T}
{C' : Type u₄}
[Category.{v₄, u₄} C']
{D' : Type u₅}
[Category.{v₅, u₅} D']
{T' : Type u₆}
[Category.{u₆, u₆} T']
{L' : Functor C' T'}
{R' : Functor D' T'}
{F₁ : Functor C C'}
{F₂ : Functor D D'}
{F : Functor T T'}
(α : F₁.comp L' ⟶ L.comp F)
(β : R.comp F ⟶ F₂.comp R')
[IsIso β]
(X : Comma L' R')
(Y : StructuredArrow X (Comma.map α β))
:
((commaMapEquivalenceFunctor α β X).obj Y).left = mk Y.hom.left
def
CategoryTheory.StructuredArrow.commaMapEquivalenceInverse
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : Type u₃}
[Category.{v₃, u₃} T]
{L : Functor C T}
{R : Functor D T}
{C' : Type u₄}
[Category.{v₄, u₄} C']
{D' : Type u₅}
[Category.{v₅, u₅} D']
{T' : Type u₆}
[Category.{u₆, u₆} T']
{L' : Functor C' T'}
{R' : Functor D' T'}
{F₁ : Functor C C'}
{F₂ : Functor D D'}
{F : Functor T T'}
(α : F₁.comp L' ⟶ L.comp F)
(β : R.comp F ⟶ F₂.comp R')
[IsIso β]
(X : Comma L' R')
:
Functor (Comma (map₂ (CategoryStruct.id (L'.obj X.left)) α) (map₂ X.hom (inv β))) (StructuredArrow X (Comma.map α β))
The inverse functor establishing the equivalence StructuredArrow.commaMapEquivalence.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.StructuredArrow.commaMapEquivalenceInverse_obj
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : Type u₃}
[Category.{v₃, u₃} T]
{L : Functor C T}
{R : Functor D T}
{C' : Type u₄}
[Category.{v₄, u₄} C']
{D' : Type u₅}
[Category.{v₅, u₅} D']
{T' : Type u₆}
[Category.{u₆, u₆} T']
{L' : Functor C' T'}
{R' : Functor D' T'}
{F₁ : Functor C C'}
{F₂ : Functor D D'}
{F : Functor T T'}
(α : F₁.comp L' ⟶ L.comp F)
(β : R.comp F ⟶ F₂.comp R')
[IsIso β]
(X : Comma L' R')
(Y : Comma (map₂ (CategoryStruct.id (L'.obj X.left)) α) (map₂ X.hom (inv β)))
:
(commaMapEquivalenceInverse α β X).obj Y = mk { left := Y.left.hom, right := Y.right.hom, w := ⋯ }
@[simp]
theorem
CategoryTheory.StructuredArrow.commaMapEquivalenceInverse_map
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : Type u₃}
[Category.{v₃, u₃} T]
{L : Functor C T}
{R : Functor D T}
{C' : Type u₄}
[Category.{v₄, u₄} C']
{D' : Type u₅}
[Category.{v₅, u₅} D']
{T' : Type u₆}
[Category.{u₆, u₆} T']
{L' : Functor C' T'}
{R' : Functor D' T'}
{F₁ : Functor C C'}
{F₂ : Functor D D'}
{F : Functor T T'}
(α : F₁.comp L' ⟶ L.comp F)
(β : R.comp F ⟶ F₂.comp R')
[IsIso β]
(X : Comma L' R')
{Y Z : Comma (map₂ (CategoryStruct.id (L'.obj X.left)) α) (map₂ X.hom (inv β))}
(f : Y ⟶ Z)
:
(commaMapEquivalenceInverse α β X).map f = homMk { left := f.left.right, right := f.right.right, w := ⋯ } ⋯
def
CategoryTheory.StructuredArrow.commaMapEquivalenceUnitIso
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : Type u₃}
[Category.{v₃, u₃} T]
{L : Functor C T}
{R : Functor D T}
{C' : Type u₄}
[Category.{v₄, u₄} C']
{D' : Type u₅}
[Category.{v₅, u₅} D']
{T' : Type u₆}
[Category.{u₆, u₆} T']
{L' : Functor C' T'}
{R' : Functor D' T'}
{F₁ : Functor C C'}
{F₂ : Functor D D'}
{F : Functor T T'}
(α : F₁.comp L' ⟶ L.comp F)
(β : R.comp F ⟶ F₂.comp R')
[IsIso β]
(X : Comma L' R')
:
Functor.id (StructuredArrow X (Comma.map α β)) ≅ (commaMapEquivalenceFunctor α β X).comp (commaMapEquivalenceInverse α β X)
The unit establishing the equivalence StructuredArrow.commaMapEquivalence.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.StructuredArrow.commaMapEquivalenceUnitIso_inv_app_right_left
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : Type u₃}
[Category.{v₃, u₃} T]
{L : Functor C T}
{R : Functor D T}
{C' : Type u₄}
[Category.{v₄, u₄} C']
{D' : Type u₅}
[Category.{v₅, u₅} D']
{T' : Type u₆}
[Category.{u₆, u₆} T']
{L' : Functor C' T'}
{R' : Functor D' T'}
{F₁ : Functor C C'}
{F₂ : Functor D D'}
{F : Functor T T'}
(α : F₁.comp L' ⟶ L.comp F)
(β : R.comp F ⟶ F₂.comp R')
[IsIso β]
(X : Comma L' R')
(X✝ : StructuredArrow X (Comma.map α β))
:
((commaMapEquivalenceUnitIso α β X).inv.app X✝).right.left = CategoryStruct.id X✝.right.left
@[simp]
theorem
CategoryTheory.StructuredArrow.commaMapEquivalenceUnitIso_inv_app_right_right
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : Type u₃}
[Category.{v₃, u₃} T]
{L : Functor C T}
{R : Functor D T}
{C' : Type u₄}
[Category.{v₄, u₄} C']
{D' : Type u₅}
[Category.{v₅, u₅} D']
{T' : Type u₆}
[Category.{u₆, u₆} T']
{L' : Functor C' T'}
{R' : Functor D' T'}
{F₁ : Functor C C'}
{F₂ : Functor D D'}
{F : Functor T T'}
(α : F₁.comp L' ⟶ L.comp F)
(β : R.comp F ⟶ F₂.comp R')
[IsIso β]
(X : Comma L' R')
(X✝ : StructuredArrow X (Comma.map α β))
:
((commaMapEquivalenceUnitIso α β X).inv.app X✝).right.right = CategoryStruct.id X✝.right.right
@[simp]
theorem
CategoryTheory.StructuredArrow.commaMapEquivalenceUnitIso_hom_app_left_down_down
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : Type u₃}
[Category.{v₃, u₃} T]
{L : Functor C T}
{R : Functor D T}
{C' : Type u₄}
[Category.{v₄, u₄} C']
{D' : Type u₅}
[Category.{v₅, u₅} D']
{T' : Type u₆}
[Category.{u₆, u₆} T']
{L' : Functor C' T'}
{R' : Functor D' T'}
{F₁ : Functor C C'}
{F₂ : Functor D D'}
{F : Functor T T'}
(α : F₁.comp L' ⟶ L.comp F)
(β : R.comp F ⟶ F₂.comp R')
[IsIso β]
(X : Comma L' R')
(X✝ : StructuredArrow X (Comma.map α β))
:
⋯ = ⋯
@[simp]
theorem
CategoryTheory.StructuredArrow.commaMapEquivalenceUnitIso_hom_app_right_left
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : Type u₃}
[Category.{v₃, u₃} T]
{L : Functor C T}
{R : Functor D T}
{C' : Type u₄}
[Category.{v₄, u₄} C']
{D' : Type u₅}
[Category.{v₅, u₅} D']
{T' : Type u₆}
[Category.{u₆, u₆} T']
{L' : Functor C' T'}
{R' : Functor D' T'}
{F₁ : Functor C C'}
{F₂ : Functor D D'}
{F : Functor T T'}
(α : F₁.comp L' ⟶ L.comp F)
(β : R.comp F ⟶ F₂.comp R')
[IsIso β]
(X : Comma L' R')
(X✝ : StructuredArrow X (Comma.map α β))
:
((commaMapEquivalenceUnitIso α β X).hom.app X✝).right.left = CategoryStruct.id X✝.right.left
@[simp]
theorem
CategoryTheory.StructuredArrow.commaMapEquivalenceUnitIso_hom_app_right_right
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : Type u₃}
[Category.{v₃, u₃} T]
{L : Functor C T}
{R : Functor D T}
{C' : Type u₄}
[Category.{v₄, u₄} C']
{D' : Type u₅}
[Category.{v₅, u₅} D']
{T' : Type u₆}
[Category.{u₆, u₆} T']
{L' : Functor C' T'}
{R' : Functor D' T'}
{F₁ : Functor C C'}
{F₂ : Functor D D'}
{F : Functor T T'}
(α : F₁.comp L' ⟶ L.comp F)
(β : R.comp F ⟶ F₂.comp R')
[IsIso β]
(X : Comma L' R')
(X✝ : StructuredArrow X (Comma.map α β))
:
((commaMapEquivalenceUnitIso α β X).hom.app X✝).right.right = CategoryStruct.id X✝.right.right
@[simp]
theorem
CategoryTheory.StructuredArrow.commaMapEquivalenceUnitIso_inv_app_left_down_down
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : Type u₃}
[Category.{v₃, u₃} T]
{L : Functor C T}
{R : Functor D T}
{C' : Type u₄}
[Category.{v₄, u₄} C']
{D' : Type u₅}
[Category.{v₅, u₅} D']
{T' : Type u₆}
[Category.{u₆, u₆} T']
{L' : Functor C' T'}
{R' : Functor D' T'}
{F₁ : Functor C C'}
{F₂ : Functor D D'}
{F : Functor T T'}
(α : F₁.comp L' ⟶ L.comp F)
(β : R.comp F ⟶ F₂.comp R')
[IsIso β]
(X : Comma L' R')
(X✝ : StructuredArrow X (Comma.map α β))
:
⋯ = ⋯
def
CategoryTheory.StructuredArrow.commaMapEquivalenceCounitIso
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : Type u₃}
[Category.{v₃, u₃} T]
{L : Functor C T}
{R : Functor D T}
{C' : Type u₄}
[Category.{v₄, u₄} C']
{D' : Type u₅}
[Category.{v₅, u₅} D']
{T' : Type u₆}
[Category.{u₆, u₆} T']
{L' : Functor C' T'}
{R' : Functor D' T'}
{F₁ : Functor C C'}
{F₂ : Functor D D'}
{F : Functor T T'}
(α : F₁.comp L' ⟶ L.comp F)
(β : R.comp F ⟶ F₂.comp R')
[IsIso β]
(X : Comma L' R')
:
(commaMapEquivalenceInverse α β X).comp (commaMapEquivalenceFunctor α β X) ≅ Functor.id (Comma (map₂ (CategoryStruct.id (L'.obj X.left)) α) (map₂ X.hom (inv β)))
The counit functor establishing the equivalence StructuredArrow.commaMapEquivalence.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.StructuredArrow.commaMapEquivalenceCounitIso_hom_app_left_left_down_down
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : Type u₃}
[Category.{v₃, u₃} T]
{L : Functor C T}
{R : Functor D T}
{C' : Type u₄}
[Category.{v₄, u₄} C']
{D' : Type u₅}
[Category.{v₅, u₅} D']
{T' : Type u₆}
[Category.{u₆, u₆} T']
{L' : Functor C' T'}
{R' : Functor D' T'}
{F₁ : Functor C C'}
{F₂ : Functor D D'}
{F : Functor T T'}
(α : F₁.comp L' ⟶ L.comp F)
(β : R.comp F ⟶ F₂.comp R')
[IsIso β]
(X : Comma L' R')
(X✝ : Comma (map₂ (CategoryStruct.id (L'.obj X.left)) α) (map₂ X.hom (inv β)))
:
⋯ = ⋯
@[simp]
theorem
CategoryTheory.StructuredArrow.commaMapEquivalenceCounitIso_inv_app_right_left_down_down
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : Type u₃}
[Category.{v₃, u₃} T]
{L : Functor C T}
{R : Functor D T}
{C' : Type u₄}
[Category.{v₄, u₄} C']
{D' : Type u₅}
[Category.{v₅, u₅} D']
{T' : Type u₆}
[Category.{u₆, u₆} T']
{L' : Functor C' T'}
{R' : Functor D' T'}
{F₁ : Functor C C'}
{F₂ : Functor D D'}
{F : Functor T T'}
(α : F₁.comp L' ⟶ L.comp F)
(β : R.comp F ⟶ F₂.comp R')
[IsIso β]
(X : Comma L' R')
(X✝ : Comma (map₂ (CategoryStruct.id (L'.obj X.left)) α) (map₂ X.hom (inv β)))
:
⋯ = ⋯
@[simp]
theorem
CategoryTheory.StructuredArrow.commaMapEquivalenceCounitIso_hom_app_right_right
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : Type u₃}
[Category.{v₃, u₃} T]
{L : Functor C T}
{R : Functor D T}
{C' : Type u₄}
[Category.{v₄, u₄} C']
{D' : Type u₅}
[Category.{v₅, u₅} D']
{T' : Type u₆}
[Category.{u₆, u₆} T']
{L' : Functor C' T'}
{R' : Functor D' T'}
{F₁ : Functor C C'}
{F₂ : Functor D D'}
{F : Functor T T'}
(α : F₁.comp L' ⟶ L.comp F)
(β : R.comp F ⟶ F₂.comp R')
[IsIso β]
(X : Comma L' R')
(X✝ : Comma (map₂ (CategoryStruct.id (L'.obj X.left)) α) (map₂ X.hom (inv β)))
:
((commaMapEquivalenceCounitIso α β X).hom.app X✝).right.right = CategoryStruct.id X✝.right.right
@[simp]
theorem
CategoryTheory.StructuredArrow.commaMapEquivalenceCounitIso_hom_app_left_right
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : Type u₃}
[Category.{v₃, u₃} T]
{L : Functor C T}
{R : Functor D T}
{C' : Type u₄}
[Category.{v₄, u₄} C']
{D' : Type u₅}
[Category.{v₅, u₅} D']
{T' : Type u₆}
[Category.{u₆, u₆} T']
{L' : Functor C' T'}
{R' : Functor D' T'}
{F₁ : Functor C C'}
{F₂ : Functor D D'}
{F : Functor T T'}
(α : F₁.comp L' ⟶ L.comp F)
(β : R.comp F ⟶ F₂.comp R')
[IsIso β]
(X : Comma L' R')
(X✝ : Comma (map₂ (CategoryStruct.id (L'.obj X.left)) α) (map₂ X.hom (inv β)))
:
((commaMapEquivalenceCounitIso α β X).hom.app X✝).left.right = CategoryStruct.id X✝.left.right
@[simp]
theorem
CategoryTheory.StructuredArrow.commaMapEquivalenceCounitIso_inv_app_left_right
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : Type u₃}
[Category.{v₃, u₃} T]
{L : Functor C T}
{R : Functor D T}
{C' : Type u₄}
[Category.{v₄, u₄} C']
{D' : Type u₅}
[Category.{v₅, u₅} D']
{T' : Type u₆}
[Category.{u₆, u₆} T']
{L' : Functor C' T'}
{R' : Functor D' T'}
{F₁ : Functor C C'}
{F₂ : Functor D D'}
{F : Functor T T'}
(α : F₁.comp L' ⟶ L.comp F)
(β : R.comp F ⟶ F₂.comp R')
[IsIso β]
(X : Comma L' R')
(X✝ : Comma (map₂ (CategoryStruct.id (L'.obj X.left)) α) (map₂ X.hom (inv β)))
:
((commaMapEquivalenceCounitIso α β X).inv.app X✝).left.right = CategoryStruct.id X✝.left.right
@[simp]
theorem
CategoryTheory.StructuredArrow.commaMapEquivalenceCounitIso_inv_app_right_right
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : Type u₃}
[Category.{v₃, u₃} T]
{L : Functor C T}
{R : Functor D T}
{C' : Type u₄}
[Category.{v₄, u₄} C']
{D' : Type u₅}
[Category.{v₅, u₅} D']
{T' : Type u₆}
[Category.{u₆, u₆} T']
{L' : Functor C' T'}
{R' : Functor D' T'}
{F₁ : Functor C C'}
{F₂ : Functor D D'}
{F : Functor T T'}
(α : F₁.comp L' ⟶ L.comp F)
(β : R.comp F ⟶ F₂.comp R')
[IsIso β]
(X : Comma L' R')
(X✝ : Comma (map₂ (CategoryStruct.id (L'.obj X.left)) α) (map₂ X.hom (inv β)))
:
((commaMapEquivalenceCounitIso α β X).inv.app X✝).right.right = CategoryStruct.id X✝.right.right
@[simp]
theorem
CategoryTheory.StructuredArrow.commaMapEquivalenceCounitIso_hom_app_right_left_down_down
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : Type u₃}
[Category.{v₃, u₃} T]
{L : Functor C T}
{R : Functor D T}
{C' : Type u₄}
[Category.{v₄, u₄} C']
{D' : Type u₅}
[Category.{v₅, u₅} D']
{T' : Type u₆}
[Category.{u₆, u₆} T']
{L' : Functor C' T'}
{R' : Functor D' T'}
{F₁ : Functor C C'}
{F₂ : Functor D D'}
{F : Functor T T'}
(α : F₁.comp L' ⟶ L.comp F)
(β : R.comp F ⟶ F₂.comp R')
[IsIso β]
(X : Comma L' R')
(X✝ : Comma (map₂ (CategoryStruct.id (L'.obj X.left)) α) (map₂ X.hom (inv β)))
:
⋯ = ⋯
@[simp]
theorem
CategoryTheory.StructuredArrow.commaMapEquivalenceCounitIso_inv_app_left_left_down_down
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : Type u₃}
[Category.{v₃, u₃} T]
{L : Functor C T}
{R : Functor D T}
{C' : Type u₄}
[Category.{v₄, u₄} C']
{D' : Type u₅}
[Category.{v₅, u₅} D']
{T' : Type u₆}
[Category.{u₆, u₆} T']
{L' : Functor C' T'}
{R' : Functor D' T'}
{F₁ : Functor C C'}
{F₂ : Functor D D'}
{F : Functor T T'}
(α : F₁.comp L' ⟶ L.comp F)
(β : R.comp F ⟶ F₂.comp R')
[IsIso β]
(X : Comma L' R')
(X✝ : Comma (map₂ (CategoryStruct.id (L'.obj X.left)) α) (map₂ X.hom (inv β)))
:
⋯ = ⋯
def
CategoryTheory.StructuredArrow.commaMapEquivalence
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{T : Type u₃}
[Category.{v₃, u₃} T]
{L : Functor C T}
{R : Functor D T}
{C' : Type u₄}
[Category.{v₄, u₄} C']
{D' : Type u₅}
[Category.{v₅, u₅} D']
{T' : Type u₆}
[Category.{u₆, u₆} T']
{L' : Functor C' T'}
{R' : Functor D' T'}
{F₁ : Functor C C'}
{F₂ : Functor D D'}
{F : Functor T T'}
(α : F₁.comp L' ⟶ L.comp F)
(β : R.comp F ⟶ F₂.comp R')
[IsIso β]
(X : Comma L' R')
:
StructuredArrow X (Comma.map α β) ≌ Comma (map₂ (CategoryStruct.id (L'.obj X.left)) α) (map₂ X.hom (inv β))
The structured arrow category on the functor Comma.map α β, with β a natural isomorphism,
is equivalent to a comma category on two instances of StructuredArrow.map₂.
Equations
- One or more equations did not get rendered due to their size.