English
The equality directSum_lof_tmul_lof expresses how the tmul of two direct sum injections distributes over the direct sum of tensor products: the left-hand side equals the right-hand side evaluated at (i1,i2).
Русский
Тождество directSum_lof_tmul_lof описывает, как tmul инъекций прямого суммирования распространяется на прямую сумму тензоров.
LaTeX
$$$$ \\mathrm{TensorProduct.directSum\\, R\\, S\\, M_1\\, M_2}\\bigl( \\mathrm{DirectSum.lof\\, S}\\ (\\iota_1\\ times\\ iota_2)\\ (i_1,i_2)\\ (m_1 \\otimes_R m_2) \\bigr) = \\mathrm{DirectSum.lof}\\ S (\\iota_1\\times \\iota_2)\\ (i_1,i_2)\\ (m_1 \\otimes_R m_2). $$$$
Lean4
/-- The linear equivalence `(⨁ i₁, M₁ i₁) ⊗ (⨁ i₂, M₂ i₂) ≃ (⨁ i₁, ⨁ i₂, M₁ i₁ ⊗ M₂ i₂)`, i.e.
"tensor product distributes over direct sum". -/
protected def directSum : ((⨁ i₁, M₁ i₁) ⊗[R] ⨁ i₂, M₂ i₂) ≃ₗ[S] ⨁ i : ι₁ × ι₂, M₁ i.1 ⊗[R] M₂ i.2 :=
by
refine LinearEquiv.ofLinear ?toFun ?invFun ?left ?right
·
exact
AlgebraTensorModule.lift <|
toModule S _ _ fun i₁ =>
flip <|
toModule R _ _ fun i₂ =>
flip <| AlgebraTensorModule.curry <| DirectSum.lof S (ι₁ × ι₂) (fun i => M₁ i.1 ⊗[R] M₂ i.2) (i₁, i₂)
· exact toModule S _ _ fun i => AlgebraTensorModule.map (lof S _ M₁ i.1) (lof R _ M₂ i.2)
· ext ⟨i₁, i₂⟩ x₁ x₂ : 4
simp only [coe_comp, Function.comp_apply, toModule_lof, AlgebraTensorModule.map_tmul,
AlgebraTensorModule.lift_apply, lift.tmul, coe_restrictScalars, flip_apply, AlgebraTensorModule.curry_apply,
curry_apply, id_comp]
· ext i₁ i₂ x₁ x₂ : 5
simp only [coe_comp, Function.comp_apply, AlgebraTensorModule.curry_apply, curry_apply, coe_restrictScalars,
AlgebraTensorModule.lift_apply, lift.tmul, toModule_lof, flip_apply, AlgebraTensorModule.map_tmul, id_coe, id_eq]
