assoc_symm_tmul — Mathlib

English

For a linear map g: P →_A P', the induced map on M ⊗_R N is obtained by composing rTensor with the associator and the base-change map: g.rTensor(M⊗N) = assoc ∘ (g.rTensor M) ∘ assoc^{-1}.

Русский

Для линейного отображения g: P →_A P' на тензорном произведении M ⊗_R N индуцированное отображение равно композиции: g.rTensor(M⊗N) = ассоциатор ∘ (g.rTensor M) ∘ ассоциатор^{-1}.

LaTeX

$$$g\mathrel{.rTensor}_{R,A} (M\otimes_R N) = \bigl\langle \text{assoc} \bigr\circ (g\rTensor M) \circ \text{assoc}^{-1}$$

Lean4

@[simp]
theorem assoc_symm_tmul (m : M) (p : P) (q : Q) : (assoc R A B M P Q).symm (m ⊗ₜ (p ⊗ₜ q)) = (m ⊗ₜ p) ⊗ₜ q :=
  rfl

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