feat: the Fuglede–Putnam–Rosenblum theorem for C⋆-algebras

Mathlib.lean

@@ -1624,6 +1624,7 @@ public import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unitary
 public import Mathlib.Analysis.CStarAlgebra.ContinuousLinearMap
 public import Mathlib.Analysis.CStarAlgebra.ContinuousMap
 public import Mathlib.Analysis.CStarAlgebra.Exponential
+public import Mathlib.Analysis.CStarAlgebra.Fuglede
 public import Mathlib.Analysis.CStarAlgebra.GelfandDuality
 public import Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal
 public import Mathlib.Analysis.CStarAlgebra.Hom

Mathlib/Algebra/Group/Action/Defs.lean

@@ -382,14 +382,25 @@ lemma mul_smul_mul_comm [Mul α] [Mul β] [SMul α β] [IsScalarTower α β β]
 
 variable [SMul M α]
 
+@[to_additive]
+lemma SemiconjBy.smul_right [Mul α] [SMulCommClass M α α] [IsScalarTower M α α] {x a b : α}
+    (h : SemiconjBy x a b) (r : M) : SemiconjBy x (r • a) (r • b) := by
+  rw [SemiconjBy, mul_smul_comm, smul_mul_assoc, h.eq]
+
+@[to_additive]
+lemma SemiconjBy.smul_left [Mul α] [SMulCommClass M α α] [IsScalarTower M α α] {x a b : α}
+    (h : SemiconjBy x a b) (r : M) : SemiconjBy (r • x) a b := by
+  rw [SemiconjBy, mul_smul_comm, smul_mul_assoc, h.eq]
+
 @[to_additive]
 lemma Commute.smul_right [Mul α] [SMulCommClass M α α] [IsScalarTower M α α] {a b : α}
     (h : Commute a b) (r : M) : Commute a (r • b) :=
-  (mul_smul_comm _ _ _).trans ((congr_arg _ h).trans <| (smul_mul_assoc _ _ _).symm)
+  SemiconjBy.smul_right h r
 
 @[to_additive]
 lemma Commute.smul_left [Mul α] [SMulCommClass M α α] [IsScalarTower M α α] {a b : α}
-    (h : Commute a b) (r : M) : Commute (r • a) b := (h.symm.smul_right r).symm
+    (h : Commute a b) (r : M) : Commute (r • a) b :=
+  SemiconjBy.smul_left h r
 
 end
 
