Continuous maps sending zero to zero #
This is the type of continuous maps from X
to R
such that (0 : X) ↦ (0 : R)
for which we
provide the scoped notation C(X, R)₀
. We provide this as a dedicated type solely for the
non-unital continuous functional calculus, as using various terms of type Ideal C(X, R)
were
overly burdensome on type class synthesis.
Of course, one could generalize to maps between pointed topological spaces, but that goes beyond the purpose of this type.
The type of continuous maps which map zero to zero.
Note that one should never use the structure projection ContinuousMapZero.toContinuousMap
and
instead favor the coercion (↑) : C(X, R)₀ → C(X, R)
available from the instance of
ContinuousMapClass
. All the instances on C(X, R)₀
from C(X, R)
passes through this coercion,
not the structure projection. Of course, the two are definitionally equal, but not reducibly so.
- toFun : X → R
- continuous_toFun : Continuous self.toFun
- map_zero' : self.toContinuousMap 0 = 0
Instances For
The type of continuous maps which map zero to zero.
Note that one should never use the structure projection ContinuousMapZero.toContinuousMap
and
instead favor the coercion (↑) : C(X, R)₀ → C(X, R)
available from the instance of
ContinuousMapClass
. All the instances on C(X, R)₀
from C(X, R)
passes through this coercion,
not the structure projection. Of course, the two are definitionally equal, but not reducibly so.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- ContinuousMapZero.instFunLike = { coe := fun (f : ContinuousMapZero X R) => f.toFun, coe_injective' := ⋯ }
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Composition of continuous maps which map zero to zero.
Equations
- g.comp f = { toContinuousMap := (↑g).comp ↑f, map_zero' := ⋯ }
Instances For
Equations
- ContinuousMapZero.instPartialOrder = PartialOrder.lift DFunLike.coe ⋯
Equations
- ContinuousMapZero.instTopologicalSpace = TopologicalSpace.induced toContinuousMap inferInstance
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
The identity function as an element of C(s, R)₀
when 0 ∈ (s : Set R)
.
Equations
- ContinuousMapZero.id h0 = { toContinuousMap := ContinuousMap.restrict s (ContinuousMap.id R), map_zero' := h0 }
Instances For
Equations
- ContinuousMapZero.instZero = { zero := { toContinuousMap := 0, map_zero' := ⋯ } }
Equations
- ContinuousMapZero.instAdd = { add := fun (f g : ContinuousMapZero X R) => { toContinuousMap := ↑f + ↑g, map_zero' := ⋯ } }
Equations
- ContinuousMapZero.instMul = { mul := fun (f g : ContinuousMapZero X R) => { toContinuousMap := ↑f * ↑g, map_zero' := ⋯ } }
Equations
- ContinuousMapZero.instSMul = { smul := fun (m : M) (f : ContinuousMapZero X R) => { toContinuousMap := m • ↑f, map_zero' := ⋯ } }
Equations
- ContinuousMapZero.instNonUnitalCommSemiring = Function.Injective.nonUnitalCommSemiring toContinuousMap ⋯ ⋯ ⋯ ⋯ ⋯
Equations
- ContinuousMapZero.instModule = Function.Injective.module M { toFun := fun (f : ContinuousMapZero X R) => { toFun := ⇑f, continuous_toFun := ⋯ }, map_zero' := ⋯, map_add' := ⋯ } ⋯ ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ContinuousMapZero.instStarRing = StarRing.mk ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
The coercion C(X, R)₀ → C(X, R)
bundled as a non-unital star algebra homomorphism.
Equations
- ContinuousMapZero.toContinuousMapHom = { toFun := fun (f : ContinuousMapZero X R) => ↑f, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯, map_star' := ⋯ }
Instances For
The coercion C(X, R)₀ → C(X, R)
bundled as a continuous linear map.
Equations
- ContinuousMapZero.toContinuousMapCLM M = { toFun := fun (f : ContinuousMapZero X R) => ↑f, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }
Instances For
The evaluation at a point, as a continuous linear map from C(X, R)₀
to R
.
Equations
- ContinuousMapZero.evalCLM 𝕜 x = (ContinuousMap.evalCLM 𝕜 x).comp (ContinuousMapZero.toContinuousMapCLM 𝕜)
Instances For
Coercion to a function as an AddMonoidHom
. Similar to ContinuousMap.coeFnAddMonoidHom
.
Equations
- ContinuousMapZero.coeFnAddMonoidHom = { toFun := fun (f : ContinuousMapZero X R) => ⇑f, map_zero' := ⋯, map_add' := ⋯ }
Instances For
Equations
- ContinuousMapZero.instSub = { sub := fun (f g : ContinuousMapZero X R) => { toContinuousMap := ↑f - ↑g, map_zero' := ⋯ } }
Equations
- ContinuousMapZero.instNeg = { neg := fun (f : ContinuousMapZero X R) => { toContinuousMap := -↑f, map_zero' := ⋯ } }
Equations
- ContinuousMapZero.instNonUnitalCommRing = Function.Injective.nonUnitalCommRing toContinuousMap ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
Equations
- ⋯ = ⋯
Equations
- ContinuousMapZero.instUniformSpace = UniformSpace.comap ContinuousMapZero.toContinuousMap inferInstance
Alias of ContinuousMapZero.isUniformEmbedding_toContinuousMap
.
Equations
- ⋯ = ⋯
The uniform equivalence C(X, R)₀ ≃ᵤ C(Y, R)₀
induced by a homeomorphism of the domains
sending 0 : X
to 0 : Y
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The functor C(·, R)₀
from topological spaces with zero (and ContinuousMapZero
maps) to
non-unital star algebras.
Equations
- ContinuousMapZero.nonUnitalStarAlgHom_precomp R f = { toFun := fun (g : ContinuousMapZero Y R) => g.comp f, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯, map_star' := ⋯ }
Instances For
The functor C(X, ·)₀
from non-unital topological star algebras (with non-unital continuous
star homomorphisms) to non-unital star algebras.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- ContinuousMapZero.instMetricSpace = IsUniformEmbedding.comapMetricSpace toContinuousMap ⋯
Equations
- ContinuousMapZero.instNorm = { norm := fun (f : ContinuousMapZero α R) => ‖↑f‖ }
Equations
- ContinuousMapZero.instNonUnitalNormedCommRing = NonUnitalNormedCommRing.mk ⋯
Equations
- ContinuousMapZero.instNormedSpaceOfNormedAlgebra = NormedSpace.mk ⋯
Equations
- ⋯ = ⋯