forget_reflects_isos — Mathlib

English

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

Русский

Забывающий функтор CommMonCat отражает изоморфизмы.

LaTeX

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

Lean4

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

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