rightDualIso_id — Mathlib

English

Similarly, for X Y with an ExactPairing X Y, the leftDualIso p p is the identity on X, i.e., leftDualIso p p = Iso.refl X.

Русский

Аналогично, для X Y с ExactPairing, leftDualIso p p равен тождественному изоморфизму на X.

LaTeX

$$$\\text{leftDualIso } p p = \\mathrm{Iso}.refl\\; X$$$

Lean4

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

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