English
Let S(i) be a family of Subalgebra R-algebras over a fixed commutative semiring R, and s a set of indices. The object pi(s,t) defined coordinatewise is a Subalgebra of the product Π i S(i). In other words, the product of subalgebras is a subalgebra of the product algebra with coordinatewise structure.
Русский
Пусть имеется семейство подалгебр {S_i} над R; множество индексов i; тогда образующийся по координатам объект π(s,t) является подалгеброй в произведении ∏_i S_i, т.е. произведение подалгебр — подалгебра в произведении.
LaTeX
$$$\pi(s,t)\le \prod_i S_i$, где $\pi(s,t)$ — подалгебра произведения по координатам $t_i$.$$
Lean4
/-- The product of subalgebras as a subalgebra. -/
@[simps coe toSubsemiring]
def pi (s : Set ι) (t : ∀ i, Subalgebra R (S i)) : Subalgebra R (Π i, S i)
where
__ := Submodule.pi s fun i ↦ (t i).toSubmodule
mul_mem' hx hy i hi := (t i).mul_mem (hx i hi) (hy i hi)
algebraMap_mem' _ i _ := (t i).algebraMap_mem _
