Documentation

Mathlib.Topology.Algebra.Module.Complement

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 a 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.projectionOntoL: if h : IsTopCompl p q, p.projectionOntoL q h is the continuous linear projection M →L[R] p along q. This is the continuous version of Submodule.projectionOnto.
Submodule.projectionL: if h : IsTopCompl p q, p.projectionL q h 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.
Submodule.prodEquivOfIsTopCompl: the bundled continuous linear equivalence p × q ≃L[R] M arising from a topological complement pair.
Submodule.quotientEquivOfIsTopCompl: the bundled continuous linear equivalence M ⧸ p ≃L[R] q arising from a topological complement pair.
ContinuousLinearMap.ofIsTopCompl: the continuous linear map induced by maps on a topological complement pair.

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.

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) :

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 ⋯)

Instances For

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

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

Instances For

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) :

theorem Submodule.isTopCompl_comm {R : Type u_1} [Ring R] {M : Type u_2} [TopologicalSpace M] [AddCommGroup M] [Module R M] {p q : Submodule R M} [ContinuousSub M] :

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 := ⋯ }

Instances For

@[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) :

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 ∘SL p.projectionOntoL q h

Instances For

@[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) :

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) :

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) :

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) :

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) :

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

Equations

h.complement = Classical.choose ⋯

Instances For

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) :

