Star structures on continuous maps.

Star structure

If β has a continuous star operation, we put a star structure on C(α, β) by using the star operation pointwise.

If β is a ⋆-ring, then C(α, β) inherits a ⋆-ring structure.

If β is a ⋆-ring and a ⋆-module over R, then the space of continuous functions from α to β is a ⋆-module over R.

instance ContinuousMap.instStar {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [Star β] [ContinuousStar β] : Star C(α, β)

Equations

• ContinuousMap.instStar = { star := fun (f : C(α, β)) => starContinuousMap.comp f }

@[simp]

theorem ContinuousMap.coe_star {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [Star β] [ContinuousStar β] (f : C(α, β)) : ⇑(star f) = star ⇑f

@[simp]

theorem ContinuousMap.star_apply {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [Star β] [ContinuousStar β] (f : C(α, β)) (x : α) : (star f) x = star (f x)

instance ContinuousMap.instTrivialStar {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [Star β] [ContinuousStar β] [TrivialStar β] : TrivialStar C(α, β)

Equations

• ⋯ = ⋯

instance ContinuousMap.instInvolutiveStarOfContinuousStar {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [InvolutiveStar β] [ContinuousStar β] : InvolutiveStar C(α, β)

Equations

• ContinuousMap.instInvolutiveStarOfContinuousStar = InvolutiveStar.mk ⋯

instance ContinuousMap.starAddMonoid {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [AddMonoid β] [ContinuousAdd β] [StarAddMonoid β] [ContinuousStar β] : StarAddMonoid C(α, β)

Equations

• ContinuousMap.starAddMonoid = StarAddMonoid.mk ⋯

instance ContinuousMap.starMul {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [Mul β] [ContinuousMul β] [StarMul β] [ContinuousStar β] : StarMul C(α, β)

Equations

• ContinuousMap.starMul = StarMul.mk ⋯

instance ContinuousMap.instStarRingOfContinuousStar {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [NonUnitalNonAssocSemiring β] [TopologicalSemiring β] [StarRing β] [ContinuousStar β] : StarRing C(α, β)

Equations

• ContinuousMap.instStarRingOfContinuousStar = StarRing.mk ⋯

instance ContinuousMap.instStarModule {R : Type u_1} {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [Star R] [Star β] [SMul R β] [StarModule R β] [ContinuousStar β] [ContinuousConstSMul R β] : StarModule R C(α, β)

Equations

• ⋯ = ⋯

def ContinuousMap.compStarAlgHom' {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (𝕜 : Type u_4) [CommSemiring 𝕜] (A : Type u_5) [TopologicalSpace A] [Semiring A] [TopologicalSemiring A] [Star A] [ContinuousStar A] [Algebra 𝕜 A] (f : C(X, Y)) : C(Y, A) →⋆ₐ[𝕜] C(X, A)

The functorial map taking f : C(X, Y) to C(Y, A) →⋆ₐ[𝕜] C(X, A) given by pre-composition with the continuous function f. See ContinuousMap.compMonoidHom' and ContinuousMap.compAddMonoidHom', ContinuousMap.compRightAlgHom for bundlings of pre-composition into a MonoidHom, an AddMonoidHom and an AlgHom, respectively, under suitable assumptions on A.

Equations

• ContinuousMap.compStarAlgHom' 𝕜 A f = { toFun := fun (g : C(Y, A)) => g.comp f, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯, map_star' := ⋯ }

@[simp]

theorem ContinuousMap.compStarAlgHom'_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (𝕜 : Type u_4) [CommSemiring 𝕜] (A : Type u_5) [TopologicalSpace A] [Semiring A] [TopologicalSemiring A] [Star A] [ContinuousStar A] [Algebra 𝕜 A] (f : C(X, Y)) (g : C(Y, A)) : (ContinuousMap.compStarAlgHom' 𝕜 A f) g = g.comp f

theorem ContinuousMap.compStarAlgHom'_id {X : Type u_1} [TopologicalSpace X] (𝕜 : Type u_4) [CommSemiring 𝕜] (A : Type u_5) [TopologicalSpace A] [Semiring A] [TopologicalSemiring A] [Star A] [ContinuousStar A] [Algebra 𝕜 A] : ContinuousMap.compStarAlgHom' 𝕜 A (ContinuousMap.id X) = StarAlgHom.id 𝕜 C(X, A)

ContinuousMap.compStarAlgHom' sends the identity continuous map to the identity StarAlgHom

theorem ContinuousMap.compStarAlgHom'_comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (𝕜 : Type u_4) [CommSemiring 𝕜] (A : Type u_5) [TopologicalSpace A] [Semiring A] [TopologicalSemiring A] [Star A] [ContinuousStar A] [Algebra 𝕜 A] (g : C(Y, Z)) (f : C(X, Y)) : ContinuousMap.compStarAlgHom' 𝕜 A (g.comp f) = (ContinuousMap.compStarAlgHom' 𝕜 A f).comp (ContinuousMap.compStarAlgHom' 𝕜 A g)

ContinuousMap.compStarAlgHom' is functorial.

def ContinuousMap.compStarAlgHom (X : Type u_1) {𝕜 : Type u_2} {A : Type u_3} {B : Type u_4} [TopologicalSpace X] [CommSemiring 𝕜] [TopologicalSpace A] [Semiring A] [TopologicalSemiring A] [Star A] [ContinuousStar A] [Algebra 𝕜 A] [TopologicalSpace B] [Semiring B] [TopologicalSemiring B] [Star B] [ContinuousStar B] [Algebra 𝕜 B] (φ : A →⋆ₐ[𝕜] B) (hφ : Continuous ⇑φ) : C(X, A) →⋆ₐ[𝕜] C(X, B)

Post-composition with a continuous star algebra homomorphism is a star algebra homomorphism between spaces of continuous maps.

Equations

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

@[simp]

theorem ContinuousMap.compStarAlgHom_apply (X : Type u_1) {𝕜 : Type u_2} {A : Type u_3} {B : Type u_4} [TopologicalSpace X] [CommSemiring 𝕜] [TopologicalSpace A] [Semiring A] [TopologicalSemiring A] [Star A] [ContinuousStar A] [Algebra 𝕜 A] [TopologicalSpace B] [Semiring B] [TopologicalSemiring B] [Star B] [ContinuousStar B] [Algebra 𝕜 B] (φ : A →⋆ₐ[𝕜] B) (hφ : Continuous ⇑φ) (f : C(X, A)) : (ContinuousMap.compStarAlgHom X φ hφ) f = { toFun := ⇑φ, continuous_toFun := hφ }.comp f

theorem ContinuousMap.compStarAlgHom_id (X : Type u_1) {𝕜 : Type u_2} {A : Type u_3} [TopologicalSpace X] [CommSemiring 𝕜] [TopologicalSpace A] [Semiring A] [TopologicalSemiring A] [Star A] [ContinuousStar A] [Algebra 𝕜 A] : ContinuousMap.compStarAlgHom X (StarAlgHom.id 𝕜 A) ⋯ = StarAlgHom.id 𝕜 C(X, A)

ContinuousMap.compStarAlgHom sends the identity StarAlgHom on A to the identity StarAlgHom on C(X, A).

theorem ContinuousMap.compStarAlgHom_comp (X : Type u_1) {𝕜 : Type u_2} {A : Type u_3} {B : Type u_4} {C : Type u_5} [TopologicalSpace X] [CommSemiring 𝕜] [TopologicalSpace A] [Semiring A] [TopologicalSemiring A] [Star A] [ContinuousStar A] [Algebra 𝕜 A] [TopologicalSpace B] [Semiring B] [TopologicalSemiring B] [Star B] [ContinuousStar B] [Algebra 𝕜 B] [TopologicalSpace C] [Semiring C] [TopologicalSemiring C] [Star C] [ContinuousStar C] [Algebra 𝕜 C] (φ : A →⋆ₐ[𝕜] B) (ψ : B →⋆ₐ[𝕜] C) (hφ : Continuous ⇑φ) (hψ : Continuous ⇑ψ) : ContinuousMap.compStarAlgHom X (ψ.comp φ) ⋯ = (ContinuousMap.compStarAlgHom X ψ hψ).comp (ContinuousMap.compStarAlgHom X φ hφ)

ContinuousMap.compStarAlgHom is functorial.

def Homeomorph.compStarAlgEquiv' {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (𝕜 : Type u_3) [CommSemiring 𝕜] (A : Type u_4) [TopologicalSpace A] [Semiring A] [TopologicalSemiring A] [StarRing A] [ContinuousStar A] [Algebra 𝕜 A] (f : X ≃ₜ Y) : C(Y, A) ≃⋆ₐ[𝕜] C(X, A)

ContinuousMap.compStarAlgHom' as a StarAlgEquiv when the continuous map f is actually a homeomorphism.

Equations

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

@[simp]

theorem Homeomorph.compStarAlgEquiv'_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (𝕜 : Type u_3) [CommSemiring 𝕜] (A : Type u_4) [TopologicalSpace A] [Semiring A] [TopologicalSemiring A] [StarRing A] [ContinuousStar A] [Algebra 𝕜 A] (f : X ≃ₜ Y) (a : C(Y, A)) : (Homeomorph.compStarAlgEquiv' 𝕜 A f) a = (ContinuousMap.compStarAlgHom' 𝕜 A ↑f) a

@[simp]

theorem Homeomorph.compStarAlgEquiv'_symm_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (𝕜 : Type u_3) [CommSemiring 𝕜] (A : Type u_4) [TopologicalSpace A] [Semiring A] [TopologicalSemiring A] [StarRing A] [ContinuousStar A] [Algebra 𝕜 A] (f : X ≃ₜ Y) (a : C(X, A)) : (Homeomorph.compStarAlgEquiv' 𝕜 A f).symm a = (ContinuousMap.compStarAlgHom' 𝕜 A ↑f.symm) a

Evaluation as a bundled map

def ContinuousMap.evalStarAlgHom {X : Type u_1} (S : Type u_2) (R : Type u_3) [TopologicalSpace X] [CommSemiring S] [CommSemiring R] [Algebra S R] [TopologicalSpace R] [TopologicalSemiring R] [StarRing R] [ContinuousStar R] (x : X) : C(X, R) →⋆ₐ[S] R

Evaluation of continuous maps at a point, bundled as a star algebra homomorphism.

Equations

• ContinuousMap.evalStarAlgHom S R x = { toAlgHom := ContinuousMap.evalAlgHom S R x, map_star' := ⋯ }

@[simp]

theorem ContinuousMap.evalStarAlgHom_apply {X : Type u_1} (S : Type u_2) (R : Type u_3) [TopologicalSpace X] [CommSemiring S] [CommSemiring R] [Algebra S R] [TopologicalSpace R] [TopologicalSemiring R] [StarRing R] [ContinuousStar R] (x : X) (f : C(X, R)) : (ContinuousMap.evalStarAlgHom S R x) f = f x