reflectsIsomorphisms_forget — Mathlib

English

The forgetful functor from CommBialgCat to CommAlgCat reflects isomorphisms.

Русский

Функтор забывания из CommBialgCat в CommAlgCat отражает изоморфизмы.

LaTeX

$$$\mathrm{forget} : \mathrm{CommBialgCat}(R) \rightarrow \mathrm{CommAlgCat}(R) \text{ reflects isomorphisms}$$$

Lean4

instance reflectsIsomorphisms_forget : (forget (CommBialgCat.{u} R)).ReflectsIsomorphisms where
  reflects {X Y} f
    _ := by
    let i := asIso ((forget (CommBialgCat.{u} R)).map f)
    let e : X ≃ₐc[R] Y := { f.hom, i.toEquiv with }
    exact (isoMk e).isIso_hom

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