English
Let p and q be predicates on A and suppose p 0 holds. If there exists a function f: C(S, R) and a uniform-embedding of algebras satisfying p a iff q a and SpectrumRestricts a f for all a ∈ A, then there is a restricted continuous functional calculus on A over the scalar subring R with predicate p; i.e., one can form ContinuousFunctionalCalculus R A p.
Русский
Пусть p и q — предикаты на A и выполняется p(0). Если существует функция f: C(S, R) и вложение алгебр, такое что для каждого a ∈ A выполняется p(a) ⇔ q(a) ∧ SpectrumRestricts(a, f), тогда существует ограниченный непрерывный функциональный расчёт над A на подкольце R с предикатом p; т.е. существует ContinuousFunctionalCalculus R A p.
LaTeX
$$$ p(0) \\wedge \\left( \\forall a \\in A,\\ p(a) \\;\\iff\\; q(a) \\land \\ SpectrumRestricts(a,f) \\right) \\ \\Longrightarrow\\ \\text{ContinuousFunctionalCalculus } R A p $$$
Lean4
/-- Given a `ContinuousFunctionalCalculus S A q`. If we form the predicate `p` for `a : A`
characterized by: `q a` and the spectrum of `a` restricts to the scalar subring `R` via
`f : C(S, R)`, then we can get a restricted functional calculus
`ContinuousFunctionalCalculus R A p`. -/
protected theorem cfc (f : C(S, R)) (halg : IsUniformEmbedding (algebraMap R S)) (h0 : p 0)
(h : ∀ a, p a ↔ q a ∧ SpectrumRestricts a f) : ContinuousFunctionalCalculus R A p
where
predicate_zero := h0
spectrum_nonempty a
ha := ((h a).mp ha).2.image ▸ (ContinuousFunctionalCalculus.spectrum_nonempty a ((h a).mp ha).1 |>.image f)
compactSpace_spectrum
a := by
have := ContinuousFunctionalCalculus.compactSpace_spectrum (R := S) a
rw [← isCompact_iff_compactSpace] at this ⊢
simpa using halg.isClosedEmbedding.isCompact_preimage this
exists_cfc_of_predicate a
ha :=
by
refine
⟨((h a).mp ha).2.starAlgHom (cfcHom ((h a).mp ha).1 (R := S)), ?hom_isClosedEmbedding, ?hom_id, ?hom_map_spectrum,
?predicate_hom⟩
case hom_isClosedEmbedding =>
exact ((h a).mp ha).2.isClosedEmbedding_starAlgHom (cfcHom_isClosedEmbedding ((h a).mp ha).1) halg
case hom_id => exact ((h a).mp ha).2.starAlgHom_id <| cfcHom_id ((h a).mp ha).1
case hom_map_spectrum =>
intro g
rw [SpectrumRestricts.starAlgHom_apply]
simp only [← @spectrum.preimage_algebraMap (R := R) S, cfcHom_map_spectrum]
ext x
constructor
· rintro ⟨y, hy⟩
have := congr_arg f hy
simp only [ContinuousMap.coe_mk, ContinuousMap.comp_apply, StarAlgHom.ofId_apply] at this
rw [((h a).mp ha).2.left_inv _, ((h a).mp ha).2.left_inv _] at this
exact ⟨_, this⟩
· rintro ⟨y, rfl⟩
rw [Set.mem_preimage]
refine ⟨⟨algebraMap R S y, spectrum.algebraMap_mem S y.prop⟩, ?_⟩
simp only [ContinuousMap.coe_mk, ContinuousMap.comp_apply, StarAlgHom.ofId_apply]
congr
exact Subtype.ext (((h a).mp ha).2.left_inv y)
case predicate_hom =>
intro g
rw [h]
refine ⟨cfcHom_predicate _ _, ?_⟩
refine .of_rightInvOn (((h a).mp ha).2.left_inv) fun s hs ↦ ?_
rw [SpectrumRestricts.starAlgHom_apply, cfcHom_map_spectrum] at hs
obtain ⟨r, rfl⟩ := hs
simp [((h a).mp ha).2.left_inv _]
