range_cfcHom — Mathlib

English

For any a with p a, the range of the continuous functional calculus cfc is exactly the subalgebra generated by a (the elemental subalgebra).

Русский

Для элемента a с условием p a образ непрерывного функционального калькулятора совпадает с подалгеброй, порождённой a (elemental).

LaTeX

$$$\\mathrm{range}(\\mathrm{cfc}\\;\\{a\\}) = \\text{elemental }\\;\\mathbb{K}\\; a,$$$

Lean4

theorem range_cfcHom {a : A} (ha : p a) : (cfcHom ha (R := 𝕜)).range = elemental 𝕜 a :=
  by
  rw [StarAlgHom.range_eq_map_top, ← ContinuousMap.elemental_id_eq_top, StarAlgebra.elemental, ←
    StarSubalgebra.topologicalClosure_map _ _ (cfcHom_isClosedEmbedding ha (R := 𝕜)).isClosedMap (cfcHom_continuous ha),
    StarAlgHom.map_adjoin]
  congr
  simpa using cfcHom_id ha

Похожие утверждения