forgetReflectIsos — Mathlib

English

The forgetful functor reflects isomorphisms: if the forgetful image of a morphism is an isomorphism, then the original morphism is an isomorphism in SemiRingCat.

Русский

Функтор забывания отражает изоморфизмы: если изображение морфизма под забывающим функтором является изоморфизмом, то сам морфизм в SemiRingCat также является изоморфизмом.

LaTeX

$$$ (\mathrm{forget SemiRingCat}).\mathrm{ReflectsIsomorphisms}. $$$

Lean4

instance forgetReflectIsos : (forget SemiRingCat).ReflectsIsomorphisms where
  reflects {X Y} f
    _ := by
    let i := asIso ((forget SemiRingCat).map f)
    let ff : X →+* Y := f.hom
    let e : X ≃+* Y := { ff, i.toEquiv with }
    exact e.toSemiRingCatIso.isIso_hom

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