Theorems · Theorem · functional analysis

CStarAlgebra.nonneg_TFAE

∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : NonUnitalRing A] [inst_2 : TopologicalSpace A] [inst_3 : StarRing A]
  [inst_4 : Module ℝ A] [inst_5 : SMulCommClass ℝ A A] [inst_6 : IsScalarTower ℝ A A] [inst_7 : StarOrderedRing A]
  [inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_9 : NonnegSpectrumClass ℝ A]
  [IsSemitopologicalRing A] [T2Space A] {a : A},
  [0 ≤ a, a = CFC.sqrt a * CFC.sqrt a, ∃ b, 0 ≤ b ∧ a = b * b, ∃ b, IsSelfAdjoint b ∧ a = b * b, ∃ b, a = star b * b,
      ∃ b, a = b * star b, a = a⁺, IsSelfAdjoint a ∧ a⁻ = 0,
      IsSelfAdjoint a ∧ QuasispectrumRestricts a ⇑ContinuousMap.realToNNReal].TFAE

For an element a in a C⋆-algebra, TFAE: 1. 0 ≤ a 2. a = sqrt a * sqrt a 3. a = b * b for some nonnegative b 4. a = b * b for some self-adjoint b 5. a = star b * b for some b 6. a = b * star b for some b 7. a = a⁺ 8. a is self-adjoint and a⁻ = 0 9. a is self-adjoint and has nonnegative spectrum

Defined in

Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

Cited by

6 results in Mathlib

Foundations

Depth 213 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

PartialOrderNonUnitalRingTopologicalSpaceStarRingModuleSMulCommClassIsScalarTowerStarOrderedRingNonUnitalContinuousFunctionalCalculusNonnegSpectrumClassIsSemitopologicalRingT2Space