From 2fcccf33f5ed7a95518a6a4602e0a586b156a13e Mon Sep 17 00:00:00 2001 From: Jireh Loreaux Date: Tue, 29 Oct 2024 22:19:32 +0000 Subject: [PATCH] =?UTF-8?q?feat:=20`(cfc=E2=82=99=20f=20a=20:=20A=E2=81=BA?= =?UTF-8?q?=C2=B9)=20=3D=20cfc=20f=20(a=20:=20A=E2=81=BA=C2=B9)`=20(#18358?= =?UTF-8?q?)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Mathlib/Algebra/Algebra/Quasispectrum.lean | 8 +++ .../Instances.lean | 50 +++++++++++++++++-- .../ContinuousFunctionalCalculus/Order.lean | 22 ++++---- 3 files changed, 66 insertions(+), 14 deletions(-) diff --git a/Mathlib/Algebra/Algebra/Quasispectrum.lean b/Mathlib/Algebra/Algebra/Quasispectrum.lean index 63ac30ba8df9a..712888eb8d3ff 100644 --- a/Mathlib/Algebra/Algebra/Quasispectrum.lean +++ b/Mathlib/Algebra/Algebra/Quasispectrum.lean @@ -360,6 +360,14 @@ lemma quasispectrum_eq_spectrum_inr' (R S : Type*) {A : Type*} [Semifield R] apply forall_congr' fun x ↦ ?_ rw [not_iff_not, Units.smul_def, Units.smul_def, ← inr_smul, ← inr_neg, isQuasiregular_inr_iff] +lemma quasispectrum_inr_eq (R S : Type*) {A : Type*} [Semifield R] + [Field S] [NonUnitalRing A] [Algebra R S] [Module S A] [IsScalarTower S A A] + [SMulCommClass S A A] [Module R A] [IsScalarTower R S A] (a : A) : + quasispectrum R (a : Unitization S A) = quasispectrum R a := by + rw [quasispectrum_eq_spectrum_union_zero, quasispectrum_eq_spectrum_inr' R S] + apply Set.union_eq_self_of_subset_right + simpa using zero_mem_spectrum_inr _ _ _ + end Unitization /-- A class for `𝕜`-algebras with a partial order where the ordering is compatible with the diff --git a/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Instances.lean b/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Instances.lean index a2cba0b1582a9..4a903ec4b4fda 100644 --- a/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Instances.lean +++ b/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Instances.lean @@ -180,16 +180,16 @@ instance IsStarNormal.instNonUnitalContinuousFunctionalCalculus {A : Type*} [NonUnitalCStarAlgebra A] : NonUnitalContinuousFunctionalCalculus ℂ (IsStarNormal : A → Prop) := RCLike.nonUnitalContinuousFunctionalCalculus Unitization.isStarNormal_inr -open Unitization in +open Unitization CStarAlgebra in lemma inr_comp_cfcₙHom_eq_cfcₙAux {A : Type*} [NonUnitalCStarAlgebra A] (a : A) [ha : IsStarNormal a] : (inrNonUnitalStarAlgHom ℂ A).comp (cfcₙHom ha) = cfcₙAux (isStarNormal_inr (R := ℂ) (A := A)) a ha := by have h (a : A) := isStarNormal_inr (R := ℂ) (A := A) (a := a) refine @UniqueNonUnitalContinuousFunctionalCalculus.eq_of_continuous_of_map_id _ _ _ _ _ _ _ _ _ _ _ inferInstance inferInstance _ (σₙ ℂ a) _ _ rfl _ _ ?_ ?_ ?_ - · show Continuous (fun f ↦ (cfcₙHom ha f : Unitization ℂ A)); fun_prop + · show Continuous (fun f ↦ (cfcₙHom ha f : A⁺¹)); fun_prop · exact isClosedEmbedding_cfcₙAux @(h) a ha |>.continuous - · trans (a : Unitization ℂ A) + · trans (a : A⁺¹) · congrm(inr $(cfcₙHom_id ha)) · exact cfcₙAux_id @(h) a ha |>.symm @@ -586,12 +586,13 @@ section NonnegSpectrumClass variable {A : Type*} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] +open scoped CStarAlgebra in instance CStarAlgebra.instNonnegSpectrumClass' : NonnegSpectrumClass ℝ A where quasispectrum_nonneg_of_nonneg a ha := by rw [Unitization.quasispectrum_eq_spectrum_inr' _ ℂ] -- should this actually be an instance on the `Unitization`? (probably scoped) - let _ := CStarAlgebra.spectralOrder (Unitization ℂ A) - have := CStarAlgebra.spectralOrderedRing (Unitization ℂ A) + let _ := CStarAlgebra.spectralOrder A⁺¹ + have := CStarAlgebra.spectralOrderedRing A⁺¹ apply spectrum_nonneg_of_nonneg rw [StarOrderedRing.nonneg_iff] at ha ⊢ have := AddSubmonoid.mem_map_of_mem (Unitization.inrNonUnitalStarAlgHom ℂ A) ha @@ -693,4 +694,43 @@ lemma cfcₙ_nnreal_eq_real {a : A} (f : ℝ≥0 → ℝ≥0) (ha : 0 ≤ a := b end NNRealEqRealNonUnital +section cfc_inr + +open CStarAlgebra + +variable {A : Type*} [NonUnitalCStarAlgebra A] + +open scoped NonUnitalContinuousFunctionalCalculus in +/-- This lemma requires a lot from type class synthesis, and so one should instead favor the bespoke +versions for `ℝ≥0`, `ℝ`, and `ℂ`. -/ +lemma Unitization.cfcₙ_eq_cfc_inr {R : Type*} [Semifield R] [StarRing R] [MetricSpace R] + [TopologicalSemiring R] [ContinuousStar R] [Module R A] [IsScalarTower R A A] + [SMulCommClass R A A] [CompleteSpace R] [Algebra R ℂ] [IsScalarTower R ℂ A] + {p : A → Prop} {p' : A⁺¹ → Prop} [NonUnitalContinuousFunctionalCalculus R p] + [ContinuousFunctionalCalculus R p'] + [UniqueNonUnitalContinuousFunctionalCalculus R (Unitization ℂ A)] + (hp : ∀ {a : A}, p' (a : A⁺¹) ↔ p a) (a : A) (f : R → R) (hf₀ : f 0 = 0 := by cfc_zero_tac) : + cfcₙ f a = cfc f (a : A⁺¹) := by + by_cases h : ContinuousOn f (σₙ R a) ∧ p a + · obtain ⟨hf, ha⟩ := h + rw [← cfcₙ_eq_cfc (quasispectrum_inr_eq R ℂ a ▸ hf)] + exact (inrNonUnitalStarAlgHom ℂ A).map_cfcₙ f a + · obtain (hf | ha) := not_and_or.mp h + · rw [cfcₙ_apply_of_not_continuousOn a hf, inr_zero, + cfc_apply_of_not_continuousOn _ (quasispectrum_eq_spectrum_inr' R ℂ a ▸ hf)] + · rw [cfcₙ_apply_of_not_predicate a ha, inr_zero, + cfc_apply_of_not_predicate _ (not_iff_not.mpr hp |>.mpr ha)] + +lemma Unitization.complex_cfcₙ_eq_cfc_inr (a : A) (f : ℂ → ℂ) (hf₀ : f 0 = 0 := by cfc_zero_tac) : + cfcₙ f a = cfc f (a : A⁺¹) := + Unitization.cfcₙ_eq_cfc_inr isStarNormal_inr .. + +/-- note: the version for `ℝ≥0`, `Unization.nnreal_cfcₙ_eq_cfc_inr`, can be found in +`Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order` -/ +lemma Unitization.real_cfcₙ_eq_cfc_inr (a : A) (f : ℝ → ℝ) (hf₀ : f 0 = 0 := by cfc_zero_tac) : + cfcₙ f a = cfc f (a : A⁺¹) := + Unitization.cfcₙ_eq_cfc_inr isSelfAdjoint_inr .. + +end cfc_inr + end diff --git a/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean b/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean index 61454ee4470ce..0be6a81f50b0a 100644 --- a/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean +++ b/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean @@ -14,7 +14,7 @@ import Mathlib.Topology.ContinuousMap.StarOrdered This file contains various basic facts about star-ordered rings (i.e. mainly C⋆-algebras) that depend on the continuous functional calculus. -We also put an order instance on `Unitization ℂ A` when `A` is a C⋆-algebra via +We also put an order instance on `A⁺¹ := Unitization ℂ A` when `A` is a C⋆-algebra via the spectral order. ## Main theorems @@ -79,22 +79,22 @@ namespace Unitization variable {A : Type*} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] -instance instPartialOrder : PartialOrder (Unitization ℂ A) := +instance instPartialOrder : PartialOrder A⁺¹ := CStarAlgebra.spectralOrder _ -instance instStarOrderedRing : StarOrderedRing (Unitization ℂ A) := +instance instStarOrderedRing : StarOrderedRing A⁺¹ := CStarAlgebra.spectralOrderedRing _ lemma inr_le_iff (a b : A) (ha : IsSelfAdjoint a := by cfc_tac) (hb : IsSelfAdjoint b := by cfc_tac) : - (a : Unitization ℂ A) ≤ (b : Unitization ℂ A) ↔ a ≤ b := by + (a : A⁺¹) ≤ (b : A⁺¹) ↔ a ≤ b := by -- TODO: prove the more general result for star monomorphisms and use it here. rw [← sub_nonneg, ← sub_nonneg (a := b), StarOrderedRing.nonneg_iff_spectrum_nonneg (R := ℝ) _, ← inr_sub ℂ b a, ← Unitization.quasispectrum_eq_spectrum_inr' ℝ ℂ] exact StarOrderedRing.nonneg_iff_quasispectrum_nonneg _ |>.symm @[simp, norm_cast] -lemma inr_nonneg_iff {a : A} : 0 ≤ (a : Unitization ℂ A) ↔ 0 ≤ a := by +lemma inr_nonneg_iff {a : A} : 0 ≤ (a : A⁺¹) ↔ 0 ≤ a := by by_cases ha : IsSelfAdjoint a · exact inr_zero ℂ (A := A) ▸ inr_le_iff 0 a · refine ⟨?_, ?_⟩ @@ -102,6 +102,10 @@ lemma inr_nonneg_iff {a : A} : 0 ≤ (a : Unitization ℂ A) ↔ 0 ≤ a := by · exact isSelfAdjoint_inr (R := ℂ) |>.mp <| .of_nonneg h · exact .of_nonneg h +lemma nnreal_cfcₙ_eq_cfc_inr (a : A) (f : ℝ≥0 → ℝ≥0) + (hf₀ : f 0 = 0 := by cfc_zero_tac) : cfcₙ f a = cfc f (a : A⁺¹) := + cfcₙ_eq_cfc_inr inr_nonneg_iff .. + end Unitization /-- `cfc_le_iff` only applies to a scalar ring where `R` is an actual `Ring`, and not a `Semiring`. @@ -364,7 +368,7 @@ instance instNonnegSpectrumClassComplexNonUnital : NonnegSpectrumClass ℂ A whe lemma norm_le_norm_of_nonneg_of_le {a b : A} (ha : 0 ≤ a := by cfc_tac) (hab : a ≤ b) : ‖a‖ ≤ ‖b‖ := by - suffices ∀ a b : Unitization ℂ A, 0 ≤ a → a ≤ b → ‖a‖ ≤ ‖b‖ by + suffices ∀ a b : A⁺¹, 0 ≤ a → a ≤ b → ‖a‖ ≤ ‖b‖ by have hb := ha.trans hab simpa only [ge_iff_le, Unitization.norm_inr] using this a b (by simpa) (by rwa [Unitization.inr_le_iff a b]) @@ -384,12 +388,12 @@ lemma norm_le_norm_of_nonneg_of_le {a b : A} (ha : 0 ≤ a := by cfc_tac) (hab : lemma conjugate_le_norm_smul {a b : A} (hb : IsSelfAdjoint b := by cfc_tac) : star a * b * a ≤ ‖b‖ • (star a * a) := by - suffices ∀ a b : Unitization ℂ A, IsSelfAdjoint b → star a * b * a ≤ ‖b‖ • (star a * a) by + suffices ∀ a b : A⁺¹, IsSelfAdjoint b → star a * b * a ≤ ‖b‖ • (star a * a) by rw [← Unitization.inr_le_iff _ _ (by aesop) ((IsSelfAdjoint.all _).smul (.star_mul_self a))] simpa [Unitization.norm_inr] using this a b <| hb.inr ℂ intro a b hb calc - star a * b * a ≤ star a * (algebraMap ℝ (Unitization ℂ A) ‖b‖) * a := + star a * b * a ≤ star a * (algebraMap ℝ A⁺¹ ‖b‖) * a := conjugate_le_conjugate hb.le_algebraMap_norm_self _ _ = ‖b‖ • (star a * a) := by simp [Algebra.algebraMap_eq_smul_one] @@ -402,7 +406,7 @@ lemma conjugate_le_norm_smul' {a b : A} (hb : IsSelfAdjoint b := by cfc_tac) : /-- The set of nonnegative elements in a C⋆-algebra is closed. -/ lemma isClosed_nonneg : IsClosed {a : A | 0 ≤ a} := by - suffices IsClosed {a : Unitization ℂ A | 0 ≤ a} by + suffices IsClosed {a : A⁺¹ | 0 ≤ a} by rw [Unitization.isometry_inr (𝕜 := ℂ) |>.isClosedEmbedding.closed_iff_image_closed] convert this.inter <| (Unitization.isometry_inr (𝕜 := ℂ)).isClosedEmbedding.isClosed_range ext a