tensorHom_toLinearMap — Mathlib

English

The comultiplication on the tensor of two coalgebras equals the tensor product of their comultiplications, via a natural isomorphism.

Русский

Коалгебраическая композиция тензора двух коалгебр эквивалентна тензорному произведению их комуляций через естественный изоморфизм.

LaTeX

$$$$ \text{Coalgebra.comul}(R)(A := (K \otimes L)) = (TensorProduct.tensorTensorTensorComm R K K L L).toLinearMap \circ_ℓ TensorProduct.map Coalgebra.comul Coalgebra.comul. $$$$

Lean4

theorem tensorHom_toLinearMap (f : M →ₗc[R] N) (g : P →ₗc[R] Q) :
    (CoalgCat.ofHom f ⊗ₘ CoalgCat.ofHom g).1.toLinearMap = TensorProduct.map f.toLinearMap g.toLinearMap :=
  rfl

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