Theorems · Definition · category theory

CategoryTheory.Join.mkNatIso

{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {E : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} E] →
            {F G : CategoryTheory.Functor (CategoryTheory.Join C D) E} →
              (eₗ : (CategoryTheory.Join.inclLeft C D).comp F ≅ (CategoryTheory.Join.inclLeft C D).comp G) →
                (eᵣ : (CategoryTheory.Join.inclRight C D).comp F ≅ (CategoryTheory.Join.inclRight C D).comp G) →
                  autoParam
                      (CategoryTheory.CategoryStruct.comp
                          (CategoryTheory.Functor.whiskerRight (CategoryTheory.Join.edgeTransform C D) F)
                          ((CategoryTheory.Prod.snd C D).isoWhiskerLeft eᵣ).hom =
                        CategoryTheory.CategoryStruct.comp ((CategoryTheory.Prod.fst C D).isoWhiskerLeft eₗ).hom
                          (CategoryTheory.Functor.whiskerRight (CategoryTheory.Join.edgeTransform C D) G))
                      CategoryTheory.Join.mkNatIso._auto_1 →
                    (F ≅ G)

Two functors out of a join of categories are naturally isomorphic if their compositions with the inclusions are isomorphic and the whiskering with the canonical transformation is respected through these isomorphisms.

Defined in

Mathlib.CategoryTheory.Join.Basic

Cited by

3 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Category