# 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`.

source
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 }

source
@[simp]
theorem ContinuousMap.coe_star {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [Star β] [ContinuousStar β] (f : C(α, β)) :
⇑(star f) = star ⇑f
source
@[simp]
theorem ContinuousMap.star_apply {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [Star β] [ContinuousStar β] (f : C(α, β)) (x : α) :
(star f) x = star (f x)
source
instance ContinuousMap.instTrivialStar {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [Star β] [ContinuousStar β] [TrivialStar β] :
TrivialStar C(α, β)
source
instance ContinuousMap.instInvolutiveStarOfContinuousStar {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [InvolutiveStar β] [ContinuousStar β] :
InvolutiveStar C(α, β)
Equations

- ContinuousMap.instInvolutiveStarOfContinuousStar = { toStar := ContinuousMap.instStar, star_involutive := ⋯ }

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

- ContinuousMap.starAddMonoid = { toInvolutiveStar := ContinuousMap.instInvolutiveStarOfContinuousStar, star_add := ⋯ }

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

- ContinuousMap.starMul = { toInvolutiveStar := ContinuousMap.instInvolutiveStarOfContinuousStar, star_mul := ⋯ }

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

- ContinuousMap.instStarRingOfContinuousStar = { toInvolutiveStar := ContinuousMap.starAddMonoid.toInvolutiveStar, star_mul := ⋯, star_add := ⋯ }

source
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(α, β)
source
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] [IsTopologicalSemiring 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' := ⋯ }

Instances For

source
@[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] [IsTopologicalSemiring A] [Star A] [ContinuousStar A] [Algebra 𝕜 A] (f : C(X, Y)) (g : C(Y, A)) :
(compStarAlgHom' 𝕜 A f) g = g.comp f
source
theorem ContinuousMap.compStarAlgHom'_id {X : Type u_1} [TopologicalSpace X] (𝕜 : Type u_4) [CommSemiring 𝕜] (A : Type u_5) [TopologicalSpace A] [Semiring A] [IsTopologicalSemiring A] [Star A] [ContinuousStar A] [Algebra 𝕜 A] :
compStarAlgHom' 𝕜 A (ContinuousMap.id X) = StarAlgHom.id 𝕜 C(X, A)

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

source
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] [IsTopologicalSemiring A] [Star A] [ContinuousStar A] [Algebra 𝕜 A] (g : C(Y, Z)) (f : C(X, Y)) :
compStarAlgHom' 𝕜 A (g.comp f) = (compStarAlgHom' 𝕜 A f).comp (compStarAlgHom' 𝕜 A g)

`ContinuousMap.compStarAlgHom'` is functorial.

source
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] [IsTopologicalSemiring A] [Star A] [ContinuousStar A] [Algebra 𝕜 A] [TopologicalSpace B] [Semiring B] [IsTopologicalSemiring 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.

Instances For

source
@[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] [IsTopologicalSemiring A] [Star A] [ContinuousStar A] [Algebra 𝕜 A] [TopologicalSpace B] [Semiring B] [IsTopologicalSemiring B] [Star B] [ContinuousStar B] [Algebra 𝕜 B] (φ : A →⋆ₐ[𝕜] B) (hφ : Continuous ⇑φ) (f : C(X, A)) :
(compStarAlgHom X φ hφ) f = { toFun := ⇑φ, continuous_toFun := hφ }.comp f
source
theorem ContinuousMap.compStarAlgHom_id (X : Type u_1) {𝕜 : Type u_2} {A : Type u_3} [TopologicalSpace X] [CommSemiring 𝕜] [TopologicalSpace A] [Semiring A] [IsTopologicalSemiring A] [Star A] [ContinuousStar A] [Algebra 𝕜 A] :
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)`.

source
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] [IsTopologicalSemiring A] [Star A] [ContinuousStar A] [Algebra 𝕜 A] [TopologicalSpace B] [Semiring B] [IsTopologicalSemiring B] [Star B] [ContinuousStar B] [Algebra 𝕜 B] [TopologicalSpace C] [Semiring C] [IsTopologicalSemiring C] [Star C] [ContinuousStar C] [Algebra 𝕜 C] (φ : A →⋆ₐ[𝕜] B) (ψ : B →⋆ₐ[𝕜] C) (hφ : Continuous ⇑φ) (hψ : Continuous ⇑ψ) :
compStarAlgHom X (ψ.comp φ) ⋯ = (compStarAlgHom X ψ hψ).comp (compStarAlgHom X φ hφ)

`ContinuousMap.compStarAlgHom` is functorial.

source
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] [IsTopologicalSemiring 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.

Instances For

source
@[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] [IsTopologicalSemiring A] [StarRing A] [ContinuousStar A] [Algebra 𝕜 A] (f : X ≃ₜ Y) (a : C(Y, A)) :
(compStarAlgEquiv' 𝕜 A f) a = (ContinuousMap.compStarAlgHom' 𝕜 A ↑f) a
source
@[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] [IsTopologicalSemiring A] [StarRing A] [ContinuousStar A] [Algebra 𝕜 A] (f : X ≃ₜ Y) (a : C(X, A)) :
(compStarAlgEquiv' 𝕜 A f).symm a = (ContinuousMap.compStarAlgHom' 𝕜 A ↑f.symm) a

### Evaluation as a bundled map #

source
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] [IsTopologicalSemiring 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' := ⋯ }

Instances For

source
@[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] [IsTopologicalSemiring R] [StarRing R] [ContinuousStar R] (x : X) (f : C(X, R)) :
(evalStarAlgHom S R x) f = f x