feat(Topology/Algebra/Module/Complement): bundle prodEquivOfIsCompl and quotientEquivOfIsCompl, add ContinuousLinearMap.ofIsTopCompl (#39260)

This PR completes the three TODO items listed at the top of `Mathlib/Topology/Algebra/Module/Complement.lean` (introduced in #38547). `Submodule.prodEquivOfIsCompl` is shown to be a homeomorphism if and only if the two submodules are topological complements. The analogous characterisation for `Submodule.quotientEquivOfIsCompl` is also provided, and `ContinuousLinearMap.ofIsTopCompl` is defined as the continuous version of `LinearMap.ofIsCompl`, taking continuous linear maps from complementary submodules and producing the induced continuous linear map on the whole space.

Author: sharky564

Mathlib/LinearAlgebra/Projection.lean

@@ -360,11 +360,11 @@ def ofIsCompl {p q : Submodule R E} (h : IsCompl p q) (φ : p →ₗ[R] F) (ψ :
 variable {p q}
 
 @[simp]
-theorem ofIsCompl_left_apply (h : IsCompl p q) {φ : p →ₗ[R] F} {ψ : q →ₗ[R] F} (u : p) :
+theorem ofIsCompl_apply_left (h : IsCompl p q) {φ : p →ₗ[R] F} {ψ : q →ₗ[R] F} (u : p) :
     ofIsCompl h φ ψ (u : E) = φ u := by simp [ofIsCompl]
 
 @[simp]
-theorem ofIsCompl_right_apply (h : IsCompl p q) {φ : p →ₗ[R] F} {ψ : q →ₗ[R] F} (v : q) :
+theorem ofIsCompl_apply_right (h : IsCompl p q) {φ : p →ₗ[R] F} {ψ : q →ₗ[R] F} (v : q) :
     ofIsCompl h φ ψ (v : E) = ψ v := by simp [ofIsCompl]
 
 theorem ofIsCompl_eq (h : IsCompl p q) {φ : p →ₗ[R] F} {ψ : q →ₗ[R] F} {χ : E →ₗ[R] F}
@@ -448,8 +448,8 @@ def ofIsComplProdEquiv {p q : Submodule R₁ E} (h : IsCompl p q) :
     invFun := fun φ => ⟨φ.domRestrict p, φ.domRestrict q⟩
     left_inv := fun φ ↦ by
       ext x
-      · exact ofIsCompl_left_apply h x
-      · exact ofIsCompl_right_apply h x
+      · exact ofIsCompl_apply_left h x
+      · exact ofIsCompl_apply_right h x
     right_inv := fun φ ↦ by
       ext x
       obtain ⟨a, b, hab, _⟩ := existsUnique_add_of_isCompl h x
@@ -829,5 +829,7 @@ namespace LinearMap
   surjective_comp_projectionOnto
 @[deprecated (since := "2026-05-04")] alias isIdempotentElem_iff_eq_isCompl_projection_range_ker :=
   isIdempotentElem_iff_eq_projection_range_ker
+@[deprecated (since := "2026-05-16")] alias ofIsCompl_left_apply := ofIsCompl_apply_left
+@[deprecated (since := "2026-05-16")] alias ofIsCompl_right_apply := ofIsCompl_apply_right
 
 end LinearMap

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.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.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
 
@@ -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 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
@@ -121,6 +115,9 @@ protected theorem IsTopCompl.symm [ContinuousSub M] (h : IsTopCompl p q) : IsTop
     rw [projection_eq_id_sub_projection h.isCompl]
     exact continuous_id.sub h.continuous_projection
 
+theorem isTopCompl_comm [ContinuousSub M] : IsTopCompl p q ↔ IsTopCompl q p :=
+  ⟨IsTopCompl.symm, IsTopCompl.symm⟩
+
 open LinearMap in
 theorem _root_.ContinuousLinearMap.IsIdempotentElem.isTopCompl {f : M →L[R] M}
     (hf : IsIdempotentElem f) : IsTopCompl f.range f.ker where
@@ -399,4 +396,145 @@ lemma ClosedComplemented.exists_submodule_equiv_prod [IsTopologicalAddGroup M]
 
 end ClosedComplemented
 
+section ContinuousLinearEquiv
+
+variable [IsTopologicalAddGroup M]
+
+/-- Two complementary submodules are topological complements if and only if the linear equivalence
+`Submodule.prodEquivOfIsCompl` is continuous in the inverse direction. -/
+theorem IsCompl.isTopCompl_iff_continuous_symm_prodEquivOfIsCompl (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 linear equivalence `Submodule.prodEquivOfIsCompl` from a pair of complementary submodules is
+always continuous. -/
+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 complementary submodules are topological complements if and only if the linear equivalence
+`Submodule.prodEquivOfIsCompl` is a homeomorphism. -/
+theorem IsCompl.isTopCompl_iff_isHomeomorph_prodEquivOfIsCompl (h : IsCompl p q) :
+    IsTopCompl p q ↔ IsHomeomorph (p.prodEquivOfIsCompl q h) := by
+  rw [(p.prodEquivOfIsCompl q h).isHomeomorph_iff,
+    isTopCompl_iff_continuous_symm_prodEquivOfIsCompl, and_iff_right]
+  exact continuous_prodEquivOfIsCompl h
+
+variable (p q) in
+/-- If two submodules are topological complements, then the linear equivalence
+`Submodule.prodEquivOfIsCompl` is a homeomorphism, bundled as a continuous linear equivalence. -/
+noncomputable def prodEquivOfIsTopCompl (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_symm_prodEquivOfIsCompl.mp h }
+
+@[simp]
+theorem toLinearEquiv_prodEquivOfIsTopCompl (h : IsTopCompl p q) :
+    (prodEquivOfIsTopCompl p q h : (p × q) ≃ₗ[R] M) = p.prodEquivOfIsCompl q h.isCompl :=
+  rfl
+
+@[simp]
+theorem prodEquivOfIsTopCompl_apply (h : IsTopCompl p q) (x : p × q) :
+    prodEquivOfIsTopCompl p q h x = (x.1 : M) + x.2 :=
+  rfl
+
+@[simp]
+theorem prodEquivOfIsTopCompl_symm_apply (h : IsTopCompl p q) (x : M) :
+    (prodEquivOfIsTopCompl p q h).symm x =
+      ((p.projectionOntoL q h x, q.projectionOntoL p h.symm x) : p × q) :=
+  prodEquivOfIsCompl_symm_apply h.isCompl x
+
+/-- Two complementary submodules are topological complements if and only if the linear equivalence
+`Submodule.quotientEquivOfIsCompl` is continuous. -/
+theorem IsCompl.isTopCompl_iff_continuous_quotientEquivOfIsCompl (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,
+    isTopCompl_comm]
+
+variable (p q) in
+/-- If two submodules are topological complements, then the linear equivalence
+`Submodule.quotientEquivOfIsCompl` is a homeomorphism, bundled as a continuous linear
+equivalence. -/
+noncomputable def quotientEquivOfIsTopCompl (h : IsTopCompl p q) : (M ⧸ p) ≃L[R] q :=
+  { p.quotientEquivOfIsCompl q h.isCompl with
+    continuous_toFun := h.isCompl.isTopCompl_iff_continuous_quotientEquivOfIsCompl.mp h
+    continuous_invFun := (p.mkQL.comp q.subtypeL).continuous }
+
+@[simp]
+theorem toLinearEquiv_quotientEquivOfIsTopCompl (h : IsTopCompl p q) :
+    (quotientEquivOfIsTopCompl p q h : (M ⧸ p) ≃ₗ[R] q) = p.quotientEquivOfIsCompl q h.isCompl :=
+  rfl
+
+@[simp]
+theorem quotientEquivOfIsTopCompl_apply (h : IsTopCompl p q) (x : M ⧸ p) :
+    quotientEquivOfIsTopCompl p q h x = p.quotientEquivOfIsCompl q h.isCompl x :=
+  rfl
+
+@[simp]
+theorem quotientEquivOfIsTopCompl_symm_apply (h : IsTopCompl p q) (y : q) :
+    (quotientEquivOfIsTopCompl p q h).symm y = p.mkQ y :=
+  rfl
+
+theorem quotientEquivOfIsTopCompl_apply_mk (h : IsTopCompl p q) (x : M) :
+    quotientEquivOfIsTopCompl p q h (Quotient.mk x) = q.projectionOnto p h.isCompl.symm x :=
+  quotientEquivOfIsCompl_apply_mk h.isCompl x
+
+end ContinuousLinearEquiv
+
 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 `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`. -/
+noncomputable def ofIsTopCompl (h : IsTopCompl p q) (φ : p →L[R] F) (ψ : q →L[R] F) : E →L[R] F :=
+  φ.coprod ψ ∘L ↑(prodEquivOfIsTopCompl p q h).symm
+
+theorem ofIsTopCompl_eq_add (h : IsTopCompl p q) (φ : p →L[R] F) (ψ : q →L[R] F) :
+    ofIsTopCompl h φ ψ = φ ∘L p.projectionOntoL q h + ψ ∘L q.projectionOntoL p h.symm := by
+  ext; simp [ofIsTopCompl]
+
+@[simp]
+theorem toLinearMap_ofIsTopCompl (h : IsTopCompl p q) (φ : p →L[R] F) (ψ : q →L[R] F) :
+    (ofIsTopCompl h φ ψ : E →ₗ[R] F) = LinearMap.ofIsCompl h.isCompl φ ψ :=
+  rfl
+
+@[simp]
+theorem ofIsTopCompl_apply (h : IsTopCompl p q) (φ : p →L[R] F) (ψ : q →L[R] F) (x : E) :
+    ofIsTopCompl h φ ψ (x : E) = LinearMap.ofIsCompl h.isCompl φ ψ x :=
+  rfl
+
+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
+
+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
+
+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; simp [LinearMap.ofIsCompl_eq h.isCompl hφ, hψ]
+
+@[simp]
+theorem ofIsTopCompl_zero (h : IsTopCompl p q) : (ofIsTopCompl h 0 0 : E →L[R] F) = 0 := by
+  ext; simp
+
+@[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
+
+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 simp
+
+end ContinuousLinearMap