leftZigzagIso_inv — Mathlib

English

In a bicategory with η : 1a ≅ f g and ε : g f ≅ 1b, the left zigzag inverse equals the right zigzag with inverted morphisms: leftZigzagIso η ε .inv = rightZigzag ε.inv η.inv.

Русский

В бикатегории с данными η и ε обратный левой зигзаг-изоморфизм равен правому зигзагу с инвертированными морфизмами.

LaTeX

$$$$ (leftZigzagIso \eta \epsilon).inv = rightZigzag (\epsilon^{-1}) (\eta^{-1}). $$$$

Lean4

@[simp]
theorem leftZigzagIso_inv : (leftZigzagIso η ε).inv = rightZigzag ε.inv η.inv := by
  simp [bicategoricalComp, bicategoricalIsoComp]

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