The separating space of a linear map

For a linear map T : E →ₗ[R] F between topological modules, the separating space T.separatingSpace is the set of y : F such that (0, y) lies in the closure of the graph of T. When E and F are first countable these are exactly the limits of T xₙ along sequences xₙ → 0. The separating space measures the failure of continuity of T, and it is the basic object of automatic continuity theory for Banach algebras.

The separating space is a closed submodule, and the closure of the graph of T is described fibrewise by it: (x, y) lies in the closure exactly when y - T x ∈ T.separatingSpace. Hence the graph of T is closed exactly when the separating space vanishes. Between Banach spaces the closed graph theorem turns this into the criterion Continuous T ↔ T.separatingSpace = ⊥, and more precisely the separating space is the smallest closed subspace modulo which T becomes continuous.

Sinclair's stability lemma controls separating spaces along a sequence of composites. Given Banach spaces E n and F, continuous linear maps R n : E (n + 1) → E n, and linear maps T n : E n → F with T (n + 1) = T n ∘ R n, the separating spaces of the T n form a decreasing sequence that is eventually constant. This is the analytic input to the theory of separating ideals in automatic continuity. Applied to continuous linear maps that intertwine T up to continuous errors, it shows that the closures of the images of the separating space under the successive products stabilize.

Main definitions

• LinearMap.separatingSpace: the separating space of a linear map, as a submodule.

Main results

• LinearMap.isClosed_separatingSpace: the separating space is closed.
• LinearMap.mem_separatingSpace_iff_mapClusterPt, LinearMap.mem_separatingSpace_iff_exists_seq: the filter and sequential descriptions.
• LinearMap.mem_closure_graph_iff: the closure of the graph, fibre by fibre.
• LinearMap.isClosed_graph_iff_separatingSpace_eq_bot.
• LinearMap.separatingSpace_add: invariance under continuous perturbations.
• LinearMap.map_separatingSpace_le, LinearMap.separatingSpace_comp_le: behaviour under composition with continuous linear maps.
• LinearMap.continuous_iff_separatingSpace_eq_bot: a linear map between Banach spaces is continuous if and only if its separating space is trivial.
• LinearMap.continuous_mkQ_comp: a linear map between Banach spaces becomes continuous modulo its separating space.
• LinearMap.continuous_comp_iff_separatingSpace_le_ker: for a continuous linear map W, the composite W ∘ T is continuous exactly when W kills the separating space of T.
• LinearMap.separatingSpace_comp: the separating space of U ∘ T is the closure of the image under U of the separating space of T.
• LinearMap.map_separatingSpace_le_of_continuous_sub: a continuous linear map U with U ∘ T - T' ∘ V continuous for a continuous linear map V sends the separating space of T into that of T'.
• LinearMap.exists_norm_le_le_norm_mkQ_apply: modulo a closed subspace not containing the separating space, T sends arbitrarily small vectors to arbitrarily large ones.
• TauCeti.antitone_separatingSpace, TauCeti.eventuallyConst_separatingSpace: Sinclair's stability lemma.
• LinearMap.eventuallyConst_topologicalClosure_map_separatingSpace: stabilization of the closed images of the separating space under successive intertwining products.

References

• H. G. Dales, Banach Algebras and Automatic Continuity, §5.2, in particular the stability lemma 5.2.5.
• A. M. Sinclair, Automatic Continuity of Linear Operators, London Math. Soc. Lecture Note Series 21.

def LinearMap.separatingSpace {R : Type u_1} {E : Type u_3} {F : Type u_4} [Ring R] [AddCommGroup E] [Module R E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousConstSMul R E] [AddCommGroup F] [Module R F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul R F] (T : E →ₗ[R] F) : Submodule R F

The separating space of a linear map T : E →ₗ[R] F between topological modules: the vertical fibre over 0 of the closure of the graph of T. For first countable spaces it consists of the limits of T xₙ along sequences xₙ → 0 (LinearMap.mem_separatingSpace_iff_exists_seq).

theorem LinearMap.mem_separatingSpace_iff_mem_closure {R : Type u_1} {E : Type u_3} {F : Type u_4} [Ring R] [AddCommGroup E] [Module R E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousConstSMul R E] [AddCommGroup F] [Module R F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul R F] (T : E →ₗ[R] F) {y : F} : y ∈ T.separatingSpace ↔ (0, y) ∈ closure ↑T.graph

