Exact source: MathlibAnnex/Analysis/CStarAlgebra/CAR/Simplicity.lean
Pinned GitHub source · Raw UTF-8 source
Back to Simplicity of the completed CAR algebra
1import MathlibAnnex.Analysis.CStarAlgebra.CAR.Completion2import MathlibAnnex.Analysis.CStarAlgebra.GNSCyclic3import Mathlib.Analysis.SpecificLimits.Normed4import Mathlib.Analysis.CStarAlgebra.ContinuousLinearMap5import Mathlib.RingTheory.TwoSidedIdeal.Operations6import Mathlib.RingTheory.SimpleRing.Basic78/-!9# Faithfulness and closed-ideal simplicity of the completed CAR algebra10-/1112set_option autoImplicit false13set_option maxHeartbeats 8000001415open scoped ComplexOrder InnerProductSpace1617namespace MathlibAnnex.CStarAlgebra.CAR1819/-- The positive-linear-map form of the completed root state. -/20noncomputable def rootPositiveState : Limit →ₚ[ℂ] ℂ :=21 PositiveLinearMap.mk₀ rootState.toLinearMap rootState_nonneg2223@[simp]24theorem rootPositiveState_apply (x : Limit) : rootPositiveState x = rootState x := rfl2526@[simp]27theorem rootPositiveState_one : rootPositiveState 1 = 1 := rootState_one2829noncomputable instance rootGNSNontrivial : Nontrivial rootPositiveState.GNS := by30 refine ⟨⟨0, rootPositiveState.gnsCyclicVector, ?_⟩⟩31 intro h32 have hn := rootPositiveState.norm_gnsCyclicVector rootPositiveState_one33 rw [← h, norm_zero] at hn34 exact zero_ne_one hn3536theorem norm_leftMulMapPreGNS_apply_le (x : Limit) (y : rootPositiveState.PreGNS) :37 ‖rootPositiveState.leftMulMapPreGNS x y‖ ≤ ‖x‖ * ‖y‖ := by38 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 := by47 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_smul50 calc51 _ ≤ rootPositiveState52 (‖x‖ ^ 2 • star (rootPositiveState.ofPreGNS y) *53 rootPositiveState.ofPreGNS y) := by54 simpa using OrderHomClass.mono rootPositiveState horder55 _ = _ := by56 simp [← Complex.coe_smul, PositiveLinearMap.preGNS_norm_sq]5758theorem norm_leftMulMapPreGNS_le (x : Limit) :59 ‖rootPositiveState.leftMulMapPreGNS x‖ ≤ ‖x‖ := by60 exact ContinuousLinearMap.opNorm_le_bound _ (norm_nonneg x)61 (norm_leftMulMapPreGNS_apply_le x)6263theorem norm_rootRepresentation_le (x : Limit) :64 ‖rootPositiveState.gnsStarAlgHom x‖ ≤ ‖x‖ := by65 change ‖rootPositiveState.leftMulMapPreGNS x |>.completion‖ ≤ ‖x‖66 apply ContinuousLinearMap.opNorm_le_bound _ (norm_nonneg x)67 intro y68 refine UniformSpace.Completion.induction_on69 (p := fun y => ‖rootPositiveState.leftMulMapPreGNS x |>.completion y‖ ≤70 ‖x‖ * ‖y‖) y ?_ ?_71 · exact isClosed_le (by fun_prop) (by fun_prop)72 · intro z73 simpa using norm_leftMulMapPreGNS_apply_le x z7475/-- 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 => by79 simpa using norm_rootRepresentation_le x8081@[simp]82theorem rootRepresentationCLM_apply (x : Limit) :83 rootRepresentationCLM x = rootPositiveState.gnsStarAlgHom x := by rfl8485theorem rootRepresentation_stage_injective (n : ℕ) :86 Function.Injective (rootPositiveState.gnsStarAlgHom.comp (ofStage n)) :=87 (rootPositiveState.gnsStarAlgHom.comp (ofStage n)).toRingHom.injective8889theorem norm_rootRepresentation_stage (n : ℕ) (x : Stage n) :90 ‖rootPositiveState.gnsStarAlgHom (ofStage n x)‖ = ‖ofStage n x‖ := by91 exact NonUnitalStarAlgHom.norm_map92 (rootPositiveState.gnsStarAlgHom.comp (ofStage n))93 (rootRepresentation_stage_injective n) x |>.trans (norm_ofStage n x).symm9495theorem norm_rootRepresentation (x : Limit) :96 ‖rootPositiveState.gnsStarAlgHom x‖ = ‖x‖ := by97 let f : Limit → ℝ := fun x => ‖rootRepresentationCLM x‖98 let g : Limit → ℝ := fun x => ‖x‖99 have hfg : f = g := (rootRepresentationCLM.continuous.norm).ext_on100 dense_stageRange continuous_norm fun x hx => by101 rcases Set.mem_iUnion.mp hx with ⟨n, hn⟩102 rcases hn with ⟨a, rfl⟩103 exact norm_rootRepresentation_stage n a104 exact congrFun hfg x105106theorem rootRepresentation_injective :107 Function.Injective rootPositiveState.gnsStarAlgHom :=108 fun x y hxy => by109 rw [← sub_eq_zero, ← norm_eq_zero, ← norm_rootRepresentation]110 rw [map_sub, hxy, sub_self, norm_zero]111112/-- Matrix coefficients of the cyclic root vector separate elements because its113GNS representation is faithful. -/114theorem exists_rootState_mul_ne_zero {x : Limit} (hx : x ≠ 0) :115 ∃ b c : Limit, rootState (b * x * c) ≠ 0 := by116 by_contra h117 push Not at h118 have horbit (c : Limit) :119 rootPositiveState.gnsStarAlgHom x120 (rootPositiveState.gnsStarAlgHom c rootPositiveState.gnsCyclicVector) = 0 := by121 apply norm_eq_zero.mp122 calc123 ‖rootPositiveState.gnsStarAlgHom x124 (rootPositiveState.gnsStarAlgHom c rootPositiveState.gnsCyclicVector)‖ =125 ‖rootPositiveState.gnsStarAlgHom (x * c)126 rootPositiveState.gnsCyclicVector‖ := by127 rw [map_mul]128 rfl129 _ = ‖(rootPositiveState.toPreGNS (x * c) : rootPositiveState.GNS)‖ := by130 rw [PositiveLinearMap.gnsStarAlgHom_apply_gnsCyclicVector]131 _ = ‖rootPositiveState.toPreGNS (x * c)‖ :=132 UniformSpace.Completion.norm_coe _133 _ = 0 := by134 have hs : ((‖rootPositiveState.toPreGNS (x * c)‖ ^ 2 : ℝ) : ℂ) = 0 := by135 calc136 ((‖rootPositiveState.toPreGNS (x * c)‖ ^ 2 : ℝ) : ℂ) =137 rootPositiveState (star (x * c) * (x * c)) := by138 simpa using rootPositiveState.preGNS_norm_sq139 (rootPositiveState.toPreGNS (x * c))140 _ = 0 := by141 change rootState (star (x * c) * (x * c)) = 0142 rw [star_mul]143 simpa only [mul_assoc] using h (star c * star x) c144 exact (sq_eq_zero_iff).mp (Complex.ofReal_injective hs)145 have hop : rootPositiveState.gnsStarAlgHom x = 0 := by146 apply ContinuousLinearMap.coeFn_injective147 exact (rootPositiveState.gnsStarAlgHom x).continuous.ext_on148 rootPositiveState.denseRange_gnsStarAlgHom_apply_gnsCyclicVector149 continuous_zero fun y hy => by150 rcases hy with ⟨c, rfl⟩151 exact horbit c152 apply hx153 apply rootRepresentation_injective154 simpa using hop155156private theorem rootProjection_ne_zero (n : ℕ) : rootProjection n ≠ 0 := by157 intro h158 have hentry := congrArg (fun x : Stage n => x 0 0) h159 simp [rootProjection] at hentry160161/-- A nonzero element of a two-sided ideal forces one projection of the root flag162into 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 := by166 obtain ⟨b, c, hbc⟩ := exists_rootState_mul_ne_zero hx167 let y := b * x * c168 let lam := rootState y169 have hlam : lam ≠ 0 := hbc170 have hyI : y ∈ I := by171 exact I.mul_mem_right (b * x) c (I.mul_mem_left b x hxI)172 have hinv : (lam⁻¹ : ℂ) ≠ 0 := inv_ne_zero hlam173 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 hden176 obtain ⟨N, hN⟩ := Metric.tendsto_atTop.mp (tendsto_norm_compressionError y) δ hδ177 have herr : ‖compressionError N y‖ < δ := by178 have := hN N le_rfl179 simpa [Real.dist_eq, abs_of_nonneg (norm_nonneg _)] using this180 let q := rootFlag N181 let z := q * y * q182 have hq : IsStarProjection q := isStarProjection_rootFlag N183 have hzI : z ∈ I := I.mul_mem_right (q * y) q (I.mul_mem_left q y hyI)184 have herr' : ‖z - lam • q‖ < δ := by185 simpa [compressionError, q, z, lam] using herr186 have hscaled_eq : q - lam⁻¹ • z = -(lam⁻¹ • (z - lam • q)) := by187 rw [smul_sub, smul_smul, inv_mul_cancel₀ hlam, one_smul]188 abel189 have hhalf : ‖(lam⁻¹ : ℂ)‖ * δ = (1 : ℝ) / 2 := by190 dsimp [δ]191 rw [one_div, mul_inv_rev, ← mul_assoc,192 mul_inv_cancel₀ (norm_ne_zero_iff.mpr hinv), one_mul]193 norm_num194 have hsmall : ‖q - lam⁻¹ • z‖ < 1 := by195 rw [hscaled_eq, norm_neg, norm_smul]196 calc197 ‖(lam⁻¹ : ℂ)‖ * ‖z - lam • q‖ <198 ‖(lam⁻¹ : ℂ)‖ * δ :=199 mul_lt_mul_of_pos_left herr' (norm_pos_iff.mpr hinv)200 _ = (1 : ℝ) / 2 := hhalf201 _ < 1 := by norm_num202 have hu : IsUnit (1 - (q - lam⁻¹ • z)) :=203 isUnit_one_sub_of_norm_lt_one hsmall204 have hzq : z * q = z := by205 dsimp [z]206 rw [mul_assoc, hq.isIdempotentElem.eq]207 have huq : (1 - (q - lam⁻¹ • z)) * q = lam⁻¹ • z := by208 rw [sub_mul, one_mul, sub_mul, hq.isIdempotentElem.eq, smul_mul_assoc, hzq]209 abel210 let U := hu.unit211 have hU : (U : Limit) = 1 - (q - lam⁻¹ • z) := hu.unit_spec212 have hqexpr : q = (↑(U⁻¹) : Limit) * (lam⁻¹ • z) := by213 calc214 q = (↑(U⁻¹) : Limit) * ((U : Limit) * q) := by215 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)221222noncomputable instance limitIsSimpleRing : IsSimpleRing Limit :=223 IsSimpleRing.of_eq_bot_or_eq_top fun I => by224 by_cases hI : I = ⊥225 · exact Or.inl hI226 · right227 obtain ⟨x, hxI, hx⟩ := SetLike.exists_of_lt (bot_lt_iff_ne_bot.mpr hI)228 have hx0 : x ≠ 0 := by simpa using hx229 obtain ⟨n, hflagI⟩ := exists_rootFlag_mem_of_ne_zero_mem I hx0 hxI230 let J : TwoSidedIdeal (Stage n) := TwoSidedIdeal.comap (ofStage n).toRingHom I231 have hpJ : rootProjection n ∈ J := by232 exact TwoSidedIdeal.mem_comap (ofStage n).toRingHom |>.2 hflagI233 have honeJ : (1 : Stage n) ∈ J :=234 IsSimpleRing.one_mem_of_ne_zero_mem J (rootProjection_ne_zero n) hpJ235 apply TwoSidedIdeal.eq_top236 have honeI : (1 : Limit) ∈ I := by237 have := TwoSidedIdeal.mem_comap (ofStage n).toRingHom |>.1 honeJ238 rw [← (ofStage n).map_one]239 exact this240 exact honeI241242/-- The completed CAR algebra is simple in the stipulated closed-two-sided-ideal sense. -/243theorem isSimpleCStarAlgebra_limit : MathlibAnnex.CStarAlgebra.IsSimpleCStarAlgebra Limit := by244 constructor245 · infer_instance246 · intro I _247 exact eq_bot_or_eq_top I248249end MathlibAnnex.CStarAlgebra.CAR