English
The mapAlongMonoidHom preserves the monoid operation; i.e., it is a monoid homomorphism between restricted products.
Русский
Отображение mapAlongMonoidHom сохраняет операцию умножения; оно является гомоморфизмом моноидов между ограниченными произведениями.
LaTeX
$$$\\operatorname{mapAlongMonoidHom}(x \\cdot y) = \\operatorname{mapAlongMonoidHom}(x) \\cdot \\operatorname{mapAlongMonoidHom}(y).$$$
Lean4
/-- Given two restricted products of rings `Πʳ (i : ι₁), [R₁ i, B₁ i]_[𝓕₁]` and
`Πʳ (j : ι₂), [R₂ j, B₂ j]_[𝓕₂]`, `RestrictedProduct.mapAlongRingHom` gives a
ring homomorphism between them. The data needed is a
function `f : ι₂ → ι₁` such that `𝓕₂` tends to `𝓕₁` along `f`, and ring homomorphisms
`φ j : R₁ (f j) → R₂ j` sending `B₁ (f j)` into `B₂ j` for an `𝓕₂`-large set of `j`'s.
-/
def mapAlongRingHom : Πʳ i, [R₁ i, B₁ i]_[𝓕₁] →+* Πʳ j, [R₂ j, B₂ j]_[𝓕₂]
where
__ := mapAlongMonoidHom R₁ R₂ f hf (fun j ↦ φ j) hφ
__ := mapAlongAddMonoidHom R₁ R₂ f hf (fun j ↦ φ j) hφ
