unop_inv — Mathlib

English

If f: X ⟶ Y in C^{op} is an isomorphism, then the unop of its inverse equals the inverse of its unop: (inv f)^{unop} = inv(f^{unop}).

Русский

Если f: X ⟶ Y в C^{op} является изоморфизмом, то (inv f)^{unop} = inv(f^{unop}).

LaTeX

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

Lean4

@[simp]
theorem unop_inv {X Y : Cᵒᵖ} (f : X ⟶ Y) [IsIso f] : (inv f).unop = inv f.unop :=
  by
  apply IsIso.eq_inv_of_hom_inv_id
  rw [← unop_comp, IsIso.inv_hom_id, unop_id]

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