directSumRight — Mathlib

English

A variant of the previous result for the left distribution, expressed through the directSumLeft equivalence.

Русский

Вариант предыдущего результата для левого распределения через эквивалентность directSumLeft.

LaTeX

$$$$ \\mathrm{TensorProduct.directSumLeft}\\, R\\, M_1\\, M_2'\\ (\\mathrm{DirectSum.lof}\\ R\\ ι_1\\ M_1\\ i\\ x \\otimes_R y) = \\mathrm{DirectSum.lof}\\ R\\ ι_1\\ (fun i \\mapsto M_1 i)\\ i\\ (x \\otimes_R y). $$$$

Lean4

/-- Tensor products distribute over a direct sum on the right. -/
def directSumRight : (M₁' ⊗[R] ⨁ i, M₂ i) ≃ₗ[R] ⨁ i, M₁' ⊗[R] M₂ i :=
  TensorProduct.comm R _ _ ≪≫ₗ directSumLeft R M₂ M₁' ≪≫ₗ
    DFinsupp.mapRange.linearEquiv fun _ => TensorProduct.comm R _ _

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