English
If M is an R–A–B bimodule with commuting actions of A and B, then M has a natural structure as a module over the tensor product A ⊗_R B, defined by (a ⊗ b) • m = a • b • m.
Русский
Пусть M является модулем над R, на который действуют алгебры A и B слева, причем их действия коммутируют; тогда M естественно является модулем над тензорным произведением A ⊗_R B, действие задано (a ⊗ b) • m = a • (b • m).
LaTeX
$$$M\\text{ is a } (A\\otimes_R B)\\text{-module with } (a\\otimes b)\\cdot m := a\\cdot(b\\cdot m).$$$
Lean4
/-- If `M` is a representation of two different `R`-algebras `A` and `B` whose actions commute,
then it is a representation the `R`-algebra `A ⊗[R] B`.
An important example arises from a semiring `S`; allowing `S` to act on itself via left and right
multiplication, the roles of `R`, `A`, `B`, `M` are played by `ℕ`, `S`, `Sᵐᵒᵖ`, `S`. This example
is important because a submodule of `S` as a `Module` over `S ⊗[ℕ] Sᵐᵒᵖ` is a two-sided ideal.
NB: This is not an instance because in the case `B = A` and `M = A ⊗[R] A` we would have a diamond
of `smul` actions. Furthermore, this would not be a mere definitional diamond but a true
mathematical diamond in which `A ⊗[R] A` had two distinct scalar actions on itself: one from its
multiplication, and one from this would-be instance. Arguably we could live with this but in any
case the real fix is to address the ambiguity in notation, probably along the lines outlined here:
https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.234773.20base.20change/near/240929258
-/
protected def module : Module (A ⊗[R] B) M where
smul x m := moduleAux x m
zero_smul m := by simp only [(· • ·), map_zero, LinearMap.zero_apply]
smul_zero x := by simp only [(· • ·), map_zero]
smul_add x m₁ m₂ := by simp only [(· • ·), map_add]
add_smul x y m := by simp only [(· • ·), map_add, LinearMap.add_apply]
one_smul
m := by
-- Porting note: was one `simp only`, not two
simp only [(· • ·), Algebra.TensorProduct.one_def]
simp only [moduleAux_apply, one_smul]
mul_smul x y
m := by
refine TensorProduct.induction_on x ?_ ?_ ?_ <;> refine TensorProduct.induction_on y ?_ ?_ ?_
· simp only [(· • ·), mul_zero, map_zero, LinearMap.zero_apply]
· intro a b
simp only [(· • ·), zero_mul, map_zero, LinearMap.zero_apply]
· intro z w _ _
simp only [(· • ·), zero_mul, map_zero, LinearMap.zero_apply]
· intro a b
simp only [(· • ·), mul_zero, map_zero, LinearMap.zero_apply]
· intro a₁ b₁ a₂ b₂
simp only [(· • ·), Algebra.TensorProduct.tmul_mul_tmul]
simp only [moduleAux_apply, mul_smul, smul_comm a₁ b₂]
· intro z w hz hw a b
simp only [(· • ·)] at hz hw ⊢
simp only [moduleAux_apply, mul_add, LinearMap.map_add, LinearMap.add_apply, moduleAux_apply, hz, hw]
· intro z w _ _
simp only [(· • ·), mul_zero, map_zero, LinearMap.zero_apply]
· intro a b z w hz hw
simp only [(· • ·)] at hz hw ⊢
simp only [LinearMap.map_add, add_mul, LinearMap.add_apply, hz, hw]
· intro u v _ _ z w hz hw
simp only [(· • ·)] at hz hw ⊢
simp only [add_mul, LinearMap.map_add, LinearMap.add_apply, hz, hw, add_add_add_comm]
