English
For ha, and any f, the spectrum of cfc_nHom_of_cfcHom R ha f equals the spectrum of f on its domain.
Русский
Для ha и любого f спектр cfc_nHom_of_cfcHom R ha f совпадает со спектром f на своей области.
LaTeX
$$$$ \\sigma_n R (cfc\\!_nHom\\_of\\_cfcHom R ha f) = σ_n(R, f) $$$$
Lean4
/-- The composition of `cfcₙHom` with the natural embedding `C(s, R)₀ → C(quasispectrum R a, R)₀`
whenever `quasispectrum R a ⊆ s`.
This is sometimes necessary in order to consider the same continuous functions applied to multiple
distinct elements, with the added constraint that `cfcₙ` does not suffice. This can occur, for
example, if it is necessary to use uniqueness of this continuous functional calculus. A practical
example can be found in the proof of `CFC.posPart_negPart_unique`. -/
@[simps!]
noncomputable def cfcₙHomSuperset {a : A} (ha : p a) {s : Set R} (hs : σₙ R a ⊆ s) :
haveI : Fact (0 ∈ s) := ⟨hs (quasispectrum.zero_mem R a)⟩
C(s, R)₀ →⋆ₙₐ[R] A :=
have : Fact (0 ∈ s) := ⟨hs (quasispectrum.zero_mem R a)⟩
cfcₙHom ha (R := R) |>.comp <|
ContinuousMapZero.nonUnitalStarAlgHom_precomp R <| ⟨⟨_, continuous_id.subtype_map hs⟩, rfl⟩
