From c57a78f1e6e36f9af9e045f226de6c084db40e63 Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Sun, 27 Oct 2024 20:54:24 +0000
Subject: [PATCH] feat(Topology/Algebra): generalize `CompleteSpace` instances
 (#17244)

---
 .../Algebra/Module/Alternating/Topology.lean  | 17 +++++-
 Mathlib/Topology/Algebra/Module/Basic.lean    | 10 ++++
 .../Algebra/Module/Multilinear/Topology.lean  | 34 ++++++++---
 .../Algebra/Module/StrongTopology.lean        | 59 +++++++++++++++----
 4 files changed, 102 insertions(+), 18 deletions(-)

diff --git a/Mathlib/Topology/Algebra/Module/Alternating/Topology.lean b/Mathlib/Topology/Algebra/Module/Alternating/Topology.lean
index 61776f9e7c9c2..6002b8905bc13 100644
--- a/Mathlib/Topology/Algebra/Module/Alternating/Topology.lean
+++ b/Mathlib/Topology/Algebra/Module/Alternating/Topology.lean
@@ -77,13 +77,28 @@ instance instUniformContinuousConstSMul {M : Type*}
     UniformContinuousConstSMul M (E [⋀^ι]→L[𝕜] F) :=
   isUniformEmbedding_toContinuousMultilinearMap.uniformContinuousConstSMul fun _ _ ↦ rfl
 
+theorem isUniformInducing_postcomp {G : Type*} [AddCommGroup G] [UniformSpace G] [UniformAddGroup G]
+    [Module 𝕜 G] (g : F →L[𝕜] G) (hg : IsUniformInducing g) :
+    IsUniformInducing (g.compContinuousAlternatingMap : (E [⋀^ι]→L[𝕜] F) → (E [⋀^ι]→L[𝕜] G)) := by
+  rw [← isUniformEmbedding_toContinuousMultilinearMap.1.of_comp_iff]
+  exact (ContinuousMultilinearMap.isUniformInducing_postcomp g hg).comp
+    isUniformEmbedding_toContinuousMultilinearMap.1
+
 section CompleteSpace
 
-variable [ContinuousSMul 𝕜 E] [ContinuousConstSMul 𝕜 F] [CompleteSpace F] [T2Space F]
+variable [ContinuousSMul 𝕜 E] [ContinuousConstSMul 𝕜 F] [CompleteSpace F]
 
 open UniformOnFun in
 theorem completeSpace (h : RestrictGenTopology {s : Set (ι → E) | IsVonNBounded 𝕜 s}) :
     CompleteSpace (E [⋀^ι]→L[𝕜] F) := by
+  wlog hF : T2Space F generalizing F
+  · rw [(isUniformInducing_postcomp (SeparationQuotient.mkCLM _ _)
+      SeparationQuotient.isUniformInducing_mk).completeSpace_congr]
+    · exact this inferInstance
+    · intro f
+      use (SeparationQuotient.outCLM _ _).compContinuousAlternatingMap f
+      ext
+      simp
   have := ContinuousMultilinearMap.completeSpace (F := F) h
   rw [completeSpace_iff_isComplete_range
     isUniformEmbedding_toContinuousMultilinearMap.isUniformInducing]
diff --git a/Mathlib/Topology/Algebra/Module/Basic.lean b/Mathlib/Topology/Algebra/Module/Basic.lean
index fbc19334443c1..70d2d820610b9 100644
--- a/Mathlib/Topology/Algebra/Module/Basic.lean
+++ b/Mathlib/Topology/Algebra/Module/Basic.lean
@@ -429,6 +429,16 @@ theorem coe_copy (f : M₁ →SL[σ₁₂] M₂) (f' : M₁ → M₂) (h : f' =
 theorem copy_eq (f : M₁ →SL[σ₁₂] M₂) (f' : M₁ → M₂) (h : f' = ⇑f) : f.copy f' h = f :=
   DFunLike.ext' h
 
+theorem range_coeFn_eq :
+    Set.range ((⇑) : (M₁ →SL[σ₁₂] M₂) → (M₁ → M₂)) =
+      {f | Continuous f} ∩ Set.range ((⇑) : (M₁ →ₛₗ[σ₁₂] M₂) → (M₁ → M₂)) := by
+  ext f
+  constructor
+  · rintro ⟨f, rfl⟩
+    exact ⟨f.continuous, f, rfl⟩
+  · rintro ⟨hfc, f, rfl⟩
+    exact ⟨⟨f, hfc⟩, rfl⟩
+
 -- make some straightforward lemmas available to `simp`.
 protected theorem map_zero (f : M₁ →SL[σ₁₂] M₂) : f (0 : M₁) = 0 :=
   map_zero f
diff --git a/Mathlib/Topology/Algebra/Module/Multilinear/Topology.lean b/Mathlib/Topology/Algebra/Module/Multilinear/Topology.lean
index 19af25db016c5..87d86ced20d2e 100644
--- a/Mathlib/Topology/Algebra/Module/Multilinear/Topology.lean
+++ b/Mathlib/Topology/Algebra/Module/Multilinear/Topology.lean
@@ -5,6 +5,7 @@ Authors: Yury Kudryashov
 -/
 import Mathlib.Topology.Algebra.Module.Multilinear.Bounded
 import Mathlib.Topology.Algebra.Module.UniformConvergence
+import Mathlib.Topology.Algebra.SeparationQuotient.Section
 import Mathlib.Topology.Hom.ContinuousEvalConst
 
 /-!
@@ -66,15 +67,20 @@ section UniformAddGroup
 
 variable [UniformSpace F] [UniformAddGroup F]
 
+lemma isUniformInducing_toUniformOnFun :
+    IsUniformInducing (toUniformOnFun :
+      ContinuousMultilinearMap 𝕜 E F → ((Π i, E i) →ᵤ[{s | IsVonNBounded 𝕜 s}] F)) := ⟨rfl⟩
+
 lemma isUniformEmbedding_toUniformOnFun :
-    IsUniformEmbedding (toUniformOnFun : ContinuousMultilinearMap 𝕜 E F → _) where
-  inj := DFunLike.coe_injective
-  comap_uniformity := rfl
+    IsUniformEmbedding (toUniformOnFun : ContinuousMultilinearMap 𝕜 E F → _) :=
+  ⟨isUniformInducing_toUniformOnFun, DFunLike.coe_injective⟩
 
 @[deprecated (since := "2024-10-01")]
 alias uniformEmbedding_toUniformOnFun := isUniformEmbedding_toUniformOnFun
 
-lemma embedding_toUniformOnFun : Embedding (toUniformOnFun : ContinuousMultilinearMap 𝕜 E F → _) :=
+lemma embedding_toUniformOnFun :
+    Embedding (toUniformOnFun : ContinuousMultilinearMap 𝕜 E F →
+      ((Π i, E i) →ᵤ[{s | IsVonNBounded 𝕜 s}] F)) :=
   isUniformEmbedding_toUniformOnFun.embedding
 
 theorem uniformContinuous_coe_fun [∀ i, ContinuousSMul 𝕜 (E i)] :
@@ -97,19 +103,33 @@ instance instUniformContinuousConstSMul {M : Type*}
   haveI := uniformContinuousConstSMul_of_continuousConstSMul M F
   isUniformEmbedding_toUniformOnFun.uniformContinuousConstSMul fun _ _ ↦ rfl
 
+theorem isUniformInducing_postcomp
+    {G : Type*} [AddCommGroup G] [UniformSpace G] [UniformAddGroup G] [Module 𝕜 G]
+    (g : F →L[𝕜] G) (hg : IsUniformInducing g) :
+    IsUniformInducing (g.compContinuousMultilinearMap :
+      ContinuousMultilinearMap 𝕜 E F → ContinuousMultilinearMap 𝕜 E G) := by
+  rw [← isUniformInducing_toUniformOnFun.of_comp_iff]
+  exact (UniformOnFun.postcomp_isUniformInducing hg).comp isUniformInducing_toUniformOnFun
+
 section CompleteSpace
 
-variable [∀ i, ContinuousSMul 𝕜 (E i)] [ContinuousConstSMul 𝕜 F] [CompleteSpace F] [T2Space F]
+variable [∀ i, ContinuousSMul 𝕜 (E i)] [ContinuousConstSMul 𝕜 F] [CompleteSpace F]
 
 open UniformOnFun in
 theorem completeSpace (h : RestrictGenTopology {s : Set (Π i, E i) | IsVonNBounded 𝕜 s}) :
     CompleteSpace (ContinuousMultilinearMap 𝕜 E F) := by
   classical
+  wlog hF : T2Space F generalizing F
+  · rw [(isUniformInducing_postcomp (SeparationQuotient.mkCLM _ _)
+      SeparationQuotient.isUniformInducing_mk).completeSpace_congr]
+    · exact this inferInstance
+    · intro f
+      use (SeparationQuotient.outCLM _ _).compContinuousMultilinearMap f
+      simp [DFunLike.ext_iff]
   have H : ∀ {m : Π i, E i},
       Continuous fun f : (Π i, E i) →ᵤ[{s | IsVonNBounded 𝕜 s}] F ↦ toFun _ f m :=
     (uniformContinuous_eval (isVonNBounded_covers) _).continuous
-  rw [completeSpace_iff_isComplete_range isUniformEmbedding_toUniformOnFun.isUniformInducing,
-    range_toUniformOnFun]
+  rw [completeSpace_iff_isComplete_range isUniformInducing_toUniformOnFun, range_toUniformOnFun]
   simp only [setOf_and, setOf_forall]
   apply_rules [IsClosed.isComplete, IsClosed.inter]
   · exact UniformOnFun.isClosed_setOf_continuous h
diff --git a/Mathlib/Topology/Algebra/Module/StrongTopology.lean b/Mathlib/Topology/Algebra/Module/StrongTopology.lean
index 3132c5f3d16b8..40a009bdf15e6 100644
--- a/Mathlib/Topology/Algebra/Module/StrongTopology.lean
+++ b/Mathlib/Topology/Algebra/Module/StrongTopology.lean
@@ -1,9 +1,10 @@
 /-
 Copyright (c) 2022 Anatole Dedecker. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Anatole Dedecker
+Authors: Anatole Dedecker, Yury Kudryashov
 -/
 import Mathlib.Topology.Algebra.Module.UniformConvergence
+import Mathlib.Topology.Algebra.SeparationQuotient.Section
 import Mathlib.Topology.Hom.ContinuousEvalConst
 
 /-!
@@ -55,7 +56,6 @@ sets).
 uniform convergence, bounded convergence
 -/
 
-
 open scoped Topology UniformConvergence Uniformity
 open Filter Set Function Bornology
 
@@ -75,17 +75,16 @@ uniform convergence on the elements of `𝔖`".
 If the continuous linear image of any element of `𝔖` is bounded, this makes `E →SL[σ] F` a
 topological vector space. -/
 @[nolint unusedArguments]
-def UniformConvergenceCLM [TopologicalSpace F] [TopologicalAddGroup F] (_ : Set (Set E)) :=
-  E →SL[σ] F
+def UniformConvergenceCLM [TopologicalSpace F] (_ : Set (Set E)) := E →SL[σ] F
 
 namespace UniformConvergenceCLM
 
-instance instFunLike [TopologicalSpace F] [TopologicalAddGroup F]
-    (𝔖 : Set (Set E)) : FunLike (UniformConvergenceCLM σ F 𝔖) E F :=
+instance instFunLike [TopologicalSpace F] (𝔖 : Set (Set E)) :
+    FunLike (UniformConvergenceCLM σ F 𝔖) E F :=
   ContinuousLinearMap.funLike
 
-instance instContinuousSemilinearMapClass [TopologicalSpace F] [TopologicalAddGroup F]
-    (𝔖 : Set (Set E)) : ContinuousSemilinearMapClass (UniformConvergenceCLM σ F 𝔖) σ E F :=
+instance instContinuousSemilinearMapClass [TopologicalSpace F] (𝔖 : Set (Set E)) :
+    ContinuousSemilinearMapClass (UniformConvergenceCLM σ F 𝔖) σ E F :=
   ContinuousLinearMap.continuousSemilinearMapClass
 
 instance instTopologicalSpace [TopologicalSpace F] [TopologicalAddGroup F] (𝔖 : Set (Set E)) :
@@ -120,9 +119,13 @@ theorem uniformity_toTopologicalSpace_eq [UniformSpace F] [UniformAddGroup F] (
       UniformConvergenceCLM.instTopologicalSpace σ F 𝔖 :=
   rfl
 
+theorem isUniformInducing_coeFn [UniformSpace F] [UniformAddGroup F] (𝔖 : Set (Set E)) :
+    IsUniformInducing (α := UniformConvergenceCLM σ F 𝔖) (UniformOnFun.ofFun 𝔖 ∘ DFunLike.coe) :=
+  ⟨rfl⟩
+
 theorem isUniformEmbedding_coeFn [UniformSpace F] [UniformAddGroup F] (𝔖 : Set (Set E)) :
     IsUniformEmbedding (α := UniformConvergenceCLM σ F 𝔖) (UniformOnFun.ofFun 𝔖 ∘ DFunLike.coe) :=
-  ⟨⟨rfl⟩, DFunLike.coe_injective⟩
+  ⟨isUniformInducing_coeFn .., DFunLike.coe_injective⟩
 
 @[deprecated (since := "2024-10-01")]
 alias uniformEmbedding_coeFn := isUniformEmbedding_coeFn
@@ -262,7 +265,7 @@ instance instUniformContinuousConstSMul (M : Type*)
     [Monoid M] [DistribMulAction M F] [SMulCommClass 𝕜₂ M F]
     [UniformSpace F] [UniformAddGroup F] [UniformContinuousConstSMul M F] (𝔖 : Set (Set E)) :
     UniformContinuousConstSMul M (UniformConvergenceCLM σ F 𝔖) :=
-  (isUniformEmbedding_coeFn σ F 𝔖).isUniformInducing.uniformContinuousConstSMul fun _ _ ↦ by rfl
+  (isUniformInducing_coeFn σ F 𝔖).uniformContinuousConstSMul fun _ _ ↦ by rfl
 
 instance instContinuousConstSMul (M : Type*)
     [Monoid M] [DistribMulAction M F] [SMulCommClass 𝕜₂ M F]
@@ -280,6 +283,32 @@ theorem tendsto_iff_tendstoUniformlyOn {ι : Type*} {p : Filter ι} [UniformSpac
   rw [(embedding_coeFn σ F 𝔖).tendsto_nhds_iff, UniformOnFun.tendsto_iff_tendstoUniformlyOn]
   rfl
 
+variable {F} in
+theorem isUniformInducing_postcomp
+    {G : Type*} [AddCommGroup G] [UniformSpace G] [UniformAddGroup G]
+    {𝕜₃ : Type*} [NormedField 𝕜₃] [Module 𝕜₃ G]
+    {τ : 𝕜₂ →+* 𝕜₃} {ρ : 𝕜₁ →+* 𝕜₃} [RingHomCompTriple σ τ ρ] [UniformSpace F] [UniformAddGroup F]
+    (g : F →SL[τ] G) (hg : IsUniformInducing g) (𝔖 : Set (Set E)) :
+    IsUniformInducing (α := UniformConvergenceCLM σ F 𝔖) (β := UniformConvergenceCLM ρ G 𝔖)
+      g.comp := by
+  rw [← (isUniformInducing_coeFn _ _ _).of_comp_iff]
+  exact (UniformOnFun.postcomp_isUniformInducing hg).comp (isUniformInducing_coeFn _ _ _)
+
+theorem completeSpace [UniformSpace F] [UniformAddGroup F] [ContinuousSMul 𝕜₂ F] [CompleteSpace F]
+    {𝔖 : Set (Set E)} (h𝔖 : RestrictGenTopology 𝔖) (h𝔖U : ⋃₀ 𝔖 = univ) :
+    CompleteSpace (UniformConvergenceCLM σ F 𝔖) := by
+  wlog hF : T2Space F generalizing F
+  · rw [(isUniformInducing_postcomp σ (SeparationQuotient.mkCLM 𝕜₂ F)
+      SeparationQuotient.isUniformInducing_mk _).completeSpace_congr]
+    exacts [this _ inferInstance, SeparationQuotient.postcomp_mkCLM_surjective F σ E]
+  rw [completeSpace_iff_isComplete_range (isUniformInducing_coeFn _ _ _)]
+  apply IsClosed.isComplete
+  have H₁ : IsClosed {f : E →ᵤ[𝔖] F | Continuous ((UniformOnFun.toFun 𝔖) f)} :=
+    UniformOnFun.isClosed_setOf_continuous h𝔖
+  convert H₁.inter <| (LinearMap.isClosed_range_coe E F σ).preimage
+    (UniformOnFun.uniformContinuous_toFun h𝔖U).continuous
+  exact ContinuousLinearMap.range_coeFn_eq
+
 variable {𝔖₁ 𝔖₂ : Set (Set E)}
 
 theorem uniformSpace_mono [UniformSpace F] [UniformAddGroup F] (h : 𝔖₂ ⊆ 𝔖₁) :
@@ -415,6 +444,16 @@ theorem isVonNBounded_iff {R : Type*} [NormedDivisionRing R]
       ∀ s, IsVonNBounded 𝕜₁ s → IsVonNBounded R (Set.image2 (fun f x ↦ f x) S s) :=
   UniformConvergenceCLM.isVonNBounded_iff
 
+theorem completeSpace [UniformSpace F] [UniformAddGroup F] [ContinuousSMul 𝕜₂ F] [CompleteSpace F]
+    [ContinuousSMul 𝕜₁ E] (h : RestrictGenTopology {s : Set E | IsVonNBounded 𝕜₁ s}) :
+    CompleteSpace (E →SL[σ] F) :=
+  UniformConvergenceCLM.completeSpace _ _ h isVonNBounded_covers
+
+instance instCompleteSpace [TopologicalAddGroup E] [ContinuousSMul 𝕜₁ E] [SequentialSpace E]
+    [UniformSpace F] [UniformAddGroup F] [ContinuousSMul 𝕜₂ F] [CompleteSpace F] :
+    CompleteSpace (E →SL[σ] F) :=
+  completeSpace <| .of_seq fun _ _ h ↦ (h.isVonNBounded_range 𝕜₁).insert _
+
 variable (G) [TopologicalSpace F] [TopologicalSpace G]
 
 /-- Pre-composition by a *fixed* continuous linear map as a continuous linear map.