triangleIso — Mathlib

English

Triangle coherence in functor categories: (associator F Id B G).hom ∘ whiskerLeft F (leftUnitor G).hom equals whiskerRight (rightUnitor F).hom G.

Русский

Треугольная когерентность в категориях функторов: (ассоциатор F Id B G).hom ∘ whiskerLeft F (leftUnitor G).hom = whiskerRight (rightUnitor F).hom G.

LaTeX

$$$\\bigl(\\mathrm{associator}\\;F\\;\\mathrm{(Id}_B)\\;G\\bigr).hom \\;\\circ\\; \\mathrm{whiskerLeft}\\,F\\,\\bigl(\\mathrm{leftUnitor}\\,G\\bigr).hom = \\mathrm{whiskerRight}\\,\\bigl(\\mathrm{rightUnitor}\\,F\\bigr).hom\\,G.$$$

Lean4

@[reassoc]
theorem triangleIso : associator F (𝟭 B) G ≪≫ isoWhiskerLeft F (leftUnitor G) = isoWhiskerRight (rightUnitor F) G := by
  cat_disch

Похожие утверждения