leftDualIso_id — Mathlib

English

For any ExactPairing X Y in a monoidal category, the left dual iso p p equals the identity on X.

Русский

Для любого точного парного объекта X и Y в моноидальной категории левый двойственный изоморфизм p p равен тождественному на X.

LaTeX

$$leftDualIso p p = Iso.refl X$$

Lean4

@[simp]
theorem leftDualIso_id {X Y : C} (p : ExactPairing X Y) : leftDualIso p p = Iso.refl X :=
  by
  ext
  simp only [leftDualIso, Iso.refl_hom, @leftAdjointMate_id]

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