Topological complements of submodules

Let M be a topological R-module. Two submodules p, q of M are said to be topological complements (Submodule.IsTopCompl) if they are algebraic complements and the algebraic isomorphism M ≃ p × q is an homeomorphism.

Not all submodules of M admit such a topological complements (even if they admit algebraic complements). In the literature, such a submodule is called topologically complemented or direct. One may also find the terminology closed complemented because, in a Banach space, a closed algebraic complement is automatically a topological complement. This is the terminology we use for now (Submodule.ClosedComplemented), but we should eventually change to something less misleading.

Main definitions

• Submodule.IsTopCompl: we say that two submodules are topological complements if they are algebraic complements and the projection on p along q is continuous. This is equivalent to the definition given above.
• Submodule.ClosedComplemented: we say that a submodule is (topologically) complemented if there exists a continuous projection M →ₗ[R] p.
• Submodule.IsTopCompl.projectionOnto: if h : IsTopCompl p q, h.projectionOnto is the continuous linear projection M →L[R] p along q. This is the continuous version of Submodule.linearProjOfIsCompl.
• Submodule.IsTopCompl.projection: if h : IsTopCompl p q, h.projection is the continuous linear projection M →L[R] M onto p along q. This is the continuous version of Submodule.IsCompl.projection.
• Submodule.ClosedComplemented.complement: an arbitrary topological complement of a topologically complemented submodule.

Main statements

• IsIdempotentElem.isTopCompl: the range and kernel of a continuous projection are topological complements.
• Submodule.IsTopCompl.isClosed: if p and q are topological complements in a Hausdorff space, they are closed.

Implementation details

In the definition of Submodule.IsTopCompl, we choose to ask for the continuity of the projection on the left submdule along the right one, because it is a simpler map to work with than the map M ≃ p × q.

Because the condition is symmetric, a lot of lemmas could have a left and a right variation. In general we only include the left version, the right one being accessible through Submodule.IsTopCompl.symm.

TODO

There is still a significant part of the algebraic API which should be ported to the topological setting. Notably, we should:

• show that Submodule.prodEquivOfIsCompl is an homeomorphism if and only if the two subspaces are topological complements, and bundle it as a ContinuousLinearEquiv when this is the case. (See the existing ClosedComplemented.exists_submodule_equiv_prod).
• show that Submodule.quotientEquivOfIsCompl is an homeomorphism if and only if the two subspaces are topological complements, and bundle it as a ContinuousLinearEquiv when this is the case.
• define ContinuousLinearMap.ofIsTopCompl, analogous to LinearMap.ofIsCompl.

structure Submodule.IsTopCompl {R : Type u_1} [Ring R] {M : Type u_2} [TopologicalSpace M] [AddCommGroup M] [Module R M] (p q : Submodule R M) : Prop

Two submodules p and q are topological complements if they are algebraic complements and the projection on p along q is continuous.

• isCompl : IsCompl p q
• continuous_projection : Continuous ⇑(p.projection q ⋯)

def Submodule.ClosedComplemented {R : Type u_1} [Ring R] {M : Type u_2} [TopologicalSpace M] [AddCommGroup M] [Module R M] (p : Submodule R M) : Prop

A submodule p is called complemented if there exists a continuous projection M →ₗ[R] p.

Equations

• p.ClosedComplemented = ∃ (f : M →L[R] ↥p), ∀ (x : ↥p), f ↑x = x

theorem Submodule.IsCompl.isTopCompl_iff {R : Type u_1} [Ring R] {M : Type u_2} [TopologicalSpace M] [AddCommGroup M] [Module R M] {p q : Submodule R M} (h : IsCompl p q) : IsTopCompl p q ↔ Continuous ⇑(p.projection q h)

theorem Submodule.IsCompl.isTopCompl_iff_projectionOnto {R : Type u_1} [Ring R] {M : Type u_2} [TopologicalSpace M] [AddCommGroup M] [Module R M] {p q : Submodule R M} (h : IsCompl p q) : IsTopCompl p q ↔ Continuous ⇑(p.projectionOnto q h)

