Mapping C(X, ℝ) to C(X, 𝕜) and back

This file contains the definitions for ContinuousMap.realToRCLike and ContinuousMap.rclikeToReal, which map C(X, ℝ) to C(X, 𝕜) and back for any RCLike 𝕜.

def ContinuousMap.realToRCLike {X : Type u_1} (𝕜 : Type u_2) [TopologicalSpace X] [RCLike 𝕜] (f : C(X, ℝ)) : C(X, 𝕜)

Lifting C(X, ℝ) to C(X, 𝕜) using RCLike.ofReal.

Equations

• ContinuousMap.realToRCLike 𝕜 f = { toFun := fun (x : X) => ↑(f x), continuous_toFun := ⋯ }

@[simp]

theorem ContinuousMap.realToRCLike_apply {X : Type u_1} (𝕜 : Type u_2) [TopologicalSpace X] [RCLike 𝕜] (f : C(X, ℝ)) (x : X) : (realToRCLike 𝕜 f) x = ↑(f x)

@[simp]

theorem ContinuousMap.isSelfAdjoint_realToRCLike {X : Type u_1} (𝕜 : Type u_2) [TopologicalSpace X] [RCLike 𝕜] {f : C(X, ℝ)} : IsSelfAdjoint (realToRCLike 𝕜 f)

@[simp]

theorem ContinuousMap.spectrum_realToRCLike {X : Type u_1} (𝕜 : Type u_2) [TopologicalSpace X] [RCLike 𝕜] (f : C(X, ℝ)) : spectrum ℝ (realToRCLike 𝕜 f) = spectrum ℝ f

def ContinuousMap.realToRCLikeOrderEmbedding (X : Type u_1) (𝕜 : Type u_2) [TopologicalSpace X] [RCLike 𝕜] : C(X, ℝ) ↪o C(X, 𝕜)

ContinuousMap.realToRCLike as an order embedding.

Equations

• ContinuousMap.realToRCLikeOrderEmbedding X 𝕜 = { toFun := ContinuousMap.realToRCLike 𝕜, inj' := ⋯, map_rel_iff' := ⋯ }

@[simp]

theorem ContinuousMap.realToRCLikeOrderEmbedding_apply (X : Type u_1) (𝕜 : Type u_2) [TopologicalSpace X] [RCLike 𝕜] (f : C(X, ℝ)) : (realToRCLikeOrderEmbedding X 𝕜) f = realToRCLike 𝕜 f

theorem ContinuousMap.realToRCLike_monotone (X : Type u_1) (𝕜 : Type u_2) [TopologicalSpace X] [RCLike 𝕜] : Monotone (realToRCLike 𝕜)

theorem ContinuousMap.realToRCLike_strictMono (X : Type u_1) (𝕜 : Type u_2) [TopologicalSpace X] [RCLike 𝕜] : StrictMono (realToRCLike 𝕜)

@[simp]

theorem ContinuousMap.realToRCLike_injective (X : Type u_1) (𝕜 : Type u_2) [TopologicalSpace X] [RCLike 𝕜] : Function.Injective (realToRCLike 𝕜)

@[simp]

theorem ContinuousMap.realToRCLike_inj {X : Type u_1} (𝕜 : Type u_2) [TopologicalSpace X] [RCLike 𝕜] {f g : C(X, ℝ)} : realToRCLike 𝕜 f = realToRCLike 𝕜 g ↔ f = g

@[simp]

theorem ContinuousMap.realToRCLike_le_realToRCLike_iff {X : Type u_1} (𝕜 : Type u_2) [TopologicalSpace X] [RCLike 𝕜] {f g : C(X, ℝ)} : realToRCLike 𝕜 f ≤ realToRCLike 𝕜 g ↔ f ≤ g

@[simp]

theorem ContinuousMap.realToRCLike_lt_realToRCLike_iff {X : Type u_1} (𝕜 : Type u_2) [TopologicalSpace X] [RCLike 𝕜] {f g : C(X, ℝ)} : realToRCLike 𝕜 f < realToRCLike 𝕜 g ↔ f < g

