English
Given a family of monoid homomorphisms φ_j : R₁(f(j)) → R₂(j) that map the restricted submonoids B₁(f(j)) into B₂(j) for a large set of j, there is a monoid homomorphism between the restricted products, built coordinatewise using φ_j.
Русский
Пусть дано семейство гомоморфизмов мономодов φ_j: R₁(f(j)) → R₂(j), которые отображают B₁(f(j)) в B₂(j) для почти всех j; существует моноидное отображение между ограниченными произведениями, определяемое по координатам φ_j.
LaTeX
$$$\\operatorname{mapAlongMonoidHom} : \\prod^{\\mathrm{r}} i, [R_1 i, B_1 i]_{\\mathcal F_1} \\to^* \\prod^{\\mathrm{r}} j, [R_2 j, B_2 j]_{\\mathcal F_2}$ with $\\operatorname{toFun}(x) = \\operatorname{mapAlong} R_1 R_2 f hf (\\varphi_j) h_\\varphi (x)$, and this is a monoid homomorphism.$$
Lean4
/-- Given two restricted products `Πʳ (i : ι₁), [R₁ i, B₁ i]_[𝓕₁]` and `Πʳ (j : ι₂), [R₂ j, B₂ j]_[𝓕₂]`
of monoids, `RestrictedProduct.mapAlongMonoidHom` gives a monoid homomorphism between them.
The data needed is a function `f : ι₂ → ι₁` such that `𝓕₂` tends to `𝓕₁` along `f`, and monoid
homomorphisms `φ j : R₁ (f j) → R₂ j` sending `B₁ (f j)` into `B₂ j` for an `𝓕₂`-large set of `j`'s.
-/
@[to_additive /-- Given two restricted products `Πʳ (i : ι₁), [R₁ i, B₁ i]_[𝓕₁]` and
`Πʳ (j : ι₂), [R₂ j, B₂ j]_[𝓕₂]` of additive monoids, `RestrictedProduct.mapAlongAddMonoidHom`
gives a additive monoid homomorphism between them. The data needed is a function `f : ι₂ → ι₁` such
that `𝓕₂` tends to `𝓕₁` along `f`, and additive monoid homomorphisms `φ j : R₁ (f j) → R₂ j`
sending `B₁ (f j)` into `B₂ j` for an `𝓕₂`-large set of `j`'s. -/
]
def mapAlongMonoidHom : Πʳ i, [R₁ i, B₁ i]_[𝓕₁] →* Πʳ j, [R₂ j, B₂ j]_[𝓕₂]
where
toFun := mapAlong R₁ R₂ f hf (fun j r ↦ φ j r) hφ
map_one' := by
ext i
exact map_one (φ i)
map_mul' x
y := by
ext i
exact map_mul (φ i) _ _
