isIso_of_f_isIso — Mathlib

English

In the center of a monoidal category, if a morphism f.f is an isomorphism, then the underlying morphism is an isomorphism; the forgetful functor reflects isomorphisms.

Русский

В центре моноидальной категории, если морфизм f.f является изоморфизмом, то базовая карта тоже изоморфизм; забывающий функтор отражает изоморфизмы.

LaTeX

$$$\\text{If } f.f \\text{ is iso, then } f \\text{ is iso}$$$

Lean4

instance isIso_of_f_isIso {X Y : Center C} (f : X ⟶ Y) [IsIso f.f] : IsIso f :=
  by
  change IsIso (isoMk f).hom
  infer_instance

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