triangle — Mathlib

English

Another triangle identity in functor categories: (associator 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\\,(\\mathrm{leftUnitor}\\;G).hom = \\mathrm{whiskerRight}\\,(\\mathrm{rightUnitor}\\;F).hom\\,G.$$$

Lean4

theorem triangle : (associator F (𝟭 B) G).hom ≫ whiskerLeft F (leftUnitor G).hom = whiskerRight (rightUnitor F).hom G :=
  by cat_disch

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