@@ -491,11 +502,23 @@ lemma smul_inv_smul (g : G) (a : α) : g • g⁻¹ • a = a := by rw [smul_smu
 section Mul
 variable [Mul H] [MulAction G H] [SMulCommClass G H H] [IsScalarTower G H H] {a b : H}
 
-@[simp] lemma Commute.smul_right_iff : Commute a (g • b) ↔ Commute a b :=
-  ⟨fun h ↦ inv_smul_smul g b ▸ h.smul_right g⁻¹, fun h ↦ h.smul_right g⟩
+@[to_additive (attr := simp)]
+lemma SemiconjBy.smul_right_iff {a b x : H} {r : G} :
+    SemiconjBy x (r • a) (r • b) ↔ SemiconjBy x a b :=
+  ⟨fun h ↦ by simpa using h.smul_right r⁻¹, (smul_right · r)⟩
+
+@[to_additive (attr := simp)]
+lemma SemiconjBy.smul_left_iff {a b x : H} {r : G} :
+    SemiconjBy (r • x) a b ↔ SemiconjBy x a b :=
+  ⟨fun h ↦ by simpa using h.smul_left r⁻¹, (smul_left · r)⟩
 
-@[simp] lemma Commute.smul_left_iff : Commute (g • a) b ↔ Commute a b := by
-  rw [Commute.symm_iff, Commute.smul_right_iff, Commute.symm_iff]
+@[to_additive (attr := simp)]
+lemma Commute.smul_right_iff : Commute a (g • b) ↔ Commute a b :=
+  SemiconjBy.smul_right_iff
+
+@[to_additive (attr := simp)]
+lemma Commute.smul_left_iff : Commute (g • a) b ↔ Commute a b :=
+  SemiconjBy.smul_left_iff
 
 end Mul
 

Mathlib/Algebra/GroupWithZero/Action/Units.lean

@@ -68,13 +68,25 @@ lemma inv_smul_eq_iff₀ (ha : a ≠ 0) {x y : β} : a⁻¹ • x = y ↔ x = a
 lemma eq_inv_smul_iff₀ (ha : a ≠ 0) {x y : β} : x = a⁻¹ • y ↔ a • x = y :=
   eq_inv_smul_iff (g := Units.mk0 a ha)
 
+@[simp]
+lemma SemiconjBy.smul_right_iff₀ [Mul β] [SMulCommClass α β β] [IsScalarTower α β β] {x y z : β}
+    (ha : a ≠ 0) : SemiconjBy x (a • y) (a • z) ↔ SemiconjBy x y z :=
+  smul_right_iff (r := Units.mk0 a ha)
+
+@[simp]
+lemma SemiconjBy.smul_left_iff₀ [Mul β] [SMulCommClass α β β] [IsScalarTower α β β] {x y z : β}
+    (ha : a ≠ 0) : SemiconjBy (a • x) y z ↔ SemiconjBy x y z :=
+  smul_left_iff (r := Units.mk0 a ha)
+
 @[simp]
 lemma Commute.smul_right_iff₀ [Mul β] [SMulCommClass α β β] [IsScalarTower α β β] {x y : β}
-    (ha : a ≠ 0) : Commute x (a • y) ↔ Commute x y := Commute.smul_right_iff (g := Units.mk0 a ha)
+    (ha : a ≠ 0) : Commute x (a • y) ↔ Commute x y :=
+  SemiconjBy.smul_right_iff₀ ha
 
 @[simp]
 lemma Commute.smul_left_iff₀ [Mul β] [SMulCommClass α β β] [IsScalarTower α β β] {x y : β}
-    (ha : a ≠ 0) : Commute (a • x) y ↔ Commute x y := Commute.smul_left_iff (g := Units.mk0 a ha)
+    (ha : a ≠ 0) : Commute (a • x) y ↔ Commute x y :=
+  SemiconjBy.smul_left_iff₀ ha
 
 /-- Right scalar multiplication as an order isomorphism. -/
 @[simps] def Equiv.smulRight (ha : a ≠ 0) : β ≃ β where

Mathlib/Analysis/CStarAlgebra/Fuglede.lean

@@ -0,0 +1,164 @@
+/-
+Copyright (c) 2026 Jireh Loreaux. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jireh Loreaux
+-/
+module
+
+public import Mathlib.Analysis.Normed.Algebra.Exponential
+public import Mathlib.Analysis.CStarAlgebra.Classes
+import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
+import Mathlib.Analysis.CStarAlgebra.Exponential
+import Mathlib.Analysis.Complex.Liouville
+
+
+/-! # The Fuglede–Putnam–Rosenblum theorem
+
+Let `A` be a C⋆-algebra, and let `a b x : A`. The Fuglede–Putnam–Rosenblum theorem states that
+if `a` and `b` are normal and `x` intertwines `a` and `b` (i.e., `SemiconjBy x a b`). Then `x` also
+intertwines `star a` and `star b`. Fuglede's original result was for `a = b` (i.e., if `x` commutes
+with `a`, then `x` also commutes with `star a`), and Putnam extended it to intertwining elements.
+
+Rosenblum later gave the elementary proof formalized here using Liouville's theorem which proceeds
+as follows. The map `f : ℂ → A` given by `z ↦ exp (z • star b) * x * exp (z • star (-a))`. When
+`x` intertwines `a` and `b` (i.e., `SemiconjBy x a b`), then it also intertwines `exp (star z • a)`
+and `exp (star z • b)`. Then the map `f` can be realized as `z ↦ u * x * v` for fixed unitaries
+`u` and `v`. In fact, `u = exp (I • 2 • ℑ (z • star b))` and `v = exp (I • 2 • ℑ (star z • a))`;
+it is here that normality of `a` and `b` is used to ensure that
+`exp (star z • a) * exp (- star (z • a)) = exp (I • 2 • ℑ (star z • a))` and likewise for `b`.
+There fore `‖f z‖ = ‖x‖` for all `z`, and since `f` is clearly entire, by Liouville's theorem,
+`f` is constant. Evaluating at `z = 0` proves that `f z = x` for all `z`. Therefore,
+`exp (z • star b) * x = x * exp (z • star a)`. Differentiating both sides and evaluating at `z = 0`
+proves that `star b * x = x * star a`, as desired.
+-/
+
+
+open NormedSpace
+
+variable {A : Type*} [CStarAlgebra A] {a b x : A} [IsStarNormal a] [IsStarNormal b]
+
+/-- The map `expMulMulExp : ℂ → A` given by `z ↦ exp (z • star b) * x * exp (z • star (-a))` for
+fixed `a b x : A`. -/
+noncomputable def expMulMulExp (a b x : A) (z : ℂ) : A := exp (z • star b) * x * exp (z • star (-a))
+
+open scoped ComplexStarModule
+open selfAdjoint
+lemma expMulMulExp_eq_expUnitary_mul_expUnitary (h : SemiconjBy x a b) (z : ℂ) :
+    expMulMulExp a b x z =
+      expUnitary ((2 : ℝ) • ℑ (z • star b)) * x * expUnitary ((2 : ℝ) • ℑ (star z • a)) := by
+  let _ : NormedAlgebra ℚ A := .restrictScalars ℚ ℂ A
+  have : SemiconjBy x (z • a) (z • b) := h.smul_right _
+  nth_rw 1 [expMulMulExp, ← (h.smul_right (star z)).exp_neg_mul_mul_exp_eq_self]
+  simp_rw [← mul_assoc, mul_assoc (_ * _ * x)]
+  congr!
+  all_goals
+    open Complex in
+    simp only [RCLike.star_def, star_neg, smul_neg, expUnitary_coe, val_smul,
+      imaginaryPart_apply_coe, star_smul, RingHomCompTriple.comp_apply, RingHom.id_apply, neg_smul,
+      smul_comm (2 : ℝ) I, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, smul_inv_smul₀,
+      smul_smul I I, I_mul_I, one_smul, neg_sub, star_star]
+    rw [sub_eq_add_neg, NormedSpace.exp_add_of_commute]
+    by_cases! hz : z = 0 <;> simp [hz, star_comm_self, Commute.symm]
+
+open Bornology in
+lemma expMulMulExp_const (h : SemiconjBy x a b) (z : ℂ) : expMulMulExp a b x z = x := by
+  have hf : Differentiable ℂ (expMulMulExp a b x : ℂ → A) := by unfold expMulMulExp; fun_prop
+  have : IsBounded (Set.range (expMulMulExp a b x)) := by
+    apply Metric.isBounded_sphere (x := (0 : A)) (r := ‖x‖) |>.subset
+    rintro - ⟨z, hz, rfl⟩
+    rw [mem_sphere_iff_norm, sub_zero, expMulMulExp_eq_expUnitary_mul_expUnitary h z,
+      CStarRing.norm_mul_coe_unitary, CStarRing.norm_coe_unitary_mul]
+  simpa [expMulMulExp] using hf.apply_eq_apply_of_bounded this z 0
+
+/- This is not public because it is superseded by `SemiconjBy.star_right`. -/
+lemma SemiconjBy.star_right_of_unital (h : SemiconjBy x a b) :
+    SemiconjBy x (star a) (star b) := by
+  suffices key : ∀ z : ℂ, x * exp (z • star a) = exp (z • star b) * x by
+    have (a : A) : HasDerivAt (fun z : ℂ ↦ exp (z • a)) a 0 := by
+      simpa using hasDerivAt_exp_smul_const a (0 : ℂ)
+    apply (this (star a)).const_mul x |>.unique
+    simpa [key] using (this (star b)).mul_const x
+  intro z
+  let _ : NormedAlgebra ℚ A := .restrictScalars ℚ ℂ A
+  let _ := invertibleExp (z • star a)
+  simpa [← mul_assoc, ← invOf_exp, expMulMulExp] using
+    congr($(expMulMulExp_const h z) * exp (z • star a)).symm
+
+/-- **Fuglede–Putnam–Rosenblum**: If `a` and `b` are normal elements in a C⋆-algebra `A` which
+are interwined by `x`, then `star a` and `star b` are also intertwined by `x`. -/
+public lemma SemiconjBy.star_right {A : Type*} [NonUnitalCStarAlgebra A] {a b x : A}
+    (ha : IsStarNormal a) (hb : IsStarNormal b) (h : SemiconjBy x a b) :
+    SemiconjBy x (star a) (star b) := by
+  apply Unitization.inr_injective (R := ℂ)
+  simp only [Unitization.inr_mul, Unitization.inr_star]
+  apply SemiconjBy.star_right_of_unital
+  simpa [SemiconjBy] using mod_cast h.eq
+
+public alias fuglede_putnam_rosenblum := SemiconjBy.star_right
+
+/-- **Fuglede–Putnam–Rosenblum**: If `a` is a normal element in a C⋆-algebra `A` which
+commutes with `x`, then `star a` commutes with `x`. -/
+public lemma IsStarNormal.commute_star_right {A : Type*} [NonUnitalCStarAlgebra A] {a x : A}
+    (ha : IsStarNormal a) (h : Commute x a) :
+    Commute x (star a) :=
+  h.semiconjBy.star_right ha ha
+
+/-- **Fuglede–Putnam–Rosenblum**: If `a` is a normal element in a C⋆-algebra `A` which
+commutes with `x`, then `star a` commutes with `x`. -/
+public lemma IsStarNormal.commute_star_left {A : Type*} [NonUnitalCStarAlgebra A] {a x : A}
+    (ha : IsStarNormal a) (h : Commute a x) :
+    Commute (star a) x :=
+  ha.commute_star_right h.symm |>.symm
+
+public lemma isStarNormal_iff_forall_exp_mul_exp_mem_unitary {a : A} :
+    IsStarNormal a ↔ ∀ x : ℝ, exp (x • a) * exp (- x • star a) ∈ unitary A := by
+  let _ : NormedAlgebra ℚ A := .restrictScalars ℚ ℂ A
+  have : IsAddTorsionFree A := IsAddTorsionFree.of_module_rat A
+  refine ⟨fun ha x ↦ ?_, fun ha ↦ ?_⟩
+  /- If `a` is normal, then clearly `exp (x • a) * exp (- x • star a) = exp (I • x • 2 • ℑ a)`
+  and the latter is clearly an exponential unitary. -/
+  · convert (selfAdjoint.expUnitary (x • (2 : ℝ) • ℑ a)).2
+    have hcomm := star_comm_self (x := a) |>.symm.smul_left x |>.smul_right (-x)
+    rw [← exp_add_of_commute hcomm]
+    open Complex in
+    simp [imaginaryPart_apply_coe, smul_comm (2 : ℝ) I, smul_comm x I, smul_smul I I, smul_add x,
+      sub_eq_add_neg]
+  /- Take any `x : ℝ` and suppose `u := exp (x • a) * exp (- x • a)` is unitary. Then
+  `exp (- x • a) * exp (x • star a) = star u = u⁻¹ = exp (x • star a) * exp (- x • a)`. -/
+  · have key : ∀ x : ℝ, exp (- x • a) * exp (x • star a) = exp (x • star a) * exp (- x • a) := by
+      intro x
+      let u : unitary A := ⟨_, ha x⟩
+      convert congr(($(Unitary.star_eq_inv u) : A))
+      · simp [u, star_exp]
+      · simp_rw [u, ← Unitary.val_inv_toUnits_apply, neg_smul, ← Units.mul_eq_one_iff_eq_inv,
+          Unitary.val_toUnits_apply]
+        let _ := invertibleExp (𝔸 := A)
+        rw [mul_assoc]
+        simp [← invOf_exp]
+    /- Compute the second derivative with respect to `x` of each side of this expression and
+    evaluate at `x = 0`. -/
+    have h_deriv (a b c : A) (y : ℝ) :
+        deriv (fun x : ℝ ↦ exp (x • a) * c * exp (x • b)) y =
+          exp (y • a) * (a * c + c * b) * exp (y • b) := by
+      rw [mul_add, add_mul, ← mul_assoc _ a, ← mul_assoc _ c b, mul_assoc _ b]
+      exact (hasDerivAt_exp_smul_const a y).mul_const c |>.mul
+        (hasDerivAt_exp_smul_const' b y) |>.deriv
+    have h_deriv₂ (a b : A) :
+        deriv (fun y ↦ deriv (fun x : ℝ ↦ exp (x • a) * exp (x • b)) y) 0 =
+          a ^ 2 + 2 • (a * b) + b ^ 2 := by
+      conv => enter [1, 1, y, 1, x, 1]; rw [← mul_one (exp (x • a))]
+      simp_rw [h_deriv, zero_smul, NormedSpace.exp_zero, mul_one, one_mul]
+      noncomm_ring
+    have h₃ := h_deriv₂ (-a) (star a)
+    have h₄ := h_deriv₂ (star a) (-a)
+    simp only [smul_neg, even_two, Even.neg_pow, neg_smul] at h₃ h₄ key
+    /- By `key`, these second derivatives evaluated at zero must be equal, so we find
+    `a ^ 2 + 2 • (- a * star a) + (star a) ^ 2 = star ^ 2 + 2 • (star a * a) + a ^ 2`,
+    and then elementary algebra shows `star a * a = a * star a`, so `a` is normal.  -/
+    simp_rw [key] at h₃
+    rw [h₃] at h₄
+    rw [isStarNormal_iff, commute_iff_eq]
+    apply nsmul_right_injective two_ne_zero
+    rw [← sub_eq_zero] at h₄ ⊢
+    rw [← h₄]
+    noncomm_ring

Mathlib/Analysis/Normed/Algebra/Exponential.lean

@@ -542,6 +542,18 @@ theorem exp_mem_unitary_of_mem_skewAdjoint [StarRing 𝔸] [ContinuousStar 𝔸]
     exp_add_of_commute (Commute.refl x).neg_left, ← exp_add_of_commute (Commute.refl x).neg_right,
     neg_add_cancel, add_neg_cancel, exp_zero, and_self_iff]
 
