leftZigzagIso_symm — Mathlib

English

The left zigzag iso is symmetric to the right zigzag iso under inversion: leftZigzagIso η ε = (rightZigzagIso ε.symm η.symm)^{-1}.

Русский

Левый зигзаг-изоморфизм симметричен правому зигзаг-изоморфизму при взятии сопряжённых: leftZigzagIso η ε = (rightZigzagIso ε.symm η.symm)^{-1}.

LaTeX

$$$$ \text{leftZigzagIso } \eta \varepsilon = \big( \text{rightZigzagIso } \varepsilon^{\mathrm{symm}} \eta^{\mathrm{symm}} \big)^{-1}, $$$$

Lean4

@[simp]
theorem leftZigzagIso_symm : (leftZigzagIso η ε).symm = rightZigzagIso ε.symm η.symm :=
  Iso.ext (leftZigzagIso_inv η ε)

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