forget_reflects_isos — Mathlib

English

The forgetful functor forget MonCat reflects isomorphisms: if a morphism becomes an isomorphism after forgetting the MonCat structure, then it was an isomorphism to begin with.

Русский

Забывающий функтор MonCat отражает изоморфизмы: если под забыванием структура MonCat превращает морфизм в изоморфизм, то он был изоморфизмом изначально.

LaTeX

$$$\text{Forget}_{MonCat}$ reflects isomorphisms.$$

Lean4

@[to_additive]
instance forget_reflects_isos : (forget MonCat.{u}).ReflectsIsomorphisms where
  reflects {X Y} f
    _ := by
    let i := asIso ((forget MonCat).map f)
    let e : X ≃* Y := { f.hom, i.toEquiv with }
    exact e.toMonCatIso.isIso_hom

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