mulMap_comm_of_commute — Mathlib

English

If every pair m ∈ M and n ∈ N commute in S, then N.mulMap M equals M.mulMap N composed with the commutativity isomorphism on the tensor product.

Русский

Если для всех m ∈ M, n ∈ N элементы S коммутируют, то N.mulMap M равен M.mulMap N, композиция с изоморфизмом коммутативности тензорного произведения.

LaTeX

$$$\forall m \in M, n \in N,\ Commute(m, n) \Rightarrow N.mulMap M = M.mulMap N \circ TensorProduct.comm R N M$$$

Lean4

theorem mulMap_comm_of_commute (hc : ∀ (m : M) (n : N), Commute m.1 n.1) :
    mulMap N M = mulMap M N ∘ₗ TensorProduct.comm R N M :=
  by
  refine TensorProduct.ext' fun n m ↦ ?_
  simp_rw [LinearMap.comp_apply, LinearEquiv.coe_coe, TensorProduct.comm_tmul, mulMap_tmul]
  exact (hc m n).symm

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