feat: golf SpectrumRestricts.closedEmbedding_starAlgHom using uniform trickery (#13014)

Author: ADedecker

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

@@ -94,7 +94,8 @@ lemma SpectrumRestricts.isSelfAdjoint (a : A) (ha : SpectrumRestricts a Complex.
 instance IsSelfAdjoint.instContinuousFunctionalCalculus [∀ x : A, CompactSpace (spectrum ℂ x)] :
     ContinuousFunctionalCalculus ℝ (IsSelfAdjoint : A → Prop) :=
   SpectrumRestricts.cfc (q := IsStarNormal) (p := IsSelfAdjoint) Complex.reCLM
-    Complex.isometry_ofReal (fun _ ↦ isSelfAdjoint_iff_isStarNormal_and_spectrumRestricts)
+    Complex.isometry_ofReal.uniformEmbedding
+    (fun _ ↦ isSelfAdjoint_iff_isStarNormal_and_spectrumRestricts)
     (fun _ _ ↦ inferInstance)
 
 lemma unitary_iff_isStarNormal_and_spectrum_subset_circle {u : A} :
@@ -161,7 +162,7 @@ open NNReal in
 instance Nonneg.instContinuousFunctionalCalculus [∀ a : A, CompactSpace (spectrum ℝ a)] :
     ContinuousFunctionalCalculus ℝ≥0 (fun x : A ↦ 0 ≤ x) :=
   SpectrumRestricts.cfc (q := IsSelfAdjoint) ContinuousMap.realToNNReal
-    isometry_subtype_coe (fun _ ↦ nonneg_iff_isSelfAdjoint_and_spectrumRestricts)
+    uniformEmbedding_subtype_val (fun _ ↦ nonneg_iff_isSelfAdjoint_and_spectrumRestricts)
     (fun _ _ ↦ inferInstance)
 
 end Nonneg
@@ -317,14 +318,15 @@ variable {A : Type*} [TopologicalSpace A] [Ring A] [StarRing A] [Algebra ℂ A]
 lemma cfcHom_real_eq_restrict {a : A} (ha : IsSelfAdjoint a) :
     cfcHom ha = ha.spectrumRestricts.starAlgHom (cfcHom ha.isStarNormal) (f := Complex.reCLM) :=
   have := UniqueContinuousFunctionalCalculus.compactSpace_spectrum a (R := ℂ)
-  ha.spectrumRestricts.cfcHom_eq_restrict Complex.isometry_ofReal ha ha.isStarNormal
+  ha.spectrumRestricts.cfcHom_eq_restrict Complex.isometry_ofReal.uniformEmbedding
+    ha ha.isStarNormal
 
 lemma cfc_real_eq_complex {a : A} (f : ℝ → ℝ) (ha : IsSelfAdjoint a := by cfc_tac)  :
     cfc f a = cfc (fun x ↦ f x.re : ℂ → ℂ) a := by
   have := UniqueContinuousFunctionalCalculus.compactSpace_spectrum a (R := ℂ)
   replace ha : IsSelfAdjoint a := ha -- hack to avoid issues caused by autoParam
-  exact ha.spectrumRestricts.cfc_eq_restrict (f := Complex.reCLM) Complex.isometry_ofReal ha
-    ha.isStarNormal f
+  exact ha.spectrumRestricts.cfc_eq_restrict (f := Complex.reCLM)
+    Complex.isometry_ofReal.uniformEmbedding ha ha.isStarNormal f
 
 end RealEqComplex
 
@@ -342,14 +344,14 @@ lemma cfcHom_nnreal_eq_restrict {a : A} (ha : 0 ≤ a) :
     cfcHom ha = (SpectrumRestricts.nnreal_of_nonneg ha).starAlgHom
       (cfcHom (IsSelfAdjoint.of_nonneg ha)) := by
   have := UniqueContinuousFunctionalCalculus.compactSpace_spectrum a (R := ℝ)
-  apply (SpectrumRestricts.nnreal_of_nonneg ha).cfcHom_eq_restrict isometry_subtype_coe
+  apply (SpectrumRestricts.nnreal_of_nonneg ha).cfcHom_eq_restrict uniformEmbedding_subtype_val
 
 lemma cfc_nnreal_eq_real {a : A} (f : ℝ≥0 → ℝ≥0) (ha : 0 ≤ a := by cfc_tac)  :
     cfc f a = cfc (fun x ↦ f x.toNNReal : ℝ → ℝ) a := by
   have := UniqueContinuousFunctionalCalculus.compactSpace_spectrum a (R := ℝ)
   replace ha : 0 ≤ a := ha -- hack to avoid issues caused by autoParam
   apply (SpectrumRestricts.nnreal_of_nonneg ha).cfc_eq_restrict
-    isometry_subtype_coe ha (.of_nonneg ha)
+    uniformEmbedding_subtype_val ha (.of_nonneg ha)
 
 end NNRealEqReal
 

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

@@ -24,8 +24,23 @@ simply by proving:
 2. `0 ≤ x ↔ IsSelfAdjoint x ∧ SpectrumRestricts Real.toNNReal x`.
 -/
 
+open Set
+
 namespace SpectrumRestricts
 
+/-- The homeomorphism `spectrum S a ≃ₜ spectrum R a` induced by `SpectrumRestricts a f`. -/
+def homeomorph {R S A : Type*} [Semifield R] [Semifield S] [Ring A]
+    [Algebra R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [TopologicalSpace R]
+    [TopologicalSpace S] [ContinuousSMul R S] {a : A} {f : C(S, R)} (h : SpectrumRestricts a f) :
+    spectrum S a ≃ₜ spectrum R a where
+  toFun := MapsTo.restrict f _ _ h.subset_preimage
+  invFun := MapsTo.restrict (algebraMap R S) _ _ (image_subset_iff.mp h.algebraMap_image.subset)
+  left_inv x := Subtype.ext <| h.rightInvOn x.2
+  right_inv x := Subtype.ext <| h.left_inv x
+  continuous_toFun := continuous_induced_rng.mpr <| f.continuous.comp continuous_induced_dom
+  continuous_invFun := continuous_induced_rng.mpr <|
+    continuous_algebraMap R S |>.comp continuous_induced_dom
+
 lemma compactSpace {R S A : Type*} [Semifield R] [Semifield S] [Ring A]
     [Algebra R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [TopologicalSpace R]
     [TopologicalSpace S] {a : A} (f : C(S, R)) (h : SpectrumRestricts a f)
@@ -60,23 +75,12 @@ variable [CompleteSpace R]
 
 lemma closedEmbedding_starAlgHom {a : A} {φ : C(spectrum S a, S) →⋆ₐ[S] A}
     (hφ : ClosedEmbedding φ) {f : C(S, R)} (h : SpectrumRestricts a f)
-    (h_isom : Isometry (algebraMap R S)) [h_cpct : CompactSpace (spectrum S a)] :
-    ClosedEmbedding (h.starAlgHom φ) := by
-  apply hφ.comp
-  simp only [RingHom.coe_coe, StarAlgHom.coe_toAlgHom, StarAlgHom.comp_apply,
-    ContinuousMap.compStarAlgHom'_apply, ContinuousMap.compStarAlgHom_apply]
-  have : CompactSpace (spectrum R a) := h.compactSpace
-  apply Isometry.closedEmbedding ?_
-  simp only [isometry_iff_dist_eq]
-  refine fun g₁ g₂ ↦ le_antisymm ?_ ?_
-  all_goals refine (ContinuousMap.dist_le dist_nonneg).mpr fun x ↦ ?_
-  · simpa [h_isom.dist_eq] using ContinuousMap.dist_apply_le_dist _
-  · obtain ⟨y, y_mem, hy⟩ : (x : R) ∈ f '' spectrum S a := h.image.symm ▸ x.2
-    lift y to spectrum S a using y_mem
-    refine le_of_eq_of_le ?_ <| ContinuousMap.dist_apply_le_dist y
-    simp only [ContinuousMap.coe_mk, ContinuousMap.comp_apply, StarAlgHom.ofId_apply]
-    rw [h_isom.dist_eq]
-    congr <;> exact Subtype.ext hy.symm
+    (halg : UniformEmbedding (algebraMap R S)) [CompactSpace (spectrum S a)] :
+    ClosedEmbedding (h.starAlgHom φ) :=
+  have := h.compactSpace
+  hφ.comp <| UniformEmbedding.toClosedEmbedding <| .comp
+    (ContinuousMap.uniformEmbedding_comp _ halg)
+    (UniformEquiv.arrowCongr h.homeomorph.symm (.refl _) |>.uniformEmbedding)
 
 lemma starAlgHom_id {a : A} {φ : C(spectrum S a, S) →⋆ₐ[S] A} {f : C(S, R)}
     (h : SpectrumRestricts a f) (h_id : φ (.restrict (spectrum S a) <| .id S) = a) :
@@ -90,15 +94,16 @@ lemma starAlgHom_id {a : A} {φ : C(spectrum S a, S) →⋆ₐ[S] A} {f : C(S, R
 characterized by: `q a` and the spectrum of `a` restricts to the scalar subring `R` via
 `f : C(S, R)`, then we can get a restricted functional calculus
 `ContinuousFunctionalCalculus R p`. -/
-protected theorem cfc (f : C(S, R)) (h_isom : Isometry (algebraMap R S))
+protected theorem cfc (f : C(S, R)) (halg : UniformEmbedding (algebraMap R S))
     (h : ∀ a, p a ↔ q a ∧ SpectrumRestricts a f) (h_cpct : ∀ a, q a → CompactSpace (spectrum S a)) :
     ContinuousFunctionalCalculus R p where
   exists_cfc_of_predicate a ha := by
     refine ⟨((h a).mp ha).2.starAlgHom (cfcHom ((h a).mp ha).1 (R := S)),
       ?hom_closedEmbedding, ?hom_id, ?hom_map_spectrum, ?predicate_hom⟩
     case hom_closedEmbedding =>
-      exact ((h a).mp ha).2.closedEmbedding_starAlgHom (cfcHom_closedEmbedding ((h a).mp ha).1)
-        h_isom (h_cpct := h_cpct a ((h a).mp ha).1)
+      have := h_cpct a ((h a).mp ha).1
+      exact ((h a).mp ha).2.closedEmbedding_starAlgHom
+        (cfcHom_closedEmbedding ((h a).mp ha).1) halg
     case hom_id => exact ((h a).mp ha).2.starAlgHom_id <| cfcHom_id ((h a).mp ha).1
     case hom_map_spectrum =>
       intro g
@@ -128,27 +133,27 @@ protected theorem cfc (f : C(S, R)) (h_isom : Isometry (algebraMap R S))
 
 variable [ContinuousFunctionalCalculus R p] [UniqueContinuousFunctionalCalculus R A]
 
-lemma cfcHom_eq_restrict (f : C(S, R)) (h_isom : Isometry (algebraMap R S)) {a : A} (hpa : p a)
-    (hqa : q a) (h : SpectrumRestricts a f) [CompactSpace (spectrum S a)] :
+lemma cfcHom_eq_restrict (f : C(S, R)) (halg : UniformEmbedding (algebraMap R S))
+    {a : A} (hpa : p a) (hqa : q a) (h : SpectrumRestricts a f) [CompactSpace (spectrum S a)] :
     cfcHom hpa = h.starAlgHom (cfcHom hqa) := by
   apply cfcHom_eq_of_continuous_of_map_id
-  · exact h.closedEmbedding_starAlgHom (cfcHom_closedEmbedding hqa) h_isom |>.continuous
+  · exact h.closedEmbedding_starAlgHom (cfcHom_closedEmbedding hqa) halg |>.continuous
   · exact h.starAlgHom_id (cfcHom_id hqa)
 
-lemma cfc_eq_restrict (f : C(S, R)) (h_isom : Isometry (algebraMap R S)) {a : A} (hpa : p a)
+lemma cfc_eq_restrict (f : C(S, R)) (halg : UniformEmbedding (algebraMap R S)) {a : A} (hpa : p a)
     (hqa : q a) (h : SpectrumRestricts a f) [CompactSpace (spectrum S a)] (g : R → R) :
     cfc g a = cfc (fun x ↦ algebraMap R S (g (f x))) a := by
   by_cases hg : ContinuousOn g (spectrum R a)
-  · rw [cfc_apply g a, cfcHom_eq_restrict f h_isom hpa hqa h, SpectrumRestricts.starAlgHom_apply,
+  · rw [cfc_apply g a, cfcHom_eq_restrict f halg hpa hqa h, SpectrumRestricts.starAlgHom_apply,
       cfcHom_eq_cfc_extend 0]
     apply cfc_congr fun x hx ↦ ?_
     lift x to spectrum S a using hx
     simp [Function.comp, Subtype.val_injective.extend_apply]
   · have : ¬ ContinuousOn (fun x ↦ algebraMap R S (g (f x)) : S → S) (spectrum S a) := by
       refine fun hg' ↦ hg ?_
-      rw [h_isom.embedding.continuousOn_iff]
-      simpa [h_isom.embedding.continuousOn_iff, Function.comp, h.left_inv _] using
-        hg'.comp h_isom.continuous.continuousOn (fun _ : R ↦ spectrum.algebraMap_mem S)
+      rw [halg.embedding.continuousOn_iff]
+      simpa [halg.embedding.continuousOn_iff, Function.comp, h.left_inv _] using
+        hg'.comp halg.embedding.continuous.continuousOn (fun _ : R ↦ spectrum.algebraMap_mem S)
     rw [cfc_apply_of_not_continuousOn a hg, cfc_apply_of_not_continuousOn a this]
 
 end SpectrumRestricts