@[deprecated Submodule.IsCompl.isTopCompl_iff_projectionOnto (since := "2026-05-05")]

theorem Submodule.IsCompl.isTopCompl_iff_linearProjOfIsCompl {R : Type u_1} [Ring R] {M : Type u_2} [TopologicalSpace M] [AddCommGroup M] [Module R M] {p q : Submodule R M} (h : IsCompl p q) : IsTopCompl p q ↔ Continuous ⇑(p.projectionOnto q h)

Alias of Submodule.IsCompl.isTopCompl_iff_projectionOnto.

theorem Submodule.IsTopCompl.continuous_projectionOnto {R : Type u_1} [Ring R] {M : Type u_2} [TopologicalSpace M] [AddCommGroup M] [Module R M] {p q : Submodule R M} (h : IsTopCompl p q) : Continuous ⇑(p.projectionOnto q ⋯)

@[deprecated Submodule.IsTopCompl.continuous_projectionOnto (since := "2026-05-05")]

theorem Submodule.IsTopCompl.continuous_linearProjOfIsCompl {R : Type u_1} [Ring R] {M : Type u_2} [TopologicalSpace M] [AddCommGroup M] [Module R M] {p q : Submodule R M} (h : IsTopCompl p q) : Continuous ⇑(p.projectionOnto q ⋯)

Alias of Submodule.IsTopCompl.continuous_projectionOnto.

theorem Submodule.IsTopCompl.symm {R : Type u_1} [Ring R] {M : Type u_2} [TopologicalSpace M] [AddCommGroup M] [Module R M] {p q : Submodule R M} [ContinuousSub M] (h : IsTopCompl p q) : IsTopCompl q p

theorem ContinuousLinearMap.IsIdempotentElem.isTopCompl {R : Type u_1} [Ring R] {M : Type u_2} [TopologicalSpace M] [AddCommGroup M] [Module R M] {f : M →L[R] M} (hf : IsIdempotentElem f) : Submodule.IsTopCompl (↑f).range (↑f).ker

theorem Submodule.isTopCompl_bot_top {R : Type u_1} [Ring R] {M : Type u_2} [TopologicalSpace M] [AddCommGroup M] [Module R M] : IsTopCompl ⊥ ⊤

theorem Submodule.isTopCompl_top_bot {R : Type u_1} [Ring R] {M : Type u_2} [TopologicalSpace M] [AddCommGroup M] [Module R M] : IsTopCompl ⊤ ⊥

theorem ContinuousLinearMap.isTopCompl_range_ker_of_leftInverse {R : Type u_1} [Ring R] {M : Type u_2} {N : Type u_3} [TopologicalSpace M] [TopologicalSpace N] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (f₁ : M →L[R] N) (f₂ : N →L[R] M) (h : Function.LeftInverse ⇑f₂ ⇑f₁) : Submodule.IsTopCompl (↑f₁).range (↑f₂).ker

theorem ContinuousLinearMap.isTopCompl_of_proj {R : Type u_1} [Ring R] {M : Type u_2} [TopologicalSpace M] [AddCommGroup M] [Module R M] {p : Submodule R M} {f : M →L[R] ↥p} (hf : ∀ (x : ↥p), f ↑x = x) : Submodule.IsTopCompl p (↑f).ker

noncomputable def Submodule.projectionOntoL {R : Type u_1} [Ring R] {M : Type u_2} [TopologicalSpace M] [AddCommGroup M] [Module R M] (p q : Submodule R M) (h : IsTopCompl p q) : M →L[R] ↥p

If h : IsTopCompl p q, h.projectionOnto is the continuous linear projection M →L[R] p along q. This is the continuous version of Submodule.linearProjOfIsCompl.

See also Submodule.IsTopCompl.projection for the same projection as an element of M →L[R] M.

Equations

• p.projectionOntoL q h = { toLinearMap := p.projectionOnto q ⋯, cont := ⋯ }

@[simp]

theorem Submodule.toLinearMap_projectionOntoL {R : Type u_1} [Ring R] {M : Type u_2} [TopologicalSpace M] [AddCommGroup M] [Module R M] {p q : Submodule R M} (h : IsTopCompl p q) : ↑(p.projectionOntoL q h) = p.projectionOnto q ⋯

