English
Under compatible scalar actions, the PiTensorProduct inherits an algebra over the larger base ring, respecting the tower of scalars.
Русский
При совместимом скалярном действии PiTensorProduct наследует алгебру над большим основанием и сохраняет башню скаляров.
LaTeX
$$$Algebra\\ R'\\ (\\ ⨂[R] i, A i)$$$
Lean4
instance instAlgebra : Algebra R' (⨂[R] i, A i) where
__ := hasSMul'
algebraMap :=
{ toFun := (· • 1)
map_one' := by simp
map_mul' r
s :=
show (r * s) • 1 = mul (r • 1) (s • 1)
by
rw [LinearMap.map_smul_of_tower, LinearMap.map_smul_of_tower, LinearMap.smul_apply, mul_comm, mul_smul]
congr
change (1 : ⨂[R] i, A i) = 1 * 1
rw [mul_one]
map_zero' := by simp
map_add' := by simp [add_smul] }
commutes' r
x := by
simp only [RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk]
change mul _ _ = mul _ _
rw [LinearMap.map_smul_of_tower, LinearMap.map_smul_of_tower, LinearMap.smul_apply]
change r • (1 * x) = r • (x * 1)
rw [mul_one, one_mul]
smul_def' r
x := by
simp only [RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk]
change _ = mul _ _
rw [LinearMap.map_smul_of_tower, LinearMap.smul_apply]
change _ = r • (1 * x)
rw [one_mul]
