The algebra morphism from locally constant functions to continuous functions.

def LocallyConstant.toContinuousMapMonoidHom {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [Monoid Y] [ContinuousMul Y] : LocallyConstant X Y →* C(X, Y)

The inclusion of locally-constant functions into continuous functions as a multiplicative monoid hom.

Equations

• LocallyConstant.toContinuousMapMonoidHom = { toFun := LocallyConstant.toContinuousMap, map_one' := ⋯, map_mul' := ⋯ }

def LocallyConstant.toContinuousMapAddMonoidHom {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [AddMonoid Y] [ContinuousAdd Y] : LocallyConstant X Y →+ C(X, Y)

The inclusion of locally-constant functions into continuous functions as an additive monoid hom.

Equations

• LocallyConstant.toContinuousMapAddMonoidHom = { toFun := LocallyConstant.toContinuousMap, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem LocallyConstant.toContinuousMapMonoidHom_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [Monoid Y] [ContinuousMul Y] (f : LocallyConstant X Y) : toContinuousMapMonoidHom f = ↑f

@[simp]

theorem LocallyConstant.toContinuousMapAddMonoidHom_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [AddMonoid Y] [ContinuousAdd Y] (f : LocallyConstant X Y) : toContinuousMapAddMonoidHom f = ↑f

def LocallyConstant.toContinuousMapLinearMap {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (R : Type u_3) [Semiring R] [AddCommMonoid Y] [Module R Y] [ContinuousAdd Y] [ContinuousConstSMul R Y] : LocallyConstant X Y →ₗ[R] C(X, Y)

The inclusion of locally-constant functions into continuous functions as a linear map.

Equations

• LocallyConstant.toContinuousMapLinearMap R = { toFun := LocallyConstant.toContinuousMap, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem LocallyConstant.toContinuousMapLinearMap_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (R : Type u_3) [Semiring R] [AddCommMonoid Y] [Module R Y] [ContinuousAdd Y] [ContinuousConstSMul R Y] (f : LocallyConstant X Y) : (toContinuousMapLinearMap R) f = ↑f

@[simp]

theorem LocallyConstant.toAddMonoidHom_toContinuousMapLinearMap {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (R : Type u_3) [Semiring R] [AddCommMonoid Y] [Module R Y] [ContinuousAdd Y] [ContinuousConstSMul R Y] : (toContinuousMapLinearMap R).toAddMonoidHom = toContinuousMapAddMonoidHom

def LocallyConstant.toContinuousMapAlgHom {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (R : Type u_3) [CommSemiring R] [Semiring Y] [Algebra R Y] [IsTopologicalSemiring Y] : LocallyConstant X Y →ₐ[R] C(X, Y)

The inclusion of locally-constant functions into continuous functions as an algebra map.

Equations

• LocallyConstant.toContinuousMapAlgHom R = { toFun := LocallyConstant.toContinuousMap, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ }

@[simp]

theorem LocallyConstant.toContinuousMapAlgHom_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (R : Type u_3) [CommSemiring R] [Semiring Y] [Algebra R Y] [IsTopologicalSemiring Y] (f : LocallyConstant X Y) : (toContinuousMapAlgHom R) f = ↑f

@[simp]

theorem LocallyConstant.toLinearMap_toContinuousMapAlgHom {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (R : Type u_3) [CommSemiring R] [Semiring Y] [Algebra R Y] [IsTopologicalSemiring Y] : (toContinuousMapAlgHom R).toLinearMap = toContinuousMapLinearMap R

theorem LocallyConstant.separatesPoints_range_toContinuousMapAlgHom {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (R : Type u_3) [CommSemiring R] [TotallySeparatedSpace X] [Semiring Y] [Algebra R Y] [IsTopologicalSemiring Y] [Nontrivial Y] : (toContinuousMapAlgHom R).range.SeparatesPoints