feat(Analysis/CStarAlgebra): IsIdempotentElem a ↔ spectrum R a ⊆ {0, 1} (#35916)

... also adds a tfae for `IsStarProjection` in C*-algebras and that if `star x * x` is idempotent then so is `x * star x`.

Author: themathqueen

Mathlib.lean

@@ -1585,6 +1585,7 @@ public import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnit
 public import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Note
 public import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
 public import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Pi
+public import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Projection
 public import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range
 public import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict
 public import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique

Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Projection.lean

@@ -0,0 +1,40 @@
+/-
+Copyright (c) 2026 Monica Omar. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Monica Omar
+-/
+module
+
+public import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
+import Mathlib.FieldTheory.IsAlgClosed.Spectrum
+
+/-! # Continuous functional caculus and projections
+
+This file collects some results related to projections, idempotents,
+and the continuous functional calculus. -/
+
+public section
+
+section Field
+variable (R : Type*) {A : Type*} {p : A → Prop} [Field R] [StarRing R] [MetricSpace R]
+  [IsTopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A]
+
+theorem isIdempotentElem_iff_quasispectrum_subset [NonUnitalRing A] [StarRing A] [Module R A]
+    [IsScalarTower R A A] [SMulCommClass R A A] [NonUnitalContinuousFunctionalCalculus R A p]
+    (a : A) (ha : p a) : IsIdempotentElem a ↔ quasispectrum R a ⊆ {0, 1} := by
+  refine ⟨IsIdempotentElem.quasispectrum_subset R, fun h ↦ ?_⟩
+  rw [IsIdempotentElem, ← cfcₙ_id' R a, ← cfcₙ_mul _ _]
+  exact cfcₙ_congr fun x hx ↦ by grind
+
+theorem isIdempotentElem_iff_spectrum_subset [Ring A] [StarRing A] [Algebra R A]
+    [NonUnitalContinuousFunctionalCalculus R A p] (a : A) (ha : p a) :
+    IsIdempotentElem a ↔ spectrum R a ⊆ {0, 1} := by
+  grind [quasispectrum_eq_spectrum_union_zero, isIdempotentElem_iff_quasispectrum_subset R]
+
+end Field
+
+theorem isIdempotentElem_star_mul_self_iff_isIdempotentElem_self_mul_star {A : Type*}
+    [TopologicalSpace A] [NonUnitalRing A] [StarRing A] [Module ℝ A] [IsScalarTower ℝ A A]
+    [SMulCommClass ℝ A A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint]
+    {x : A} : IsIdempotentElem (star x * x) ↔ IsIdempotentElem (x * star x) := by
+  simp [isIdempotentElem_iff_quasispectrum_subset ℝ, quasispectrum.mul_comm]

Mathlib/Analysis/CStarAlgebra/Projection.lean

@@ -8,6 +8,8 @@ module
 public import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
 public import Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Isometric
 
+import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Projection
+
 /-!
 
 # Projections in C⋆-algebras
@@ -31,10 +33,17 @@ public section
 
 open scoped CStarAlgebra
 
-section Normal
+section NonUnital
+variable {A : Type*} [TopologicalSpace A] [NonUnitalRing A] [StarRing A]
+
+lemma isStarProjection_iff_quasispectrum_subset_and_isSelfAdjoint [Module ℝ A] [IsScalarTower ℝ A A]
+    [SMulCommClass ℝ A A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] {p : A} :
+    IsStarProjection p ↔ quasispectrum ℝ p ⊆ {0, 1} ∧ IsSelfAdjoint p :=
+  (isStarProjection_iff p).eq ▸
+    and_congr_left_iff.mpr fun h ↦ isIdempotentElem_iff_quasispectrum_subset ℝ p h
 
-variable {A : Type*} [TopologicalSpace A]
-  [NonUnitalRing A] [StarRing A] [Module ℂ A] [IsScalarTower ℂ A A] [SMulCommClass ℂ A A]
+section Normal
+variable [Module ℂ A] [IsScalarTower ℂ A A] [SMulCommClass ℂ A A]
   [NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal]
 
 /-- An idempotent element in a non-unital C⋆-algebra is self-adjoint iff it is normal. -/
@@ -43,15 +52,38 @@ theorem IsIdempotentElem.isSelfAdjoint_iff_isStarNormal {p : A} (hp : IsIdempote
   simp only [isSelfAdjoint_iff_isStarNormal_and_quasispectrumRestricts,
     QuasispectrumRestricts.real_iff, and_iff_left_iff_imp]
   intro h x hx
-  rcases hp.quasispectrum_subset hx with (hx | hx) <;> simp [Set.mem_singleton_iff.mp hx]
+  rcases hp.quasispectrum_subset _ hx with (hx | hx) <;> simp [Set.mem_singleton_iff.mp hx]
 
 /-- An element in a non-unital C⋆-algebra is a star projection
 if and only if it is idempotent and normal. -/
 theorem isStarProjection_iff_isIdempotentElem_and_isStarNormal {p : A} :
     IsStarProjection p ↔ IsIdempotentElem p ∧ IsStarNormal p :=
   (isStarProjection_iff p).eq ▸ and_congr_right_iff.eq ▸ fun h => h.isSelfAdjoint_iff_isStarNormal
 
+theorem isStarProjection_iff_quasispectrum_subset_and_isStarNormal {p : A} :
+    IsStarProjection p ↔ quasispectrum ℂ p ⊆ {0, 1} ∧ IsStarNormal p :=
+  isStarProjection_iff_isIdempotentElem_and_isStarNormal (p := p).eq ▸
+    and_congr_left_iff.mpr fun h ↦ isIdempotentElem_iff_quasispectrum_subset ℂ p h
+
 end Normal
+end NonUnital
+
+section Unital
+variable {A : Type*} [TopologicalSpace A] [Ring A] [StarRing A]
+
+lemma isStarProjection_iff_spectrum_subset_and_isSelfAdjoint [Algebra ℝ A]
+    [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] {p : A} :
+    IsStarProjection p ↔ spectrum ℝ p ⊆ {0, 1} ∧ IsSelfAdjoint p :=
+  (isStarProjection_iff p).eq ▸
+    and_congr_left_iff.mpr fun h ↦ isIdempotentElem_iff_spectrum_subset ℝ p h
+
+theorem isStarProjection_iff_spectrum_subset_and_isStarNormal [Algebra ℂ A]
+    [NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal] {p : A} :
+    IsStarProjection p ↔ spectrum ℂ p ⊆ {0, 1} ∧ IsStarNormal p :=
+  isStarProjection_iff_isIdempotentElem_and_isStarNormal (p := p).eq ▸
+    and_congr_left_iff.mpr fun h ↦ isIdempotentElem_iff_spectrum_subset ℂ p h
+
+end Unital
 
 namespace IsStarProjection
 

Mathlib/FieldTheory/IsAlgClosed/Spectrum.lean

@@ -167,9 +167,20 @@ theorem IsIdempotentElem.spectrum_subset (𝕜 : Type*) {A : Type*} [Field 𝕜]
   refine fun a ha => eq_zero_or_one_of_sq_eq_self ?_
   simpa [pow_two p, hp.eq, sub_eq_zero] using ha
 
+lemma IsIdempotentElem.finite_spectrum (𝕜 : Type*) {A : Type*} [Field 𝕜] [Ring A] [Algebra 𝕜 A]
+    {p : A} (hp : IsIdempotentElem p) : (spectrum 𝕜 p).Finite :=
+  have : ({0, 1} : Set 𝕜).encard = (2 : ℕ) := Set.encard_pair (by simp)
+  Set.finite_of_encard_le_coe (this ▸ Set.encard_le_encard (hp.spectrum_subset 𝕜))
+
 set_option backward.isDefEq.respectTransparency false in
 open Unitization in
-theorem IsIdempotentElem.quasispectrum_subset {𝕜 A : Type*} [Field 𝕜] [NonUnitalRing A] [Module 𝕜 A]
-    [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] {p : A} (hp : IsIdempotentElem p) :
+theorem IsIdempotentElem.quasispectrum_subset (𝕜 : Type*) {A : Type*} [Field 𝕜] [NonUnitalRing A]
+    [Module 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] {p : A} (hp : IsIdempotentElem p) :
     quasispectrum 𝕜 p ⊆ {0, 1} :=
   quasispectrum_eq_spectrum_inr' 𝕜 𝕜 p ▸ (hp.inr _ |>.spectrum_subset _)
+
+theorem IsIdempotentElem.finite_quasispectrum (𝕜 : Type*) {A : Type*} [Field 𝕜] [NonUnitalRing A]
+    [Module 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] {p : A} (hp : IsIdempotentElem p) :
+    (quasispectrum 𝕜 p).Finite :=
+  have : ({0, 1} : Set 𝕜).encard = (2 : ℕ) := Set.encard_pair (by simp)
+  Set.finite_of_encard_le_coe (this ▸ Set.encard_le_encard (hp.quasispectrum_subset 𝕜))