@[simp]

theorem Submodule.projectionOntoL_apply_left {R : Type u_1} [Ring R] {M : Type u_2} [TopologicalSpace M] [AddCommGroup M] [Module R M] {p q : Submodule R M} (h : IsTopCompl p q) (x : ↥p) : (p.projectionOntoL q h) ↑x = x

theorem Submodule.range_projectionOntoL {R : Type u_1} [Ring R] {M : Type u_2} [TopologicalSpace M] [AddCommGroup M] [Module R M] {p q : Submodule R M} (h : IsTopCompl p q) : (↑(p.projectionOntoL q h)).range = ⊤

theorem Submodule.projectionOntoL_surjective {R : Type u_1} [Ring R] {M : Type u_2} [TopologicalSpace M] [AddCommGroup M] [Module R M] {p q : Submodule R M} (h : IsTopCompl p q) : Function.Surjective ⇑(p.projectionOntoL q h)

@[simp]

theorem Submodule.projectionOntoL_apply_eq_zero_iff {R : Type u_1} [Ring R] {M : Type u_2} [TopologicalSpace M] [AddCommGroup M] [Module R M] {p q : Submodule R M} (h : IsTopCompl p q) {x : M} : (p.projectionOntoL q h) x = 0 ↔ x ∈ q

theorem Submodule.projectionOntoL_apply_eq_zero_of_mem_right {R : Type u_1} [Ring R] {M : Type u_2} [TopologicalSpace M] [AddCommGroup M] [Module R M] {p q : Submodule R M} (h : IsTopCompl p q) {x : M} : x ∈ q → (p.projectionOntoL q h) x = 0

Alias of the reverse direction of Submodule.projectionOntoL_apply_eq_zero_iff.

@[simp]

theorem Submodule.projectionOntoL_apply_right {R : Type u_1} [Ring R] {M : Type u_2} [TopologicalSpace M] [AddCommGroup M] [Module R M] {p q : Submodule R M} (h : IsTopCompl p q) (x : ↥q) : (p.projectionOntoL q h) ↑x = 0

theorem Submodule.ker_projectionOntoL {R : Type u_1} [Ring R] {M : Type u_2} [TopologicalSpace M] [AddCommGroup M] [Module R M] {p q : Submodule R M} (h : IsTopCompl p q) : (↑(p.projectionOntoL q h)).ker = q

theorem Submodule.isQuotientMap_projectionOntoL {R : Type u_1} [Ring R] {M : Type u_2} [TopologicalSpace M] [AddCommGroup M] [Module R M] {p q : Submodule R M} (h : IsTopCompl p q) : Topology.IsQuotientMap ⇑(p.projectionOntoL q h)

noncomputable def Submodule.projectionL {R : Type u_1} [Ring R] {M : Type u_2} [TopologicalSpace M] [AddCommGroup M] [Module R M] (p q : Submodule R M) (h : IsTopCompl p q) : M →L[R] M

If h : IsTopCompl p q, h.projection is the continuous linear projection M →L[R] M onto p along q. This is the continuous version of Submodule.IsCompl.projection.

See also Submodule.IsTopCompl.projectionOnto for the same projection as an element of M →L[R] p.

Equations

• p.projectionL q h = p.subtypeL.comp (p.projectionOntoL q h)

@[simp]

theorem Submodule.toLinearMap_projectionL {R : Type u_1} [Ring R] {M : Type u_2} [TopologicalSpace M] [AddCommGroup M] [Module R M] {p q : Submodule R M} (h : IsTopCompl p q) : ↑(p.projectionL q h) = p.projection q ⋯

theorem Submodule.projectionL_apply {R : Type u_1} [Ring R] {M : Type u_2} [TopologicalSpace M] [AddCommGroup M] [Module R M] {p q : Submodule R M} (h : IsTopCompl p q) (x : M) : (p.projectionL q h) x = ↑((p.projectionOntoL q h) x)

@[simp]

