English
The inclusion of locally constant functions into continuous ones is an algebra hom over a base ring R, preserving addition, multiplication, and scalar actions, and commuting with algebra maps.
Русский
Включение локально константных функций в непрерывные функции образует алгебра-гомоморф над R, сохраняющий сложение, умножение и скаляры, а также совместимый со структурой алгебры.
LaTeX
$$\\(LocallyConstant\\, X\\, Y \\to_A[R] C(X, Y)\\) is an R-algebra hom, preserving 1, 0, +, · and commuting with algebra maps.$$
Lean4
/-- The inclusion of locally-constant functions into continuous functions as an algebra map. -/
@[simps]
def toContinuousMapAlgHom (R : Type*) [CommSemiring R] [Semiring Y] [Algebra R Y] [IsTopologicalSemiring Y] :
LocallyConstant X Y →ₐ[R] C(X, Y) where
toFun := (↑)
map_one' := by
ext
simp
map_mul' x
y := by
ext
simp
map_zero' := by
ext
simp
map_add' x
y := by
ext
simp
commutes'
r := by
ext x
simp [Algebra.smul_def]
