homTensorHomMap — Mathlib

English

If f and g are linear equivalences, then congr f g applied to m ⊗ n yields f m ⊗ g n.

Русский

Если f и g — линейные эквивалентности, то congr f g применённое к m ⊗ n даёт f(m) ⊗ g(n).

LaTeX

$$$\mathrm{congr} f g (m \otimes n) = f(m) \otimes g(n)$$$

Lean4

/-- Heterobasic version of `TensorProduct.homTensorHomMap` -/
def homTensorHomMap : ((M →ₗ[A] P) ⊗[R] (N →ₗ[R] Q)) →ₗ[B] (M ⊗[R] N →ₗ[A] P ⊗[R] Q) :=
  lift <| mapBilinear R A B M N P Q

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