English
Auxiliary smul on a basic representative is given by the canonical tmul: SMul.aux r (.of (m, n)) = (r • m) ⊗ n.
Русский
Вспомогательное действие скаляра на базовом представителе задаётся каноническим tmul: SMul.aux r (.of (m,n)) = (r•m) ⊗ n.
LaTeX
$$$ \\mathrm{SMul}.\\mathrm{aux} \\, r \\, (\\mathrm{of}(m,n)) = (r \\cdot m) \\otimes_R n. $$$
Lean4
/-- Given two modules over a commutative semiring `R`, if one of the factors carries a
(distributive) action of a second type of scalars `R'`, which commutes with the action of `R`, then
the tensor product (over `R`) carries an action of `R'`.
This instance defines this `R'` action in the case that it is the left module which has the `R'`
action. Two natural ways in which this situation arises are:
* Extension of scalars
* A tensor product of a group representation with a module not carrying an action
Note that in the special case that `R = R'`, since `R` is commutative, we just get the usual scalar
action on a tensor product of two modules. This special case is important enough that, for
performance reasons, we define it explicitly below. -/
instance leftHasSMul : SMul R' (M ⊗[R] N) :=
⟨fun r =>
(addConGen (TensorProduct.Eqv R M N)).lift (SMul.aux r : _ →+ M ⊗[R] N) <|
AddCon.addConGen_le fun x y hxy =>
match x, y, hxy with
| _, _, .of_zero_left n => (AddCon.ker_rel _).2 <| by simp_rw [map_zero, SMul.aux_of, smul_zero, zero_tmul]
| _, _, .of_zero_right m => (AddCon.ker_rel _).2 <| by simp_rw [map_zero, SMul.aux_of, tmul_zero]
| _, _, .of_add_left m₁ m₂ n => (AddCon.ker_rel _).2 <| by simp_rw [map_add, SMul.aux_of, smul_add, add_tmul]
| _, _, .of_add_right m n₁ n₂ => (AddCon.ker_rel _).2 <| by simp_rw [map_add, SMul.aux_of, tmul_add]
| _, _, .of_smul s m n => (AddCon.ker_rel _).2 <| by rw [SMul.aux_of, SMul.aux_of, ← smul_comm, smul_tmul]
| _, _, .add_comm x y => (AddCon.ker_rel _).2 <| by simp_rw [map_add, add_comm]⟩
