English
For predicates p a and q a with SpectrumRestricts a f, the restricted cfcₙHom equals the nonUnitalStarAlgHom applied to the q-case cfcₙHom.
Русский
При p и q и SpectrumRestricts a f, ограниченный cfcₙHom равен nonUnitalStarAlgHom, применённому к cfcₙHom(qa).
LaTeX
$$$cfc\\nHom\\ hpa = h.nonUnitalStarAlgHom (cfc\\nHom hqa)$$$
Lean4
/-- Given a `NonUnitalContinuousFunctionalCalculus S A q`. If we form the predicate `p` for `a : A`
characterized by: `q a` and the quasispectrum of `a` restricts to the scalar subring `R` via
`f : C(S, R)`, then we can get a restricted functional calculus
`NonUnitalContinuousFunctionalCalculus R A p`. -/
protected theorem cfc (f : C(S, R)) (halg : IsUniformEmbedding (algebraMap R S)) (h0 : p 0)
(h : ∀ a, p a ↔ q a ∧ QuasispectrumRestricts a f) : NonUnitalContinuousFunctionalCalculus R A p
where
predicate_zero := h0
compactSpace_quasispectrum
a := by
have := NonUnitalContinuousFunctionalCalculus.compactSpace_quasispectrum (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.nonUnitalStarAlgHom (cfcₙHom ((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_nonUnitalStarAlgHom (cfcₙHom_isClosedEmbedding ((h a).mp ha).1) halg
case hom_id => exact ((h a).mp ha).2.nonUnitalStarAlgHom_id <| cfcₙHom_id ((h a).mp ha).1
case hom_map_spectrum =>
intro g
rw [nonUnitalStarAlgHom_apply]
simp only [← @quasispectrum.preimage_algebraMap (R := R) S, cfcₙHom_map_quasispectrum]
ext x
constructor
· rintro ⟨y, hy⟩
have := congr_arg f hy
simp only [comp_apply, coe_mk, ContinuousMap.coe_mk, 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, quasispectrum.algebraMap_mem S y.prop⟩, ?_⟩
simp only [comp_apply, coe_mk, ContinuousMap.coe_mk, StarAlgHom.ofId_apply]
congr
exact Subtype.ext (((h a).mp ha).2.left_inv y)
case predicate_hom =>
intro g
rw [h]
refine ⟨cfcₙHom_predicate _ _, ?_⟩
refine { rightInvOn := fun s hs ↦ ?_, left_inv := ((h a).mp ha).2.left_inv }
rw [nonUnitalStarAlgHom_apply, cfcₙHom_map_quasispectrum] at hs
obtain ⟨r, rfl⟩ := hs
simp [((h a).mp ha).2.left_inv _]
