Theorems · Theorem · category theory

CategoryTheory.Join.mapIsoWhiskerLeft_inv_app

∀ {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] {E' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} E'] (H : CategoryTheory.Functor C E) {Fᵣ Gᵣ : CategoryTheory.Functor D E'}
  (α : Fᵣ ≅ Gᵣ) (x : CategoryTheory.Join C D),
  (CategoryTheory.Join.mapIsoWhiskerLeft H α).inv.app x =
    match x with
    | CategoryTheory.Join.left x => CategoryTheory.CategoryStruct.id (CategoryTheory.Join.left (H.obj x))
    | CategoryTheory.Join.right x => (CategoryTheory.Join.inclRight E E').map (α.inv.app x)

Defined in

Mathlib.CategoryTheory.Join.Basic

Cited by

4 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Category