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.

structure ContinuousMapZero (X : Type u_1) (R : Type u_2) [Zero X] [Zero R] [TopologicalSpace X] [TopologicalSpace R] extends C(X, R) : Type (max u_1 u_2)

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

def ContinuousMapZero.«termC(_,_)₀» : Lean.ParserDescr

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.

instance ContinuousMapZero.instFunLike {X : Type u_1} {R : Type u_3} [Zero X] [Zero R] [TopologicalSpace X] [TopologicalSpace R] : FunLike (ContinuousMapZero X R) X R

Equations

• ContinuousMapZero.instFunLike = { coe := fun (f : ContinuousMapZero X R) => f.toFun, coe_injective' := ⋯ }

instance ContinuousMapZero.instContinuousMapClass {X : Type u_1} {R : Type u_3} [Zero X] [Zero R] [TopologicalSpace X] [TopologicalSpace R] : ContinuousMapClass (ContinuousMapZero X R) X R

instance ContinuousMapZero.instZeroHomClass {X : Type u_1} {R : Type u_3} [Zero X] [Zero R] [TopologicalSpace X] [TopologicalSpace R] : ZeroHomClass (ContinuousMapZero X R) X R

def Set.zeroOfFactMem {X : Type u_4} [Zero X] (s : Set X) [Fact (0 ∈ s)] : Zero ↑s

not marked as an instance because it would be a bad one in general, but it can be useful when working with ContinuousMapZero and the non-unital continuous functional calculus.

Equations

• s.zeroOfFactMem = { zero := ⟨0, ⋯⟩ }

theorem ContinuousMapZero.ext {X : Type u_1} {R : Type u_3} [Zero X] [Zero R] [TopologicalSpace X] [TopologicalSpace R] {f g : ContinuousMapZero X R} (h : ∀ (x : X), f x = g x) : f = g

theorem ContinuousMapZero.ext_iff {X : Type u_1} {R : Type u_3} [Zero X] [Zero R] [TopologicalSpace X] [TopologicalSpace R] {f g : ContinuousMapZero X R} : f = g ↔ ∀ (x : X), f x = g x

@[simp]

theorem ContinuousMapZero.coe_mk {X : Type u_1} {R : Type u_3} [Zero X] [Zero R] [TopologicalSpace X] [TopologicalSpace R] {f : C(X, R)} {h0 : f 0 = 0} : ⇑{ toContinuousMap := f, map_zero' := h0 } = ⇑f

theorem ContinuousMapZero.toContinuousMap_injective {X : Type u_1} {R : Type u_3} [Zero X] [Zero R] [TopologicalSpace X] [TopologicalSpace R] : Function.Injective _root_.toContinuousMap

theorem ContinuousMapZero.range_toContinuousMap {X : Type u_1} {R : Type u_3} [Zero X] [Zero R] [TopologicalSpace X] [TopologicalSpace R] : Set.range _root_.toContinuousMap = {f : C(X, R) | f 0 = 0}

def ContinuousMapZero.comp {X : Type u_1} {Y : Type u_2} {R : Type u_3} [Zero X] [Zero Y] [Zero R] [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace R] (g : ContinuousMapZero Y R) (f : ContinuousMapZero X Y) : ContinuousMapZero X R

Composition of continuous maps which map zero to zero.

Equations

• g.comp f = { toContinuousMap := (↑g).comp ↑f, map_zero' := ⋯ }

@[simp]

theorem ContinuousMapZero.comp_apply {X : Type u_1} {Y : Type u_2} {R : Type u_3} [Zero X] [Zero Y] [Zero R] [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace R] (g : ContinuousMapZero Y R) (f : ContinuousMapZero X Y) (x : X) : (g.comp f) x = g (f x)

instance ContinuousMapZero.instPartialOrder {X : Type u_1} {R : Type u_3} [Zero X] [Zero R] [TopologicalSpace X] [TopologicalSpace R] [PartialOrder R] : PartialOrder (ContinuousMapZero X R)

Equations

• ContinuousMapZero.instPartialOrder = PartialOrder.lift DFunLike.coe ⋯

theorem ContinuousMapZero.le_def {X : Type u_1} {R : Type u_3} [Zero X] [Zero R] [TopologicalSpace X] [TopologicalSpace R] [PartialOrder R] (f g : ContinuousMapZero X R) : f ≤ g ↔ ∀ (x : X), f x ≤ g x

instance ContinuousMapZero.instTopologicalSpace {X : Type u_1} {R : Type u_3} [Zero X] [Zero R] [TopologicalSpace X] [TopologicalSpace R] : TopologicalSpace (ContinuousMapZero X R)

Equations

• ContinuousMapZero.instTopologicalSpace = TopologicalSpace.induced toContinuousMap inferInstance

theorem ContinuousMapZero.isEmbedding_toContinuousMap {X : Type u_1} {R : Type u_3} [Zero X] [Zero R] [TopologicalSpace X] [TopologicalSpace R] : Topology.IsEmbedding _root_.toContinuousMap

@[deprecated ContinuousMapZero.isEmbedding_toContinuousMap (since := "2024-10-26")]

theorem ContinuousMapZero.embedding_toContinuousMap {X : Type u_1} {R : Type u_3} [Zero X] [Zero R] [TopologicalSpace X] [TopologicalSpace R] : Topology.IsEmbedding _root_.toContinuousMap

Alias of ContinuousMapZero.isEmbedding_toContinuousMap.

instance ContinuousMapZero.instT0Space {X : Type u_1} {R : Type u_3} [Zero X] [Zero R] [TopologicalSpace X] [TopologicalSpace R] [T0Space R] : T0Space (ContinuousMapZero X R)

instance ContinuousMapZero.instR0Space {X : Type u_1} {R : Type u_3} [Zero X] [Zero R] [TopologicalSpace X] [TopologicalSpace R] [R0Space R] : R0Space (ContinuousMapZero X R)

instance ContinuousMapZero.instT1Space {X : Type u_1} {R : Type u_3} [Zero X] [Zero R] [TopologicalSpace X] [TopologicalSpace R] [T1Space R] : T1Space (ContinuousMapZero X R)

instance ContinuousMapZero.instR1Space {X : Type u_1} {R : Type u_3} [Zero X] [Zero R] [TopologicalSpace X] [TopologicalSpace R] [R1Space R] : R1Space (ContinuousMapZero X R)

instance ContinuousMapZero.instT2Space {X : Type u_1} {R : Type u_3} [Zero X] [Zero R] [TopologicalSpace X] [TopologicalSpace R] [T2Space R] : T2Space (ContinuousMapZero X R)

instance ContinuousMapZero.instRegularSpace {X : Type u_1} {R : Type u_3} [Zero X] [Zero R] [TopologicalSpace X] [TopologicalSpace R] [RegularSpace R] : RegularSpace (ContinuousMapZero X R)

instance ContinuousMapZero.instT3Space {X : Type u_1} {R : Type u_3} [Zero X] [Zero R] [TopologicalSpace X] [TopologicalSpace R] [T3Space R] : T3Space (ContinuousMapZero X R)

instance ContinuousMapZero.instContinuousEvalConst {X : Type u_1} {R : Type u_3} [Zero X] [Zero R] [TopologicalSpace X] [TopologicalSpace R] : ContinuousEvalConst (ContinuousMapZero X R) X R

instance ContinuousMapZero.instContinuousEval {X : Type u_1} {R : Type u_3} [Zero X] [Zero R] [TopologicalSpace X] [TopologicalSpace R] [LocallyCompactPair X R] : ContinuousEval (ContinuousMapZero X R) X R

theorem ContinuousMapZero.isClosedEmbedding_toContinuousMap {X : Type u_1} {R : Type u_3} [Zero X] [Zero R] [TopologicalSpace X] [TopologicalSpace R] [T1Space R] : Topology.IsClosedEmbedding _root_.toContinuousMap

theorem ContinuousMapZero.continuous_comp_left {X : Type u_4} {Y : Type u_5} {Z : Type u_6} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [Zero X] [Zero Y] [Zero Z] (f : ContinuousMapZero X Y) : Continuous fun (g : ContinuousMapZero Y Z) => g.comp f

def ContinuousMapZero.id {R : Type u_3} [Zero R] [TopologicalSpace R] {s : Set R} [Zero ↑s] (h0 : ↑0 = 0) : ContinuousMapZero (↑s) R

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 }

@[simp]

theorem ContinuousMapZero.id_toFun {R : Type u_3} [Zero R] [TopologicalSpace R] {s : Set R} [Zero ↑s] (h0 : ↑0 = 0) (a✝ : ↑s) : (ContinuousMapZero.id h0) a✝ = ↑a✝

@[simp]

theorem ContinuousMapZero.toContinuousMap_id {R : Type u_3} [Zero R] [TopologicalSpace R] {s : Set R} [Zero ↑s] (h0 : ↑0 = 0) : ↑(ContinuousMapZero.id h0) = ContinuousMap.restrict s (ContinuousMap.id R)

noncomputable def ContinuousMapZero.mkD {X : Type u_1} {R : Type u_2} [Zero R] [TopologicalSpace X] [TopologicalSpace R] [Zero X] (f : X → R) (default : ContinuousMapZero X R) : ContinuousMapZero X R

Interpret f : α → β as an element of C(α, β)₀, falling back to the default value default : C(α, β)₀ if f is not continuous or does not map 0 to 0. This is mainly intended to be used for C(α, β)₀-valued integration. For example, if a family of functions f : ι → α → β satisfies that f i is continuous and maps 0 to 0 for almost every i, you can write the C(α, β)₀-valued integral "∫ i, f i" as ∫ i, ContinuousMapZero.mkD (f i) 0.

Equations

• ContinuousMapZero.mkD f default = if h : Continuous f ∧ f 0 = 0 then { toFun := f, continuous_toFun := ⋯, map_zero' := ⋯ } else default

theorem ContinuousMapZero.mkD_of_continuous {X : Type u_1} {R : Type u_2} [Zero R] [TopologicalSpace X] [TopologicalSpace R] [Zero X] {f : X → R} {g : ContinuousMapZero X R} (hf : Continuous f) (hf₀ : f 0 = 0) : mkD f g = { toFun := f, continuous_toFun := hf, map_zero' := hf₀ }

theorem ContinuousMapZero.mkD_of_not_continuous {X : Type u_1} {R : Type u_2} [Zero R] [TopologicalSpace X] [TopologicalSpace R] [Zero X] {f : X → R} {g : ContinuousMapZero X R} (hf : ¬Continuous f) : mkD f g = g

theorem ContinuousMapZero.mkD_of_not_zero {X : Type u_1} {R : Type u_2} [Zero R] [TopologicalSpace X] [TopologicalSpace R] [Zero X] {f : X → R} {g : ContinuousMapZero X R} (hf : f 0 ≠ 0) : mkD f g = g

theorem ContinuousMapZero.mkD_apply_of_continuous {X : Type u_1} {R : Type u_2} [Zero R] [TopologicalSpace X] [TopologicalSpace R] [Zero X] {f : X → R} {g : ContinuousMapZero X R} {x : X} (hf : Continuous f) (hf₀ : f 0 = 0) : (mkD f g) x = f x

theorem ContinuousMapZero.mkD_of_continuousOn {X : Type u_1} {R : Type u_2} [Zero R] [TopologicalSpace X] [TopologicalSpace R] {s : Set X} [Zero ↑s] {f : X → R} {g : ContinuousMapZero (↑s) R} (hf : ContinuousOn f s) (hf₀ : f ↑0 = 0) : mkD (s.restrict f) g = { toFun := s.restrict f, continuous_toFun := ⋯, map_zero' := hf₀ }

theorem ContinuousMapZero.mkD_of_not_continuousOn {X : Type u_1} {R : Type u_2} [Zero R] [TopologicalSpace X] [TopologicalSpace R] {s : Set X} [Zero ↑s] {f : X → R} {g : ContinuousMapZero (↑s) R} (hf : ¬ContinuousOn f s) : mkD (s.restrict f) g = g

theorem ContinuousMapZero.mkD_apply_of_continuousOn {X : Type u_1} {R : Type u_2} [Zero R] [TopologicalSpace X] [TopologicalSpace R] {s : Set X} [Zero ↑s] {f : X → R} {g : ContinuousMapZero (↑s) R} {x : ↑s} (hf : ContinuousOn f s) (hf₀ : f ↑0 = 0) : (mkD (s.restrict f) g) x = f ↑x

theorem ContinuousMapZero.mkD_eq_mkD_of_map_zero {X : Type u_1} {R : Type u_2} [Zero R] [TopologicalSpace X] [TopologicalSpace R] [Zero X] (f : X → R) (g : ContinuousMapZero X R) (f_zero : f 0 = 0) : ↑(mkD f g) = ContinuousMap.mkD f ↑g

Link between ContinuousMapZero.mkD and ContinuousMap.mkD.

instance ContinuousMapZero.instZero {X : Type u_1} {R : Type u_2} [Zero X] [TopologicalSpace X] [TopologicalSpace R] [Zero R] : Zero (ContinuousMapZero X R)

Equations

• ContinuousMapZero.instZero = { zero := { toContinuousMap := 0, map_zero' := ⋯ } }

@[simp]

theorem ContinuousMapZero.coe_zero {X : Type u_1} {R : Type u_2} [Zero X] [TopologicalSpace X] [TopologicalSpace R] [Zero R] : ⇑0 = 0

instance ContinuousMapZero.instAdd {X : Type u_1} {R : Type u_2} [Zero X] [TopologicalSpace X] [TopologicalSpace R] [AddZeroClass R] [ContinuousAdd R] : Add (ContinuousMapZero X R)

Equations

• ContinuousMapZero.instAdd = { add := fun (f g : ContinuousMapZero X R) => { toContinuousMap := ↑f + ↑g, map_zero' := ⋯ } }

@[simp]

theorem ContinuousMapZero.coe_add {X : Type u_1} {R : Type u_2} [Zero X] [TopologicalSpace X] [TopologicalSpace R] [AddZeroClass R] [ContinuousAdd R] (f g : ContinuousMapZero X R) : ⇑(f + g) = ⇑f + ⇑g

instance ContinuousMapZero.instNeg {X : Type u_1} {R : Type u_2} [Zero X] [TopologicalSpace X] [TopologicalSpace R] [NegZeroClass R] [ContinuousNeg R] : Neg (ContinuousMapZero X R)

Equations

• ContinuousMapZero.instNeg = { neg := fun (f : ContinuousMapZero X R) => { toContinuousMap := -↑f, map_zero' := ⋯ } }

@[simp]

theorem ContinuousMapZero.coe_neg {X : Type u_1} {R : Type u_2} [Zero X] [TopologicalSpace X] [TopologicalSpace R] [NegZeroClass R] [ContinuousNeg R] (f : ContinuousMapZero X R) : ⇑(-f) = -⇑f

instance ContinuousMapZero.instSub {X : Type u_1} {R : Type u_2} [Zero X] [TopologicalSpace X] [TopologicalSpace R] [SubNegZeroMonoid R] [ContinuousSub R] : Sub (ContinuousMapZero X R)

Equations

• ContinuousMapZero.instSub = { sub := fun (f g : ContinuousMapZero X R) => { toContinuousMap := ↑f - ↑g, map_zero' := ⋯ } }

@[simp]

theorem ContinuousMapZero.coe_sub {X : Type u_1} {R : Type u_2} [Zero X] [TopologicalSpace X] [TopologicalSpace R] [SubNegZeroMonoid R] [ContinuousSub R] (f g : ContinuousMapZero X R) : ⇑(f - g) = ⇑f - ⇑g

instance ContinuousMapZero.instMul {X : Type u_1} {R : Type u_2} [Zero X] [TopologicalSpace X] [TopologicalSpace R] [MulZeroClass R] [ContinuousMul R] : Mul (ContinuousMapZero X R)

Equations

• ContinuousMapZero.instMul = { mul := fun (f g : ContinuousMapZero X R) => { toContinuousMap := ↑f * ↑g, map_zero' := ⋯ } }

@[simp]

theorem ContinuousMapZero.coe_mul {X : Type u_1} {R : Type u_2} [Zero X] [TopologicalSpace X] [TopologicalSpace R] [MulZeroClass R] [ContinuousMul R] (f g : ContinuousMapZero X R) : ⇑(f * g) = ⇑f * ⇑g

instance ContinuousMapZero.instSMul {X : Type u_1} {R : Type u_2} [Zero X] [TopologicalSpace X] [TopologicalSpace R] {M : Type u_3} [Zero R] [SMulZeroClass M R] [ContinuousConstSMul M R] : SMul M (ContinuousMapZero X R)

Equations

• ContinuousMapZero.instSMul = { smul := fun (m : M) (f : ContinuousMapZero X R) => { toContinuousMap := m • ↑f, map_zero' := ⋯ } }

@[simp]

theorem ContinuousMapZero.coe_smul {X : Type u_1} {R : Type u_2} [Zero X] [TopologicalSpace X] [TopologicalSpace R] {M : Type u_3} [Zero R] [SMulZeroClass M R] [ContinuousConstSMul M R] (m : M) (f : ContinuousMapZero X R) : ⇑(m • f) = m • ⇑f

instance ContinuousMapZero.instAddCommMonoid {X : Type u_1} {R : Type u_2} [Zero X] [TopologicalSpace X] [TopologicalSpace R] [AddCommMonoid R] [ContinuousAdd R] : AddCommMonoid (ContinuousMapZero X R)

Equations

• One or more equations did not get rendered due to their size.

instance ContinuousMapZero.instModule {X : Type u_1} {R : Type u_2} [Zero X] [TopologicalSpace X] [TopologicalSpace R] [AddCommMonoid R] [ContinuousAdd R] {M : Type u_3} [Semiring M] [Module M R] [ContinuousConstSMul M R] : Module M (ContinuousMapZero X R)

Equations

• ContinuousMapZero.instModule = { toSMul := ContinuousMapZero.instSMul, one_smul := ⋯, mul_smul := ⋯, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯ }

instance ContinuousMapZero.instSMulCommClass {X : Type u_1} {R : Type u_2} [Zero X] [TopologicalSpace X] [TopologicalSpace R] [AddCommMonoid R] {M : Type u_3} {N : Type u_4} [SMulZeroClass M R] [ContinuousConstSMul M R] [SMulZeroClass N R] [ContinuousConstSMul N R] [SMulCommClass M N R] : SMulCommClass M N (ContinuousMapZero X R)

instance ContinuousMapZero.instIsScalarTower {X : Type u_1} {R : Type u_2} [Zero X] [TopologicalSpace X] [TopologicalSpace R] [AddCommMonoid R] {M : Type u_3} {N : Type u_4} [SMulZeroClass M R] [ContinuousConstSMul M R] [SMulZeroClass N R] [ContinuousConstSMul N R] [SMul M N] [IsScalarTower M N R] : IsScalarTower M N (ContinuousMapZero X R)

instance ContinuousMapZero.instAddCommGroup {X : Type u_1} {R : Type u_2} [Zero X] [TopologicalSpace X] [TopologicalSpace R] [AddCommGroup R] [IsTopologicalAddGroup R] : AddCommGroup (ContinuousMapZero X R)

Equations

• One or more equations did not get rendered due to their size.

instance ContinuousMapZero.instNonUnitalCommSemiring {X : Type u_1} {R : Type u_2} [Zero X] [TopologicalSpace X] [TopologicalSpace R] [CommSemiring R] [IsTopologicalSemiring R] : NonUnitalCommSemiring (ContinuousMapZero X R)

Equations

• One or more equations did not get rendered due to their size.

instance ContinuousMapZero.instSMulCommClass' {X : Type u_1} {R : Type u_2} [Zero X] [TopologicalSpace X] [TopologicalSpace R] [CommSemiring R] [IsTopologicalSemiring R] {M : Type u_3} [SMulZeroClass M R] [SMulCommClass M R R] [ContinuousConstSMul M R] : SMulCommClass M (ContinuousMapZero X R) (ContinuousMapZero X R)

instance ContinuousMapZero.instIsScalarTower' {X : Type u_1} {R : Type u_2} [Zero X] [TopologicalSpace X] [TopologicalSpace R] [CommSemiring R] [IsTopologicalSemiring R] {M : Type u_3} [SMulZeroClass M R] [IsScalarTower M R R] [ContinuousConstSMul M R] : IsScalarTower M (ContinuousMapZero X R) (ContinuousMapZero X R)

instance ContinuousMapZero.instStarRing {X : Type u_1} {R : Type u_2} [Zero X] [TopologicalSpace X] [TopologicalSpace R] [CommSemiring R] [IsTopologicalSemiring R] [StarRing R] [ContinuousStar R] : StarRing (ContinuousMapZero X R)

Equations

• ContinuousMapZero.instStarRing = { star := fun (f : ContinuousMapZero X R) => { toContinuousMap := star ↑f, map_zero' := ⋯ }, star_involutive := ⋯, star_mul := ⋯, star_add := ⋯ }

instance ContinuousMapZero.instStarModule {X : Type u_1} {R : Type u_2} [Zero X] [TopologicalSpace X] [TopologicalSpace R] [CommSemiring R] [IsTopologicalSemiring R] [StarRing R] {M : Type u_3} [SMulZeroClass M R] [ContinuousConstSMul M R] [Star M] [StarModule M R] [ContinuousStar R] : StarModule M (ContinuousMapZero X R)

@[simp]

theorem ContinuousMapZero.coe_star {X : Type u_1} {R : Type u_2} [Zero X] [TopologicalSpace X] [TopologicalSpace R] [CommSemiring R] [IsTopologicalSemiring R] [StarRing R] [ContinuousStar R] (f : ContinuousMapZero X R) : ⇑(star f) = star ⇑f

instance ContinuousMapZero.instTrivialStar {X : Type u_1} {R : Type u_2} [Zero X] [TopologicalSpace X] [TopologicalSpace R] [CommSemiring R] [IsTopologicalSemiring R] [StarRing R] [ContinuousStar R] [TrivialStar R] : TrivialStar (ContinuousMapZero X R)

instance ContinuousMapZero.instCanLift {X : Type u_1} {R : Type u_2} [Zero X] [TopologicalSpace X] [TopologicalSpace R] [CommSemiring R] : CanLift C(X, R) (ContinuousMapZero X R) _root_.toContinuousMap fun (f : C(X, R)) => f 0 = 0

def ContinuousMapZero.toContinuousMapHom {X : Type u_1} {R : Type u_2} [Zero X] [TopologicalSpace X] [TopologicalSpace R] [CommSemiring R] [IsTopologicalSemiring R] [StarRing R] [ContinuousStar R] : ContinuousMapZero X R →⋆ₙₐ[R] C(X, R)

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' := ⋯ }

@[simp]

theorem ContinuousMapZero.toContinuousMapHom_apply {X : Type u_1} {R : Type u_2} [Zero X] [TopologicalSpace X] [TopologicalSpace R] [CommSemiring R] [IsTopologicalSemiring R] [StarRing R] [ContinuousStar R] (f : ContinuousMapZero X R) : toContinuousMapHom f = ↑f

theorem ContinuousMapZero.coe_toContinuousMapHom {X : Type u_1} {R : Type u_2} [Zero X] [TopologicalSpace X] [TopologicalSpace R] [CommSemiring R] [IsTopologicalSemiring R] [StarRing R] [ContinuousStar R] : ⇑toContinuousMapHom = _root_.toContinuousMap

def ContinuousMapZero.toContinuousMapCLM {X : Type u_1} {R : Type u_2} [Zero X] [TopologicalSpace X] [TopologicalSpace R] [CommSemiring R] [IsTopologicalSemiring R] (M : Type u_3) [Semiring M] [Module M R] [ContinuousConstSMul M R] : ContinuousMapZero X R →L[M] C(X, R)

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 := ⋯ }

@[simp]

theorem ContinuousMapZero.toContinuousMapCLM_apply {X : Type u_1} {R : Type u_2} [Zero X] [TopologicalSpace X] [TopologicalSpace R] [CommSemiring R] [IsTopologicalSemiring R] (M : Type u_3) [Semiring M] [Module M R] [ContinuousConstSMul M R] (f : ContinuousMapZero X R) : (toContinuousMapCLM M) f = ↑f

def ContinuousMapZero.evalCLM {X : Type u_1} {R : Type u_2} [Zero X] [TopologicalSpace X] [TopologicalSpace R] [CommSemiring R] [IsTopologicalSemiring R] (𝕜 : Type u_3) [Semiring 𝕜] [Module 𝕜 R] [ContinuousConstSMul 𝕜 R] (x : X) : ContinuousMapZero X R →L[𝕜] R

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 𝕜)

@[simp]

theorem ContinuousMapZero.evalCLM_apply {X : Type u_1} {R : Type u_2} [Zero X] [TopologicalSpace X] [TopologicalSpace R] [CommSemiring R] [IsTopologicalSemiring R] {𝕜 : Type u_3} [Semiring 𝕜] [Module 𝕜 R] [ContinuousConstSMul 𝕜 R] (x : X) (f : ContinuousMapZero X R) : (evalCLM 𝕜 x) f = f x

def ContinuousMapZero.coeFnAddMonoidHom {X : Type u_1} {R : Type u_2} [Zero X] [TopologicalSpace X] [TopologicalSpace R] [CommSemiring R] [IsTopologicalSemiring R] : ContinuousMapZero X R →+ X → R

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' := ⋯ }

@[simp]

theorem ContinuousMapZero.coeFnAddMonoidHom_apply {X : Type u_1} {R : Type u_2} [Zero X] [TopologicalSpace X] [TopologicalSpace R] [CommSemiring R] [IsTopologicalSemiring R] (f : ContinuousMapZero X R) : coeFnAddMonoidHom f = ⇑f

@[simp]

theorem ContinuousMapZero.coe_sum {X : Type u_1} {R : Type u_2} [Zero X] [TopologicalSpace X] [TopologicalSpace R] [CommSemiring R] [IsTopologicalSemiring R] {ι : Type u_3} (s : Finset ι) (f : ι → ContinuousMapZero X R) : ⇑(s.sum f) = ∑ i ∈ s, ⇑(f i)

instance ContinuousMapZero.instNonUnitalCommRing {X : Type u_3} {R : Type u_4} [Zero X] [TopologicalSpace X] [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] : NonUnitalCommRing (ContinuousMapZero X R)

Equations

• One or more equations did not get rendered due to their size.

instance ContinuousMapZero.instContinuousNeg {X : Type u_3} {R : Type u_4} [Zero X] [TopologicalSpace X] [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] : ContinuousNeg (ContinuousMapZero X R)

instance ContinuousMapZero.instUniformSpace {X : Type u_1} {R : Type u_2} [Zero X] [TopologicalSpace X] [Zero R] [UniformSpace R] : UniformSpace (ContinuousMapZero X R)

Equations

• ContinuousMapZero.instUniformSpace = UniformSpace.comap ContinuousMapZero.toContinuousMap inferInstance

theorem ContinuousMapZero.isUniformEmbedding_toContinuousMap {X : Type u_1} {R : Type u_2} [Zero X] [TopologicalSpace X] [Zero R] [UniformSpace R] : IsUniformEmbedding _root_.toContinuousMap

instance ContinuousMapZero.instCompleteSpaceOfT1SpaceOfContinuousMap {X : Type u_1} {R : Type u_2} [Zero X] [TopologicalSpace X] [Zero R] [UniformSpace R] [T1Space R] [CompleteSpace C(X, R)] : CompleteSpace (ContinuousMapZero X R)

theorem ContinuousMapZero.isUniformEmbedding_comp {X : Type u_1} {R : Type u_2} [Zero X] [TopologicalSpace X] [Zero R] [UniformSpace R] {Y : Type u_3} [UniformSpace Y] [Zero Y] (g : ContinuousMapZero Y R) (hg : IsUniformEmbedding ⇑g) : IsUniformEmbedding fun (x : ContinuousMapZero X Y) => g.comp x

def UniformEquiv.arrowCongrLeft₀ {X : Type u_1} {R : Type u_2} [Zero X] [TopologicalSpace X] [Zero R] [UniformSpace R] {Y : Type u_3} [TopologicalSpace Y] [Zero Y] (f : X ≃ₜ Y) (hf : f 0 = 0) : ContinuousMapZero X R ≃ᵤ ContinuousMapZero Y R

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.

def ContinuousMapZero.nonUnitalStarAlgHom_precomp {X : Type u_1} {Y : Type u_2} (R : Type u_4) [Zero X] [Zero Y] [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace R] [CommSemiring R] [StarRing R] [IsTopologicalSemiring R] [ContinuousStar R] (f : ContinuousMapZero X Y) : ContinuousMapZero Y R →⋆ₙₐ[R] ContinuousMapZero X R

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' := ⋯ }

@[simp]

theorem ContinuousMapZero.nonUnitalStarAlgHom_precomp_apply {X : Type u_1} {Y : Type u_2} (R : Type u_4) [Zero X] [Zero Y] [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace R] [CommSemiring R] [StarRing R] [IsTopologicalSemiring R] [ContinuousStar R] (f : ContinuousMapZero X Y) (g : ContinuousMapZero Y R) : (nonUnitalStarAlgHom_precomp R f) g = g.comp f

def ContinuousMapZero.nonUnitalStarAlgHom_postcomp (X : Type u_1) {M : Type u_3} {R : Type u_4} {S : Type u_5} [Zero X] [CommSemiring M] [TopologicalSpace X] [TopologicalSpace R] [TopologicalSpace S] [CommSemiring R] [StarRing R] [IsTopologicalSemiring R] [ContinuousStar R] [CommSemiring S] [StarRing S] [IsTopologicalSemiring S] [ContinuousStar S] [Module M R] [Module M S] [ContinuousConstSMul M R] [ContinuousConstSMul M S] (φ : R →⋆ₙₐ[M] S) (hφ : Continuous ⇑φ) : ContinuousMapZero X R →⋆ₙₐ[M] ContinuousMapZero X S

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.

@[simp]

theorem ContinuousMapZero.nonUnitalStarAlgHom_postcomp_apply (X : Type u_1) {M : Type u_3} {R : Type u_4} {S : Type u_5} [Zero X] [CommSemiring M] [TopologicalSpace X] [TopologicalSpace R] [TopologicalSpace S] [CommSemiring R] [StarRing R] [IsTopologicalSemiring R] [ContinuousStar R] [CommSemiring S] [StarRing S] [IsTopologicalSemiring S] [ContinuousStar S] [Module M R] [Module M S] [ContinuousConstSMul M R] [ContinuousConstSMul M S] (φ : R →⋆ₙₐ[M] S) (hφ : Continuous ⇑φ) (f : ContinuousMapZero X R) : (nonUnitalStarAlgHom_postcomp X φ hφ) f = { toFun := ⇑φ, continuous_toFun := hφ, map_zero' := ⋯ }.comp f

noncomputable instance ContinuousMapZero.instMetricSpace {α : Type u_1} {R : Type u_3} [TopologicalSpace α] [CompactSpace α] [Zero α] [MetricSpace R] [Zero R] : MetricSpace (ContinuousMapZero α R)

Equations

• ContinuousMapZero.instMetricSpace = IsUniformEmbedding.comapMetricSpace toContinuousMap ⋯

theorem ContinuousMapZero.isometry_toContinuousMap {α : Type u_1} {R : Type u_3} [TopologicalSpace α] [CompactSpace α] [Zero α] [MetricSpace R] [Zero R] : Isometry toContinuousMap

noncomputable instance ContinuousMapZero.instNorm {α : Type u_1} {R : Type u_3} [TopologicalSpace α] [CompactSpace α] [Zero α] [NormedAddCommGroup R] : Norm (ContinuousMapZero α R)

Equations

• ContinuousMapZero.instNorm = { norm := fun (f : ContinuousMapZero α R) => ‖↑f‖ }

theorem ContinuousMapZero.norm_def {α : Type u_1} {R : Type u_3} [TopologicalSpace α] [CompactSpace α] [Zero α] [NormedAddCommGroup R] (f : ContinuousMapZero α R) : ‖f‖ = ‖↑f‖

noncomputable instance ContinuousMapZero.instNormedAddCommGroup {α : Type u_1} {R : Type u_3} [TopologicalSpace α] [CompactSpace α] [Zero α] [NormedAddCommGroup R] : NormedAddCommGroup (ContinuousMapZero α R)

Equations

• One or more equations did not get rendered due to their size.

noncomputable instance ContinuousMapZero.instNonUnitalNormedCommRing {α : Type u_1} {R : Type u_3} [TopologicalSpace α] [CompactSpace α] [Zero α] [NormedCommRing R] : NonUnitalNormedCommRing (ContinuousMapZero α R)

Equations

• One or more equations did not get rendered due to their size.

noncomputable instance ContinuousMapZero.instNormedSpaceOfNormedAlgebra {α : Type u_1} {𝕜 : Type u_2} {R : Type u_3} [TopologicalSpace α] [CompactSpace α] [Zero α] [NormedField 𝕜] [NormedCommRing R] [NormedAlgebra 𝕜 R] : NormedSpace 𝕜 (ContinuousMapZero α R)

Equations

• ContinuousMapZero.instNormedSpaceOfNormedAlgebra = { toModule := ContinuousMapZero.instModule, norm_smul_le := ⋯ }

instance ContinuousMapZero.instCStarRing {α : Type u_1} {R : Type u_3} [TopologicalSpace α] [CompactSpace α] [Zero α] [NormedCommRing R] [StarRing R] [CStarRing R] : CStarRing (ContinuousMapZero α R)