isoOfHom_op_inv — Mathlib

English

The inverse of the isomorphism constructed in the opposite category corresponds, via op, to the inverse of the corresponding isomorphism in the original category.

Русский

Обратное изоморфизма, полученного в противоположной категории, через операцию оп равно противоположному образу обратного изоморфизма в исходной категории.

LaTeX

$$$\\text{(isoOfHom }L^{op}W^{op}w)^{-1} = (\\text{isoOfHom }L W w.unop\\,W)^{-1}.op$$$

Lean4

theorem isoOfHom_op_inv {X Y : Cᵒᵖ} (w : X ⟶ Y) (hw : W.op w) :
    (isoOfHom L.op W.op w hw).inv = (isoOfHom L W w.unop hw).inv.op :=
  congr_arg Quiver.Hom.op (congr_arg Iso.inv (isoOfHom_unop L W w hw))

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