English
The square transformObjPrecomposeObjSquare is compatible with identity morphisms, i.e., applying the iso corresponding to 1_X yields a commutative relation involving whiskers and left/right unitors that reduces to identity in the expected coherence diagram.
Русский
Квадрат transformObjPrecomposeObjSquare совместим с единичными морфизмами: применение соответствующего изоморфизма 1_X приводит к тождественности в соответствующей диаграмме когерентности.
LaTeX
$$$ (\\text{CatCommSq}.iso (\\text{precompose } F G|>.obj 1_X) (\\text{transform X}.obj 1 ψ) (\\text{transform X}.obj 1 ψ) (\\text{precompose F' G'}.obj 1_X)).hom \\\\;\\circ \\\\; \\mathrm{whiskerLeft}((\\text{transform X}.obj ψ), (\\text{precomposeObjId } F G X).hom) =$$
Lean4
/-- The square `precomposeTransformSquare` respects compositions. -/
theorem precomposeObjTransformObjSquare_iso_hom_comp {X : Type u₇} {Y : Type u₈} {Z : Type u₉} [Category.{v₇} X]
[Category.{v₈} Y] [Category.{v₉} Z] (ψ : CatCospanTransform F G F₁ G₁) (U : X ⥤ Y) (V : Y ⥤ Z) :
(CatCommSq.iso (precompose F G |>.obj <| U ⋙ V) (transform Z |>.obj ψ) (transform X |>.obj ψ)
(precompose F₁ G₁ |>.obj <| U ⋙ V)).hom ≫
whiskerLeft (transform Z |>.obj ψ) (precomposeObjComp F₁ G₁ U V).hom =
whiskerRight (precomposeObjComp F G U V).hom (transform X |>.obj ψ) ≫
(Functor.associator _ _ _).hom ≫
whiskerLeft (precompose F G |>.obj V) (CatCommSq.iso _ (transform _ |>.obj ψ) _ _).hom ≫
(Functor.associator _ _ _).inv ≫
whiskerRight (CatCommSq.iso _ _ _ _).hom (precompose F₁ G₁ |>.obj U) ≫ (Functor.associator _ _ _).hom :=
by cat_disch
