English
Let X be a topological space and Y, Z be algebras over a commutative ring R. For any AlgHom R Y Z, the map LocallyConstant(X,Y) →LocallyConstant(X,Z) induced by composition with f is an AlgHom.
Русский
Пусть X — топологическое пространство, Y и Z — алгебры над R. Для любого AlgHom R Y Z отображение LocallyConstant(X,Y) → LocallyConstant(X,Z), задаваемое композициией с f, является AlgHom.
LaTeX
$$$(\\operatorname{map}_{\\mathsf{A}}(f)) : \\operatorname{LocallyConstant}(X,Y) \\to_{R} \\operatorname{LocallyConstant}(X,Z), \\quad (\\operatorname{map}_{\\mathsf{A}}(f))(\\varphi) = f \\circ \\varphi.$$$
Lean4
/-- `LocallyConstant.map` as an `AlgHom` -/
@[simps!]
def mapₐ (R : Type*) [CommSemiring R] [Semiring Y] [Algebra R Y] [Semiring Z] [Algebra R Z] (f : Y →ₐ[R] Z) :
LocallyConstant X Y →ₐ[R] LocallyConstant X Z
where
toRingHom := mapRingHom f
commutes' _ := by aesop