theorem Submodule.coe_projectionOntoL_apply {R : Type u_1} [Ring R] {M : Type u_2} [TopologicalSpace M] [AddCommGroup M] [Module R M] {p q : Submodule R M} (h : IsTopCompl p q) (x : M) : ↑((p.projectionOntoL q h) x) = (p.projectionL q h) x

@[simp]

theorem Submodule.projectionL_apply_mem {R : Type u_1} [Ring R] {M : Type u_2} [TopologicalSpace M] [AddCommGroup M] [Module R M] {p q : Submodule R M} (h : IsTopCompl p q) (x : M) : (p.projectionL q h) x ∈ p

@[simp]

theorem Submodule.projectionL_apply_left {R : Type u_1} [Ring R] {M : Type u_2} [TopologicalSpace M] [AddCommGroup M] [Module R M] {p q : Submodule R M} (h : IsTopCompl p q) (x : ↥p) : (p.projectionL q h) ↑x = ↑x

theorem Submodule.range_projectionL {R : Type u_1} [Ring R] {M : Type u_2} [TopologicalSpace M] [AddCommGroup M] [Module R M] {p q : Submodule R M} (h : IsTopCompl p q) : (↑(p.projectionL q h)).range = p

@[simp]

theorem Submodule.projectionL_apply_eq_zero_iff {R : Type u_1} [Ring R] {M : Type u_2} [TopologicalSpace M] [AddCommGroup M] [Module R M] {p q : Submodule R M} (h : IsTopCompl p q) {x : M} : (p.projectionL q h) x = 0 ↔ x ∈ q

theorem Submodule.projectionL_apply_eq_zero_of_mem_right {R : Type u_1} [Ring R] {M : Type u_2} [TopologicalSpace M] [AddCommGroup M] [Module R M] {p q : Submodule R M} (h : IsTopCompl p q) {x : M} : x ∈ q → (p.projectionL q h) x = 0

Alias of the reverse direction of Submodule.projectionL_apply_eq_zero_iff.

@[simp]

theorem Submodule.projectionL_apply_right {R : Type u_1} [Ring R] {M : Type u_2} [TopologicalSpace M] [AddCommGroup M] [Module R M] {p q : Submodule R M} (h : IsTopCompl p q) (x : ↥q) : (p.projectionL q h) ↑x = 0

theorem Submodule.ker_projectionL {R : Type u_1} [Ring R] {M : Type u_2} [TopologicalSpace M] [AddCommGroup M] [Module R M] {p q : Submodule R M} (h : IsTopCompl p q) : (↑(p.projectionL q h)).ker = q

@[simp]

theorem Submodule.isIdempotentElem_projectionL {R : Type u_1} [Ring R] {M : Type u_2} [TopologicalSpace M] [AddCommGroup M] [Module R M] {p q : Submodule R M} (h : IsTopCompl p q) : IsIdempotentElem (p.projectionL q h)

theorem Submodule.projectionL_add_projectionL_eq_self {R : Type u_1} [Ring R] {M : Type u_2} [TopologicalSpace M] [AddCommGroup M] [Module R M] {p q : Submodule R M} [ContinuousSub M] (h : IsTopCompl p q) (x : M) : (p.projectionL q h) x + (q.projectionL p ⋯) x = x

theorem Submodule.projectionL_add_projectionL_eq_id {R : Type u_1} [Ring R] {M : Type u_2} [TopologicalSpace M] [AddCommGroup M] [Module R M] {p q : Submodule R M} [IsTopologicalAddGroup M] (h : IsTopCompl p q) : p.projectionL q h + q.projectionL p ⋯ = ContinuousLinearMap.id R M

theorem Submodule.projectionL_eq_self_sub_projectionL {R : Type u_1} [Ring R] {M : Type u_2} [TopologicalSpace M] [AddCommGroup M] [Module R M] {p q : Submodule R M} [ContinuousSub M] (h : IsTopCompl p q) (x : M) : (q.projectionL p ⋯) x = x - (p.projectionL q h) x

