English
Let X be a topological space and Y, Z be monoids. For any monoid hom f : Y →* Z, the map φ ↦ f ∘ φ sends a locally constant function φ : X → Y to a locally constant function X → Z, and this construction yields a monoid hom LocallyConstant(X, Y) → LocallyConstant(X, Z).
Русский
Пусть X — топологическое пространство, Y и Z — моноиды. Для любого моноидного гомоморфизма f : Y →* Z отображение φ ↦ f ∘ φ переводит локально константную функцию φ : X → Y в локально константную функцию X → Z, и полученное отображение является моноид-гомоморфизм LocallyConstant(X, Y) → LocallyConstant(X, Z).
LaTeX
$$$(\\operatorname{mapMonoidHom}(f)) : \\operatorname{LocallyConstant}(X,Y) \\to \\operatorname{LocallyConstant}(X,Z), \\quad (\\operatorname{mapMonoidHom}(f))(\\varphi) = f \\circ \\varphi,$$$
Lean4
/-- `LocallyConstant.map` as a `MonoidHom`. -/
@[to_additive (attr := simps) /-- `LocallyConstant.map` as an `AddMonoidHom`. -/
]
def mapMonoidHom [MulOneClass Y] [MulOneClass Z] (f : Y →* Z) : LocallyConstant X Y →* LocallyConstant X Z
where
toFun := map f
map_one' := by aesop
map_mul' := by aesop
