English
If each A_i is an algebra over R and there is an algebra structure over R' mapping into the PiTensorProduct, then PiTensorProduct is an R'-algebra.
Русский
Если каждая A_i — алгебра над R, и имеется структура алгебры над R' в PiTensorProduct, то PiTensorProduct является R'-алгеброй.
LaTeX
$$$Algebra\\ R'\\ (\\ PiTensorProduct R f i => A_i)$$$
Lean4
theorem algebraMap_apply (r : R') (i : ι) [DecidableEq ι] :
algebraMap R' (⨂[R] i, A i) r = tprod R (Pi.mulSingle i (algebraMap R' (A i) r)) :=
by
change r • tprod R 1 = _
have : Pi.mulSingle i (algebraMap R' (A i) r) = update (fun i ↦ 1) i (r • 1) := by
rw [Algebra.algebraMap_eq_smul_one]; rfl
rw [this, ← smul_one_smul R r (1 : A i), MultilinearMap.map_update_smul, update_eq_self, smul_one_smul, Pi.one_def]