theorem Submodule.projectionL_eq_id_sub_projectionL {R : Type u_1} [Ring R] {M : Type u_2} [TopologicalSpace M] [AddCommGroup M] [Module R M] {p q : Submodule R M} [IsTopologicalAddGroup M] (h : IsTopCompl p q) : q.projectionL p ⋯ = ContinuousLinearMap.id R M - p.projectionL q h

@[simp]

theorem Submodule.projectionL_eq_self_iff {R : Type u_1} [Ring R] {M : Type u_2} [TopologicalSpace M] [AddCommGroup M] [Module R M] {p q : Submodule R M} [ContinuousSub M] (h : IsTopCompl p q) (x : M) : (p.projectionL q h) x = x ↔ x ∈ p

The projection to p along q of x equals x if and only if x ∈ p.

theorem ContinuousLinearMap.IsIdempotentElem.eq_projectionL {R : Type u_1} [Ring R] {M : Type u_2} [TopologicalSpace M] [AddCommGroup M] [Module R M] {f : M →L[R] M} (hf : IsIdempotentElem f) : f = (↑f).range.projectionL (↑f).ker ⋯

theorem ContinuousLinearMap.isIdempotentElem_iff_eq_projectionL_range_ker {R : Type u_1} [Ring R] {M : Type u_2} [TopologicalSpace M] [AddCommGroup M] [Module R M] {f : M →L[R] M} : IsIdempotentElem f ↔ ∃ (h : Submodule.IsTopCompl (↑f).range (↑f).ker), f = (↑f).range.projectionL (↑f).ker h

theorem Submodule.IsTopCompl.closedComplemented {R : Type u_1} [Ring R] {M : Type u_2} [TopologicalSpace M] [AddCommGroup M] [Module R M] {p q : Submodule R M} (h : IsTopCompl p q) : p.ClosedComplemented

theorem Submodule.IsTopCompl.isClosed' {R : Type u_1} [Ring R] {M : Type u_2} [TopologicalSpace M] [AddCommGroup M] [Module R M] {p q : Submodule R M} [T1Space ↥p] (h : IsTopCompl p q) : IsClosed ↑q

A variant of Submodule.IsTopCompl.isClosed. This has the very mild advantage over h.symm.isClosed that it doesn't assume ContinuousSub M.

theorem Submodule.IsTopCompl.isClosed {R : Type u_1} [Ring R] {M : Type u_2} [TopologicalSpace M] [AddCommGroup M] [Module R M] {p q : Submodule R M} [T1Space ↥q] [ContinuousSub M] (h : IsTopCompl p q) : IsClosed ↑p

If p and q are topological complements and q is Hausdorff, then p is closed.

theorem Submodule.IsTopCompl.t3Space {R : Type u_1} [Ring R] {M : Type u_2} [TopologicalSpace M] [AddCommGroup M] [Module R M] {p q : Submodule R M} [IsTopologicalAddGroup M] (h : IsTopCompl p q) (hq : IsClosed ↑q) : T3Space ↥p

theorem Submodule.IsTopCompl.t2Space {R : Type u_1} [Ring R] {M : Type u_2} [TopologicalSpace M] [AddCommGroup M] [Module R M] {p q : Submodule R M} [IsTopologicalAddGroup M] (h : IsTopCompl p q) (hq : IsClosed ↑q) : T2Space ↥p

If p and q are topological complements and q is closed, then p is Hausdorff.

theorem Submodule.ClosedComplemented.exists_isTopCompl {R : Type u_1} [Ring R] {M : Type u_2} [TopologicalSpace M] [AddCommGroup M] [Module R M] {p : Submodule R M} (h : p.ClosedComplemented) : ∃ (q : Submodule R M), IsTopCompl p q

theorem Submodule.closedComplemented_iff_exists_isTopCompl {R : Type u_1} [Ring R] {M : Type u_2} [TopologicalSpace M] [AddCommGroup M] [Module R M] {p : Submodule R M} : p.ClosedComplemented ↔ ∃ (q : Submodule R M), IsTopCompl p q

