Theorems · Theorem · general topology

ContinuousMap.starAlgHom_ext_map_X

∀ {𝕜 : Type u_1} {A : Type u_2} [inst : RCLike 𝕜] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : Algebra 𝕜 A]
  [inst_4 : TopologicalSpace A] [T2Space A] {s : Set 𝕜} [CompactSpace ↑s] {φ ψ : C(↑s, 𝕜) →⋆ₐ[𝕜] A},
  Continuous ⇑φ →
    Continuous ⇑ψ →
      φ ((Polynomial.toContinuousMapOnAlgHom s) Polynomial.X) =
          ψ ((Polynomial.toContinuousMapOnAlgHom s) Polynomial.X) →
        φ = ψ

Continuous star algebra homomorphisms from C(s, 𝕜) into a star 𝕜-algebra A which agree at X : 𝕜[X] (interpreted as a continuous map) are, in fact, equal.

Defined in

Mathlib.Topology.ContinuousMap.StoneWeierstrass

Cited by

0 results in Mathlib

Foundations

Depth 194 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RCLikeRingStarRingAlgebraTopologicalSpaceT2SpaceCompactSpace