From 4e7a8e477ddd92f93003f8f6aba14da630a2c6a7 Mon Sep 17 00:00:00 2001 From: sharky564 Date: Sat, 2 May 2026 17:51:49 +1000 Subject: [PATCH 01/10] Added CLM.ofIsTopCompl --- .../Topology/Algebra/Module/Complement.lean | 52 +++++++++++++++++++ 1 file changed, 52 insertions(+) diff --git a/Mathlib/Topology/Algebra/Module/Complement.lean b/Mathlib/Topology/Algebra/Module/Complement.lean index 5945ceef62f939..6e9dd0dd70342a 100644 --- a/Mathlib/Topology/Algebra/Module/Complement.lean +++ b/Mathlib/Topology/Algebra/Module/Complement.lean @@ -400,3 +400,55 @@ lemma ClosedComplemented.exists_submodule_equiv_prod [IsTopologicalAddGroup M] end ClosedComplemented end Submodule + +namespace ContinuousLinearMap + +variable {R : Type*} [Ring R] {E F : Type*} + [TopologicalSpace E] [AddCommGroup E] [Module R E] [IsTopologicalAddGroup E] + [TopologicalSpace F] [AddCommGroup F] [Module R F] [ContinuousAdd F] + {p q : Submodule R E} + +/-- Given continuous linear maps `φ : p →L[R] F` and `ψ : q →L[R] F` from topological complement +submodules of `E`, the induced continuous linear map `E →L[R] F`. -/ +noncomputable def ofIsTopCompl (h : IsTopCompl p q) (φ : p →L[R] F) (ψ : q →L[R] F) : E →L[R] F := + φ ∘L h.projectionOnto + ψ ∘L h.symm.projectionOnto + +@[simp] +theorem coe_ofIsTopCompl (h : IsTopCompl p q) (φ : p →L[R] F) (ψ : q →L[R] F) : + (ofIsTopCompl h φ ψ : E →ₗ[R] F) = LinearMap.ofIsCompl h.isCompl φ ψ := by + rw [LinearMap.ofIsCompl_eq_add] + rfl + +@[simp] +theorem ofIsTopCompl_apply_left (h : IsTopCompl p q) (φ : p →L[R] F) (ψ : q →L[R] F) (x : p) : + ofIsTopCompl h φ ψ (x : E) = φ x := by + simp [ofIsTopCompl] + +@[simp] +theorem ofIsTopCompl_apply_right (h : IsTopCompl p q) (φ : p →L[R] F) (ψ : q →L[R] F) (x : q) : + ofIsTopCompl h φ ψ (x : E) = ψ x := by + simp [ofIsTopCompl] + +theorem ofIsTopCompl_eq (h : 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 φ ψ = χ := by + ext x + obtain ⟨_, _, rfl, _⟩ := existsUnique_add_of_isCompl h.isCompl x + simp [hφ, hψ] + +@[simp] +theorem ofIsTopCompl_zero (h : IsTopCompl p q) : + (ofIsTopCompl h 0 0 : E →L[R] F) = 0 := by + ext; simp [ofIsTopCompl] + +@[simp] +theorem ofIsTopCompl_add (h : IsTopCompl p q) (φ₁ φ₂ : p →L[R] F) (ψ₁ ψ₂ : q →L[R] F) : + ofIsTopCompl h (φ₁ + φ₂) (ψ₁ + ψ₂) = ofIsTopCompl h φ₁ ψ₁ + ofIsTopCompl h φ₂ ψ₂ := by + ext; simp [ofIsTopCompl]; abel + +@[simp] +theorem range_ofIsTopCompl (h : IsTopCompl p q) (φ : p →L[R] F) (ψ : q →L[R] F) : + LinearMap.range (ofIsTopCompl h φ ψ : E →ₗ[R] F) = φ.range ⊔ ψ.range := by + rw [coe_ofIsTopCompl] + exact LinearMap.range_ofIsCompl h.isCompl + +end ContinuousLinearMap From d67a851898f8f6ce3b25cb7c36f1a50eb80673b7 Mon Sep 17 00:00:00 2001 From: sharky564 Date: Sat, 2 May 2026 21:53:27 +1000 Subject: [PATCH 02/10] Simplified proof --- Mathlib/Topology/Algebra/Module/Complement.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Topology/Algebra/Module/Complement.lean b/Mathlib/Topology/Algebra/Module/Complement.lean index 6e9dd0dd70342a..3e4987eb535ea2 100644 --- a/Mathlib/Topology/Algebra/Module/Complement.lean +++ b/Mathlib/Topology/Algebra/Module/Complement.lean @@ -443,7 +443,7 @@ theorem ofIsTopCompl_zero (h : IsTopCompl p q) : @[simp] theorem ofIsTopCompl_add (h : IsTopCompl p q) (φ₁ φ₂ : p →L[R] F) (ψ₁ ψ₂ : q →L[R] F) : ofIsTopCompl h (φ₁ + φ₂) (ψ₁ + ψ₂) = ofIsTopCompl h φ₁ ψ₁ + ofIsTopCompl h φ₂ ψ₂ := by - ext; simp [ofIsTopCompl]; abel + ext; simp [ofIsTopCompl, add_add_add_comm] @[simp] theorem range_ofIsTopCompl (h : IsTopCompl p q) (φ : p →L[R] F) (ψ : q →L[R] F) : From 0d6b87019fe2cf9232beb60e39b8f1a25d70fe52 Mon Sep 17 00:00:00 2001 From: sharky564 Date: Sat, 2 May 2026 22:38:57 +1000 Subject: [PATCH 03/10] Added top compl for complete space --- Mathlib/Analysis/Normed/Module/Complemented.lean | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/Mathlib/Analysis/Normed/Module/Complemented.lean b/Mathlib/Analysis/Normed/Module/Complemented.lean index 9e92be0d1137c1..099f7b396229f4 100644 --- a/Mathlib/Analysis/Normed/Module/Complemented.lean +++ b/Mathlib/Analysis/Normed/Module/Complemented.lean @@ -108,6 +108,11 @@ theorem ClosedComplemented.of_isCompl_isClosed (h : IsCompl p q) (hp : IsClosed alias IsCompl.closedComplemented_of_isClosed := ClosedComplemented.of_isCompl_isClosed +theorem IsCompl.isTopCompl_of_isClosed (h : IsCompl p q) (hp : IsClosed (p : Set E)) + (hq : IsClosed (q : Set E)) : IsTopCompl p q := by + rw [h.isTopCompl_iff_isHomeomorph_prodEquiv] + exact (Submodule.prodEquivOfClosedCompl p q h hp hq).toHomeomorph.isHomeomorph + theorem closedComplemented_iff_isClosed_exists_isClosed_isCompl : p.ClosedComplemented ↔ IsClosed (p : Set E) ∧ ∃ q : Submodule 𝕜 E, IsClosed (q : Set E) ∧ IsCompl p q := From 888a55d57c7145d20f09d12b73d26241db214a5a Mon Sep 17 00:00:00 2001 From: sharky564 Date: Wed, 13 May 2026 01:29:06 +1000 Subject: [PATCH 04/10] Ported work over --- .../Topology/Algebra/Module/Complement.lean | 125 +++++++++++++++--- 1 file changed, 108 insertions(+), 17 deletions(-) diff --git a/Mathlib/Topology/Algebra/Module/Complement.lean b/Mathlib/Topology/Algebra/Module/Complement.lean index 3e4987eb535ea2..9ede93a9d48b04 100644 --- a/Mathlib/Topology/Algebra/Module/Complement.lean +++ b/Mathlib/Topology/Algebra/Module/Complement.lean @@ -1,7 +1,7 @@ /- Copyright (c) 2026 Anatole Dedecker. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Anatole Dedecker +Authors: Anatole Dedecker, Sharvil Kesarwani -/ module @@ -29,14 +29,20 @@ change to something less misleading. 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 +* `Submodule.IsTopCompl.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.linearProjOfIsCompl`. -* `Submodule.IsTopCompl.projection`: if `h : IsTopCompl p q`, `h.projection` is the continuous + `Submodule.projectionOnto`. +* `Submodule.IsTopCompl.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.IsTopCompl.prodEquiv`: the bundled continuous linear equivalence `p × q ≃L[R] M` + arising from a topological complement pair. +* `Submodule.IsTopCompl.quotientEquiv`: 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 @@ -55,18 +61,6 @@ Because the condition is symmetric, a lot of lemmas could have a left and a righ 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`. - -/ @[expose] public section @@ -399,6 +393,103 @@ lemma ClosedComplemented.exists_submodule_equiv_prod [IsTopologicalAddGroup M] end ClosedComplemented +section ContinuousLinearEquiv + +variable [IsTopologicalAddGroup M] + +/-- Two submodules `p` and `q` are topological complements if and only if the algebraic equivalence +`p.prodEquivOfIsCompl q h` is continuous in the inverse direction. -/ +theorem _root_.IsCompl.isTopCompl_iff_continuous_prodEquiv_symm (h : IsCompl p q) : + IsTopCompl p q ↔ Continuous (p.prodEquivOfIsCompl q h).symm := + ⟨fun hTop ↦ ((p.projectionOntoL q hTop).prod (q.projectionOntoL p hTop.symm)).continuous.congr + fun x ↦ (prodEquivOfIsCompl_symm_apply h x).symm, + fun hCont ↦ ⟨h, continuous_subtype_val.comp <| continuous_fst.comp hCont⟩⟩ + +/-- The algebraic equivalence `p.prodEquivOfIsCompl q h : p × q ≃ₗ[R] M` from a pair of +complementary submodules is always continuous as a map `p × q → M`. -/ +theorem continuous_prodEquivOfIsCompl (h : IsCompl p q) : + Continuous (p.prodEquivOfIsCompl q h) := + (continuous_subtype_val.comp continuous_fst).add (continuous_subtype_val.comp continuous_snd) + +/-- Two submodules `p` and `q` are topological complements if and only if the algebraic equivalence +`p.prodEquivOfIsCompl q h` is a homeomorphism. -/ +theorem _root_.IsCompl.isTopCompl_iff_isHomeomorph_prodEquiv (h : IsCompl p q) : + IsTopCompl p q ↔ IsHomeomorph (p.prodEquivOfIsCompl q h) := by + rw [(p.prodEquivOfIsCompl q h).isHomeomorph_iff, h.isTopCompl_iff_continuous_prodEquiv_symm, + and_iff_right] + exact continuous_prodEquivOfIsCompl h + +/-- If two submodules `p` and `q` are topological complements, then the algebraic equivalence +`p.prodEquivOfIsCompl q h.isCompl` is a homeomorphism, bundled as a continuous linear equivalence. +-/ +noncomputable def IsTopCompl.prodEquiv (h : IsTopCompl p q) : (p × q) ≃L[R] M := + { p.prodEquivOfIsCompl q h.isCompl with + continuous_toFun := continuous_prodEquivOfIsCompl h.isCompl + continuous_invFun := h.isCompl.isTopCompl_iff_continuous_prodEquiv_symm.mp h } + +@[simp] +theorem IsTopCompl.coe_prodEquiv (h : IsTopCompl p q) : + (h.prodEquiv : (p × q) →ₗ[R] M) = p.prodEquivOfIsCompl q h.isCompl := + rfl + +@[simp] +theorem IsTopCompl.coe_prodEquiv_symm (h : IsTopCompl p q) : + (h.prodEquiv.symm : M →ₗ[R] p × q) = (p.prodEquivOfIsCompl q h.isCompl).symm := + rfl + +@[simp] +theorem IsTopCompl.prodEquiv_apply (h : IsTopCompl p q) (x : p × q) : + h.prodEquiv x = (x.1 : M) + x.2 := + rfl + +@[simp] +theorem IsTopCompl.prodEquiv_symm_apply (h : IsTopCompl p q) (x : M) : + h.prodEquiv.symm x = ((p.projectionOntoL q h x, q.projectionOntoL p h.symm x) : p × q) := + prodEquivOfIsCompl_symm_apply h.isCompl x + +/-- Two submodules `p` and `q` are topological complements if and only if the algebraic equivalence +`p.quotientEquivOfIsCompl q h` is continuous. -/ +theorem IsCompl.isTopCompl_iff_continuous_quotientEquiv (h : IsCompl p q) : + IsTopCompl p q ↔ Continuous (p.quotientEquivOfIsCompl q h) := by + have hproj : ⇑(p.quotientEquivOfIsCompl q h) ∘ ⇑p.mkQ = ⇑(q.projectionOnto p h.symm) := by + funext; simp + rw [p.isQuotientMap_mkQL.continuous_iff, coe_mkQL, hproj, ← h.symm.isTopCompl_iff_projectionOnto] + exact ⟨IsTopCompl.symm, IsTopCompl.symm⟩ + +/-- If two submodules `p` and `q` are topological complements, then the algebraic equivalence +`p.quotientEquivOfIsCompl q h.isCompl` is a homeomorphism, bundled as a continuous linear +equivalence. -/ +noncomputable def IsTopCompl.quotientEquiv (h : IsTopCompl p q) : (M ⧸ p) ≃L[R] q := + { p.quotientEquivOfIsCompl q h.isCompl with + continuous_toFun := (h.isCompl.isTopCompl_iff_continuous_quotientEquiv).mp h + continuous_invFun := (p.mkQL.comp q.subtypeL).continuous } + +@[simp] +theorem IsTopCompl.coe_quotientEquiv (h : IsTopCompl p q) : + (h.quotientEquiv : (M ⧸ p) →ₗ[R] q) = p.quotientEquivOfIsCompl q h.isCompl := + rfl + +@[simp] +theorem IsTopCompl.coe_quotientEquiv_symm (h : IsTopCompl p q) : + (h.quotientEquiv.symm : q →ₗ[R] M ⧸ p) = (p.quotientEquivOfIsCompl q h.isCompl).symm := + rfl + +theorem IsTopCompl.quotientEquiv_apply (h : IsTopCompl p q) (x : M ⧸ p) : + h.quotientEquiv x = p.quotientEquivOfIsCompl q h.isCompl x := + rfl + +@[simp] +theorem IsTopCompl.quotientEquiv_symm_apply (h : IsTopCompl p q) (y : q) : + h.quotientEquiv.symm y = p.mkQ y := + rfl + +@[simp] +theorem IsTopCompl.quotientEquiv_apply_mk (h : IsTopCompl p q) (x : M) : + h.quotientEquiv (Submodule.Quotient.mk x) = q.projectionOnto p h.isCompl.symm x := + quotientEquivOfIsCompl_apply_mk h.isCompl x + +end ContinuousLinearEquiv + end Submodule namespace ContinuousLinearMap @@ -411,7 +502,7 @@ variable {R : Type*} [Ring R] {E F : Type*} /-- Given continuous linear maps `φ : p →L[R] F` and `ψ : q →L[R] F` from topological complement submodules of `E`, the induced continuous linear map `E →L[R] F`. -/ noncomputable def ofIsTopCompl (h : IsTopCompl p q) (φ : p →L[R] F) (ψ : q →L[R] F) : E →L[R] F := - φ ∘L h.projectionOnto + ψ ∘L h.symm.projectionOnto + φ ∘L p.projectionOntoL q h + ψ ∘L q.projectionOntoL p h.symm @[simp] theorem coe_ofIsTopCompl (h : IsTopCompl p q) (φ : p →L[R] F) (ψ : q →L[R] F) : From dd74e447739e2f8e8385a69115c96751d42a8311 Mon Sep 17 00:00:00 2001 From: sharky564 Date: Wed, 13 May 2026 01:43:07 +1000 Subject: [PATCH 05/10] Removed unnecessary --- Mathlib/Analysis/Normed/Module/Complemented.lean | 5 ----- 1 file changed, 5 deletions(-) diff --git a/Mathlib/Analysis/Normed/Module/Complemented.lean b/Mathlib/Analysis/Normed/Module/Complemented.lean index 099f7b396229f4..9e92be0d1137c1 100644 --- a/Mathlib/Analysis/Normed/Module/Complemented.lean +++ b/Mathlib/Analysis/Normed/Module/Complemented.lean @@ -108,11 +108,6 @@ theorem ClosedComplemented.of_isCompl_isClosed (h : IsCompl p q) (hp : IsClosed alias IsCompl.closedComplemented_of_isClosed := ClosedComplemented.of_isCompl_isClosed -theorem IsCompl.isTopCompl_of_isClosed (h : IsCompl p q) (hp : IsClosed (p : Set E)) - (hq : IsClosed (q : Set E)) : IsTopCompl p q := by - rw [h.isTopCompl_iff_isHomeomorph_prodEquiv] - exact (Submodule.prodEquivOfClosedCompl p q h hp hq).toHomeomorph.isHomeomorph - theorem closedComplemented_iff_isClosed_exists_isClosed_isCompl : p.ClosedComplemented ↔ IsClosed (p : Set E) ∧ ∃ q : Submodule 𝕜 E, IsClosed (q : Set E) ∧ IsCompl p q := From 6105a43841a1bfea3716226ec54e830589fcc740 Mon Sep 17 00:00:00 2001 From: sharky564 Date: Wed, 13 May 2026 23:02:03 +1000 Subject: [PATCH 06/10] Simp lint fixes --- Mathlib/Topology/Algebra/Module/Complement.lean | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/Mathlib/Topology/Algebra/Module/Complement.lean b/Mathlib/Topology/Algebra/Module/Complement.lean index 9ede93a9d48b04..fbde8b8391a382 100644 --- a/Mathlib/Topology/Algebra/Module/Complement.lean +++ b/Mathlib/Topology/Algebra/Module/Complement.lean @@ -536,10 +536,7 @@ theorem ofIsTopCompl_add (h : IsTopCompl p q) (φ₁ φ₂ : p →L[R] F) (ψ₁ ofIsTopCompl h (φ₁ + φ₂) (ψ₁ + ψ₂) = ofIsTopCompl h φ₁ ψ₁ + ofIsTopCompl h φ₂ ψ₂ := by ext; simp [ofIsTopCompl, add_add_add_comm] -@[simp] theorem range_ofIsTopCompl (h : IsTopCompl p q) (φ : p →L[R] F) (ψ : q →L[R] F) : - LinearMap.range (ofIsTopCompl h φ ψ : E →ₗ[R] F) = φ.range ⊔ ψ.range := by - rw [coe_ofIsTopCompl] - exact LinearMap.range_ofIsCompl h.isCompl + LinearMap.range (ofIsTopCompl h φ ψ : E →ₗ[R] F) = φ.range ⊔ ψ.range := by simp end ContinuousLinearMap From d9332d48ba44c6048fefea15532aa37f0752575f Mon Sep 17 00:00:00 2001 From: sharky564 Date: Wed, 13 May 2026 23:34:58 +1000 Subject: [PATCH 07/10] Trigger CI From e9e7038c1323c122775bac771dcfc30768beae4d Mon Sep 17 00:00:00 2001 From: sharky564 Date: Wed, 13 May 2026 23:44:37 +1000 Subject: [PATCH 08/10] Why is git doing this? --- Mathlib/Topology/Algebra/Module/Complement.lean | 12 ------------ 1 file changed, 12 deletions(-) diff --git a/Mathlib/Topology/Algebra/Module/Complement.lean b/Mathlib/Topology/Algebra/Module/Complement.lean index 50571f7f610c4c..856fdf83751143 100644 --- a/Mathlib/Topology/Algebra/Module/Complement.lean +++ b/Mathlib/Topology/Algebra/Module/Complement.lean @@ -61,18 +61,6 @@ Because the condition is symmetric, a lot of lemmas could have a left and a righ 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 a 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 a 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`. - -/ @[expose] public section From 30740ba512940294c3db8f0f26409af3297f8eb6 Mon Sep 17 00:00:00 2001 From: Sharvil Kesarwani Date: Thu, 14 May 2026 00:00:50 +1000 Subject: [PATCH 09/10] Update Mathlib/Topology/Algebra/Module/Complement.lean Co-authored-by: Anatole Dedecker --- Mathlib/Topology/Algebra/Module/Complement.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Topology/Algebra/Module/Complement.lean b/Mathlib/Topology/Algebra/Module/Complement.lean index 856fdf83751143..6ecc2ac630eb95 100644 --- a/Mathlib/Topology/Algebra/Module/Complement.lean +++ b/Mathlib/Topology/Algebra/Module/Complement.lean @@ -29,7 +29,7 @@ change to something less misleading. 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.projectionOntoL`: if `h : IsTopCompl p q`, `p.projectionOntoL q h` is the +* `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.IsTopCompl.projectionL`: if `h : IsTopCompl p q`, `p.projectionL q h` is the continuous From ec534da9cc486bfbefce4e3b13de3e26648602e5 Mon Sep 17 00:00:00 2001 From: Sharvil Kesarwani Date: Thu, 14 May 2026 00:01:06 +1000 Subject: [PATCH 10/10] Update Mathlib/Topology/Algebra/Module/Complement.lean Co-authored-by: Anatole Dedecker --- Mathlib/Topology/Algebra/Module/Complement.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Topology/Algebra/Module/Complement.lean b/Mathlib/Topology/Algebra/Module/Complement.lean index 6ecc2ac630eb95..d57b21796b9b71 100644 --- a/Mathlib/Topology/Algebra/Module/Complement.lean +++ b/Mathlib/Topology/Algebra/Module/Complement.lean @@ -32,7 +32,7 @@ change to something less misleading. * `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.IsTopCompl.projectionL`: if `h : IsTopCompl p q`, `p.projectionL q h` is the continuous +* `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