The separating space is the vertical fibre over 0 of the closure of the graph.

theorem LinearMap.isClosed_separatingSpace {R : Type u_1} {E : Type u_3} {F : Type u_4} [Ring R] [AddCommGroup E] [Module R E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousConstSMul R E] [AddCommGroup F] [Module R F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul R F] (T : E →ₗ[R] F) : IsClosed ↑T.separatingSpace

The separating space is closed.

theorem LinearMap.mem_separatingSpace_iff_mapClusterPt {R : Type u_1} {E : Type u_3} {F : Type u_4} [Ring R] [AddCommGroup E] [Module R E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousConstSMul R E] [AddCommGroup F] [Module R F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul R F] (T : E →ₗ[R] F) {y : F} : y ∈ T.separatingSpace ↔ MapClusterPt y (nhds 0) ⇑T

y lies in the separating space of T exactly when it is a cluster point of T at 0.

theorem LinearMap.mem_separatingSpace_iff_exists_seq {R : Type u_1} {E : Type u_3} {F : Type u_4} [Ring R] [AddCommGroup E] [Module R E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousConstSMul R E] [AddCommGroup F] [Module R F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul R F] (T : E →ₗ[R] F) [FirstCountableTopology E] [FirstCountableTopology F] {y : F} : y ∈ T.separatingSpace ↔ ∃ (x : ℕ → E), Filter.Tendsto x Filter.atTop (nhds 0) ∧ Filter.Tendsto (⇑T ∘ x) Filter.atTop (nhds y)

For first countable spaces, y lies in the separating space of T exactly when T xₙ → y for some sequence xₙ → 0.

theorem LinearMap.mem_closure_graph_iff {R : Type u_1} {E : Type u_3} {F : Type u_4} [Ring R] [AddCommGroup E] [Module R E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousConstSMul R E] [AddCommGroup F] [Module R F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul R F] (T : E →ₗ[R] F) {x : E} {y : F} : (x, y) ∈ closure ↑T.graph ↔ y - T x ∈ T.separatingSpace

The closure of the graph of T is the graph of T thickened by the separating space.

theorem LinearMap.isClosed_graph_iff_separatingSpace_eq_bot {R : Type u_1} {E : Type u_3} {F : Type u_4} [Ring R] [AddCommGroup E] [Module R E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousConstSMul R E] [AddCommGroup F] [Module R F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul R F] (T : E →ₗ[R] F) : IsClosed ↑T.graph ↔ T.separatingSpace = ⊥

The graph of a linear map is closed if and only if its separating space is trivial.

theorem LinearMap.separatingSpace_eq_bot_of_continuous {R : Type u_1} {E : Type u_3} {F : Type u_4} [Ring R] [AddCommGroup E] [Module R E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousConstSMul R E] [AddCommGroup F] [Module R F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul R F] (T : E →ₗ[R] F) [T2Space F] (hT : Continuous ⇑T) : T.separatingSpace = ⊥

A continuous linear map into a Hausdorff space has trivial separating space.

theorem LinearMap.map_separatingSpace_le {R : Type u_1} {E : Type u_3} {F : Type u_4} {G : Type u_5} [Ring R] [AddCommGroup E] [Module R E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousConstSMul R E] [AddCommGroup F] [Module R F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul R F] [AddCommGroup G] [Module R G] [TopologicalSpace G] [IsTopologicalAddGroup G] [ContinuousConstSMul R G] (T : E →ₗ[R] F) (U : F →L[R] G) : Submodule.map (↑U) T.separatingSpace ≤ (↑U ∘ₗ T).separatingSpace

A continuous linear map U sends the separating space of T into that of U ∘ T.

theorem LinearMap.separatingSpace_le_ker_of_continuous_comp {R : Type u_1} {E : Type u_3} {F : Type u_4} {G : Type u_5} [Ring R] [AddCommGroup E] [Module R E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousConstSMul R E] [AddCommGroup F] [Module R F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul R F] [AddCommGroup G] [Module R G] [TopologicalSpace G] [IsTopologicalAddGroup G] [ContinuousConstSMul R G] (T : E →ₗ[R] F) [T2Space G] (U : F →L[R] G) (hU : Continuous ⇑(↑U ∘ₗ T)) : T.separatingSpace ≤ (↑U).ker

If U ∘ T is continuous for a continuous linear map U into a Hausdorff space, then U vanishes on the separating space of T.

