clean proof of Stone-Weierstrass analogue

Stream: maths

[Jireh Loreaux]

We have the Stone-Weierstrass theorem for compact spaces in docs#polynomialFunctions.topologicalClosure (the real case) and docs#polynomialFunctions.starClosure_topologicalClosure (the IsROrC case). At this point, we don't have the version for locally compact spaces.

I need a similar statement, which is that for s : Set 𝕜 with s compact and containing 0 : 𝕜, then the topological closure of the non-unital star subalgebra generated by the polynomial X : 𝕜[X] (viewed a continuous map in C(s, 𝕜)) is dense in the subtype C(s, R)₀ := { f : C(s, R) // f 0 = 0 } (technically it's f ⟨0, (h : 0 ∈ s)⟩ = 0, but let's not muddy the waters). You may assume that I have all the relevant structure on this subtype (it's a non-unital commutative star ring, an ideal, etc.), I'm just trying to keep things simple.

What's the best way to prove this? As I see it, there are a few options:

1. Prove the Stone-Weierstrass theorem for locally compact spaces, identify C(s, 𝕜)₀ with C₀(s \ {0}, 𝕜) and go from there.
2. Consider the map C(s, 𝕜) → C(s, 𝕜)₀given by f ↦ f - (f 0)which just subtracts off a constant function. This map is continuous and linear. Show that any element of the star-closure of the polynomial functions maps into the non-unital star subalgebra generated by X : 𝕜[X]. This is messy because we don't have a nice induction principle to apply (if it were just polynomials it wouldn't be so bad), and also because this map is only linear. Then use continuity and the existing Stone-Weierstrass theorem to conclude the result.

Am I missing some easier way? If not, which of the above do you think is a better approach?

[Anatole Dedecker]

I don’t see why 2 would be messy after turning the closure result into filter stuff

[Jireh Loreaux]

The closure bit is the easy part. (I've just edited to swap the last two sentences of (2) so that it's clearer.)

[Anatole Dedecker]

I can’t believe that is the issue…

[Jireh Loreaux]

I know. It feels incredibly stupid, which is why I'm asking here. :laughing: If you can do it easily I would be grateful!

[Anatole Dedecker]

Let me try

[Filippo A. E. Nuccio]

Ping @Yoh Tanimoto , who was interested in all this.

[Jireh Loreaux]

Anatole and I have been discussing this privately. I think I see a path to make it work without too much hassle.

[Filippo A. E. Nuccio]

Oh, I see.

[Jireh Loreaux]

That shouldn't preclude anyone from thinking about it if they want to though.

[Filippo A. E. Nuccio]

I had been thinking about this a while ago and came up with your strategy but did no even try to write something, postponing for better times.

[Filippo A. E. Nuccio]

But nice that you came up with a solution!

[Anatole Dedecker]

Sorry maybe we should have had some of our discussion in this stream. Basically the topological part is very easy and then I spent half of my day struggling with algebra :sweat_smile:

You can have a look at what I did here. Unless I'm missing something obvious, my first lemma contains absolutely all the mathematical content for the general case. The hard part then is showing that the intersection between the kernel of evaluation at zero and the unital star-subalgebra generated by $z$ is exactly the non-unital star subalgebra generated by $z$. I think most of the troubles come from API holes and this approach could be reasonable in theory, but Jireh wants to explore another direction as well.

[Jireh Loreaux]

Also my fault for taking the discussion private. I think, unless I'm missing something, that we can use Anatole's first lemma, along with the following approach. We let S := NonUnitalStarSubalgebra.adjoin 𝕜 {(ContinuousMap.id 𝕜).restrict s} : NonUnitalStarSubalgebra C(s, 𝕜). Then we'll take the T := StarSubalgebra.adjoin 𝕜 S, which, after not much work given the API we already have, should be provably equal to span {1, S}. Now, it is clear that S separates points (because (ContinousMap.id 𝕜).restrict s itself does), and therefore so does T, so Stone-Weierstrass applies to T, and then we apply Anatole's lemma taking φ to be the evaluation map (at zero).

[Anatole Dedecker]

I think that should work and avoid a lot of the troubles so it sounds great. I think some of the holes I uncovered deserve to be filled though so I'll try to make my approach look kind of good.

[Anatole Dedecker]

Question for any lurking algebraist : do you expect these lemmas to be useful ? How would you have stated them ? The two use case in mind are S = {Polynomial.X} in Polynomial K and S = range MvPolynomial.X in MvPolynomial σ K.

