associator_hom_toLinearMap — Mathlib

English

The linear map underlying the tensor of two coalgebra morphisms equals the tensor product of their linear maps.

Русский

Линейное отображение, лежащее в основе тензорной композиции двух морфизмов коалгебр, равно тензорному произведению их линейных отображений.

LaTeX

$$$$ (f : M \to N) \otimes (g : P \to Q) \text{ under } (CoalgCat.ofHom f \otimes_ℓ CoalgCat.ofHom g).1.toLinearMap = \ TensorProduct.map f.toLinearMap g.toLinearMap. $$$$

Lean4

theorem associator_hom_toLinearMap :
    (α_ (CoalgCat.of R M) (CoalgCat.of R N) (CoalgCat.of R P)).hom.1.toLinearMap =
      (TensorProduct.assoc R M N P).toLinearMap :=
  TensorProduct.ext <| TensorProduct.ext <| by ext; rfl

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