feat(ContinuousFunctionalCalculus): add several lemmas involving the CFC and algebraMap (#14065)

This PR adds several lemmas about the interaction between the (non-unital) CFC and `algebraMap`. Several lemmas require some sort of nontriviality statement for the CFC (i.e. the predicate can't be false everywhere), I just stated it as an `hp : p 0` hypothesis in the lemma statements; it seems like the most convenient way in practice and probably the easiest to automate.

Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>

Author: dupuisf

Mathlib/Analysis/NormedSpace/Star/ContinuousFunctionalCalculus/Instances.lean

@@ -415,7 +415,7 @@ lemma SpectrumRestricts.eq_zero_of_neg {a : A} (ha : IsSelfAdjoint a)
     a = 0 := by
   nontriviality A
   rw [SpectrumRestricts.nnreal_iff] at ha₁ ha₂
-  apply eq_zero_of_spectrum_subset_zero (R := ℝ) a
+  apply CFC.eq_zero_of_spectrum_subset_zero (R := ℝ) a
   rw [Set.subset_singleton_iff]
   simp only [← spectrum.neg_eq, Set.mem_neg] at ha₂
   peel ha₁ with x hx _

Mathlib/Topology/ContinuousFunction/FunctionalCalculus.lean

@@ -569,19 +569,58 @@ lemma cfc_comp_polynomial (q : R[X]) (f : R → R) (a : A)
     cfc (f <| q.eval ·) a = cfc f (aeval a q) := by
   rw [cfc_comp' .., cfc_polynomial ..]
 
-lemma eq_algebraMap_of_spectrum_subset_singleton (r : R) (h_spec : spectrum R a ⊆ {r})
+lemma CFC.eq_algebraMap_of_spectrum_subset_singleton (r : R) (h_spec : spectrum R a ⊆ {r})
     (ha : p a := by cfc_tac) : a = algebraMap R A r := by
   simpa [cfc_id R a, cfc_const r a] using
     cfc_congr (f := id) (g := fun _ : R ↦ r) (a := a) fun x hx ↦ by simpa using h_spec hx
 
-lemma eq_zero_of_spectrum_subset_zero (h_spec : spectrum R a ⊆ {0}) (ha : p a := by cfc_tac) :
+lemma CFC.eq_zero_of_spectrum_subset_zero (h_spec : spectrum R a ⊆ {0}) (ha : p a := by cfc_tac) :
     a = 0 := by
   simpa using eq_algebraMap_of_spectrum_subset_singleton a 0 h_spec
 
-lemma eq_one_of_spectrum_subset_one (h_spec : spectrum R a ⊆ {1}) (ha : p a := by cfc_tac) :
+lemma CFC.eq_one_of_spectrum_subset_one (h_spec : spectrum R a ⊆ {1}) (ha : p a := by cfc_tac) :
     a = 1 := by
   simpa using eq_algebraMap_of_spectrum_subset_singleton a 1 h_spec
 
+lemma CFC.spectrum_algebraMap_subset (r : R) : spectrum R (algebraMap R A r) ⊆ {r} := by
+  rw [← cfc_const r 0 (cfc_predicate_zero R),
+    cfc_map_spectrum (fun _ ↦ r) 0 (cfc_predicate_zero R)]
+  rintro - ⟨x, -, rfl⟩
+  simp
+
+lemma CFC.spectrum_algebraMap_eq [Nontrivial A] (r : R) :
+    spectrum R (algebraMap R A r) = {r} := by
+  have hp : p 0 := cfc_predicate_zero R
+  rw [← cfc_const r 0 hp, cfc_map_spectrum (fun _ => r) 0 hp]
+  exact Set.Nonempty.image_const (⟨0, spectrum.zero_mem (R := R) not_isUnit_zero⟩) _
+
+lemma CFC.spectrum_zero_eq [Nontrivial A] :
+    spectrum R (0 : A) = {0} := by
+  have : (0 : A) = algebraMap R A 0 := Eq.symm (RingHom.map_zero (algebraMap R A))
+  rw [this, spectrum_algebraMap_eq]
+
+lemma CFC.spectrum_one_eq [Nontrivial A] :
+    spectrum R (1 : A) = {1} := by
+  have : (1 : A) = algebraMap R A 1 := Eq.symm (RingHom.map_one (algebraMap R A))
+  rw [this, spectrum_algebraMap_eq]
+
+@[simp]
+lemma cfc_algebraMap (r : R) (f : R → R) : cfc f (algebraMap R A r) = algebraMap R A (f r) := by
+  have h₁ : ContinuousOn f (spectrum R (algebraMap R A r)) :=
+  continuousOn_singleton _ _ |>.mono <| CFC.spectrum_algebraMap_subset r
+  rw [cfc_apply f (algebraMap R A r) (cfc_predicate_algebraMap r),
+    ← AlgHomClass.commutes (cfcHom (p := p) (cfc_predicate_algebraMap r)) (f r)]
+  congr
+  ext ⟨x, hx⟩
+  apply CFC.spectrum_algebraMap_subset r at hx
+  simp_all
+
+@[simp] lemma cfc_apply_zero {f : R → R} : cfc f (0 : A) = algebraMap R A (f 0) := by
+  simpa using cfc_algebraMap (A := A) 0 f
+
+@[simp] lemma cfc_apply_one {f : R → R} : cfc f (1 : A) = algebraMap R A (f 1) := by
+  simpa using cfc_algebraMap (A := A) 1 f
+
 end CFC
 
 end Basic

Mathlib/Topology/ContinuousFunction/NonUnitalFunctionalCalculus.lean

@@ -434,10 +434,23 @@ lemma cfcₙ_comp_star (hf : ContinuousOn f (star '' (σₙ R a)) := by cfc_cont
     cfcₙ (f <| star ·) a = cfcₙ f (star a) := by
   rw [cfcₙ_comp' f star a, cfcₙ_star_id a]
 
-lemma eq_zero_of_quasispectrum_eq_zero (h_spec : σₙ R a ⊆ {0}) (ha : p a := by cfc_tac) :
+lemma CFC.eq_zero_of_quasispectrum_eq_zero (h_spec : σₙ R a ⊆ {0}) (ha : p a := by cfc_tac) :
     a = 0 := by
   simpa [cfcₙ_id R a] using cfcₙ_congr (a := a) (f := id) (g := fun _ : R ↦ 0) fun x ↦ by simp_all
 
+lemma CFC.quasispectrum_zero_eq : σₙ R (0 : A) = {0} := by
+  refine Set.eq_singleton_iff_unique_mem.mpr ⟨quasispectrum.zero_mem R 0, fun x hx ↦ ?_⟩
+  rw [← cfcₙ_zero R (0 : A),
+    cfcₙ_map_quasispectrum _ _ (by cfc_cont_tac) (by cfc_zero_tac) (cfcₙ_predicate_zero R)] at hx
+  simp_all
+
+@[simp] lemma cfcₙ_apply_zero {f : R → R} : cfcₙ f (0 : A) = 0 := by
+  by_cases hf0 : f 0 = 0
+  · nth_rw 2 [← cfcₙ_zero R 0]
+    apply cfcₙ_congr
+    simpa [CFC.quasispectrum_zero_eq]
+  · exact cfcₙ_apply_of_not_map_zero _ hf0
+
 end CFCn
 
 end Main