chore: rename StarSubalgebra.adjoin to StarAlgebra.adjoin (#11339)

This makes it consistent with all the other `adjoin` in the library

Author: ADedecker

Mathlib/Algebra/Algebra/Subalgebra/Unitization.lean

@@ -328,9 +328,9 @@ theorem starLift_range_le
     | _ r a => simpa using add_mem (algebraMap_mem S r) (h ⟨a, rfl⟩)
 
 theorem starLift_range (f : A →⋆ₙₐ[R] C) :
-    (starLift f).range = StarSubalgebra.adjoin R (NonUnitalStarAlgHom.range f : Set C) :=
+    (starLift f).range = StarAlgebra.adjoin R (NonUnitalStarAlgHom.range f : Set C) :=
   eq_of_forall_ge_iff fun c ↦ by
-    rw [starLift_range_le, StarSubalgebra.adjoin_le_iff]
+    rw [starLift_range_le, StarAlgebra.adjoin_le_iff]
     rfl
 
 end Unitization
@@ -351,7 +351,7 @@ def unitization : Unitization R s →⋆ₐ[R] A :=
 theorem unitization_apply (x : Unitization R s) : unitization s x = algebraMap R A x.fst + x.snd :=
   rfl
 
-theorem unitization_range : (unitization s).range = StarSubalgebra.adjoin R s := by
+theorem unitization_range : (unitization s).range = StarAlgebra.adjoin R s := by
   rw [unitization, Unitization.starLift_range]
   simp only [NonUnitalStarAlgHom.coe_range, NonUnitalStarSubalgebraClass.coeSubtype,
     Subtype.range_coe_subtype]
@@ -372,8 +372,8 @@ theorem unitization_injective (h1 : (1 : A) ∉ s) : Function.Injective (unitiza
 isomorphic to its `StarSubalgebra.adjoin`. -/
 @[simps! apply_coe]
 noncomputable def unitizationStarAlgEquiv (h1 : (1 : A) ∉ s) :
-    Unitization R s ≃⋆ₐ[R] StarSubalgebra.adjoin R (s : Set A) :=
-  let starAlgHom : Unitization R s →⋆ₐ[R] StarSubalgebra.adjoin R (s : Set A) :=
+    Unitization R s ≃⋆ₐ[R] StarAlgebra.adjoin R (s : Set A) :=
+  let starAlgHom : Unitization R s →⋆ₐ[R] StarAlgebra.adjoin R (s : Set A) :=
     ((unitization s).codRestrict _
       fun x ↦ (unitization_range s).le <| Set.mem_range_self x)
   StarAlgEquiv.ofBijective starAlgHom <| by

Mathlib/Algebra/Star/Subalgebra.lean

@@ -410,7 +410,9 @@ end Subalgebra
 /-! ### The star subalgebra generated by a set -/
 
 
-namespace StarSubalgebra
+namespace StarAlgebra
+
+open StarSubalgebra
 
 variable {F R A B : Type*} [CommSemiring R] [StarRing R]
 variable [Semiring A] [Algebra R A] [StarRing A] [StarModule R A]
@@ -424,35 +426,35 @@ def adjoin (s : Set A) : StarSubalgebra R A :=
     star_mem' := fun hx => by
       rwa [Subalgebra.mem_carrier, ← Subalgebra.mem_star_iff, Subalgebra.star_adjoin_comm,
         Set.union_star, star_star, Set.union_comm] }
-#align star_subalgebra.adjoin StarSubalgebra.adjoin
+#align star_subalgebra.adjoin StarAlgebra.adjoin
 
 theorem adjoin_eq_starClosure_adjoin (s : Set A) : adjoin R s = (Algebra.adjoin R s).starClosure :=
   toSubalgebra_injective <|
     show Algebra.adjoin R (s ∪ star s) = Algebra.adjoin R s ⊔ star (Algebra.adjoin R s) from
       (Subalgebra.star_adjoin_comm R s).symm ▸ Algebra.adjoin_union s (star s)
-#align star_subalgebra.adjoin_eq_star_closure_adjoin StarSubalgebra.adjoin_eq_starClosure_adjoin
+#align star_subalgebra.adjoin_eq_star_closure_adjoin StarAlgebra.adjoin_eq_starClosure_adjoin
 
 theorem adjoin_toSubalgebra (s : Set A) :
     (adjoin R s).toSubalgebra = Algebra.adjoin R (s ∪ star s) :=
   rfl
-#align star_subalgebra.adjoin_to_subalgebra StarSubalgebra.adjoin_toSubalgebra
+#align star_subalgebra.adjoin_to_subalgebra StarAlgebra.adjoin_toSubalgebra
 
 @[aesop safe 20 apply (rule_sets := [SetLike])]
 theorem subset_adjoin (s : Set A) : s ⊆ adjoin R s :=
   (Set.subset_union_left s (star s)).trans Algebra.subset_adjoin
-#align star_subalgebra.subset_adjoin StarSubalgebra.subset_adjoin
+#align star_subalgebra.subset_adjoin StarAlgebra.subset_adjoin
 
 theorem star_subset_adjoin (s : Set A) : star s ⊆ adjoin R s :=
   (Set.subset_union_right s (star s)).trans Algebra.subset_adjoin
-#align star_subalgebra.star_subset_adjoin StarSubalgebra.star_subset_adjoin
+#align star_subalgebra.star_subset_adjoin StarAlgebra.star_subset_adjoin
 
 theorem self_mem_adjoin_singleton (x : A) : x ∈ adjoin R ({x} : Set A) :=
   Algebra.subset_adjoin <| Set.mem_union_left _ (Set.mem_singleton x)
-#align star_subalgebra.self_mem_adjoin_singleton StarSubalgebra.self_mem_adjoin_singleton
+#align star_subalgebra.self_mem_adjoin_singleton StarAlgebra.self_mem_adjoin_singleton
 
 theorem star_self_mem_adjoin_singleton (x : A) : star x ∈ adjoin R ({x} : Set A) :=
   star_mem <| self_mem_adjoin_singleton R x
-#align star_subalgebra.star_self_mem_adjoin_singleton StarSubalgebra.star_self_mem_adjoin_singleton
+#align star_subalgebra.star_self_mem_adjoin_singleton StarAlgebra.star_self_mem_adjoin_singleton
 
 variable {R}
 
@@ -462,23 +464,23 @@ protected theorem gc : GaloisConnection (adjoin R : Set A → StarSubalgebra R A
   exact
     ⟨fun h => (Set.subset_union_left s _).trans h, fun h =>
       Set.union_subset h fun x hx => star_star x ▸ star_mem (show star x ∈ S from h hx)⟩
-#align star_subalgebra.gc StarSubalgebra.gc
+#align star_subalgebra.gc StarAlgebra.gc
 
 /-- Galois insertion between `adjoin` and `coe`. -/
 protected def gi : GaloisInsertion (adjoin R : Set A → StarSubalgebra R A) (↑) where
-  choice s hs := (adjoin R s).copy s <| le_antisymm (StarSubalgebra.gc.le_u_l s) hs
-  gc := StarSubalgebra.gc
-  le_l_u S := (StarSubalgebra.gc (S : Set A) (adjoin R S)).1 <| le_rfl
+  choice s hs := (adjoin R s).copy s <| le_antisymm (StarAlgebra.gc.le_u_l s) hs
+  gc := StarAlgebra.gc
+  le_l_u S := (StarAlgebra.gc (S : Set A) (adjoin R S)).1 <| le_rfl
   choice_eq _ _ := StarSubalgebra.copy_eq _ _ _
-#align star_subalgebra.gi StarSubalgebra.gi
+#align star_subalgebra.gi StarAlgebra.gi
 
 theorem adjoin_le {S : StarSubalgebra R A} {s : Set A} (hs : s ⊆ S) : adjoin R s ≤ S :=
-  StarSubalgebra.gc.l_le hs
-#align star_subalgebra.adjoin_le StarSubalgebra.adjoin_le
+  StarAlgebra.gc.l_le hs
+#align star_subalgebra.adjoin_le StarAlgebra.adjoin_le
 
 theorem adjoin_le_iff {S : StarSubalgebra R A} {s : Set A} : adjoin R s ≤ S ↔ s ⊆ S :=
-  StarSubalgebra.gc _ _
-#align star_subalgebra.adjoin_le_iff StarSubalgebra.adjoin_le_iff
+  StarAlgebra.gc _ _
+#align star_subalgebra.adjoin_le_iff StarAlgebra.adjoin_le_iff
 
 theorem _root_.Subalgebra.starClosure_eq_adjoin (S : Subalgebra R A) :
     S.starClosure = adjoin R (S : Set A) :=
@@ -496,7 +498,7 @@ theorem adjoin_induction {s : Set A} {p : A → Prop} {a : A} (h : a ∈ adjoin
   Algebra.adjoin_induction h
     (fun x hx => hx.elim (fun hx => mem x hx) fun hx => star_star x ▸ star _ (mem _ hx))
     algebraMap add mul
-#align star_subalgebra.adjoin_induction StarSubalgebra.adjoin_induction
+#align star_subalgebra.adjoin_induction StarAlgebra.adjoin_induction
 
 @[elab_as_elim]
 theorem adjoin_induction₂ {s : Set A} {p : A → A → Prop} {a b : A} (ha : a ∈ adjoin R s)
@@ -524,7 +526,7 @@ theorem adjoin_induction₂ {s : Set A} {p : A → A → Prop} {a b : A} (ha : a
   · cases' hx with hx hx
     · exact Halg_right _ _ hx
     · exact star_star x ▸ Hstar_left _ _ (Halg_right r _ hx)
-#align star_subalgebra.adjoin_induction₂ StarSubalgebra.adjoin_induction₂
+#align star_subalgebra.adjoin_induction₂ StarAlgebra.adjoin_induction₂
 
 /-- The difference with `StarSubalgebra.adjoin_induction` is that this acts on the subtype. -/
 @[elab_as_elim]
@@ -541,7 +543,7 @@ theorem adjoin_induction' {s : Set A} {p : adjoin R s → Prop} (a : adjoin R s)
       fun x y hx hy =>
       Exists.elim hx fun hx' hx => Exists.elim hy fun hy' hy => ⟨mul_mem hx' hy', mul _ _ hx hy⟩,
       fun x hx => Exists.elim hx fun hx' hx => ⟨star_mem hx', star _ hx⟩]
-#align star_subalgebra.adjoin_induction' StarSubalgebra.adjoin_induction'
+#align star_subalgebra.adjoin_induction' StarAlgebra.adjoin_induction'
 
 variable (R)
 
@@ -567,7 +569,7 @@ def adjoinCommSemiringOfComm {s : Set A} (hcomm : ∀ a : A, a ∈ s → ∀ b :
             · exact star_star a ▸ (hcomm_star _ hb _ ha).symm
             · simpa only [star_mul, star_star] using congr_arg star (hcomm _ hb _ ha))
       exact congr_arg Subtype.val (mul_comm (⟨x, hx⟩ : Algebra.adjoin R (s ∪ star s)) ⟨y, hy⟩) }
-#align star_subalgebra.adjoin_comm_semiring_of_comm StarSubalgebra.adjoinCommSemiringOfComm
+#align star_subalgebra.adjoin_comm_semiring_of_comm StarAlgebra.adjoinCommSemiringOfComm
 
 /-- If all elements of `s : Set A` commute pairwise and also commute pairwise with elements of
 `star s`, then `StarSubalgebra.adjoin R s` is commutative. See note [reducible non-instances]. -/
@@ -577,9 +579,9 @@ def adjoinCommRingOfComm (R : Type u) {A : Type v} [CommRing R] [StarRing R] [Ri
     (hcomm : ∀ a : A, a ∈ s → ∀ b : A, b ∈ s → a * b = b * a)
     (hcomm_star : ∀ a : A, a ∈ s → ∀ b : A, b ∈ s → a * star b = star b * a) :
     CommRing (adjoin R s) :=
-  { StarSubalgebra.adjoinCommSemiringOfComm R hcomm hcomm_star,
+  { StarAlgebra.adjoinCommSemiringOfComm R hcomm hcomm_star,
     (adjoin R s).toSubalgebra.toRing with }
-#align star_subalgebra.adjoin_comm_ring_of_comm StarSubalgebra.adjoinCommRingOfComm
+#align star_subalgebra.adjoin_comm_ring_of_comm StarAlgebra.adjoinCommRingOfComm
 
 /-- The star subalgebra `StarSubalgebra.adjoin R {x}` generated by a single `x : A` is commutative
 if `x` is normal. -/
@@ -592,23 +594,30 @@ instance adjoinCommSemiringOfIsStarNormal (x : A) [IsStarNormal x] :
     fun a ha b hb => by
     rw [Set.mem_singleton_iff] at ha hb
     simpa only [ha, hb] using (star_comm_self' x).symm
-#align star_subalgebra.adjoin_comm_semiring_of_is_star_normal StarSubalgebra.adjoinCommSemiringOfIsStarNormal
+#align star_subalgebra.adjoin_comm_semiring_of_is_star_normal StarAlgebra.adjoinCommSemiringOfIsStarNormal
 
 /-- The star subalgebra `StarSubalgebra.adjoin R {x}` generated by a single `x : A` is commutative
 if `x` is normal. -/
 instance adjoinCommRingOfIsStarNormal (R : Type u) {A : Type v} [CommRing R] [StarRing R] [Ring A]
     [Algebra R A] [StarRing A] [StarModule R A] (x : A) [IsStarNormal x] :
     CommRing (adjoin R ({x} : Set A)) :=
   { (adjoin R ({x} : Set A)).toSubalgebra.toRing with mul_comm := mul_comm }
-#align star_subalgebra.adjoin_comm_ring_of_is_star_normal StarSubalgebra.adjoinCommRingOfIsStarNormal
+#align star_subalgebra.adjoin_comm_ring_of_is_star_normal StarAlgebra.adjoinCommRingOfIsStarNormal
 
 /-! ### Complete lattice structure -/
 
+end StarAlgebra
 
-variable {R} -- Porting note: redundant binder annotation update
+namespace StarSubalgebra
+
+variable {F R A B : Type*} [CommSemiring R] [StarRing R]
+
+variable [Semiring A] [Algebra R A] [StarRing A] [StarModule R A]
+
+variable [Semiring B] [Algebra R B] [StarRing B] [StarModule R B]
 
 instance completeLattice : CompleteLattice (StarSubalgebra R A) where
-  __ := GaloisInsertion.liftCompleteLattice StarSubalgebra.gi
+  __ := GaloisInsertion.liftCompleteLattice StarAlgebra.gi
   bot := { toSubalgebra := ⊥, star_mem' := fun ⟨r, hr⟩ => ⟨star r, hr ▸ algebraMap_star_comm _⟩ }
   bot_le S := (bot_le : ⊥ ≤ S.toSubalgebra)
 
@@ -718,7 +727,7 @@ end StarSubalgebra
 
 namespace StarAlgHom
 
-open StarSubalgebra
+open StarSubalgebra StarAlgebra
 
 variable {F R A B : Type*} [CommSemiring R] [StarRing R]
 variable [Semiring A] [Algebra R A] [StarRing A] [StarModule R A]
@@ -747,8 +756,8 @@ theorem ext_of_adjoin_eq_top {s : Set A} (h : adjoin R s = ⊤) ⦃f g : F⦄ (h
 
 theorem map_adjoin (f : A →⋆ₐ[R] B) (s : Set A) :
     map f (adjoin R s) = adjoin R (f '' s) :=
-  GaloisConnection.l_comm_of_u_comm Set.image_preimage (gc_map_comap f) StarSubalgebra.gc
-    StarSubalgebra.gc fun _ => rfl
+  GaloisConnection.l_comm_of_u_comm Set.image_preimage (gc_map_comap f) StarAlgebra.gc
+    StarAlgebra.gc fun _ => rfl
 #align star_alg_hom.map_adjoin StarAlgHom.map_adjoin
 
 theorem ext_adjoin {s : Set A} [FunLike F (adjoin R s) B]

Mathlib/Topology/Algebra/StarSubalgebra.lean

@@ -185,7 +185,7 @@ end StarSubalgebra
 
 section Elemental
 
-open StarSubalgebra
+open StarSubalgebra StarAlgebra
 
 variable (R : Type*) {A B : Type*} [CommSemiring R] [StarRing R]
 variable [TopologicalSpace A] [Semiring A] [StarRing A] [TopologicalSemiring A]

Mathlib/Topology/ContinuousFunction/Polynomial.lean

@@ -227,7 +227,7 @@ theorem polynomialFunctions.le_equalizer {A : Type*} [Semiring A] [Algebra R A]
   rw [polynomialFunctions.eq_adjoin_X s]
   exact φ.adjoin_le_equalizer ψ fun x hx => (Set.mem_singleton_iff.1 hx).symm ▸ h
 
-open StarSubalgebra
+open StarAlgebra
 
 theorem polynomialFunctions.starClosure_eq_adjoin_X [StarRing R] [ContinuousStar R] (s : Set R) :
     (polynomialFunctions s).starClosure = adjoin R {toContinuousMapOnAlgHom s X} := by

test/set_like.lean

@@ -29,7 +29,7 @@ example [Ring R] (S : Set R) (hx : x ∈ S) (hy : y ∈ S) (hz : z ∈ S) (n m :
 
 example [CommRing R] [Ring A] [Algebra R A] [StarRing R] [StarRing A] [StarModule R A]
     (r : R) (a b c : A) (n : ℕ) :
-    -b + star (algebraMap R A r) + a ^ n * c ∈ StarSubalgebra.adjoin R {a, b, c} := by
+    -b + star (algebraMap R A r) + a ^ n * c ∈ StarAlgebra.adjoin R {a, b, c} := by
   aesop
 
 example [Monoid M] (x : M) (n : ℕ) : x ^ n ∈ Submonoid.closure {x} := by