op_inv — Mathlib

English

If f: X → Y is an isomorphism in a category C, then the opposite of its inverse equals the inverse of its opposite: (inv f)^{op} = (f^{op})^{-1}.

Русский

Если f: X → Y является изоморфизмом в категории C, то (f^{-1})^{op} = (f^{op})^{-1}.

LaTeX

$$$\\\\forall C [\\\\text{Category}(C)], \\\\forall X,Y \\\\in C, \\\\forall f: X \to Y, \\\\text{IsIso}(f) \\\\Rightarrow (f^{-1})^{\\\\mathrm{op}} = (f^{\\\\mathrm{op}})^{-1}.$$$

Lean4

@[simp]
theorem op_inv {X Y : C} (f : X ⟶ Y) [IsIso f] : (inv f).op = inv f.op :=
  by
  apply IsIso.eq_inv_of_hom_inv_id
  rw [← op_comp, IsIso.inv_hom_id, op_id]

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