open MvPolynomial in
theorem bar_key [CommRing K] [CommRing A] [Algebra K A] {s : Set A} {a b : A}
    (ha : a ∈ Algebra.adjoin K s) (hb : b ∈ NonUnitalAlgebra.adjoin K s) :
    a * b ∈ NonUnitalAlgebra.adjoin K s := by
  obtain ⟨P, rfl⟩ : ∃ P : MvPolynomial s K, aeval ((↑) : s → A) P = a := by
    rwa [Algebra.adjoin_eq_range, AlgHom.mem_range] at ha
  refine P.induction_on (M := fun Q ↦ aeval ((↑) : s → A) Q * b ∈ _)
    (fun x ↦ ?_) (fun Q R hQ hR ↦ ?_) (fun Q x hQ ↦ ?_)
  · simpa only [aeval_C, algebraMap_smul, ← smul_eq_mul] using SMulMemClass.smul_mem x hb
  · simpa only [add_mul, map_add] using add_mem hQ hR
  · simpa only [map_mul, aeval_X, mul_comm _ (x : A), mul_assoc]
      using mul_mem (NonUnitalAlgebra.subset_adjoin K x.2) hQ

open MvPolynomial in
theorem bar [CommRing K] [CommRing A] [Algebra K A] {s : Set A}
    (H : Algebra.adjoin K s = ⊤) :
    (Ideal.span s : Set A) = NonUnitalAlgebra.adjoin K s := by
  refine subset_antisymm (fun a ha ↦ ?_) (fun a ha ↦ ?_)
  · exact Submodule.span_induction ha (NonUnitalAlgebra.subset_adjoin K) (zero_mem _)
      (fun _ _ ↦ add_mem) (fun b c hc ↦ bar_key (H.symm ▸ trivial) hc)
  · exact NonUnitalAlgebra.adjoin_induction (p := (· ∈ Ideal.span s)) ha
      Ideal.subset_span (fun _ _ ↦ add_mem) (zero_mem _)
      (fun _ _ hx _ ↦ Ideal.mul_mem_right _ _ hx) (fun r Q hQ ↦ Submodule.smul_of_tower_mem _ r hQ)

[Antoine Chambert-Loir]

Anatole Dedecker said:

Question for any lurking algebraist : do you expect these lemmas to be useful ? How would you have stated them ? The two use case in mind are S = {Polynomial.X} in Polynomial K and S = range MvPolynomial.X in MvPolynomial σ K.

I don't understand what the second one means, but the first one seems to say that NonUnitalAlgebra.adjoin K s is a module over Algebra.adjoin K s.
(By the way, both result seems to generalize to CommSemiring K and Semiring A.)

[Junyan Xu]

If you prove the analogue of docs#Algebra.adjoin_eq_span for NonUnitalAlgebra (with Submonoid replaced by Subsemigroup) and that Submonoid.closure s = {1} ∪ Subsemigroup.closure S, it should then easily follow that Subalgebra.toSubmodule (Algebra.adjoin K s) = Submodule.span K ({1} ∪ NonUnitalAlgebra.adjoin K s), even for not necessarily commutative A. It seems we are missing (Algebra.adjoin K s).toNonUnitalSubalgebra = NonUnitalAlgebra.adjoin K ({1} ∪ s) too.

In the proof of bar_key, using MvPolynomial doesn't allow noncommutative A. You might try to use docs#Algebra.adjoin_eq_range_freeAlgebra_lift, but I think using docs#Algebra.adjoin_induction is easier than both. Regarding bar, using docs#Submodule.span_smul_of_span_eq_top and the adjoin_eq_span theorems you can reduce it to the statement that (Submonoid.closure s) • s = Subsemigroup.closure s.

[Anatole Dedecker]

Antoine Chambert-Loir said:

I don't understand what the second one means, but the first one seems to say that NonUnitalAlgebra.adjoin K s is a module over Algebra.adjoin K s.
(By the way, both result seems to generalize to CommSemiring K and Semiring A.)

