English
The forgetful functor from CommBialgCat to a base category reflects isomorphisms: if the forgetful image of a morphism is an isomorphism, then the morphism is an isomorphism in CommBialgCat.
Русский
Функтор забывания из CommBialgCat в базовую категорию отражает изоморфизмы: если образ забывания морфизма является изоморфизмом, то сам морфизм — изоморфизм в CommBialgCat.
LaTeX
$$$\mathrm{forget} : \mathrm{CommBialgCat}(R) \to \mathrm{...} \; \text{ReflectsIsomorphisms}$$$
Lean4
/-- Build a `BialgEquiv` from an isomorphism in the category `CommBialgCat R`. -/
@[simps apply, simps -isSimp symm_apply]
def bialgEquivOfIso (i : A ≅ B) : A ≃ₐc[R] B where
__ := i.hom.hom
toFun := i.hom
invFun := i.inv
left_inv x := by simp
right_inv x := by simp
