Theorems · Theorem · functional analysis

StarAlgHom.ext_topologicalClosure

∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R]
  [inst_2 : TopologicalSpace A] [inst_3 : Semiring A] [inst_4 : Algebra R A] [inst_5 : StarRing A]
  [inst_6 : StarModule R A] [inst_7 : IsSemitopologicalSemiring A] [inst_8 : ContinuousStar A]
  [inst_9 : TopologicalSpace B] [inst_10 : Semiring B] [inst_11 : Algebra R B] [inst_12 : StarRing B] [T2Space B]
  {S : StarSubalgebra R A} {φ ψ : ↥S.topologicalClosure →⋆ₐ[R] B},
  Continuous ⇑φ → Continuous ⇑ψ → φ.comp (StarSubalgebra.inclusion ⋯) = ψ.comp (StarSubalgebra.inclusion ⋯) → φ = ψ

Continuous StarAlgHoms from the topological closure of a StarSubalgebra whose compositions with the StarSubalgebra.inclusion map agree are, in fact, equal.

Defined in

Mathlib.Topology.Algebra.StarSubalgebra

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommSemiringStarRingTopologicalSpaceSemiringAlgebraStarRingStarModuleIsSemitopologicalSemiringContinuousStarTopologicalSpaceSemiringAlgebraStarRingT2Space