Facts about star-ordered rings that depend on the continuous functional calculus #
This file contains various basic facts about star-ordered rings (i.e. mainly C⋆-algebras) that depend on the continuous functional calculus.
We also put an order instance on Unitization ℂ A
when A
is a C⋆-algebra via
the spectral order.
Main theorems #
IsSelfAdjoint.le_algebraMap_norm_self
andIsSelfAdjoint.le_algebraMap_norm_self
, which respectively show thata ≤ algebraMap ℝ A ‖a‖
and-(algebraMap ℝ A ‖a‖) ≤ a
in a C⋆-algebra.mul_star_le_algebraMap_norm_sq
andstar_mul_le_algebraMap_norm_sq
, which give similar statements fora * star a
andstar a * a
.CStarAlgebra.norm_le_norm_of_nonneg_of_le
: in a non-unital C⋆-algebra, if0 ≤ a ≤ b
, then‖a‖ ≤ ‖b‖
.CStarAlgebra.conjugate_le_norm_smul
: in a non-unital C⋆-algebra, we have thatstar a * b * a ≤ ‖b‖ • (star a * a)
(and a primed version for thea * b * star a
case).CStarAlgebra.inv_le_inv_iff
: in a unital C⋆-algebra,b⁻¹ ≤ a⁻¹
iffa ≤ b
.
Tags #
continuous functional calculus, normal, selfadjoint
Equations
- Unitization.instPartialOrder = CStarAlgebra.spectralOrder (Unitization ℂ A)
Equations
- ⋯ = ⋯
cfc_le_iff
only applies to a scalar ring where R
is an actual Ring
, and not a Semiring
.
However, this theorem still holds for ℝ≥0
as long as the algebra A
itself is an ℝ
-algebra.
In a unital ℝ
-algebra A
with a continuous functional calculus, an element a : A
is larger
than some algebraMap ℝ A r
if and only if every element of the ℝ
-spectrum is nonnegative.
In a unital C⋆-algebra, if a
is nonnegative and invertible, and a ≤ b
, then b
is
invertible.
In a unital C⋆-algebra, if 0 ≤ a ≤ b
and a
and b
are units, then b⁻¹ ≤ a⁻¹
.
In a unital C⋆-algebra, if 0 ≤ a
and 0 ≤ b
and a
and b
are units, then a⁻¹ ≤ b⁻¹
if and only if b ≤ a
.
Equations
- ⋯ = ⋯
The set of nonnegative elements in a C⋆-algebra is closed.