forget_reflects_isos — Mathlib

English

The forgetful functor from HopfAlgCat to its underlying structure reflects isomorphisms: if the underlying map is an isomorphism, then the original morphism is an isomorphism in HopfAlgCat.

Русский

Забывающий функтор отражает изоморфизмы: если отображение под забвением является изоморфизмом, то исходный морфизм в HopfAlgCat — тоже изоморфизм.

LaTeX

$$HopfAlgCat.forget_reflects_isos$$

Lean4

instance forget_reflects_isos : (forget (HopfAlgCat.{v} R)).ReflectsIsomorphisms where
  reflects {X Y} f
    _ := by
    let i := asIso ((forget (HopfAlgCat.{v} R)).map f)
    let e : X ≃ₐc[R] Y := { f.toBialgHom, i.toEquiv with }
    exact ⟨e.toHopfAlgIso.isIso_hom.1⟩

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