I just needed that the non-unital subalgebra generated by all variables in a polynomial ring is actually an ideal, the goal being to prove that this subalgebra is precisely the kernel of evaluation at zero. I originally did a version just for polynomials but ended up writing it more generally (I didn't claim it was full generality!)

[Anatole Dedecker]

Junyan Xu said:

If you prove the analogue of docs#Algebra.adjoin_eq_span for NonUnitalAlgebra (with Submonoid replaced by Subsemigroup) and that Submonoid.closure s = {1} ∪ Subsemigroup.closure S, it should then easily follow that Subalgebra.toSubmodule (Algebra.adjoin K s) = Submodule.span K ({1} ∪ NonUnitalAlgebra.adjoin K s), even for not necessarily commutative A. It seems we are missing (Algebra.adjoin K s).toNonUnitalSubalgebra = NonUnitalAlgebra.adjoin K ({1} ∪ s) too.

Aha, this sounds like the right way to do it indeed. Thanks!

[Anatole Dedecker]

In the proof of bar_key, using MvPolynomial doesn't allow noncommutative A. You might try to use docs#Algebra.adjoin_eq_range_freeAlgebra_lift, but I think using docs#Algebra.adjoin_induction is easier than both.

I think I had trouble doing the induction like that, let me check why.

Regarding bar, using docs#Submodule.span_smul_of_span_eq_top and the adjoin_eq_span theorems you can reduce it to the statement that (Submonoid.closure s) • s = Subsemigroup.closure s.

Nice, thanks!

[Anatole Dedecker]

The problem with adjoin_induction is I end up with this subgoal:

∀ (x y : A), x * b ∈ NonUnitalAlgebra.adjoin K s → y * b ∈ NonUnitalAlgebra.adjoin K s → (x * y) * b ∈ NonUnitalAlgebra.adjoin K s

Which doesn't seem provable. I haven't thought more about the deep reasons for this, I also expected the two inductions to be equivalent.

[Jireh Loreaux]

I think you must have miscopied that sub goal because it's just simpa [add_mul] using add_mem

[Anatole Dedecker]

Fixed, thanks!

[Anatole Dedecker]

I guess the more natural way to do it is non-unital adjoin_eq_span + docs#Submodule.span_induction + docs#Subsemigroup.closure_induction

[Jireh Loreaux]

I have the adjoin_eq_span and Submonoid.closure s = {1} ∪ Subsemigroup.closure s results locally now, so don't duplicate effort.

[Yoh Tanimoto]

Jireh Loreaux said:

We have the Stone-Weierstrass theorem for compact spaces in docs#polynomialFunctions.topologicalClosure (the real case) and docs#polynomialFunctions.starClosure_topologicalClosure (the IsROrC case). At this point, we don't have the version for locally compact spaces.

I need a similar statement, which is that for s : Set 𝕜 with s compact and containing 0 : 𝕜, then the topological closure of the non-unital star subalgebra generated by the polynomial X : 𝕜[X] (viewed a continuous map in C(s, 𝕜)) is dense in the subtype C(s, R)₀ := { f : C(s, R) // f 0 = 0 } (technically it's f ⟨0, (h : 0 ∈ s)⟩ = 0, but let's not muddy the waters). You may assume that I have all the relevant structure on this subtype (it's a non-unital commutative star ring, an ideal, etc.), I'm just trying to keep things simple.

What's the best way to prove this? As I see it, there are a few options:

1. Prove the Stone-Weierstrass theorem for locally compact spaces, identify C(s, 𝕜)₀ with C₀(s \ {0}, 𝕜) and go from there.
2. Consider the map C(s, 𝕜) → C(s, 𝕜)₀given by f ↦ f - (f 0)which just subtracts off a constant function. This map is continuous and linear. Show that any element of the star-closure of the polynomial functions maps into the non-unital star subalgebra generated by X : 𝕜[X]. This is messy because we don't have a nice induction principle to apply (if it were just polynomials it wouldn't be so bad), and also because this map is only linear. Then use continuity and the existing Stone-Weierstrass theorem to conclude the result.

Am I missing some easier way? If not, which of the above do you think is a better approach?

I think 1. is more natural, as it goes along the more general unitization of a non-unital algebra.

[Jireh Loreaux]

@Yoh Tanimoto see this message where I lay out the current plan.

[Jireh Loreaux]

@Anatole Dedecker I don't have time to PR this right now, but you (or anyone else) is welcome to.

import Mathlib

namespace NonUnitalAlgebra

variable {R A : Type*} [CommSemiring R] [NonUnitalSemiring A] [Module R A]
  [IsScalarTower R A A] [SMulCommClass R A A]

-- This is the version we should actually have as `NonUnitalAlgebra.adjoin_induction'`, but
-- currently that is used for the subtype.
/-- A dependent version of `NonUnitalAlgebra.adjoin_induction`. -/
theorem adjoin_induction'' {s : Set A} {p : ∀ x, x ∈ adjoin R s → Prop}
    (Hs : ∀ (x) (h : x ∈ s), p x (subset_adjoin R h))
    (Hadd : ∀ x hx y hy, p x hx → p y hy → p (x + y) (add_mem ‹_› ‹_›))
    (H0 : p 0 (zero_mem _))
    (Hmul : ∀ x hx y hy, p x hx → p y hy → p (x * y) (mul_mem ‹_› ‹_›))
    (Hsmul : ∀ (r : R) (x hx), p x hx → p (r • x) (SMulMemClass.smul_mem _ ‹_›))
    {a} (ha : a ∈ adjoin R s) : p a ha :=
  adjoin_induction' ⟨a, ha⟩ (p := fun x ↦ p x.1 x.2) Hs (fun x y ↦ Hadd x.1 x.2 y.1 y.2)
    H0 (fun x y ↦ Hmul x.1 x.2 y.1 y.2) (fun r x ↦ Hsmul r x.1 x.2)

open Submodule

lemma adjoin_eq_span (s : Set A) : (adjoin R s).toSubmodule = span R (Subsemigroup.closure s) := by
  apply le_antisymm
  · intro x hx
    induction hx using adjoin_induction'' with
    | Hs x hx => exact subset_span <| Subsemigroup.subset_closure hx
    | Hadd x _ y _ hpx hpy => exact add_mem hpx hpy
    | H0 => exact zero_mem _
    | Hmul x _ y _ hpx hpy =>
      apply span_induction₂ hpx hpy ?Hs (by simp) (by simp) ?Hadd_l ?Hadd_r ?Hsmul_l ?Hsmul_r
      case Hs => exact fun x hx y hy ↦ subset_span <| mul_mem hx hy
      case Hadd_l => exact fun x y z hxz hyz ↦ by simpa [add_mul] using add_mem hxz hyz
      case Hadd_r => exact fun x y z hxz hyz ↦ by simpa [mul_add] using add_mem hxz hyz
      case Hsmul_l => exact fun r x y hxy ↦ by simpa [smul_mul_assoc] using smul_mem _ _ hxy
      case Hsmul_r => exact fun r x y hxy ↦ by simpa [mul_smul_comm] using smul_mem _ _ hxy
    | Hsmul r x _ hpx => exact smul_mem _ _ hpx
  · apply span_le.2 _
    show Subsemigroup.closure s ≤ (adjoin R s).toNonUnitalSubsemiring.toSubsemigroup
    exact Subsemigroup.closure_le.2 (subset_adjoin R)

end NonUnitalAlgebra

namespace NonUnitalStarAlgebra

variable {R A : Type*} [CommSemiring R] [NonUnitalSemiring A] [Module R A]
  [IsScalarTower R A A] [SMulCommClass R A A] [StarRing R] [StarRing A] [StarModule R A]

open scoped Pointwise
open Submodule

lemma adjoin_eq_span (s : Set A) :
    (adjoin R s).toSubmodule = span R (Subsemigroup.closure (s ∪ star s)) := by
  rw [adjoin_toNonUnitalSubalgebra, NonUnitalAlgebra.adjoin_eq_span]

end NonUnitalStarAlgebra

namespace Submonoid

variable {M : Type*} [Monoid M]

/-- The `Submonoid.closure` of a set is `1` union the its `Subsemigroup.closure`. -/
lemma closure_eq_one_union (s : Set M) :
    closure s = {(1 : M)} ∪ (Subsemigroup.closure s : Set M) := by
  apply le_antisymm
  · intro x hx
    induction hx using closure_induction' with
    | Hs x hx => exact Or.inr <| Subsemigroup.subset_closure hx
    | H1 => exact Or.inl <| by simp
    | Hmul x hx y hy hx hy =>
      simp only [Set.singleton_union, Set.mem_insert_iff, SetLike.mem_coe] at hx hy
      obtain ⟨(rfl | hx), (rfl | hy)⟩ := And.intro hx hy
      all_goals simp_all
      exact Or.inr <| mul_mem hx hy
  · rintro x (hx | hx)
    · exact (show x = 1 by simpa using hx) ▸ one_mem (closure s)
    · induction hx using Subsemigroup.closure_induction' with
      | Hs x hx => exact subset_closure hx
      | Hmul x _ y _ hx hy => exact mul_mem hx hy

end Submonoid

[Junyan Xu]

Anatole Dedecker said:

The problem with adjoin_induction is I end up with this subgoal:

∀ (x y : A), x * b ∈ NonUnitalAlgebra.adjoin K s → y * b ∈ NonUnitalAlgebra.adjoin K s → (x * y) * b ∈ NonUnitalAlgebra.adjoin K s

Which doesn't seem provable. I haven't thought more about the deep reasons for this, I also expected the two inductions to be equivalent.

We just need to generalize the variable b:

import Mathlib

open MvPolynomial in
theorem bar_key [CommRing K] [CommRing A] [Algebra K A] {s : Set A} {a b : A}
    (ha : a ∈ Algebra.adjoin K s) (hb : b ∈ NonUnitalAlgebra.adjoin K s) :
    a * b ∈ NonUnitalAlgebra.adjoin K s := by
  revert b; change ∀ b, _ -- makes b explicit, otherwise `refine` introduces it automatically and anonymously
  refine Algebra.adjoin_induction ha ?_ ?_ ?_ ?_
  · intro b hb x hx; exact mul_mem (NonUnitalAlgebra.subset_adjoin _ hb) hx
  · intro k x hx; rw [← Algebra.smul_def]; exact NonUnitalSubalgebra.smul_mem' _ _ hx
  · intro b c hb hc x hx; rw [add_mul]; exact add_mem (hb x hx) (hc x hx)
  · intro b c hb hc x hx; rw [mul_assoc]; exact hb _ (hc _ hx)