map_comp_comulAlgHom — Mathlib

English

If f is an AlgEquiv A ≃ₐ[R] B, then the associated linear map of the corresponding BialgEquiv equals f.

Русский

Если f — AlgEquiv A ≃ₐ[R] B, то соответствующее линейное отображение связанной BialgEquiv равно f.

LaTeX

$$$\\text{toLinearMap}(\\text{ofAlgEquiv}(f, \\dots)) = f$$$

Lean4

@[simp]
theorem map_comp_comulAlgHom (f : F) :
    (Algebra.TensorProduct.map f f).comp (comulAlgHom R A) = (comulAlgHom R B).comp f :=
  AlgHom.toLinearMap_injective (CoalgHomClass.map_comp_comul f)

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