feat : added spectrum.conjugate_units results to Algebra.Algebra.Spectrum, and spectrum.conjugate_unitary results to Algebra.Star.Unitary. (#13729)

Included proofs that conjugation by a unit preserves the spectrum, and conjugation by a unitary preserves the spectrum.

Author: JonBannon

Mathlib/Algebra/Algebra/Spectrum.lean

@@ -449,3 +449,28 @@ theorem AlgEquiv.spectrum_eq {F R A B : Type*} [CommSemiring R] [Ring A] [Ring B
   Set.Subset.antisymm (AlgHom.spectrum_apply_subset _ _) <| by
     simpa only [AlgEquiv.coe_algHom, AlgEquiv.coe_coe_symm_apply_coe_apply] using
       AlgHom.spectrum_apply_subset (f : A ≃ₐ[R] B).symm (f a)
+
+section ConjugateUnits
+
+variable {R A : Type*} [CommSemiring R] [Ring A] [Algebra R A]
+
+/-- Conjugation by a unit preserves the spectrum, inverse on right. -/
+@[simp]
+lemma spectrum.units_conjugate {a : A} {u : Aˣ} :
+    spectrum R (u * a * u⁻¹) = spectrum R a := by
+  suffices ∀ (b : A) (v : Aˣ), spectrum R (v * b * v⁻¹) ⊆ spectrum R b by
+    refine le_antisymm (this a u) ?_
+    apply le_of_eq_of_le ?_ <| this (u * a * u⁻¹) u⁻¹
+    simp [mul_assoc]
+  intro a u μ hμ
+  rw [spectrum.mem_iff] at hμ ⊢
+  contrapose! hμ
+  simpa [mul_sub, sub_mul, Algebra.right_comm] using u.isUnit.mul hμ |>.mul u⁻¹.isUnit
+
+/-- Conjugation by a unit preserves the spectrum, inverse on left. -/
+@[simp]
+lemma spectrum.units_conjugate' {a : A} {u : Aˣ} :
+    spectrum R (u⁻¹ * a * u) = spectrum R a := by
+  simpa using spectrum.units_conjugate (u := u⁻¹)
+
+end ConjugateUnits

Mathlib/Algebra/Star/Unitary.lean

@@ -5,6 +5,7 @@ Authors: Shing Tak Lam, Frédéric Dupuis
 -/
 import Mathlib.Algebra.Group.Submonoid.Operations
 import Mathlib.Algebra.Star.SelfAdjoint
+import Mathlib.Algebra.Algebra.Spectrum
 
 #align_import algebra.star.unitary from "leanprover-community/mathlib"@"247a102b14f3cebfee126293341af5f6bed00237"
 
@@ -239,4 +240,24 @@ instance : HasDistribNeg (unitary R) :=
 
 end Ring
 
+section UnitaryConjugate
+
+universe u
+
+variable {R A : Type*} [CommSemiring R] [Ring A] [Algebra R A] [StarMul A]
+
+/-- Unitary conjugation preserves the spectrum, star on left. -/
+@[simp]
+lemma spectrum.unitary_conjugate {a : A} {u : unitary A} :
+    spectrum R (u * a * (star u : A)) = spectrum R a :=
+  spectrum.units_conjugate (u := unitary.toUnits u)
+
+/-- Unitary conjugation preserves the spectrum, star on right. -/
+@[simp]
+lemma spectrum.unitary_conjugate' {a : A} {u : unitary A} :
+    spectrum R ((star u : A) * a * u) = spectrum R a := by
+  simpa using spectrum.unitary_conjugate (u := star u)
+
+end UnitaryConjugate
+
 end unitary

Mathlib/Analysis/NormedSpace/Star/Basic.lean

@@ -33,7 +33,6 @@ To get a C⋆-algebra `E` over field `𝕜`, use
 
 -/
 
-
 open Topology
 
 local postfix:max "⋆" => star