Exact source: MathlibAnnex/Analysis/CStarAlgebra/CAR/Simplicity.lean, lines 63–73.
Back to Simplicity of the completed CAR algebra
1import MathlibAnnex.Analysis.CStarAlgebra.CAR.Completion 2import MathlibAnnex.Analysis.CStarAlgebra.GNSCyclic 3import Mathlib.Analysis.SpecificLimits.Normed 4import Mathlib.Analysis.CStarAlgebra.ContinuousLinearMap 5import Mathlib.RingTheory.TwoSidedIdeal.Operations 6import Mathlib.RingTheory.SimpleRing.Basic 7 8/-! 9# Faithfulness and closed-ideal simplicity of the completed CAR algebra 10-/ 11 12set_option autoImplicit false 13set_option maxHeartbeats 800000 14 15open scoped ComplexOrder InnerProductSpace 16 17namespace MathlibAnnex.CStarAlgebra.CAR 18 19/-- The positive-linear-map form of the completed root state. -/ 20noncomputable def rootPositiveState : Limit →ₚ[ℂ] ℂ := 21 PositiveLinearMap.mk₀ rootState.toLinearMap rootState_nonneg 22 23@[simp] 24theorem rootPositiveState_apply (x : Limit) : rootPositiveState x = rootState x := rfl 25 26@[simp] 27theorem rootPositiveState_one : rootPositiveState 1 = 1 := rootState_one 28 29noncomputable instance rootGNSNontrivial : Nontrivial rootPositiveState.GNS := by 30 refine ⟨⟨0, rootPositiveState.gnsCyclicVector, ?_⟩⟩ 31 intro h 32 have hn := rootPositiveState.norm_gnsCyclicVector rootPositiveState_one 33 rw [← h, norm_zero] at hn 34 exact zero_ne_one hn 35 36theorem norm_leftMulMapPreGNS_apply_le (x : Limit) (y : rootPositiveState.PreGNS) : 37 ‖rootPositiveState.leftMulMapPreGNS x y‖ ≤ ‖x‖ * ‖y‖ := by 38 rw [PositiveLinearMap.leftMulMapPreGNS_apply] 39 rw [← sq_le_sq₀ (by positivity) (by positivity), mul_pow, 40 ← RCLike.ofReal_le_ofReal (K := ℂ), RCLike.ofReal_pow, 41 RCLike.ofReal_eq_complex_ofReal, PositiveLinearMap.preGNS_norm_sq] 42 have horder : 43 star (rootPositiveState.ofPreGNS y) * star x * 44 (x * rootPositiveState.ofPreGNS y) ≤ 45 ‖x‖ ^ 2 • star (rootPositiveState.ofPreGNS y) * 46 rootPositiveState.ofPreGNS y := by 47 rw [← mul_assoc, mul_assoc _ (star x), sq, 48 ← CStarRing.norm_star_mul_self (x := x), smul_mul_assoc] 49 exact CStarAlgebra.star_left_conjugate_le_norm_smul 50 calc 51 _ ≤ rootPositiveState 52 (‖x‖ ^ 2 • star (rootPositiveState.ofPreGNS y) * 53 rootPositiveState.ofPreGNS y) := by 54 simpa using OrderHomClass.mono rootPositiveState horder 55 _ = _ := by 56 simp [← Complex.coe_smul, PositiveLinearMap.preGNS_norm_sq] 57 58theorem norm_leftMulMapPreGNS_le (x : Limit) : 59 ‖rootPositiveState.leftMulMapPreGNS x‖ ≤ ‖x‖ := by 60 exact ContinuousLinearMap.opNorm_le_bound _ (norm_nonneg x) 61 (norm_leftMulMapPreGNS_apply_le x) 62 63theorem norm_rootRepresentation_le (x : Limit) : 64 ‖rootPositiveState.gnsStarAlgHom x‖ ≤ ‖x‖ := by 65 change ‖rootPositiveState.leftMulMapPreGNS x |>.completion‖ ≤ ‖x‖ 66 apply ContinuousLinearMap.opNorm_le_bound _ (norm_nonneg x) 67 intro y 68 refine UniformSpace.Completion.induction_on 69 (p := fun y => ‖rootPositiveState.leftMulMapPreGNS x |>.completion y‖ ≤ 70 ‖x‖ * ‖y‖) y ?_ ?_ 71 · exact isClosed_le (by fun_prop) (by fun_prop) 72 · intro z 73 simpa using norm_leftMulMapPreGNS_apply_le x z 74 75/-- The root GNS representation, bundled as a continuous linear map in its algebra argument. -/ 76noncomputable def rootRepresentationCLM : 77 Limit →L[ℂ] (rootPositiveState.GNS →L[ℂ] rootPositiveState.GNS) := 78 (rootPositiveState.gnsStarAlgHom).toLinearMap.mkContinuous 1 fun x => by 79 simpa using norm_rootRepresentation_le x 80 81@[simp] 82theorem rootRepresentationCLM_apply (x : Limit) : 83 rootRepresentationCLM x = rootPositiveState.gnsStarAlgHom x := by rfl 84 85theorem rootRepresentation_stage_injective (n : ℕ) : 86 Function.Injective (rootPositiveState.gnsStarAlgHom.comp (ofStage n)) := 87 (rootPositiveState.gnsStarAlgHom.comp (ofStage n)).toRingHom.injective 88 89theorem norm_rootRepresentation_stage (n : ℕ) (x : Stage n) : 90 ‖rootPositiveState.gnsStarAlgHom (ofStage n x)‖ = ‖ofStage n x‖ := by 91 exact NonUnitalStarAlgHom.norm_map 92 (rootPositiveState.gnsStarAlgHom.comp (ofStage n)) 93 (rootRepresentation_stage_injective n) x |>.trans (norm_ofStage n x).symm 94 95theorem norm_rootRepresentation (x : Limit) : 96 ‖rootPositiveState.gnsStarAlgHom x‖ = ‖x‖ := by 97 let f : Limit → ℝ := fun x => ‖rootRepresentationCLM x‖ 98 let g : Limit → ℝ := fun x => ‖x‖ 99 have hfg : f = g := (rootRepresentationCLM.continuous.norm).ext_on 100 dense_stageRange continuous_norm fun x hx => by 101 rcases Set.mem_iUnion.mp hx with ⟨n, hn⟩ 102 rcases hn with ⟨a, rfl⟩ 103 exact norm_rootRepresentation_stage n a 104 exact congrFun hfg x 105 106theorem rootRepresentation_injective : 107 Function.Injective rootPositiveState.gnsStarAlgHom := 108 fun x y hxy => by 109 rw [← sub_eq_zero, ← norm_eq_zero, ← norm_rootRepresentation] 110 rw [map_sub, hxy, sub_self, norm_zero] 111 112/-- Matrix coefficients of the cyclic root vector separate elements because its 113GNS representation is faithful. -/ 114theorem exists_rootState_mul_ne_zero {x : Limit} (hx : x ≠ 0) : 115 ∃ b c : Limit, rootState (b * x * c) ≠ 0 := by 116 by_contra h 117 push Not at h 118 have horbit (c : Limit) : 119 rootPositiveState.gnsStarAlgHom x 120 (rootPositiveState.gnsStarAlgHom c rootPositiveState.gnsCyclicVector) = 0 := by 121 apply norm_eq_zero.mp 122 calc 123 ‖rootPositiveState.gnsStarAlgHom x 124 (rootPositiveState.gnsStarAlgHom c rootPositiveState.gnsCyclicVector)‖ = 125 ‖rootPositiveState.gnsStarAlgHom (x * c) 126 rootPositiveState.gnsCyclicVector‖ := by 127 rw [map_mul] 128 rfl 129 _ = ‖(rootPositiveState.toPreGNS (x * c) : rootPositiveState.GNS)‖ := by 130 rw [PositiveLinearMap.gnsStarAlgHom_apply_gnsCyclicVector] 131 _ = ‖rootPositiveState.toPreGNS (x * c)‖ := 132 UniformSpace.Completion.norm_coe _ 133 _ = 0 := by 134 have hs : ((‖rootPositiveState.toPreGNS (x * c)‖ ^ 2 : ℝ) : ℂ) = 0 := by 135 calc 136 ((‖rootPositiveState.toPreGNS (x * c)‖ ^ 2 : ℝ) : ℂ) = 137 rootPositiveState (star (x * c) * (x * c)) := by 138 simpa using rootPositiveState.preGNS_norm_sq 139 (rootPositiveState.toPreGNS (x * c)) 140 _ = 0 := by 141 change rootState (star (x * c) * (x * c)) = 0 142 rw [star_mul] 143 simpa only [mul_assoc] using h (star c * star x) c 144 exact (sq_eq_zero_iff).mp (Complex.ofReal_injective hs) 145 have hop : rootPositiveState.gnsStarAlgHom x = 0 := by 146 apply ContinuousLinearMap.coeFn_injective 147 exact (rootPositiveState.gnsStarAlgHom x).continuous.ext_on 148 rootPositiveState.denseRange_gnsStarAlgHom_apply_gnsCyclicVector 149 continuous_zero fun y hy => by 150 rcases hy with ⟨c, rfl⟩ 151 exact horbit c 152 apply hx 153 apply rootRepresentation_injective 154 simpa using hop 155 156private theorem rootProjection_ne_zero (n : ℕ) : rootProjection n ≠ 0 := by 157 intro h 158 have hentry := congrArg (fun x : Stage n => x 0 0) h 159 simp [rootProjection] at hentry 160 161/-- A nonzero element of a two-sided ideal forces one projection of the root flag 162into that ideal. The inverse is obtained by a Neumann-series perturbation of `1`. -/ 163theorem exists_rootFlag_mem_of_ne_zero_mem (I : TwoSidedIdeal Limit) 164 {x : Limit} (hx : x ≠ 0) (hxI : x ∈ I) : 165 ∃ n, rootFlag n ∈ I := by 166 obtain ⟨b, c, hbc⟩ := exists_rootState_mul_ne_zero hx 167 let y := b * x * c 168 let lam := rootState y 169 have hlam : lam ≠ 0 := hbc 170 have hyI : y ∈ I := by 171 exact I.mul_mem_right (b * x) c (I.mul_mem_left b x hxI) 172 have hinv : (lam⁻¹ : ℂ) ≠ 0 := inv_ne_zero hlam 173 let δ : ℝ := 1 / (2 * ‖(lam⁻¹ : ℂ)‖) 174 have hden : 0 < 2 * ‖(lam⁻¹ : ℂ)‖ := mul_pos two_pos (norm_pos_iff.mpr hinv) 175 have hδ : 0 < δ := one_div_pos.mpr hden 176 obtain ⟨N, hN⟩ := Metric.tendsto_atTop.mp (tendsto_norm_compressionError y) δ hδ 177 have herr : ‖compressionError N y‖ < δ := by 178 have := hN N le_rfl 179 simpa [Real.dist_eq, abs_of_nonneg (norm_nonneg _)] using this 180 let q := rootFlag N 181 let z := q * y * q 182 have hq : IsStarProjection q := isStarProjection_rootFlag N 183 have hzI : z ∈ I := I.mul_mem_right (q * y) q (I.mul_mem_left q y hyI) 184 have herr' : ‖z - lam • q‖ < δ := by 185 simpa [compressionError, q, z, lam] using herr 186 have hscaled_eq : q - lam⁻¹ • z = -(lam⁻¹ • (z - lam • q)) := by 187 rw [smul_sub, smul_smul, inv_mul_cancel₀ hlam, one_smul] 188 abel 189 have hhalf : ‖(lam⁻¹ : ℂ)‖ * δ = (1 : ℝ) / 2 := by 190 dsimp [δ] 191 rw [one_div, mul_inv_rev, ← mul_assoc, 192 mul_inv_cancel₀ (norm_ne_zero_iff.mpr hinv), one_mul] 193 norm_num 194 have hsmall : ‖q - lam⁻¹ • z‖ < 1 := by 195 rw [hscaled_eq, norm_neg, norm_smul] 196 calc 197 ‖(lam⁻¹ : ℂ)‖ * ‖z - lam • q‖ < 198 ‖(lam⁻¹ : ℂ)‖ * δ := 199 mul_lt_mul_of_pos_left herr' (norm_pos_iff.mpr hinv) 200 _ = (1 : ℝ) / 2 := hhalf 201 _ < 1 := by norm_num 202 have hu : IsUnit (1 - (q - lam⁻¹ • z)) := 203 isUnit_one_sub_of_norm_lt_one hsmall 204 have hzq : z * q = z := by 205 dsimp [z] 206 rw [mul_assoc, hq.isIdempotentElem.eq] 207 have huq : (1 - (q - lam⁻¹ • z)) * q = lam⁻¹ • z := by 208 rw [sub_mul, one_mul, sub_mul, hq.isIdempotentElem.eq, smul_mul_assoc, hzq] 209 abel 210 let U := hu.unit 211 have hU : (U : Limit) = 1 - (q - lam⁻¹ • z) := hu.unit_spec 212 have hqexpr : q = (↑(U⁻¹) : Limit) * (lam⁻¹ • z) := by 213 calc 214 q = (↑(U⁻¹) : Limit) * ((U : Limit) * q) := by 215 rw [← mul_assoc, Units.inv_mul, one_mul] 216 _ = (↑(U⁻¹) : Limit) * (lam⁻¹ • z) := by rw [hU, huq] 217 refine ⟨N, ?_⟩ 218 rw [show rootFlag N = q by rfl, hqexpr, Algebra.smul_def] 219 exact I.mul_mem_left (↑(U⁻¹) : Limit) _ 220 (I.mul_mem_left (algebraMap ℂ Limit lam⁻¹) z hzI) 221 222noncomputable instance limitIsSimpleRing : IsSimpleRing Limit := 223 IsSimpleRing.of_eq_bot_or_eq_top fun I => by 224 by_cases hI : I = ⊥ 225 · exact Or.inl hI 226 · right 227 obtain ⟨x, hxI, hx⟩ := SetLike.exists_of_lt (bot_lt_iff_ne_bot.mpr hI) 228 have hx0 : x ≠ 0 := by simpa using hx 229 obtain ⟨n, hflagI⟩ := exists_rootFlag_mem_of_ne_zero_mem I hx0 hxI 230 let J : TwoSidedIdeal (Stage n) := TwoSidedIdeal.comap (ofStage n).toRingHom I 231 have hpJ : rootProjection n ∈ J := by 232 exact TwoSidedIdeal.mem_comap (ofStage n).toRingHom |>.2 hflagI 233 have honeJ : (1 : Stage n) ∈ J := 234 IsSimpleRing.one_mem_of_ne_zero_mem J (rootProjection_ne_zero n) hpJ 235 apply TwoSidedIdeal.eq_top 236 have honeI : (1 : Limit) ∈ I := by 237 have := TwoSidedIdeal.mem_comap (ofStage n).toRingHom |>.1 honeJ 238 rw [← (ofStage n).map_one] 239 exact this 240 exact honeI 241 242/-- The completed CAR algebra is simple in the stipulated closed-two-sided-ideal sense. -/ 243theorem isSimpleCStarAlgebra_limit : MathlibAnnex.CStarAlgebra.IsSimpleCStarAlgebra Limit := by 244 constructor 245 · infer_instance 246 · intro I _ 247 exact eq_bot_or_eq_top I 248 249end MathlibAnnex.CStarAlgebra.CAR