left_triangle_hom — Mathlib

English

For an equivalence e, the left zigzag of unit and counit equals the left unitor hom composed with the right unitor inv.

Русский

Для эквивалентности e левая зигзагообразная конструкция единицы и counit равна композиции (λ_e.hom) с (ρ_e.hom)^{-1}.

LaTeX

$$$\\text{leftZigzag } e.unit.hom\\, e.counit.hom = (\\lambda_{e.hom}).hom \\; \\circ \\; (\\rho_{e.hom}).inv$$$

Lean4

theorem left_triangle_hom (e : a ≌ b) : leftZigzag e.unit.hom e.counit.hom = (λ_ e.hom).hom ≫ (ρ_ e.hom).inv :=
  congrArg Iso.hom e.left_triangle

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