Commit 2025-09-11 14:47 cafcdcb2

feat: {NonUnital}{Star}Subalgebra.map_topologicalClosure (#29535) This adds the following 5 results for each of variant of {NonUnital}{Star}Subalgebra

lemma map_topologicalClosure_le (hφ : Continuous φ) :
    map φ s.topologicalClosure ≤ (map φ s).topologicalClosure :=
  image_closure_subset_closure_image hφ
lemma topologicalClosure_map_le (hφ : IsClosedMap φ) :
    (map φ s).topologicalClosure ≤ map φ s.topologicalClosure :=
  hφ.closure_image_subset _
lemma topologicalClosure_map (hφ : IsClosedMap φ) (hφ' : Continuous φ) :
    (map φ s).topologicalClosure = map φ s.topologicalClosure :=
  SetLike.coe_injective <| hφ.closure_image_eq_of_continuous hφ' _
lemma topologicalClosure_adjoin_le_centralizer_centralizer (s : Set A) :
    (adjoin R s).topologicalClosure ≤ centralizer R (centralizer R s) :=
  topologicalClosure_minimal (adjoin_le_centralizer_centralizer R s) (Set.isClosed_centralizer _)
lemma elemental.le_centralizer_centralizer (x : A) :
    elemental R x ≤ centralizer R (centralizer R {x}) :=
  topologicalClosure_adjoin_le_centralizer_centralizer R {x}

In the case of Subalgebra, we repurpose the existing Subalgebra.topologicalClosure_map, as this was the wrong name for the lemma anyway. Moreover, for those results we use the bundled ContinuousAlgHom for continuity. There's also some minor clean up of the explicitness of some variables in topologicalClosure_minimal.