The algebra morphism from locally constant functions to continuous functions. #
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.
Instances For
theorem
LocallyConstant.toContinuousMapAddMonoidHom.proof_1
{X : Type u_1}
{Y : Type u_2}
[TopologicalSpace X]
[TopologicalSpace Y]
[AddMonoid Y]
[ContinuousAdd Y]
:
↑0 = 0
theorem
LocallyConstant.toContinuousMapAddMonoidHom.proof_2
{X : Type u_2}
{Y : Type u_1}
[TopologicalSpace X]
[TopologicalSpace Y]
[AddMonoid Y]
[ContinuousAdd Y]
(x : LocallyConstant X Y)
(y : LocallyConstant X Y)
:
ZeroHom.toFun { toFun := LocallyConstant.toContinuousMap, map_zero' := (_ : ↑0 = 0) } (x + y) = ZeroHom.toFun { toFun := LocallyConstant.toContinuousMap, map_zero' := (_ : ↑0 = 0) } x + ZeroHom.toFun { toFun := LocallyConstant.toContinuousMap, map_zero' := (_ : ↑0 = 0) } y
@[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)
:
↑LocallyConstant.toContinuousMapAddMonoidHom f = ↑f
@[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)
:
↑LocallyConstant.toContinuousMapMonoidHom f = ↑f
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.
Instances For
@[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)
:
↑(LocallyConstant.toContinuousMapLinearMap R) 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]
:
The inclusion of locally-constant functions into continuous functions as a linear map.
Instances For
@[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]
[TopologicalSemiring Y]
(f : LocallyConstant X Y)
:
↑(LocallyConstant.toContinuousMapAlgHom R) f = ↑f
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]
[TopologicalSemiring Y]
:
The inclusion of locally-constant functions into continuous functions as an algebra map.