English
From an algebra hom f: A →ₐ[R] B that preserves counit and comultiplication, there exists a bialgebra hom A →ₐc[R] B extending f and respecting counit and comultiplication.
Русский
Из алгебра-гомоморфа f: A →ₐ[R] B, сохраняющего единицу по counit и comul, существует биалгебра-гомоморф φ: A →ₐc[R] B, который расширяет f и сохраняет counit и comul.
LaTeX
$$$\exists \phi : A \to_{R}^{c} B\; (\text{such that } \phi_{\mathrm{toAlgHom}} = f \ \land\ (counit\_comp) \land\ (map\_comp\_comul)).$$$
Lean4
/-- Construct a bialgebra hom from an algebra hom respecting counit and comultiplication. -/
@[simps!]
def ofAlgHom (f : A →ₐ[R] B) (counit_comp : (counitAlgHom R B).comp f = counitAlgHom R A)
(map_comp_comul : (Algebra.TensorProduct.map f f).comp (comulAlgHom _ _) = (comulAlgHom _ _).comp f) : A →ₐc[R] B
where
__ := f
map_smul' := map_smul f
counit_comp := congr(($counit_comp).toLinearMap)
map_comp_comul := congr(($map_comp_comul).toLinearMap)
