English
Given two restricted products and a coherent map f between index sets along with coordinatewise maps φ, there is a induced mapAlong between the restricted products.
Русский
Пусть существуют два ограниченных произведения и отображение f между индексами, затем существует отображение along между ограниченными произведениями.
LaTeX
$$$\text{mapAlong}_{f}(x) = (\phi_j(x_{f(j)}))_{j}$ with appropriate coherence.$$
Lean4
/-- `RestrictedProduct.evalMonoidHom j` is the monoid homomorphism from the restricted
product `Πʳ i, [R i, B i]_[𝓕]` to the component `R j`.
-/
@[to_additive /-- `RestrictedProduct.evalAddMonoidHom j` is the monoid homomorphism from the
restricted product `Πʳ i, [R i, B i]_[𝓕]` to the component `R j`. -/
]
def evalMonoidHom (j : ι) [Π i, Monoid (R i)] [∀ i, SubmonoidClass (S i) (R i)] : (Πʳ i, [R i, B i]_[𝓕]) →* R j
where
toFun x := x j
map_one' := rfl
map_mul' _ _ := rfl
