Theorems · Definition · category theory

CategoryTheory.StructuredArrow.commaMapEquivalence

{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {T : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} T] →
            {L : CategoryTheory.Functor C T} →
              {R : CategoryTheory.Functor D T} →
                {C' : Type u₄} →
                  [inst_3 : CategoryTheory.Category.{v₄, u₄} C'] →
                    {D' : Type u₅} →
                      [inst_4 : CategoryTheory.Category.{v₅, u₅} D'] →
                        {T' : Type u₆} →
                          [inst_5 : CategoryTheory.Category.{v₆, u₆} T'] →
                            {L' : CategoryTheory.Functor C' T'} →
                              {R' : CategoryTheory.Functor D' T'} →
                                {F₁ : CategoryTheory.Functor C C'} →
                                  {F₂ : CategoryTheory.Functor D D'} →
                                    {F : CategoryTheory.Functor T T'} →
                                      (α : F₁.comp L' ⟶ L.comp F) →
                                        (β : R.comp F ⟶ F₂.comp R') →
                                          [inst_6 : CategoryTheory.IsIso β] →
                                            (X : CategoryTheory.Comma L' R') →
                                              CategoryTheory.StructuredArrow X (CategoryTheory.Comma.map α β) ≌
                                                CategoryTheory.Comma
                                                  (CategoryTheory.StructuredArrow.map₂
                                                    (CategoryTheory.CategoryStruct.id (L'.obj X.left)) α)
                                                  (CategoryTheory.StructuredArrow.map₂ X.hom (CategoryTheory.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₂.

Defined in

Mathlib.CategoryTheory.Comma.StructuredArrow.CommaMap

Cited by

1 results in Mathlib

Foundations

Depth 37 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.IsIso