+lemma _root_.SemiconjBy.exp_right {x a b : 𝔸} (h : SemiconjBy x a b) :
+    SemiconjBy x (exp a) (exp b) := by
+  rw [exp_eq_tsum ℚ]
+  apply SemiconjBy.tsum_right x (expSeries_summable' _) (expSeries_summable' _)
+  exact fun _ ↦ h.pow_right _ |>.smul_right _
+
+lemma _root_.SemiconjBy.exp_neg_mul_mul_exp_eq_self {x a b : 𝔸} (h : SemiconjBy x a b) :
+    exp (-b) * x * exp a = x := by
+  apply (isUnit_exp b).mul_left_cancel
+  let hb := invertibleExp b
+  simp [← invOf_exp, ← mul_assoc, h.exp_right.eq]
+
 open scoped Function in -- required for scoped `on` notation
 /-- In a Banach-algebra `𝔸` over `𝕂 = ℝ` or `𝕂 = ℂ`, if a family of elements `f i` mutually
 commute then `NormedSpace.exp (∑ i, f i) = ∏ i, NormedSpace.exp (f i)`. -/

Mathlib/Analysis/SpecialFunctions/Exponential.lean

@@ -390,6 +390,17 @@ theorem hasDerivAt_exp_smul_const' (x : 𝔸) (t : 𝕂) :
   hasDerivAt_exp_smul_const_of_mem_ball' _ _ <|
     (expSeries_radius_eq_top 𝕂 𝔸).symm ▸ edist_lt_top _ _
 
