toHopfAlgEquiv_toBialgHom — Mathlib

English

The forgetful functor from HopfAlgCat R to its associated algebraic category reflects isomorphisms: if a morphism becomes an isomorphism after forgetting, it was already an isomorphism in HopfAlgCat.

Русский

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

LaTeX

$$$(\text{forget}_{HopfAlgCat}) \text{ReflectsIsomorphisms}$$$

Lean4

@[simp]
theorem toHopfAlgEquiv_toBialgHom (i : X ≅ Y) : (i.toHopfAlgEquiv : X →ₐc[R] Y) = i.hom.1 :=
  rfl

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