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.{v₆, 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')
:
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.{v₆, 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)
:
@[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.{v₆, 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)
:
@[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.{v₆, 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 α β))
:
@[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.{v₆, 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 α β))
:
@[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.{v₆, 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 α β))
:
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.{v₆, 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')
:
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.{v₆, 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 β)))
:
@[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.{v₆, 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)
:
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.{v₆, 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.{v₆, 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_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.{v₆, 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.{v₆, 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_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.{v₆, 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.{v₆, 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_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.{v₆, 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_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.{v₆, 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_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.{v₆, 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.{v₆, 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.{v₆, 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')
:
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.