Theorems · Theorem · functional analysis

CStarAlgebra.isStrictlyPositive_TFAE

∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : TopologicalSpace A]
  [inst_4 : StarOrderedRing A] [inst_5 : Algebra ℝ A] [inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint]
  [inst_7 : NonnegSpectrumClass ℝ A] [IsSemitopologicalRing A] [T2Space A] {a : A},
  [IsStrictlyPositive a, IsStrictlyPositive (CFC.sqrt a) ∧ a = CFC.sqrt a * CFC.sqrt a,
      IsUnit (CFC.sqrt a) ∧ a = CFC.sqrt a * CFC.sqrt a, ∃ b, IsStrictlyPositive b ∧ a = b * b,
      ∃ b, IsUnit b ∧ IsSelfAdjoint b ∧ a = b * b, ∃ b, IsUnit b ∧ a = star b * b, ∃ b, IsUnit b ∧ a = b * star b,
      0 ≤ a ∧ IsUnit a, IsSelfAdjoint a ∧ ∀ x ∈ spectrum ℝ a, 0 < x].TFAE

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

Defined in

Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

Cited by

7 results in Mathlib

Foundations

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

Assumes

PartialOrderRingStarRingTopologicalSpaceStarOrderedRingAlgebraContinuousFunctionalCalculusNonnegSpectrumClassIsSemitopologicalRingT2Space