Separating ideals

A closed two-sided ideal J of a topological algebra B is a separating ideal when, for every sequence b in B, the two nests of closed subspaces closure (b 0 ⋯ b (n - 1) J) and closure (J b (n - 1) ⋯ b 0) are eventually constant. Separating ideals are the algebraic shadow of Sinclair's stability lemma: the separating space of a surjective algebra homomorphism, or more generally of a linear map into B whose commutators with the actions of B are continuous, is a separating ideal. The structure theory of separating ideals in semisimple algebras builds on this to prove the classical automatic-continuity theorems.

The nests are written with products in Module.End R B of the multiplication operators LinearMap.mulLeft R (b i) and LinearMap.mulRight R (b i), so that no identity of B is needed and the 0-th term of each nest is the closure of J itself.

Main definitions

• Submodule.IsSeparatingIdeal: a closed two-sided ideal, given as a scalar submodule, whose left and right nests stabilize along every sequence.

Main results

• Submodule.isSeparatingIdeal_of_finiteDimensional: a finite-dimensional two-sided ideal is a separating ideal.
• LinearMap.isSeparatingIdeal_separatingSpace: if T : E → B is a linear map between Banach spaces, B a Banach algebra, and x ↦ T (L b x) - b * T x and x ↦ T (R b x) - T x * b are continuous for continuous linear operators L b and R b on E, then the separating space of T is a separating ideal. This applies to Banach B-bimodules with actions L and R.
• NonUnitalAlgHom.isSeparatingIdeal_separatingSpace: the separating space of a surjective homomorphism between Banach algebras, not assumed continuous, is a separating ideal.

References

• H. G. Dales, Banach Algebras and Automatic Continuity, §5.2: separating ideals and the separating spaces of homomorphisms and intertwining maps.
• A. M. Sinclair, Automatic Continuity of Linear Operators, London Math. Soc. Lecture Note Series 21.

structure Submodule.IsSeparatingIdeal {R : Type u_1} {B : Type u_2} [CommSemiring R] [NonUnitalSemiring B] [Module R B] [IsScalarTower R B B] [SMulCommClass R B B] [TopologicalSpace B] [ContinuousAdd B] [ContinuousConstSMul R B] (J : Submodule R B) : Prop

A separating ideal of a topological algebra B is a closed two-sided ideal J, given as a scalar submodule, such that for every sequence b in B the nests of closed subspaces closure (b 0 ⋯ b (n - 1) J) and closure (J b (n - 1) ⋯ b 0) are eventually constant. The products are formed in Module.End R B from left and right multiplication operators.

• isClosed : IsClosed ↑J

  A separating ideal is closed.

• mul_mem_left (b : B) {y : B} : y ∈ J → b * y ∈ J

  A separating ideal is a left ideal.

• mul_mem_right (b : B) {y : B} : y ∈ J → y * b ∈ J

  A separating ideal is a right ideal.

• eventuallyConst_left (b : ℕ → B) : Filter.EventuallyConst (fun (n : ℕ) => (map (List.map (fun (i : ℕ) => LinearMap.mulLeft R (b i)) (List.range n)).prod J).topologicalClosure) Filter.atTop

  The left nest closure (b 0 ⋯ b (n - 1) J) is eventually constant.

• eventuallyConst_right (b : ℕ → B) : Filter.EventuallyConst (fun (n : ℕ) => (map (List.map (fun (i : ℕ) => LinearMap.mulRight R (b i)) (List.range n)).prod J).topologicalClosure) Filter.atTop

  The right nest closure (J b (n - 1) ⋯ b 0) is eventually constant.

theorem Submodule.isSeparatingIdeal_of_finiteDimensional {𝕜 : Type u_1} {B : Type u_2} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [NonUnitalRing B] [Module 𝕜 B] [IsScalarTower 𝕜 B B] [SMulCommClass 𝕜 B B] [TopologicalSpace B] [IsTopologicalAddGroup B] [ContinuousSMul 𝕜 B] [T2Space B] (J : Submodule 𝕜 B) [FiniteDimensional 𝕜 ↥J] (hleft : ∀ (b : B) {y : B}, y ∈ J → b * y ∈ J) (hright : ∀ (b : B) {y : B}, y ∈ J → y * b ∈ J) : J.IsSeparatingIdeal

A finite-dimensional two-sided ideal of a Hausdorff topological algebra over a complete field is a separating ideal: its nests are decreasing chains of finite-dimensional, hence closed, subspaces.

theorem LinearMap.isSeparatingIdeal_separatingSpace {𝕜 : Type u_1} {E : Type u_2} {B : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] [NonUnitalNormedRing B] [NormedSpace 𝕜 B] [IsScalarTower 𝕜 B B] [SMulCommClass 𝕜 B B] [CompleteSpace B] (T : E →ₗ[𝕜] B) (L R : B → E →L[𝕜] E) (hL : ∀ (b : B), Continuous fun (x : E) => T ((L b) x) - b * T x) (hR : ∀ (b : B), Continuous fun (x : E) => T ((R b) x) - T x * b) : T.separatingSpace.IsSeparatingIdeal

Separating spaces of intertwining maps are separating ideals. Let T : E → B be a linear map, not assumed continuous, from a Banach space into a Banach algebra, and let L b and R b be continuous linear operators on E such that x ↦ T (L b x) - b * T x and x ↦ T (R b x) - T x * b are continuous for each b. Then the separating space of T is a separating ideal of B. This applies to a Banach B-bimodule E with actions L and R; the bimodule laws themselves are not needed.

theorem NonUnitalAlgHom.isSeparatingIdeal_separatingSpace {𝕜 : Type u_1} {A : Type u_2} {B : Type u_3} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [CompleteSpace A] [NonUnitalNormedRing B] [NormedSpace 𝕜 B] [IsScalarTower 𝕜 B B] [SMulCommClass 𝕜 B B] [CompleteSpace B] (θ : A →ₙₐ[𝕜] B) (hθ : Function.Surjective ⇑θ) : (↑θ).separatingSpace.IsSeparatingIdeal

The separating space of a surjective homomorphism is a separating ideal. For a surjective homomorphism θ : A → B of Banach algebras, not assumed continuous, the separating space of θ is a separating ideal of B.