English
If φ is a closed embedding, SpectrumRestricts yields a closed embedding for the descended star-algebra homomorphism under an appropriate uniform embedding assumption.
Русский
Если φ — замкнутое вложение, то при ограничении спектра получается замкнутое вложение для спускного звездоалгебрного однородного отображения при подходящем предположении о равномерном вложении.
LaTeX
$$$\\text{IsClosedEmbedding}(\\mathrm{h.starAlgHom}(\\phi))$ under the given hypotheses.$$
Lean4
/-- If the spectrum of an element restricts to a smaller scalar ring, then a continuous functional
calculus over the larger scalar ring descends to the smaller one. -/
@[simps!]
def starAlgHom {R : Type u} {S : Type v} {A : Type w} [Semifield R] [StarRing R] [TopologicalSpace R]
[IsTopologicalSemiring R] [ContinuousStar R] [Semifield S] [StarRing S] [TopologicalSpace S]
[IsTopologicalSemiring S] [ContinuousStar S] [Ring A] [StarRing A] [Algebra R S] [Algebra R A] [Algebra S A]
[IsScalarTower R S A] [StarModule R S] [ContinuousSMul R S] {a : A} (φ : C(spectrum S a, S) →⋆ₐ[S] A) {f : C(S, R)}
(h : SpectrumRestricts a f) : C(spectrum R a, R) →⋆ₐ[R] A :=
(φ.restrictScalars R).comp <|
(ContinuousMap.compStarAlgHom (spectrum S a) (.ofId R S) (algebraMapCLM R S).continuous).comp <|
ContinuousMap.compStarAlgHom' R R
⟨Subtype.map f h.subset_preimage,
(map_continuous f).subtype_map fun x (hx : x ∈ spectrum S a) => h.subset_preimage hx⟩
