chore(NormedSpace/Complemented): review API (#8596)

- use `And` instead of `Exists`;
- move lemmas from `Subspace` to `Submodule` namespace;
- rename some lemmas to enable dot notation;
- add `ClosedComplemented.exists_submodule_equiv_prod`.

Mathlib/Analysis/NormedSpace/Complemented.lean

@@ -77,7 +77,7 @@ theorem equivProdOfSurjectiveOfIsCompl_apply {f : E →L[𝕜] F} {g : E →L[
 
 end ContinuousLinearMap
 
-namespace Subspace
+namespace Submodule
 
 variable [CompleteSpace E] (p q : Subspace 𝕜 E)
 
@@ -88,57 +88,59 @@ def prodEquivOfClosedCompl (h : IsCompl p q) (hp : IsClosed (p : Set E))
   haveI := hp.completeSpace_coe; haveI := hq.completeSpace_coe
   refine' (p.prodEquivOfIsCompl q h).toContinuousLinearEquivOfContinuous _
   exact (p.subtypeL.coprod q.subtypeL).continuous
-#align subspace.prod_equiv_of_closed_compl Subspace.prodEquivOfClosedCompl
+#align subspace.prod_equiv_of_closed_compl Submodule.prodEquivOfClosedCompl
 
 /-- Projection to a closed submodule along a closed complement. -/
 def linearProjOfClosedCompl (h : IsCompl p q) (hp : IsClosed (p : Set E))
     (hq : IsClosed (q : Set E)) : E →L[𝕜] p :=
   ContinuousLinearMap.fst 𝕜 p q ∘L ↑(prodEquivOfClosedCompl p q h hp hq).symm
-#align subspace.linear_proj_of_closed_compl Subspace.linearProjOfClosedCompl
+#align subspace.linear_proj_of_closed_compl Submodule.linearProjOfClosedCompl
 
 variable {p q}
 
 @[simp]
 theorem coe_prodEquivOfClosedCompl (h : IsCompl p q) (hp : IsClosed (p : Set E))
     (hq : IsClosed (q : Set E)) :
     ⇑(p.prodEquivOfClosedCompl q h hp hq) = p.prodEquivOfIsCompl q h := rfl
-#align subspace.coe_prod_equiv_of_closed_compl Subspace.coe_prodEquivOfClosedCompl
+#align subspace.coe_prod_equiv_of_closed_compl Submodule.coe_prodEquivOfClosedCompl
 
 @[simp]
 theorem coe_prodEquivOfClosedCompl_symm (h : IsCompl p q) (hp : IsClosed (p : Set E))
     (hq : IsClosed (q : Set E)) :
     ⇑(p.prodEquivOfClosedCompl q h hp hq).symm = (p.prodEquivOfIsCompl q h).symm := rfl
-#align subspace.coe_prod_equiv_of_closed_compl_symm Subspace.coe_prodEquivOfClosedCompl_symm
+#align subspace.coe_prod_equiv_of_closed_compl_symm Submodule.coe_prodEquivOfClosedCompl_symm
 
 @[simp]
 theorem coe_continuous_linearProjOfClosedCompl (h : IsCompl p q) (hp : IsClosed (p : Set E))
     (hq : IsClosed (q : Set E)) :
     (p.linearProjOfClosedCompl q h hp hq : E →ₗ[𝕜] p) = p.linearProjOfIsCompl q h := rfl
-#align subspace.coe_continuous_linear_proj_of_closed_compl Subspace.coe_continuous_linearProjOfClosedCompl
+#align subspace.coe_continuous_linear_proj_of_closed_compl Submodule.coe_continuous_linearProjOfClosedCompl
 
 @[simp]
 theorem coe_continuous_linearProjOfClosedCompl' (h : IsCompl p q) (hp : IsClosed (p : Set E))
     (hq : IsClosed (q : Set E)) :
     ⇑(p.linearProjOfClosedCompl q h hp hq) = p.linearProjOfIsCompl q h := rfl
-#align subspace.coe_continuous_linear_proj_of_closed_compl' Subspace.coe_continuous_linearProjOfClosedCompl'
+#align subspace.coe_continuous_linear_proj_of_closed_compl' Submodule.coe_continuous_linearProjOfClosedCompl'
 
-theorem closedComplemented_of_closed_compl (h : IsCompl p q) (hp : IsClosed (p : Set E))
+theorem ClosedComplemented.of_isCompl_isClosed (h : IsCompl p q) (hp : IsClosed (p : Set E))
     (hq : IsClosed (q : Set E)) : p.ClosedComplemented :=
   ⟨p.linearProjOfClosedCompl q h hp hq, Submodule.linearProjOfIsCompl_apply_left h⟩
-#align subspace.closed_complemented_of_closed_compl Subspace.closedComplemented_of_closed_compl
+#align subspace.closed_complemented_of_closed_compl Submodule.ClosedComplemented.of_isCompl_isClosed
 
-theorem closedComplemented_iff_has_closed_compl :
+alias IsCompl.closedComplemented_of_isClosed := ClosedComplemented.of_isCompl_isClosed
+
+theorem closedComplemented_iff_isClosed_exists_isClosed_isCompl :
     p.ClosedComplemented ↔
-      IsClosed (p : Set E) ∧ ∃ (q : Subspace 𝕜 E) (_ : IsClosed (q : Set E)), IsCompl p q :=
-  ⟨fun h => ⟨h.isClosed, h.has_closed_complement⟩,
-    fun ⟨hp, ⟨_, hq, hpq⟩⟩ => closedComplemented_of_closed_compl hpq hp hq⟩
-#align subspace.closed_complemented_iff_has_closed_compl Subspace.closedComplemented_iff_has_closed_compl
+      IsClosed (p : Set E) ∧ ∃ q : Submodule 𝕜 E, IsClosed (q : Set E) ∧ IsCompl p q :=
+  ⟨fun h => ⟨h.isClosed, h.exists_isClosed_isCompl⟩,
+    fun ⟨hp, ⟨_, hq, hpq⟩⟩ => .of_isCompl_isClosed hpq hp hq⟩
+#align subspace.closed_complemented_iff_has_closed_compl Submodule.closedComplemented_iff_isClosed_exists_isClosed_isCompl
 
-theorem closedComplemented_of_quotient_finiteDimensional [CompleteSpace 𝕜]
+theorem ClosedComplemented.of_quotient_finiteDimensional [CompleteSpace 𝕜]
     [FiniteDimensional 𝕜 (E ⧸ p)] (hp : IsClosed (p : Set E)) : p.ClosedComplemented := by
   obtain ⟨q, hq⟩ : ∃ q, IsCompl p q := p.exists_isCompl
   haveI : FiniteDimensional 𝕜 q := (p.quotientEquivOfIsCompl q hq).finiteDimensional
-  exact closedComplemented_of_closed_compl hq hp q.closed_of_finiteDimensional
-#align subspace.closed_complemented_of_quotient_finite_dimensional Subspace.closedComplemented_of_quotient_finiteDimensional
+  exact .of_isCompl_isClosed hq hp q.closed_of_finiteDimensional
+#align subspace.closed_complemented_of_quotient_finite_dimensional Submodule.ClosedComplemented.of_quotient_finiteDimensional
 
-end Subspace
+end Submodule

Mathlib/Topology/Algebra/Module/Basic.lean

@@ -2672,11 +2672,11 @@ def ClosedComplemented (p : Submodule R M) : Prop :=
   ∃ f : M →L[R] p, ∀ x : p, f x = x
 #align submodule.closed_complemented Submodule.ClosedComplemented
 
-theorem ClosedComplemented.has_closed_complement {p : Submodule R M} [T1Space p]
+theorem ClosedComplemented.exists_isClosed_isCompl {p : Submodule R M} [T1Space p]
     (h : ClosedComplemented p) :
-    ∃ (q : Submodule R M) (_ : IsClosed (q : Set M)), IsCompl p q :=
+    ∃ q : Submodule R M, IsClosed (q : Set M) ∧ IsCompl p q :=
   Exists.elim h fun f hf => ⟨ker f, isClosed_ker f, LinearMap.isCompl_of_proj hf⟩
-#align submodule.closed_complemented.has_closed_complement Submodule.ClosedComplemented.has_closed_complement
+#align submodule.closed_complemented.has_closed_complement Submodule.ClosedComplemented.exists_isClosed_isCompl
 
 protected theorem ClosedComplemented.isClosed [TopologicalAddGroup M] [T1Space M]
     {p : Submodule R M} (h : ClosedComplemented p) : IsClosed (p : Set M) := by
@@ -2695,6 +2695,20 @@ theorem closedComplemented_top : ClosedComplemented (⊤ : Submodule R M) :=
   ⟨(id R M).codRestrict ⊤ fun _x => trivial, fun x => Subtype.ext_iff_val.2 <| by simp⟩
 #align submodule.closed_complemented_top Submodule.closedComplemented_top
 
+/-- 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. -/
+lemma ClosedComplemented.exists_submodule_equiv_prod [TopologicalAddGroup 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, e.symm x = x.1 + x.2) :=
+  let ⟨f, hf⟩ := hp
+  ⟨LinearMap.ker f, .equivOfRightInverse _ p.subtypeL hf,
+    fun _ ↦ by ext <;> simp [hf], fun _ ↦ by ext <;> simp [hf], fun _ ↦ rfl⟩
+
 end Submodule
 
 theorem ContinuousLinearMap.closedComplemented_ker_of_rightInverse {R : Type*} [Ring R]