Exact source: MathlibAnnex/Analysis/CStarAlgebra/CloseProjections.lean, lines 138–146.
Back to Exact projection links for one approximately inner automorphism
1import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute 2import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order 3import Mathlib.Analysis.Normed.Ring.Units 4 5/-! 6# Close projections in a unital C-star algebra 7 8Two star projections at distance strictly less than one are unitarily conjugate. 9The proof constructs the standard invertible intertwiner and takes its polar part. 10-/ 11 12set_option autoImplicit false 13 14open scoped NNReal Ring 15 16namespace IsStarProjection 17 18variable {A : Type*} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] 19 20omit [PartialOrder A] [StarOrderedRing A] in 21/-- Conjugation of a star projection by a unitary is a star projection. -/ 22theorem unitary_conjugate {p : A} (hp : IsStarProjection p) (u : unitary A) : 23 IsStarProjection ((u : A) * p * star (u : A)) := by 24 constructor 25 · rw [isIdempotentElem_iff] 26 calc 27 ((u : A) * p * star (u : A)) * ((u : A) * p * star (u : A)) = 28 (u : A) * p * (star (u : A) * (u : A)) * p * star (u : A) := by 29 simp only [mul_assoc] 30 _ = (u : A) * p * p * star (u : A) := by 31 rw [Unitary.star_mul_self_of_mem u.prop, mul_one] 32 _ = (u : A) * (p * p) * star (u : A) := by simp only [mul_assoc] 33 _ = (u : A) * p * star (u : A) := by rw [hp.isIdempotentElem.eq] 34 · rw [isSelfAdjoint_iff] 35 simp [star_mul, hp.isSelfAdjoint.star_eq, mul_assoc] 36 37/-- The standard intertwiner between two projections. -/ 38def closeIntertwiner (p q : A) : A := 39 q * p + (1 - q) * (1 - p) 40 41omit [PartialOrder A] [StarOrderedRing A] in 42theorem closeIntertwiner_mul (p q : A) (hp : IsStarProjection p) 43 (hq : IsStarProjection q) : 44 closeIntertwiner p q * p = q * closeIntertwiner p q := by 45 have hl : closeIntertwiner p q * p = q * p := by 46 simp [closeIntertwiner, add_mul, mul_assoc, hp.isIdempotentElem.eq, 47 hp.one_sub_mul_self] 48 have hr : q * closeIntertwiner p q = q * p := by 49 simp [closeIntertwiner, mul_add, ← mul_assoc, hq.isIdempotentElem.eq, 50 hq.mul_one_sub_self] 51 exact hl.trans hr.symm 52 53omit [PartialOrder A] [StarOrderedRing A] in 54theorem closeIntertwiner_sub_one (p q : A) (hp : IsStarProjection p) : 55 closeIntertwiner p q - 1 = (q - p) * (2 * p - 1) := by 56 simp only [closeIntertwiner] 57 noncomm_ring [hp.isIdempotentElem.eq] 58 59omit [PartialOrder A] [StarOrderedRing A] in 60theorem norm_closeIntertwiner_sub_one (p q : A) [Nontrivial A] 61 (hp : IsStarProjection p) : 62 ‖closeIntertwiner p q - 1‖ = ‖p - q‖ := by 63 rw [closeIntertwiner_sub_one p q hp] 64 let s : unitary A := ⟨2 * p - 1, hp.two_mul_sub_one_mem_unitary⟩ 65 change ‖(q - p) * (s : A)‖ = ‖p - q‖ 66 rw [CStarRing.norm_mul_coe_unitary] 67 exact norm_sub_rev q p 68 69omit [PartialOrder A] [StarOrderedRing A] in 70theorem isUnit_closeIntertwiner (p q : A) [Nontrivial A] 71 (hp : IsStarProjection p) (hclose : ‖p - q‖ < 1) : 72 IsUnit (closeIntertwiner p q) := by 73 have hnear : ‖closeIntertwiner p q - (1 : A)‖ < 74 (‖(↑((1 : Aˣ)⁻¹) : A)‖)⁻¹ := by 75 simpa [norm_closeIntertwiner_sub_one p q hp] using hclose 76 exact (Units.ofNearby (1 : Aˣ) (closeIntertwiner p q) hnear).isUnit 77 78/-- The polar part of an invertible intertwiner of self-adjoint elements is unitary and 79is still an intertwiner. -/ 80theorem exists_unitary_of_isUnit_of_mul_eq {x p q : A} (hx : IsUnit x) 81 (hp : IsSelfAdjoint p) (hq : IsSelfAdjoint q) (hxp : x * p = q * x) : 82 ∃ u : unitary A, (u : A) * p = q * u := by 83 let a : A := star x * x 84 let s : A := CFC.sqrt a 85 let t : A := s⁻¹ʳ 86 let u : A := x * t 87 have ha_pos : IsStrictlyPositive a := by 88 apply CStarAlgebra.isStrictlyPositive_iff_eq_star_mul_self.mpr 89 exact ⟨x, hx, rfl⟩ 90 have hs_unit : IsUnit s := by 91 exact ha_pos.isUnit_cfcSqrt a 92 have hs_self : IsSelfAdjoint s := IsSelfAdjoint.of_nonneg (CFC.sqrt_nonneg a) 93 have ht_self : IsSelfAdjoint t := hs_self.ringInverse 94 have hu_unit : IsUnit u := hx.mul hs_unit.ringInverse 95 have hstar : p * star x = star x * q := by 96 have := congrArg star hxp 97 simpa [star_mul, hp.star_eq, hq.star_eq] using this 98 have ha_comm : Commute a p := by 99 rw [commute_iff_eq] 100 dsimp only [a] 101 calc 102 star x * x * p = star x * (x * p) := by rw [mul_assoc] 103 _ = star x * (q * x) := by rw [hxp] 104 _ = (star x * q) * x := by rw [mul_assoc] 105 _ = (p * star x) * x := by rw [hstar] 106 _ = p * (star x * x) := by rw [mul_assoc] 107 have hs_comm : Commute s p := by 108 dsimp only [s] 109 simpa [CFC.sqrt] using ha_comm.cfcₙ_nnreal NNReal.sqrt 110 have ht_comm : Commute t p := by 111 dsimp only [t] 112 rw [Ring.inverse_of_isUnit hs_unit] 113 exact Commute.units_inv_left (by simpa using hs_comm) 114 have hu_star_mul : star u * u = 1 := by 115 dsimp only [u] 116 rw [star_mul, ht_self.star_eq] 117 calc 118 t * star x * (x * t) = t * (star x * x) * t := by simp only [mul_assoc] 119 _ = t * a * t := rfl 120 _ = t * (s * s) * t := by rw [CFC.sqrt_mul_sqrt_self a ha_pos.nonneg] 121 _ = (t * s) * (s * t) := by simp only [mul_assoc] 122 _ = 1 := by 123 rw [show t * s = 1 by exact Ring.inverse_mul_cancel s hs_unit, 124 show s * t = 1 by exact Ring.mul_inverse_cancel s hs_unit, one_mul] 125 have hu_mem : u ∈ unitary A := hu_unit.mem_unitary_of_star_mul_self hu_star_mul 126 let U : unitary A := ⟨u, hu_mem⟩ 127 refine ⟨U, ?_⟩ 128 change u * p = q * u 129 dsimp only [u] 130 calc 131 x * t * p = x * (t * p) := by rw [mul_assoc] 132 _ = x * (p * t) := by rw [ht_comm.eq] 133 _ = (x * p) * t := by rw [mul_assoc] 134 _ = (q * x) * t := by rw [hxp] 135 _ = q * (x * t) := by rw [mul_assoc] 136 137/-- Star projections at distance less than one are unitarily conjugate. -/ 138theorem exists_unitary_conjugate_of_norm_sub_lt_one {p q : A} [Nontrivial A] 139 (hp : IsStarProjection p) (hq : IsStarProjection q) (hclose : ‖p - q‖ < 1) : 140 ∃ u : unitary A, (u : A) * p * star u = q := by 141 have hx := isUnit_closeIntertwiner p q hp hclose 142 obtain ⟨u, hu⟩ := exists_unitary_of_isUnit_of_mul_eq hx hp.isSelfAdjoint 143 hq.isSelfAdjoint (closeIntertwiner_mul p q hp hq) 144 refine ⟨u, ?_⟩ 145 rw [hu, mul_assoc, Unitary.coe_mul_star_self, mul_one] 146 147end IsStarProjection