theorem LinearMap.separatingSpace_comp_le {R : Type u_1} {D : Type u_2} {E : Type u_3} {F : Type u_4} [Ring R] [AddCommGroup D] [Module R D] [TopologicalSpace D] [IsTopologicalAddGroup D] [ContinuousConstSMul R D] [AddCommGroup E] [Module R E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousConstSMul R E] [AddCommGroup F] [Module R F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul R F] (T : E →ₗ[R] F) (V : D →L[R] E) : (T ∘ₗ ↑V).separatingSpace ≤ T.separatingSpace

Precomposing with a continuous linear map can only shrink the separating space.

@[simp]

theorem LinearMap.separatingSpace_add {R : Type u_1} {E : Type u_3} {F : Type u_4} [Ring R] [AddCommGroup E] [Module R E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousConstSMul R E] [AddCommGroup F] [Module R F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul R F] (T : E →ₗ[R] F) (P : E →L[R] F) : (T + ↑P).separatingSpace = T.separatingSpace

The separating space is unchanged by adding a continuous linear map.

theorem LinearMap.separatingSpace_eq_of_continuous_sub {R : Type u_1} {E : Type u_3} {F : Type u_4} [Ring R] [AddCommGroup E] [Module R E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousConstSMul R E] [AddCommGroup F] [Module R F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul R F] {T₁ T₂ : E →ₗ[R] F} (h : Continuous ⇑(T₁ - T₂)) : T₁.separatingSpace = T₂.separatingSpace

Two linear maps differing by a continuous linear map have the same separating space.

theorem LinearMap.map_separatingSpace_le_of_continuous_sub {R : Type u_1} {D : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} [Ring R] [AddCommGroup D] [Module R D] [TopologicalSpace D] [IsTopologicalAddGroup D] [ContinuousConstSMul R D] [AddCommGroup E] [Module R E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousConstSMul R E] [AddCommGroup F] [Module R F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul R F] [AddCommGroup G] [Module R G] [TopologicalSpace G] [IsTopologicalAddGroup G] [ContinuousConstSMul R G] (T : E →ₗ[R] F) (T' : D →ₗ[R] G) (U : F →L[R] G) (V : E →L[R] D) (h : Continuous ⇑(↑U ∘ₗ T - T' ∘ₗ ↑V)) : Submodule.map (↑U) T.separatingSpace ≤ T'.separatingSpace

If U ∘ T - T' ∘ V is continuous for continuous linear maps U and V, then U maps the separating space of T into that of T'. Taking T' = T and U, V the left or right actions of an algebra on F and E, this says that the separating space of a map whose commutators with the actions are continuous is a submodule.

theorem LinearMap.isClosed_graph_mkQ_comp {R : Type u_1} {E : Type u_3} {F : Type u_4} [Ring R] [AddCommGroup E] [Module R E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousConstSMul R E] [AddCommGroup F] [Module R F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul R F] (T : E →ₗ[R] F) : IsClosed ↑(T.separatingSpace.mkQ ∘ₗ T).graph

The graph of T becomes closed after passing to the quotient by its separating space.

