instReflectsIsomorphismsForget — Mathlib

English

The forgetful functor forget from Center C reflects isomorphisms; the isomorphism in Center is detected by its hom component.

Русский

Забывающий функтор из центра отражает изоморфизмы; изоморфизм в центре определяется по компоненте hom.

LaTeX

$$$ (forget C).ReflectsIsomorphisms$$$

Lean4

instance : (forget C).ReflectsIsomorphisms where
  reflects f i := by dsimp at i; change IsIso (isoMk f).hom; infer_instance

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