+variable (𝕂) in
+@[fun_prop]
+lemma differentiable_exp_smul_const (x : 𝔸) :
+    Differentiable 𝕂 (fun t : 𝕂 ↦ exp (t • x)) :=
+  (⟨_, hasDerivAt_exp_smul_const x ·⟩)
+
+@[fun_prop]
+lemma differentiableAt_exp_smul_const (x : 𝔸) (r : 𝕂) :
+    DifferentiableAt 𝕂 (fun t : 𝕂 ↦ exp (t • x)) r :=
+  differentiable_exp_smul_const 𝕂 x |>.differentiableAt
+
 end RCLike
 
 end exp_smul

Mathlib/Topology/Algebra/InfiniteSum/Ring.lean

@@ -60,14 +60,24 @@ protected theorem Summable.tsum_mul_right (a) (hf : Summable f L) :
     ∑'[L] i, f i * a = (∑'[L] i, f i) * a :=
   (hf.hasSum.mul_right _).tsum_eq
 
-theorem Commute.tsum_right (a) (h : ∀ i, Commute a (f i)) : Commute a (∑'[L] i, f i) := by
+theorem SemiconjBy.tsum_left {a b : α} (h : ∀ (i : ι), SemiconjBy (f i) a b) :
+    SemiconjBy (∑'[L] (i : ι), f i) a b := by
   classical
   by_cases hf : Summable f L
-  · exact (hf.tsum_mul_left a).symm.trans ((tsum_congr h).trans (hf.tsum_mul_right a))
-  · exact (tsum_eq_zero_of_not_summable hf).symm ▸ Commute.zero_right _
+  · rw [SemiconjBy, ← hf.tsum_mul_right a, ← hf.tsum_mul_left b, tsum_congr h]
+  · simp [tsum_eq_zero_of_not_summable hf]
+
+theorem SemiconjBy.tsum_right {f g : ι → α} (a : α) (hf : Summable f L) (hg : Summable g L)
+    (h : ∀ (i : ι), SemiconjBy a (f i) (g i)) :
+    SemiconjBy a (∑'[L] (i : ι), f i) (∑'[L] (i : ι), g i) := by
+  rw [SemiconjBy, ← hf.tsum_mul_left a, ← hg.tsum_mul_right a]
+  exact tsum_congr fun i => h i
 
 theorem Commute.tsum_left (a) (h : ∀ i, Commute (f i) a) : Commute (∑'[L] i, f i) a :=
-  (Commute.tsum_right _ fun i ↦ (h i).symm).symm
+  SemiconjBy.tsum_left h
+
+theorem Commute.tsum_right (a) (h : ∀ i, Commute a (f i)) : Commute a (∑'[L] i, f i) :=
+  (Commute.tsum_left _ fun i ↦ (h i).symm).symm
 
 end tsum