feat: add induction principle for elementalStarAlgebra (#12039)

Mathlib/RingTheory/Adjoin/Basic.lean

@@ -127,6 +127,16 @@ theorem adjoin_induction' {p : adjoin R s → Prop} (mem : ∀ (x) (h : x ∈ s)
           Exists.elim hy fun hy' hy => ⟨Subalgebra.mul_mem _ hx' hy', mul _ _ hx hy⟩
 #align algebra.adjoin_induction' Algebra.adjoin_induction'
 
+@[elab_as_elim]
+theorem adjoin_induction'' {x : A} (hx : x ∈ adjoin R s)
+    {p : (x : A) → x ∈ adjoin R s → Prop} (mem : ∀ x (h : x ∈ s), p x (subset_adjoin h))
+    (algebraMap : ∀ (r : R), p (algebraMap R A r) (algebraMap_mem _ r))
+    (add : ∀ x hx y hy, p x hx → p y hy → p (x + y) (add_mem hx hy))
+    (mul : ∀ x hx y hy, p x hx → p y hy → p (x * y) (mul_mem hx hy)) :
+    p x hx := by
+  refine adjoin_induction' mem algebraMap ?_ ?_ ⟨x, hx⟩ (p := fun x : adjoin R s ↦ p x.1 x.2)
+  exacts [fun x y ↦ add x.1 x.2 y.1 y.2, fun x y ↦ mul x.1 x.2 y.1 y.2]
+
 @[simp]
 theorem adjoin_adjoin_coe_preimage {s : Set A} : adjoin R (((↑) : adjoin R s → A) ⁻¹' s) = ⊤ := by
   refine eq_top_iff.2 fun x ↦

Mathlib/Topology/Algebra/StarSubalgebra.lean

@@ -218,7 +218,7 @@ instance {R A} [CommRing R] [StarRing R] [TopologicalSpace A] [Ring A] [Algebra
     CommRing (elementalStarAlgebra R x) :=
   StarSubalgebra.commRingTopologicalClosure _ mul_comm
 
-protected theorem isClosed (x : A) : IsClosed (elementalStarAlgebra R x : Set A) :=
+theorem isClosed (x : A) : IsClosed (elementalStarAlgebra R x : Set A) :=
   isClosed_closure
 #align elemental_star_algebra.is_closed elementalStarAlgebra.isClosed
 
@@ -237,14 +237,38 @@ theorem closedEmbedding_coe (x : A) : ClosedEmbedding ((↑) : elementalStarAlge
   { induced := rfl
     inj := Subtype.coe_injective
     isClosed_range := by
-      convert elementalStarAlgebra.isClosed R x
+      convert isClosed R x
       exact
         Set.ext fun y =>
           ⟨by
             rintro ⟨y, rfl⟩
             exact y.prop, fun hy => ⟨⟨y, hy⟩, rfl⟩⟩ }
 #align elemental_star_algebra.closed_embedding_coe elementalStarAlgebra.closedEmbedding_coe
 
+@[elab_as_elim]
+theorem induction_on {x y : A}
+    (hy : y ∈ elementalStarAlgebra R x) {P : (u : A) → u ∈ elementalStarAlgebra R x → Prop}
+    (self : P x (self_mem R x)) (star_self : P (star x) (star_self_mem R x))
+    (algebraMap : ∀ r, P (algebraMap R A r) (_root_.algebraMap_mem _ r))
+    (add : ∀ u hu v hv, P u hu → P v hv → P (u + v) (add_mem hu hv))
+    (mul : ∀ u hu v hv, P u hu → P v hv → P (u * v) (mul_mem hu hv))
+    (closure : ∀ s : Set A, (hs : s ⊆ elementalStarAlgebra R x) → (∀ u, (hu : u ∈ s) →
+      P u (hs hu)) → ∀ v, (hv : v ∈ closure s) → P v (closure_minimal hs (isClosed R x) hv)) :
+    P y hy := by
+  apply closure (adjoin R {x} : Set A) subset_closure (fun y hy ↦ ?_) y hy
+  rw [SetLike.mem_coe, ← mem_toSubalgebra, adjoin_toSubalgebra] at hy
+  induction hy using Algebra.adjoin_induction'' with
+  | mem u hu =>
+    obtain ((rfl : u = x) | (hu : star u = x)) := by simpa using hu
+    · exact self
+    · simp_rw [← hu, star_star] at star_self
+      exact star_self
+  | algebraMap r => exact algebraMap r
+  | add u hu_mem v hv_mem hu hv =>
+    exact add u (subset_closure hu_mem) v (subset_closure hv_mem) (hu hu_mem) (hv hv_mem)
+  | mul u hu_mem v hv_mem hu hv =>
+    exact mul u (subset_closure hu_mem) v (subset_closure hv_mem) (hu hu_mem) (hv hv_mem)
+
 theorem starAlgHomClass_ext [T2Space B] {F : Type*} {a : A}
     [FunLike F (elementalStarAlgebra R a) B] [AlgHomClass F R _ B] [StarAlgHomClass F R _ B]
     {φ ψ : F} (hφ : Continuous φ)