inv_as_inv — Mathlib

English

In the single-object category built from a group G, every morphism f has its inverse given by the group inverse. In particular, inv(f) = f^{-1} for any morphism f: x → y.

Русский

В категории с одним объектом, построенной из группы G, для любой морфизм f: x → y обратный морфизм равен обратному элементу группы: inv(f) = f^{-1}.

LaTeX

$$$\\forall x,y:\\mathrm{SingleObj}(G),\\forall f:\\mathrm{Hom}(x,y),\\ \\mathrm{inv}(f)=f^{-1}$$$

Lean4

theorem inv_as_inv {x y : SingleObj G} (f : x ⟶ y) : inv f = f⁻¹ :=
  by
  apply IsIso.inv_eq_of_hom_inv_id
  rw [comp_as_mul, inv_mul_cancel, id_as_one]

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