English
The nonunital continuous functional calculus over the larger scalar ring descends to the smaller one when the quasispectrum restricts accordingly.
Русский
Неединичный непрерывный функциональный расчёт над большим скалярным кольцом спускается к меньшему, если квази-спектрограничение выполняется.
LaTeX
$$$\\text{QuasispectrumRestricts.nonUnitalStarAlgHom}$ exists such that restriction along $f$ yields a nonunital calculus over $R$.$$
Lean4
/-- If the quasispectrum of an element restricts to a smaller scalar ring, then a non-unital
continuous functional calculus over the larger scalar ring descends to the smaller one. -/
@[simps!]
def nonUnitalStarAlgHom {R : Type u} {S : Type v} {A : Type w} [Semifield R] [StarRing R] [TopologicalSpace R]
[IsTopologicalSemiring R] [ContinuousStar R] [Field S] [StarRing S] [TopologicalSpace S] [IsTopologicalRing S]
[ContinuousStar S] [NonUnitalRing A] [StarRing A] [Algebra R S] [Module R A] [Module S A] [IsScalarTower S A A]
[SMulCommClass S A A] [IsScalarTower R S A] [StarModule R S] [ContinuousSMul R S] {a : A}
(φ : C(σₙ S a, S)₀ →⋆ₙₐ[S] A) {f : C(S, R)} (h : QuasispectrumRestricts a f) : C(σₙ R a, R)₀ →⋆ₙₐ[R] A :=
(φ.restrictScalars R).comp <|
(nonUnitalStarAlgHom_postcomp (σₙ S a) (StarAlgHom.ofId R S) (algebraMapCLM R S).continuous) |>.comp <|
nonUnitalStarAlgHom_precomp R
⟨⟨Subtype.map f h.subset_preimage,
(map_continuous f).subtype_map fun x (hx : x ∈ σₙ S a) => h.subset_preimage hx⟩,
Subtype.ext h.map_zero⟩