theorem LinearMap.continuous_iff_separatingSpace_eq_bot {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (T : E →ₗ[𝕜] F) [CompleteSpace E] [CompleteSpace F] : Continuous ⇑T ↔ T.separatingSpace = ⊥

A linear map between Banach spaces is continuous if and only if its separating space is trivial.

theorem LinearMap.continuous_mkQ_comp {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (T : E →ₗ[𝕜] F) [CompleteSpace E] [CompleteSpace F] : Continuous ⇑(T.separatingSpace.mkQ ∘ₗ T)

A linear map between Banach spaces becomes continuous modulo its separating space.

theorem LinearMap.continuous_comp_iff_separatingSpace_le_ker {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (T : E →ₗ[𝕜] F) [CompleteSpace E] [CompleteSpace F] [AddCommGroup G] [Module 𝕜 G] [TopologicalSpace G] [IsTopologicalAddGroup G] [ContinuousConstSMul 𝕜 G] [T2Space G] (W : F →L[𝕜] G) : Continuous ⇑(↑W ∘ₗ T) ↔ T.separatingSpace ≤ (↑W).ker

For a linear map T between Banach spaces and a continuous linear map W into a Hausdorff space, W ∘ T is continuous if and only if W vanishes on the separating space of T.

theorem LinearMap.separatingSpace_comp {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (T : E →ₗ[𝕜] F) [CompleteSpace E] [CompleteSpace F] [AddCommGroup G] [Module 𝕜 G] [TopologicalSpace G] [IsTopologicalAddGroup G] [ContinuousSMul 𝕜 G] (U : F →L[𝕜] G) : (↑U ∘ₗ T).separatingSpace = (Submodule.map (↑U) T.separatingSpace).topologicalClosure

For a linear map T between Banach spaces and a continuous linear map U into a topological vector space, the separating space of U ∘ T is the closure of the image under U of the separating space of T.

theorem LinearMap.exists_norm_le_le_norm_mkQ_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (T : E →ₗ[𝕜] F) {N : Submodule 𝕜 F} [IsClosed ↑N] (hT : ¬T.separatingSpace ≤ N) {δ : ℝ} (hδ : 0 < δ) (c : ℝ) : ∃ (x : E), ‖x‖ ≤ δ ∧ c ≤ ‖N.mkQ (T x)‖

If the separating space of a linear map T between normed spaces is not contained in a closed subspace N, then modulo N the map T sends arbitrarily small vectors to arbitrarily large ones.

The stability lemma

theorem TauCeti.antitone_separatingSpace {𝕜 : Type u_1} {F : Type u_2} [Ring 𝕜] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul 𝕜 F] {E : ℕ → Type u_3} [(n : ℕ) → AddCommGroup (E n)] [(n : ℕ) → Module 𝕜 (E n)] [(n : ℕ) → TopologicalSpace (E n)] [∀ (n : ℕ), IsTopologicalAddGroup (E n)] [∀ (n : ℕ), ContinuousConstSMul 𝕜 (E n)] {T : (n : ℕ) → E n →ₗ[𝕜] F} {R : (n : ℕ) → E (n + 1) →L[𝕜] E n} (hT : ∀ (n : ℕ), T (n + 1) = T n ∘ₗ ↑(R n)) : Antitone fun (n : ℕ) => (T n).separatingSpace

For linear maps T n : E n →ₗ F with T (n + 1) = T n ∘ R n for continuous linear maps R n : E (n + 1) → E n, the separating spaces of the T n decrease.

theorem TauCeti.eventuallyConst_separatingSpace {𝕜 : Type u_1} {F : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : ℕ → Type u_3} [(n : ℕ) → NormedAddCommGroup (E n)] [(n : ℕ) → NormedSpace 𝕜 (E n)] {R : (n : ℕ) → E (n + 1) →L[𝕜] E n} [CompleteSpace F] [∀ (n : ℕ), CompleteSpace (E n)] {T : (n : ℕ) → E n →ₗ[𝕜] F} (hT : ∀ (n : ℕ), T (n + 1) = T n ∘ₗ ↑(R n)) : Filter.EventuallyConst (fun (n : ℕ) => (T n).separatingSpace) Filter.atTop

Sinclair's stability lemma. Let E n and F be Banach spaces, let R n : E (n + 1) → E n be continuous linear maps, and let T n : E n →ₗ F be linear maps, not assumed continuous, with T (n + 1) = T n ∘ R n, so that T n = T 0 ∘ R 0 ∘ ⋯ ∘ R (n - 1). Then the decreasing sequence of separating spaces of the T n is eventually constant.

Stability of the images of the separating space

theorem LinearMap.eventuallyConst_topologicalClosure_map_separatingSpace {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] (T : E →ₗ[𝕜] F) (R : ℕ → E →L[𝕜] E) (S : ℕ → F →L[𝕜] F) (hRS : ∀ (n : ℕ), Continuous ⇑(↑(S n) ∘ₗ T - T ∘ₗ ↑(R n))) {V : ℕ → F →L[𝕜] F} (hV0 : V 0 = ContinuousLinearMap.id 𝕜 F) (hV : ∀ (n : ℕ), V (n + 1) = V n ∘SL S n) : Filter.EventuallyConst (fun (n : ℕ) => (Submodule.map (↑(V n)) T.separatingSpace).topologicalClosure) Filter.atTop

Stability of the images of the separating space. Let T : E → F be a linear map between Banach spaces, and let R n on E and S n on F be continuous linear maps such that each S n ∘ T - T ∘ R n is continuous. If V n = S 0 ∘ ⋯ ∘ S (n - 1), then the closures of the images of the separating space of T under V n are eventually constant.