range_cfcₙHom — Mathlib

English

The range of the nonunital star calculus homomorphism cfcₙHom ha is exactly the elemental subalgebra generated by a.

Русский

Диапазон неконечной звездообразной функциональной алгебры cfcₙHom ha равен элементарной подалгебре, порожденной a.

LaTeX

$$$\\mathrm{range}(\\mathrm{cfc\\,ₙHom}\\; ha) = \\mathrm{elemental}\\; 𝕜\\; a$$$

Lean4

theorem range_cfcₙHom {a : A} (ha : p a) : NonUnitalStarAlgHom.range (cfcₙHom ha (R := 𝕜)) = elemental 𝕜 a :=
  by
  rw [← NonUnitalStarAlgebra.map_top, ← ContinuousMapZero.elemental_eq_top, NonUnitalStarAlgebra.elemental, ←
    NonUnitalStarSubalgebra.topologicalClosure_map _ (cfcₙHom_isClosedEmbedding ha (R := 𝕜)).isClosedMap
      (cfcₙHom_continuous ha),
    NonUnitalStarAlgHom.map_adjoin]
  congr
  simpa using cfcₙHom_id ha

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