directSumLeft_tmul_lof — Mathlib

English

The symmetric inverse of directSum distributes so that (directSum R S M₁ M₂).symm (DirectSum.lof (i₁,i₂) (m₁ ⊗ m₂)) equals DirectSum.lof i₁ m₁ ⊗ DirectSum.lof i₂ m₂.

Русский

Обратное симметрично распределяет: симметрическое отображение DirectSumLoF переводит прямой элемент в тензорный элемент.

LaTeX

$$$$ (\\mathrm{TensorProduct.directSum}\\, R\\, S\\, M_1\\, M_2).symm\\ (\\mathrm{DirectSum.lof}\\ S\\ (ι_1 × ι_2)\\ (i_1,i_2)\\ (m_1 ⊗ m_2)) = (\\mathrm{DirectSum.lof}\\ S\\ ι_1\\ M_1\\ i_1\\ m_1 ⊗ m_2). $$$$

Lean4

@[simp]
theorem directSumLeft_tmul_lof (i : ι₁) (x : M₁ i) (y : M₂') :
    directSumLeft R M₁ M₂' (DirectSum.lof R _ _ i x ⊗ₜ[R] y) = DirectSum.lof R _ _ i (x ⊗ₜ[R] y) :=
  by
  dsimp only [directSumLeft, LinearEquiv.ofLinear_apply, lift.tmul]
  rw [DirectSum.toModule_lof R i]
  rfl

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