English
Let X be a topological space and Y, Z be Y- and Z-modules over a ring R. For any R-linear map f : Y →ₗ[R] Z, the pointwise application φ ↦ f ∘ φ sends LocallyConstant(X,Y) to LocallyConstant(X,Z) and defines a linear map LocallyConstant(X,Y) → LocallyConstant(X,Z).
Русский
Пусть X — топологическое пространство, Y и Z — модули над кольцом R. Для любого R-линейного отображения f : Y →ₗ[R] Z отображение φ ↦ f ∘ φ отправляет LocallyConstant(X,Y) в LocallyConstant(X,Z) и образует линейное отображение LocallyConstant(X,Y) → LocallyConstant(X,Z).
LaTeX
$$$(\\operatorname{map}_{\\ell}(f)) : \\operatorname{LocallyConstant}(X,Y) \\to_{R} \\operatorname{LocallyConstant}(X,Z), \\quad (\\operatorname{map}_{\\ell}(f))(\\varphi) = f \\circ \\varphi.$$$
Lean4
/-- `LocallyConstant.map` as a linear map. -/
@[simps!]
def mapₗ (R : Type*) [Semiring R] [AddCommMonoid Y] [Module R Y] [AddCommMonoid Z] [Module R Z] (f : Y →ₗ[R] Z) :
LocallyConstant X Y →ₗ[R] LocallyConstant X Z
where
toFun := map f
map_add' := by aesop
map_smul' := by aesop
