English
The spectral order on a C*-algebra makes it a StarOrderedRing.
Русский
Спектральный порядок на C*-алгебре превращает её в StarOrderedRing.
LaTeX
$$Theorem: StarOrderedRing of CStarAlgebra.spectralOrder$$
Lean4
/-- The partial order on a C⋆-algebra defined by `x ≤ y` if and only if `y - x` is
selfadjoint and has nonnegative spectrum.
This is not declared as an instance because one may already have a partial order with better
definitional properties. However, it can be useful to invoke this as an instance in proofs. -/
@[reducible]
def spectralOrder : PartialOrder A
where
le x y := IsSelfAdjoint (y - x) ∧ QuasispectrumRestricts (y - x) ContinuousMap.realToNNReal
le_refl := by
simp only [sub_self, IsSelfAdjoint.zero, true_and, forall_const]
rw [quasispectrumRestricts_iff_spectrumRestricts_inr' ℂ, SpectrumRestricts.nnreal_iff]
nontriviality A
simp
le_antisymm x y hxy
hyx :=
by
rw [← Unitization.isSelfAdjoint_inr (R := ℂ), quasispectrumRestricts_iff_spectrumRestricts_inr' ℂ,
Unitization.inr_sub ℂ] at hxy hyx
rw [← sub_eq_zero]
apply Unitization.inr_injective (R := ℂ)
rw [Unitization.inr_zero, Unitization.inr_sub]
exact hyx.2.eq_zero_of_neg hyx.1 (neg_sub (x : A⁺¹) (y : A⁺¹) ▸ hxy.2)
le_trans x y z hxy
hyz :=
by
simp +singlePass only [← Unitization.isSelfAdjoint_inr (R := ℂ),
quasispectrumRestricts_iff_spectrumRestricts_inr' ℂ] at hxy hyz ⊢
exact ⟨by simpa using hyz.1.add hxy.1, by simpa using hyz.2.nnreal_add hyz.1 hxy.1 hxy.2⟩
