Theorems · Theorem · category theory

CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjPrecomposeObjSquare_iso_hom_id

∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {X : Type u₇}
  {Y : Type u₈} [inst_3 : CategoryTheory.Category.{v₇, u₇} X] [inst_4 : CategoryTheory.Category.{v₈, u₈} Y]
  (U : CategoryTheory.Functor X Y) (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CatCommSq.iso
          ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform Y).obj
            (CategoryTheory.Limits.CatCospanTransform.id F G))
          ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj U)
          ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj U)
          ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj
            (CategoryTheory.Limits.CatCospanTransform.id F G))).hom
      (((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj U).whiskerLeft
        (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjId X F G).hom) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Functor.whiskerRight
        (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjId Y F G).hom
        ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj U))
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj U).leftUnitor.hom
        ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj U).rightUnitor.inv)

The square transformObjPrecomposeObjSquare respects identities.

Defined in

Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Category