feat: (cfcₙ f a : A⁺¹) = cfc f (a : A⁺¹) (#18358)

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

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

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,29 +79,33 @@ 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 ⟨?_, ?_⟩
     all_goals refine fun h ↦ (ha ?_).elim
     · 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