English
In a C*-algebra with the required structure, the following nine conditions are equivalent: (1) a is strictly positive; (2) sqrt(a) is strictly positive and a = sqrt(a) sqrt(a); (3) sqrt(a) is a unit and a = sqrt(a) sqrt(a); (4) a = b^2 with b strictly positive; (5) a = b^2 with b unit, self-adjoint; (6) a = b^* b with b unit; (7) a = b b^* with b unit; (8) 0 ≤ a and a is a unit; (9) a is self-adjoint and has strictly positive spectrum.
Русский
В алгебре C*- с требуемой структурой взаимно эквивалентны девять условий, перечисленных выше (TF AE).
LaTeX
$$\text{IsStrictlyPositive}(a) \\iff \text{IsStrictlyPositive}(\sqrt{a}) \land a = \sqrt{a} \cdot \sqrt{a} \\iff \text{IsUnit}(\sqrt{a}) \land a = \sqrt{a} \cdot \sqrt{a} \\iff \exists b, \text{IsStrictlyPositive}(b) \land a = b \cdot b \\iff \exists b, \text{IsUnit}(b) \land \text{IsSelfAdjoint}(b) \land a = b \cdot b \\iff \exists b, \text{IsUnit}(b) \land a = \star b \cdot b \\iff \exists b, \text{IsUnit}(b) \land a = b \cdot \star b \\iff (0 \le a) \land \text{IsUnit}(a) \\iff \text{IsSelfAdjoint}(a) \land \forall x \in \operatorname{spectrum}_{\mathbb{R}}(a), 0 < x$$
Lean4
/-- 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. -/
theorem _root_.CStarAlgebra.isStrictlyPositive_TFAE {a : A} :
[IsStrictlyPositive a, IsStrictlyPositive (sqrt a) ∧ a = sqrt a * sqrt a, IsUnit (sqrt a) ∧ a = sqrt a * 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 :=
by
tfae_have 1 ↔ 8 := IsStrictlyPositive.iff_of_unital
tfae_have 1 ↔ 9 :=
⟨fun h => ⟨h.isSelfAdjoint, StarOrderedRing.isStrictlyPositive_iff_spectrum_pos a |>.mp h⟩, fun h =>
(StarOrderedRing.isStrictlyPositive_iff_spectrum_pos a).mpr h.2⟩
tfae_have 1 → 2 := fun h => ⟨h.sqrt, sqrt_mul_sqrt_self a |>.symm⟩
tfae_have 2 → 3 := fun h => ⟨h.1.isUnit, h.2⟩
tfae_have 3 → 4 := fun h => ⟨sqrt a, h.1.isStrictlyPositive (sqrt_nonneg _), h.2⟩
tfae_have 4 → 5 := fun ⟨b, hb, hab⟩ => ⟨b, hb.isUnit, hb.isSelfAdjoint, hab⟩
tfae_have 5 → 6 := fun ⟨b, hb, hbsa, hab⟩ => ⟨b, hb, hbsa.symm ▸ hab⟩
tfae_have 6 → 7 := fun ⟨b, hb, hab⟩ => ⟨star b, hb.star, star_star b |>.symm ▸ hab⟩
tfae_have 7 → 8 := fun ⟨b, hb, hab⟩ => ⟨hab ▸ mul_star_self_nonneg _, hab ▸ hb.mul hb.star⟩
tfae_finish