@[simp]

theorem ContinuousMap.isometry_realToRCLike (X : Type u_1) (𝕜 : Type u_2) [TopologicalSpace X] [RCLike 𝕜] [CompactSpace X] : Isometry (realToRCLike 𝕜)

@[simp]

theorem ContinuousMap.continuous_realToRCLike (X : Type u_1) (𝕜 : Type u_2) [TopologicalSpace X] [RCLike 𝕜] : Continuous (realToRCLike 𝕜)

noncomputable def ContinuousMap.realToRCLikeStarAlgHom (X : Type u_1) (𝕜 : Type u_2) [TopologicalSpace X] [RCLike 𝕜] : C(X, ℝ) →⋆ₐ[ℝ] C(X, 𝕜)

ContinuousMap.realToRCLike as a ⋆-algebra map.

Equations

• ContinuousMap.realToRCLikeStarAlgHom X 𝕜 = ContinuousMap.compStarAlgHom X (RCLike.ofRealStarAlgHom 𝕜) ⋯

@[simp]

theorem ContinuousMap.realToRCLikeStarAlgHom_apply {X : Type u_1} (𝕜 : Type u_2) [TopologicalSpace X] [RCLike 𝕜] (f : C(X, ℝ)) : (realToRCLikeStarAlgHom X 𝕜) f = realToRCLike 𝕜 f

theorem ContinuousMap.realToRCLike_star {X : Type u_1} (𝕜 : Type u_2) [TopologicalSpace X] [RCLike 𝕜] (f : C(X, ℝ)) : realToRCLike 𝕜 (star f) = star (realToRCLike 𝕜 f)

@[simp]

theorem ContinuousMap.realToRCLike_mul {X : Type u_1} (𝕜 : Type u_2) [TopologicalSpace X] [RCLike 𝕜] (f g : C(X, ℝ)) : realToRCLike 𝕜 (f * g) = realToRCLike 𝕜 f * realToRCLike 𝕜 g

def ContinuousMap.rclikeToReal {X : Type u_1} {𝕜 : Type u_2} [TopologicalSpace X] [RCLike 𝕜] (f : C(X, 𝕜)) : C(X, ℝ)

Mapping C(X, 𝕜) to C(X, ℝ) using RCLike.re.

Equations

• f.rclikeToReal = { toFun := fun (x : X) => RCLike.re (f x), continuous_toFun := ⋯ }

@[simp]

theorem ContinuousMap.rclikeToReal_apply {X : Type u_1} {𝕜 : Type u_2} [TopologicalSpace X] [RCLike 𝕜] (f : C(X, 𝕜)) (x : X) : f.rclikeToReal x = RCLike.re (f x)

theorem ContinuousMap.rclikeToReal_monotone (X : Type u_1) (𝕜 : Type u_2) [TopologicalSpace X] [RCLike 𝕜] : Monotone rclikeToReal

@[simp]

theorem ContinuousMap.continuous_rclikeToReal (X : Type u_1) (𝕜 : Type u_2) [TopologicalSpace X] [RCLike 𝕜] : Continuous rclikeToReal

@[simp]

theorem ContinuousMap.rclikeToReal_realToRCLike {X : Type u_1} (𝕜 : Type u_2) [TopologicalSpace X] [RCLike 𝕜] (f : C(X, ℝ)) : (realToRCLike 𝕜 f).rclikeToReal = f

theorem ContinuousMap.IsSelfAdjoint.realToRCLike_rclikeToReal {X : Type u_1} {𝕜 : Type u_2} [TopologicalSpace X] [RCLike 𝕜] {f : C(X, 𝕜)} (hf : IsSelfAdjoint f) : realToRCLike 𝕜 f.rclikeToReal = f

theorem ContinuousMap.range_realToRCLike_eq_isSelfAdjoint (X : Type u_1) (𝕜 : Type u_2) [TopologicalSpace X] [RCLike 𝕜] : Set.range (realToRCLike 𝕜) = {f : C(X, 𝕜) | IsSelfAdjoint f}