@[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.

theorem Submodule.IsCompl.isTopCompl_iff_continuous_symm_prodEquivOfIsCompl {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 : IsCompl p q) :

IsTopCompl p q ↔ Continuous ⇑(p.prodEquivOfIsCompl q h).symm

Two complementary submodules are topological complements if and only if the linear equivalence Submodule.prodEquivOfIsCompl is continuous in the inverse direction.

theorem Submodule.continuous_prodEquivOfIsCompl {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 : IsCompl p q) :

Continuous ⇑(p.prodEquivOfIsCompl q h)

The linear equivalence Submodule.prodEquivOfIsCompl from a pair of complementary submodules is always continuous.

theorem Submodule.IsCompl.isTopCompl_iff_isHomeomorph_prodEquivOfIsCompl {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 : IsCompl p q) :

IsTopCompl p q ↔ IsHomeomorph ⇑(p.prodEquivOfIsCompl q h)

Two complementary submodules are topological complements if and only if the linear equivalence Submodule.prodEquivOfIsCompl is a homeomorphism.

noncomputable def Submodule.prodEquivOfIsTopCompl {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 × ↥q) ≃L[R] M

If two submodules are topological complements, then the linear equivalence Submodule.prodEquivOfIsCompl is a homeomorphism, bundled as a continuous linear equivalence.

Equations

p.prodEquivOfIsTopCompl q h = { toLinearEquiv := p.prodEquivOfIsCompl q ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ }

Instances For

@[simp]

theorem Submodule.toLinearEquiv_prodEquivOfIsTopCompl {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.prodEquivOfIsTopCompl q h) = p.prodEquivOfIsCompl q ⋯

@[simp]

theorem Submodule.prodEquivOfIsTopCompl_apply {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) (x : ↥p × ↥q) :

(p.prodEquivOfIsTopCompl q h) x = ↑x.1 + ↑x.2

@[simp]

theorem Submodule.prodEquivOfIsTopCompl_symm_apply {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) (x : M) :

(p.prodEquivOfIsTopCompl q h).symm x = ((p.projectionOntoL q h) x, (q.projectionOntoL p ⋯) x)

theorem Submodule.IsCompl.isTopCompl_iff_continuous_quotientEquivOfIsCompl {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 : IsCompl p q) :

IsTopCompl p q ↔ Continuous ⇑(p.quotientEquivOfIsCompl q h)

Two complementary submodules are topological complements if and only if the linear equivalence Submodule.quotientEquivOfIsCompl is continuous.

noncomputable def Submodule.quotientEquivOfIsTopCompl {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) :

(M ⧸ p) ≃L[R] ↥q

If two submodules are topological complements, then the linear equivalence Submodule.quotientEquivOfIsCompl is a homeomorphism, bundled as a continuous linear equivalence.

Equations

p.quotientEquivOfIsTopCompl q h = { toLinearEquiv := p.quotientEquivOfIsCompl q ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ }

Instances For

@[simp]

theorem Submodule.toLinearEquiv_quotientEquivOfIsTopCompl {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.quotientEquivOfIsTopCompl q h) = p.quotientEquivOfIsCompl q ⋯

@[simp]

theorem Submodule.quotientEquivOfIsTopCompl_apply {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) (x : M ⧸ p) :

(p.quotientEquivOfIsTopCompl q h) x = (p.quotientEquivOfIsCompl q ⋯) x

@[simp]

theorem Submodule.quotientEquivOfIsTopCompl_symm_apply {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) (y : ↥q) :

(p.quotientEquivOfIsTopCompl q h).symm y = p.mkQ ↑y

theorem Submodule.quotientEquivOfIsTopCompl_apply_mk {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) (x : M) :

(p.quotientEquivOfIsTopCompl q h) (Quotient.mk x) = (q.projectionOnto p ⋯) x

noncomputable def ContinuousLinearMap.ofIsTopCompl {R : Type u_1} [Ring R] {E : Type u_2} {F : Type u_3} [TopologicalSpace E] [AddCommGroup E] [Module R E] [IsTopologicalAddGroup E] [TopologicalSpace F] [AddCommGroup F] [Module R F] [ContinuousAdd F] {p q : Submodule R E} (h : Submodule.IsTopCompl p q) (φ : ↥p →L[R] F) (ψ : ↥q →L[R] F) :

Given continuous linear maps φ : p →L[R] F and ψ : q →L[R] F from topological complement submodules p and q of E, ContinuousLinearMap.ofIsCompl is the induced continuous linear map E →L[R] F over the entire module.

This is the continuous version of LinearMap.ofIsCompl.

Equations

ContinuousLinearMap.ofIsTopCompl h φ ψ = φ.coprod ψ ∘SL ↑(p.prodEquivOfIsTopCompl q h).symm

Instances For

theorem ContinuousLinearMap.ofIsTopCompl_eq_add {R : Type u_1} [Ring R] {E : Type u_2} {F : Type u_3} [TopologicalSpace E] [AddCommGroup E] [Module R E] [IsTopologicalAddGroup E] [TopologicalSpace F] [AddCommGroup F] [Module R F] [ContinuousAdd F] {p q : Submodule R E} (h : Submodule.IsTopCompl p q) (φ : ↥p →L[R] F) (ψ : ↥q →L[R] F) :

ofIsTopCompl h φ ψ = φ ∘SL p.projectionOntoL q h + ψ ∘SL q.projectionOntoL p ⋯

@[simp]

theorem ContinuousLinearMap.toLinearMap_ofIsTopCompl {R : Type u_1} [Ring R] {E : Type u_2} {F : Type u_3} [TopologicalSpace E] [AddCommGroup E] [Module R E] [IsTopologicalAddGroup E] [TopologicalSpace F] [AddCommGroup F] [Module R F] [ContinuousAdd F] {p q : Submodule R E} (h : Submodule.IsTopCompl p q) (φ : ↥p →L[R] F) (ψ : ↥q →L[R] F) :

↑(ofIsTopCompl h φ ψ) = LinearMap.ofIsCompl ⋯ ↑φ ↑ψ

@[simp]

theorem ContinuousLinearMap.ofIsTopCompl_apply {R : Type u_1} [Ring R] {E : Type u_2} {F : Type u_3} [TopologicalSpace E] [AddCommGroup E] [Module R E] [IsTopologicalAddGroup E] [TopologicalSpace F] [AddCommGroup F] [Module R F] [ContinuousAdd F] {p q : Submodule R E} (h : Submodule.IsTopCompl p q) (φ : ↥p →L[R] F) (ψ : ↥q →L[R] F) (x : E) :

(ofIsTopCompl h φ ψ) x = (LinearMap.ofIsCompl ⋯ ↑φ ↑ψ) x

theorem ContinuousLinearMap.ofIsTopCompl_apply_left {R : Type u_1} [Ring R] {E : Type u_2} {F : Type u_3} [TopologicalSpace E] [AddCommGroup E] [Module R E] [IsTopologicalAddGroup E] [TopologicalSpace F] [AddCommGroup F] [Module R F] [ContinuousAdd F] {p q : Submodule R E} (h : Submodule.IsTopCompl p q) (φ : ↥p →L[R] F) (ψ : ↥q →L[R] F) (x : ↥p) :

(ofIsTopCompl h φ ψ) ↑x = φ x

theorem ContinuousLinearMap.ofIsTopCompl_apply_right {R : Type u_1} [Ring R] {E : Type u_2} {F : Type u_3} [TopologicalSpace E] [AddCommGroup E] [Module R E] [IsTopologicalAddGroup E] [TopologicalSpace F] [AddCommGroup F] [Module R F] [ContinuousAdd F] {p q : Submodule R E} (h : Submodule.IsTopCompl p q) (φ : ↥p →L[R] F) (ψ : ↥q →L[R] F) (x : ↥q) :

(ofIsTopCompl h φ ψ) ↑x = ψ x

theorem ContinuousLinearMap.ofIsTopCompl_eq {R : Type u_1} [Ring R] {E : Type u_2} {F : Type u_3} [TopologicalSpace E] [AddCommGroup E] [Module R E] [IsTopologicalAddGroup E] [TopologicalSpace F] [AddCommGroup F] [Module R F] [ContinuousAdd F] {p q : Submodule R E} (h : Submodule.IsTopCompl p q) {φ : ↥p →L[R] F} {ψ : ↥q →L[R] F} {χ : E →L[R] F} (hφ : ∀ (u : ↥p), φ u = χ ↑u) (hψ : ∀ (u : ↥q), ψ u = χ ↑u) :

ofIsTopCompl h φ ψ = χ

@[simp]

theorem ContinuousLinearMap.ofIsTopCompl_zero {R : Type u_1} [Ring R] {E : Type u_2} {F : Type u_3} [TopologicalSpace E] [AddCommGroup E] [Module R E] [IsTopologicalAddGroup E] [TopologicalSpace F] [AddCommGroup F] [Module R F] [ContinuousAdd F] {p q : Submodule R E} (h : Submodule.IsTopCompl p q) :

ofIsTopCompl h 0 0 = 0

@[simp]

theorem ContinuousLinearMap.ofIsTopCompl_add {R : Type u_1} [Ring R] {E : Type u_2} {F : Type u_3} [TopologicalSpace E] [AddCommGroup E] [Module R E] [IsTopologicalAddGroup E] [TopologicalSpace F] [AddCommGroup F] [Module R F] [ContinuousAdd F] {p q : Submodule R E} (h : Submodule.IsTopCompl p q) (φ₁ φ₂ : ↥p →L[R] F) (ψ₁ ψ₂ : ↥q →L[R] F) :

ofIsTopCompl h (φ₁ + φ₂) (ψ₁ + ψ₂) = ofIsTopCompl h φ₁ ψ₁ + ofIsTopCompl h φ₂ ψ₂

theorem ContinuousLinearMap.range_ofIsTopCompl {R : Type u_1} [Ring R] {E : Type u_2} {F : Type u_3} [TopologicalSpace E] [AddCommGroup E] [Module R E] [IsTopologicalAddGroup E] [TopologicalSpace F] [AddCommGroup F] [Module R F] [ContinuousAdd F] {p q : Submodule R E} (h : Submodule.IsTopCompl p q) (φ : ↥p →L[R] F) (ψ : ↥q →L[R] F) :

(↑(ofIsTopCompl h φ ψ)).range = (↑φ).range ⊔ (↑ψ).range