From 63cf17c8fd1b7a2d02b4fe827d4a40445b16c634 Mon Sep 17 00:00:00 2001 From: Jireh Loreaux Date: Thu, 2 Apr 2026 14:11:38 -0500 Subject: [PATCH 1/8] =?UTF-8?q?feat:=20the=20Fuglede=E2=80=93Putnam?= =?UTF-8?q?=E2=80=93Rosenblum=20theorem=20for=20C=E2=8B=86-algebras?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Mathlib/Algebra/Group/Action/Defs.lean | 35 +++- .../Algebra/GroupWithZero/Action/Units.lean | 16 +- Mathlib/Analysis/CStarAlgebra/Fuglede.lean | 169 ++++++++++++++++++ .../Analysis/Normed/Algebra/Exponential.lean | 12 ++ .../SpecialFunctions/Exponential.lean | 11 ++ .../Topology/Algebra/InfiniteSum/Ring.lean | 18 +- 6 files changed, 249 insertions(+), 12 deletions(-) create mode 100644 Mathlib/Analysis/CStarAlgebra/Fuglede.lean diff --git a/Mathlib/Algebra/Group/Action/Defs.lean b/Mathlib/Algebra/Group/Action/Defs.lean index 2df4f9a3156d6e..57bc2b7910a181 100644 --- a/Mathlib/Algebra/Group/Action/Defs.lean +++ b/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 diff --git a/Mathlib/Algebra/GroupWithZero/Action/Units.lean b/Mathlib/Algebra/GroupWithZero/Action/Units.lean index 589da6bcd04ecb..8c2b1ddc03bf3a 100644 --- a/Mathlib/Algebra/GroupWithZero/Action/Units.lean +++ b/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 diff --git a/Mathlib/Analysis/CStarAlgebra/Fuglede.lean b/Mathlib/Analysis/CStarAlgebra/Fuglede.lean new file mode 100644 index 00000000000000..ce6691937e10d4 --- /dev/null +++ b/Mathlib/Analysis/CStarAlgebra/Fuglede.lean @@ -0,0 +1,169 @@ +/- +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 +public import Mathlib.Algebra.Algebra.Unitization +public import Mathlib.Analysis.Calculus.FDeriv.Defs +import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic +import Mathlib.Analysis.CStarAlgebra.Exponential +import Mathlib.Analysis.Calculus.FDeriv.Mul +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 + +attribute [norm_cast] Unitization.inr_mul + +/-- **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 diff --git a/Mathlib/Analysis/Normed/Algebra/Exponential.lean b/Mathlib/Analysis/Normed/Algebra/Exponential.lean index 0cf9823c36161a..e2371ed20f6302 100644 --- a/Mathlib/Analysis/Normed/Algebra/Exponential.lean +++ b/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)`. -/ diff --git a/Mathlib/Analysis/SpecialFunctions/Exponential.lean b/Mathlib/Analysis/SpecialFunctions/Exponential.lean index ef467fa804f67e..c14b597bb6ce24 100644 --- a/Mathlib/Analysis/SpecialFunctions/Exponential.lean +++ b/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 diff --git a/Mathlib/Topology/Algebra/InfiniteSum/Ring.lean b/Mathlib/Topology/Algebra/InfiniteSum/Ring.lean index 2f76d921b78973..6832869eb318da 100644 --- a/Mathlib/Topology/Algebra/InfiniteSum/Ring.lean +++ b/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 From 1960074c031d67b35442eb1b95b8bb17061e0dee Mon Sep 17 00:00:00 2001 From: Jireh Loreaux Date: Thu, 2 Apr 2026 15:07:22 -0500 Subject: [PATCH 2/8] mk_all and minimize imports --- Mathlib.lean | 1 + Mathlib/Analysis/CStarAlgebra/Fuglede.lean | 5 ----- 2 files changed, 1 insertion(+), 5 deletions(-) diff --git a/Mathlib.lean b/Mathlib.lean index 26ccae3d54292d..131bdf04b0b678 100644 --- a/Mathlib.lean +++ b/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 diff --git a/Mathlib/Analysis/CStarAlgebra/Fuglede.lean b/Mathlib/Analysis/CStarAlgebra/Fuglede.lean index ce6691937e10d4..b0d73a5ce11278 100644 --- a/Mathlib/Analysis/CStarAlgebra/Fuglede.lean +++ b/Mathlib/Analysis/CStarAlgebra/Fuglede.lean @@ -7,11 +7,8 @@ module public import Mathlib.Analysis.Normed.Algebra.Exponential public import Mathlib.Analysis.CStarAlgebra.Classes -public import Mathlib.Algebra.Algebra.Unitization -public import Mathlib.Analysis.Calculus.FDeriv.Defs import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic import Mathlib.Analysis.CStarAlgebra.Exponential -import Mathlib.Analysis.Calculus.FDeriv.Mul import Mathlib.Analysis.Complex.Liouville @@ -87,8 +84,6 @@ lemma SemiconjBy.star_right_of_unital (h : SemiconjBy x a b) : simpa [← mul_assoc, ← invOf_exp, expMulMulExp] using congr($(expMulMulExp_const h z) * exp (z • star a)).symm -attribute [norm_cast] Unitization.inr_mul - /-- **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} From dbd4d25ae38f1541b65a2e42d863a1f62e1b56bc Mon Sep 17 00:00:00 2001 From: Jireh Loreaux Date: Sat, 4 Apr 2026 16:17:37 -0500 Subject: [PATCH 3/8] add fuglede reference --- docs/references.bib | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) diff --git a/docs/references.bib b/docs/references.bib index 47ffaebdad1117..27decf69f36df2 100644 --- a/docs/references.bib +++ b/docs/references.bib @@ -2131,6 +2131,23 @@ @InProceedings{ fuerer-lochbihler-schneider-traytel2020 bibsource = {dblp computer science bibliography, https://dblp.org} } +@article{ fuglede1950, + author = {Fuglede, Bent}, + title = {A commutativity theorem for normal operators}, + JOURNAL = {Proc. Nat. Acad. Sci. U.S.A.}, + FJOURNAL = {Proceedings of the National Academy of Sciences of the United + States of America}, + VOLUME = {36}, + YEAR = {1950}, + PAGES = {35--40}, + ISSN = {0027-8424}, + MRCLASS = {46.3X}, + MRNUMBER = {32944}, +MRREVIEWER = {B.\ R.\ Gelbaum}, + DOI = {10.1073/pnas.36.1.35}, + URL = {https://doi.org/10.1073/pnas.36.1.35}, +} + @Book{ fulton2004, title = {Representation theory: a first course}, author = {Fulton, William and Harris, Joe}, From b8fbb9c2f0c4f811def06bcdb3f61537658bb0cc Mon Sep 17 00:00:00 2001 From: Jireh Loreaux Date: Sat, 4 Apr 2026 17:24:33 -0500 Subject: [PATCH 4/8] code review --- Mathlib/Analysis/CStarAlgebra/Fuglede.lean | 63 +++++++++++------- docs/references.bib | 76 ++++++++++++++++++---- 2 files changed, 100 insertions(+), 39 deletions(-) diff --git a/Mathlib/Analysis/CStarAlgebra/Fuglede.lean b/Mathlib/Analysis/CStarAlgebra/Fuglede.lean index b0d73a5ce11278..18a9b69adae13b 100644 --- a/Mathlib/Analysis/CStarAlgebra/Fuglede.lean +++ b/Mathlib/Analysis/CStarAlgebra/Fuglede.lean @@ -15,25 +15,45 @@ 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 +if `a` and `b` are normal and `x` intertwines `a` and `b` (i.e., `SemiconjBy x a b`, that is, +`x * a = b * x`), then `x` also intertwines `star a` and `star b`. Fuglede's original result +[fuglede1950] was for `a = b` (i.e., if `x` commutes with `a`, then `x` also commutes with +`star a`), and Putnam [putnam1951] extended it to intertwining elements. + +Rosenblum [rosenblum1958] later gave the elementary proof formalized here using Liouville's theorem which proceeds +as follows. Consider 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, +Therefore `‖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. + +In a follow-up paper, Cater [cater1961] proved a number of related results using similar techniques. +We include one of these below, but the proof is independent of the Fuglede–Putnam–Rosenblum theorem. + +## Main results + ++ `fuglede_putnam_rosenblum`: If `a` and `b` are normal elements in a C⋆-algebra `A` which + are interwined by `x` (i.e., `SemiconjBy x a b`, that is, `x * a = b * x`), then `star a` and + `star b` are also intertwined by `x`. ++ + +## References + ++ [fuglede1950] Bent Fuglede, "A commutativity theorem for normal operators" ++ [putnam1951] C. R. Putnam, "On normal operators in Hilbert space" ++ [rosenblum1958] M. Rosenblum, "On a theorem of Fuglede and Putnam" ++ [cater1961] S. Cater, "Observations on a paper by Rosenblum" + -/ -open NormedSpace +open NormedSpace selfAdjoint Bornology +open scoped ComplexStarModule variable {A : Type*} [CStarAlgebra A] {a b x : A} [IsStarNormal a] [IsStarNormal b] @@ -41,32 +61,24 @@ variable {A : Type*} [CStarAlgebra A] {a b x : A} [IsStarNormal a] [IsStarNormal 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 : ℂ) : +lemma expMulMulExp_eq_expUnitary_mul_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 + simp [imaginaryPart_apply_coe, smul_comm (2 : ℝ) I, smul_smul I I, sub_eq_add_neg] + grind [exp_add_of_commute, Commute.smul_right, Commute.neg_right] + 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, + rw [mem_sphere_iff_norm, sub_zero, expMulMulExp_eq_expUnitary_mul_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 @@ -110,6 +122,7 @@ public lemma IsStarNormal.commute_star_left {A : Type*} [NonUnitalCStarAlgebra A Commute (star a) x := ha.commute_star_right h.symm |>.symm +/-- A characterization of normal elements in a C⋆-algebra in terms of exponentials. -/ 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 diff --git a/docs/references.bib b/docs/references.bib index 27decf69f36df2..7230efdcf2c506 100644 --- a/docs/references.bib +++ b/docs/references.bib @@ -1074,6 +1074,22 @@ @Book{ cassels1986local doi = {10.1017/CBO9781139171885} } +@Article{ cater1961, + author = {Cater, S.}, + title = {Observations on a paper by {R}osenblum}, + journal = {Proc. Amer. Math. Soc.}, + fjournal = {Proceedings of the American Mathematical Society}, + volume = {12}, + year = {1961}, + pages = {560--561}, + issn = {0002-9939,1088-6826}, + mrclass = {47.40}, + mrnumber = {130560}, + mrreviewer = {S.\ Kurepa}, + doi = {10.2307/2034244}, + url = {https://doi.org/10.2307/2034244} +} + @Article{ chapman1996, author = {Chapman, Robin}, title = {A Polynomial Taking Integer Values}, @@ -2131,21 +2147,21 @@ @InProceedings{ fuerer-lochbihler-schneider-traytel2020 bibsource = {dblp computer science bibliography, https://dblp.org} } -@article{ fuglede1950, +@Article{ fuglede1950, author = {Fuglede, Bent}, - title = {A commutativity theorem for normal operators}, - JOURNAL = {Proc. Nat. Acad. Sci. U.S.A.}, - FJOURNAL = {Proceedings of the National Academy of Sciences of the United - States of America}, - VOLUME = {36}, - YEAR = {1950}, - PAGES = {35--40}, - ISSN = {0027-8424}, - MRCLASS = {46.3X}, - MRNUMBER = {32944}, -MRREVIEWER = {B.\ R.\ Gelbaum}, - DOI = {10.1073/pnas.36.1.35}, - URL = {https://doi.org/10.1073/pnas.36.1.35}, + title = {A commutativity theorem for normal operators}, + journal = {Proc. Nat. Acad. Sci. U.S.A.}, + fjournal = {Proceedings of the National Academy of Sciences of the + United States of America}, + volume = {36}, + year = {1950}, + pages = {35--40}, + issn = {0027-8424}, + mrclass = {46.3X}, + mrnumber = {32944}, + mrreviewer = {B.\ R.\ Gelbaum}, + doi = {10.1073/pnas.36.1.35}, + url = {https://doi.org/10.1073/pnas.36.1.35} } @Book{ fulton2004, @@ -4559,6 +4575,22 @@ @InCollection{ proetale2015 zbl = {1351.19001} } +@Article{ putnam1951, + author = {Putnam, C. R.}, + title = {On normal operators in {H}ilbert space}, + journal = {Amer. J. Math.}, + fjournal = {American Journal of Mathematics}, + volume = {73}, + year = {1951}, + pages = {357--362}, + issn = {0002-9327,1080-6377}, + mrclass = {46.3X}, + mrnumber = {40585}, + mrreviewer = {B.\ R.\ Gelbaum}, + doi = {10.2307/2372180}, + url = {https://doi.org/10.2307/2372180} +} + @Book{ Quillen1967, author = {Quillen, Daniel G.}, title = {Homotopical algebra}, @@ -4710,6 +4742,22 @@ @Article{ rooij1970 pages = {21--30} } +@Article{ rosenblum1958, + author = {Rosenblum, M.}, + title = {On a theorem of {F}uglede and {P}utnam}, + journal = {J. London Math. Soc.}, + fjournal = {The Journal of the London Mathematical Society}, + volume = {33}, + year = {1958}, + pages = {376--377}, + issn = {0024-6107,1469-7750}, + mrclass = {46.00}, + mrnumber = {99598}, + mrreviewer = {S.\ K.\ Berberian}, + doi = {10.1112/jlms/s1-33.3.376}, + url = {https://doi.org/10.1112/jlms/s1-33.3.376} +} + @Article{ Rosenlicht_1972, author = {Rosenlicht, Maxwell}, title = {Integration in finite terms}, From 6d00c96c57f44dfd9c8586b9e9202527562df952 Mon Sep 17 00:00:00 2001 From: Jireh Loreaux Date: Sat, 4 Apr 2026 17:27:11 -0500 Subject: [PATCH 5/8] Apply suggestions from code review Co-authored-by: David Loeffler --- Mathlib/Analysis/Normed/Algebra/Exponential.lean | 5 ++--- Mathlib/Topology/Algebra/InfiniteSum/Ring.lean | 3 +-- 2 files changed, 3 insertions(+), 5 deletions(-) diff --git a/Mathlib/Analysis/Normed/Algebra/Exponential.lean b/Mathlib/Analysis/Normed/Algebra/Exponential.lean index e2371ed20f6302..6526b80dcde8bc 100644 --- a/Mathlib/Analysis/Normed/Algebra/Exponential.lean +++ b/Mathlib/Analysis/Normed/Algebra/Exponential.lean @@ -550,9 +550,8 @@ lemma _root_.SemiconjBy.exp_right {x a b : 𝔸} (h : SemiconjBy x a b) : 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] + let := invertibleExp b + simpa [← invOf_exp, mul_assoc, invOf_mul_eq_iff_eq_mul_left] using h.exp_right open scoped Function in -- required for scoped `on` notation /-- In a Banach-algebra `𝔸` over `𝕂 = ℝ` or `𝕂 = ℂ`, if a family of elements `f i` mutually diff --git a/Mathlib/Topology/Algebra/InfiniteSum/Ring.lean b/Mathlib/Topology/Algebra/InfiniteSum/Ring.lean index 6832869eb318da..a81c1ec803c300 100644 --- a/Mathlib/Topology/Algebra/InfiniteSum/Ring.lean +++ b/Mathlib/Topology/Algebra/InfiniteSum/Ring.lean @@ -62,7 +62,6 @@ protected theorem Summable.tsum_mul_right (a) (hf : Summable f L) : 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 · rw [SemiconjBy, ← hf.tsum_mul_right a, ← hf.tsum_mul_left b, tsum_congr h] · simp [tsum_eq_zero_of_not_summable hf] @@ -71,7 +70,7 @@ theorem SemiconjBy.tsum_right {f g : ι → α} (a : α) (hf : Summable f L) (hg (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 + exact tsum_congr h theorem Commute.tsum_left (a) (h : ∀ i, Commute (f i) a) : Commute (∑'[L] i, f i) a := SemiconjBy.tsum_left h From 0e4683061986444d03b0ffb648e5965991b5433b Mon Sep 17 00:00:00 2001 From: Jireh Loreaux Date: Sat, 4 Apr 2026 17:55:31 -0500 Subject: [PATCH 6/8] fix --- Mathlib/Analysis/CStarAlgebra/Fuglede.lean | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/Mathlib/Analysis/CStarAlgebra/Fuglede.lean b/Mathlib/Analysis/CStarAlgebra/Fuglede.lean index 18a9b69adae13b..1075c36062ea6d 100644 --- a/Mathlib/Analysis/CStarAlgebra/Fuglede.lean +++ b/Mathlib/Analysis/CStarAlgebra/Fuglede.lean @@ -20,8 +20,9 @@ if `a` and `b` are normal and `x` intertwines `a` and `b` (i.e., `SemiconjBy x a [fuglede1950] was for `a = b` (i.e., if `x` commutes with `a`, then `x` also commutes with `star a`), and Putnam [putnam1951] extended it to intertwining elements. -Rosenblum [rosenblum1958] later gave the elementary proof formalized here using Liouville's theorem which proceeds -as follows. Consider the map `f : ℂ → A` given by `z ↦ exp (z • star b) * x * exp (z • star (-a))`. +Rosenblum [rosenblum1958] later gave the elementary proof formalized here using Liouville's theorem +which proceeds as follows. Consider 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 From a681d867c3e1a1f7642f345add5977fe5215d533 Mon Sep 17 00:00:00 2001 From: Jireh Loreaux Date: Mon, 6 Apr 2026 10:44:23 -0500 Subject: [PATCH 7/8] Apply suggestions from code review Co-authored-by: David Loeffler --- Mathlib/Analysis/CStarAlgebra/Fuglede.lean | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/Mathlib/Analysis/CStarAlgebra/Fuglede.lean b/Mathlib/Analysis/CStarAlgebra/Fuglede.lean index 1075c36062ea6d..fe490c6eefabc9 100644 --- a/Mathlib/Analysis/CStarAlgebra/Fuglede.lean +++ b/Mathlib/Analysis/CStarAlgebra/Fuglede.lean @@ -34,14 +34,16 @@ Therefore `‖f z‖ = ‖x‖` for all `z`, and since `f` is clearly entire, by proves that `star b * x = x * star a`, as desired. In a follow-up paper, Cater [cater1961] proved a number of related results using similar techniques. -We include one of these below, but the proof is independent of the Fuglede–Putnam–Rosenblum theorem. +We include one of these below, `isStarNormal_iff_forall_exp_mul_exp_mem_unitary`, +but the proof is independent of the Fuglede–Putnam–Rosenblum theorem. ## Main results + `fuglede_putnam_rosenblum`: If `a` and `b` are normal elements in a C⋆-algebra `A` which are interwined by `x` (i.e., `SemiconjBy x a b`, that is, `x * a = b * x`), then `star a` and `star b` are also intertwined by `x`. -+ ++ `isStarNormal_iff_forall_exp_mul_exp_mem_unitary`: A characterization of normal elements in a + C⋆-algebra in terms of exponentials. ## References @@ -125,7 +127,7 @@ public lemma IsStarNormal.commute_star_left {A : Type*} [NonUnitalCStarAlgebra A /-- A characterization of normal elements in a C⋆-algebra in terms of exponentials. -/ 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 + 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 ↦ ?_⟩ From 51ff3796cb090696aa57e51d35c0576977939a8a Mon Sep 17 00:00:00 2001 From: Jireh Loreaux Date: Mon, 6 Apr 2026 10:45:20 -0500 Subject: [PATCH 8/8] `open Complex` --- Mathlib/Analysis/CStarAlgebra/Fuglede.lean | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) diff --git a/Mathlib/Analysis/CStarAlgebra/Fuglede.lean b/Mathlib/Analysis/CStarAlgebra/Fuglede.lean index fe490c6eefabc9..3160eca1627e37 100644 --- a/Mathlib/Analysis/CStarAlgebra/Fuglede.lean +++ b/Mathlib/Analysis/CStarAlgebra/Fuglede.lean @@ -34,7 +34,7 @@ Therefore `‖f z‖ = ‖x‖` for all `z`, and since `f` is clearly entire, by proves that `star b * x = x * star a`, as desired. In a follow-up paper, Cater [cater1961] proved a number of related results using similar techniques. -We include one of these below, `isStarNormal_iff_forall_exp_mul_exp_mem_unitary`, +We include one of these below, `isStarNormal_iff_forall_exp_mul_exp_mem_unitary`, but the proof is independent of the Fuglede–Putnam–Rosenblum theorem. ## Main results @@ -42,7 +42,7 @@ but the proof is independent of the Fuglede–Putnam–Rosenblum theorem. + `fuglede_putnam_rosenblum`: If `a` and `b` are normal elements in a C⋆-algebra `A` which are interwined by `x` (i.e., `SemiconjBy x a b`, that is, `x * a = b * x`), then `star a` and `star b` are also intertwined by `x`. -+ `isStarNormal_iff_forall_exp_mul_exp_mem_unitary`: A characterization of normal elements in a ++ `isStarNormal_iff_forall_exp_mul_exp_mem_unitary`: A characterization of normal elements in a C⋆-algebra in terms of exponentials. ## References @@ -55,7 +55,7 @@ but the proof is independent of the Fuglede–Putnam–Rosenblum theorem. -/ -open NormedSpace selfAdjoint Bornology +open NormedSpace selfAdjoint Bornology Complex open scoped ComplexStarModule variable {A : Type*} [CStarAlgebra A] {a b x : A} [IsStarNormal a] [IsStarNormal b] @@ -72,7 +72,6 @@ lemma expMulMulExp_eq_expUnitary_mul_mul_expUnitary (h : SemiconjBy x a b) (z : simp_rw [← mul_assoc, mul_assoc (_ * _ * x)] congr! all_goals - open Complex in simp [imaginaryPart_apply_coe, smul_comm (2 : ℝ) I, smul_smul I I, sub_eq_add_neg] grind [exp_add_of_commute, Commute.smul_right, Commute.neg_right] @@ -136,7 +135,6 @@ public lemma isStarNormal_iff_forall_exp_mul_exp_mem_unitary {a : A} : · 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