English
Let (αi)i∈I be a family of objects each equipped with a central scalar action of M. Then the Pi-type ∀i αi carries a natural central M-action defined pointwise, i.e. for all a in M and f in ∀i αi, (op a) • f = a • f, equivalently ((op a) • f)(i) = a • f(i) for all i.
Русский
Пусть для каждого индекса i из множества I задано множество αi, на каждом из которых действует центрально скалярное действие множества M. Тогда произведение по индексу i, то есть ∀i αi, будет иметь естественное центральное скалярное действие, задаваемое по координатам: для всех a∈M и f∈∏i αi имеем (op a) • f = a • f, то есть ((op a) • f)(i) = a • f(i) для всех i.
LaTeX
$$$IsCentralScalar\ M\left(\prod_{i\in I} \alpha_i\right)\quad\text{where}\quad (\mathrm{op}\,a)\cdot f = a\cdot f\text{ for all }a\in M, f\in\prod_{i\in I}\alpha_i,$ and equivalently $((\mathrm{op}\,a)\cdot f)(i)=a\cdot f(i)$ for all $i$.$$
Lean4
@[to_additive]
instance isCentralScalar [∀ i, SMul M (α i)] [∀ i, SMul Mᵐᵒᵖ (α i)] [∀ i, IsCentralScalar M (α i)] :
IsCentralScalar M (∀ i, α i) where op_smul_eq_smul _ _ := funext fun _ ↦ op_smul_eq_smul _ _