theorem Submodule.ClosedComplemented.exists_isClosed_isCompl {R : Type u_1} [Ring R] {M : Type u_2} [TopologicalSpace M] [AddCommGroup M] [Module R M] {p : Submodule R M} [T1Space ↥p] (h : p.ClosedComplemented) : ∃ (q : Submodule R M), IsClosed ↑q ∧ IsCompl p q

noncomputable def Submodule.ClosedComplemented.complement {R : Type u_1} [Ring R] {M : Type u_2} [TopologicalSpace M] [AddCommGroup M] [Module R M] {p : Submodule R M} (h : p.ClosedComplemented) : Submodule R M

An arbitrary choice of topological complement of a topologically complemented submodule.

Equations

• h.complement = Classical.choose ⋯

theorem Submodule.ClosedComplemented.isTopCompl_complement {R : Type u_1} [Ring R] {M : Type u_2} [TopologicalSpace M] [AddCommGroup M] [Module R M] {p : Submodule R M} (h : p.ClosedComplemented) : IsTopCompl p h.complement

theorem Submodule.ClosedComplemented.isCompl_complement {R : Type u_1} [Ring R] {M : Type u_2} [TopologicalSpace M] [AddCommGroup M] [Module R M] {p : Submodule R M} (h : p.ClosedComplemented) : IsCompl p h.complement

theorem Submodule.ClosedComplemented.isClosed_complement {R : Type u_1} [Ring R] {M : Type u_2} [TopologicalSpace M] [AddCommGroup M] [Module R M] {p : Submodule R M} [T1Space ↥p] (h : p.ClosedComplemented) : IsClosed ↑h.complement

theorem Submodule.ClosedComplemented.isClosed {R : Type u_1} [Ring R] {M : Type u_2} [TopologicalSpace M] [AddCommGroup M] [Module R M] [ContinuousSub M] [T1Space M] {p : Submodule R M} (h : p.ClosedComplemented) : IsClosed ↑p

@[simp]

theorem Submodule.closedComplemented_bot {R : Type u_1} [Ring R] {M : Type u_2} [TopologicalSpace M] [AddCommGroup M] [Module R M] : ⊥.ClosedComplemented

@[simp]

theorem Submodule.closedComplemented_top {R : Type u_1} [Ring R] {M : Type u_2} [TopologicalSpace M] [AddCommGroup M] [Module R M] : ⊤.ClosedComplemented

theorem ContinuousLinearMap.closedComplemented_range_of_leftInverse {R : Type u_1} [Ring R] {M : Type u_2} {N : Type u_3} [TopologicalSpace M] [TopologicalSpace N] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (f₁ : M →L[R] N) (f₂ : N →L[R] M) (h : Function.LeftInverse ⇑f₂ ⇑f₁) : (↑f₁).range.ClosedComplemented

theorem ContinuousLinearMap.closedComplemented_ker_of_rightInverse {R : Type u_1} [Ring R] {M : Type u_2} {N : Type u_3} [TopologicalSpace M] [TopologicalSpace N] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [ContinuousSub M] (f₁ : M →L[R] N) (f₂ : N →L[R] M) (h : Function.RightInverse ⇑f₂ ⇑f₁) : (↑f₁).ker.ClosedComplemented

theorem Submodule.ClosedComplemented.exists_submodule_equiv_prod {R : Type u_1} [Ring R] {M : Type u_2} [TopologicalSpace M] [AddCommGroup M] [Module R M] [IsTopologicalAddGroup M] {p : Submodule R M} (hp : p.ClosedComplemented) : ∃ (q : Submodule R M) (e : M ≃L[R] ↥p × ↥q), (∀ (x : ↥p), e ↑x = (x, 0)) ∧ (∀ (y : ↥q), e ↑y = (0, y)) ∧ ∀ (x : ↥p × ↥q), e.symm x = ↑x.1 + ↑x.2

If p is a closed complemented submodule, then there exists a submodule q and a continuous linear equivalence M ≃L[R] (p × q) such that e (x : p) = (x, 0), e (y : q) = (0, y), and e.symm x = x.1 + x.2.

In fact, the properties of e imply the properties of e.symm and vice versa, but we provide both for convenience.