feat(Topology/Algebra/Module): Add more theorems for IsModuleTopology (leanprover-community#24527)

Add theorems that surjective linear maps to the module topology are open.
Add IsModuleTopology instance for quotients.
Add IsModuleTopology instance for finite dimensional T2 vector spaces over a complete normed field and use it to shorten some proofs.



Co-authored-by: Oliver Nash <github@olivernash.org>
Co-authored-by: Oliver Nash <7734364+ocfnash@users.noreply.github.com>

Author: 2 people

Mathlib/Analysis/Fourier/AddCircleMulti.lean

@@ -152,6 +152,11 @@ theorem coeFn_mFourierLp (p : ℝ≥0∞) [Fact (1 ≤ p)] (n : d → ℤ) :
     mFourierLp p n =ᵐ[volume] mFourier n :=
   ContinuousMap.coeFn_toLp volume (mFourier n)
 
+-- shortcut instance: avoids `synthInstance.maxHeartbeats` issue in `span_mFourierLp_closure_eq_top`
+instance {p : ℝ≥0∞} [Fact (1 ≤ p)] :
+    ContinuousSMul ℂ (Lp ℂ p (volume : Measure (UnitAddTorus d))) :=
+  inferInstance
+
 /-- For each `1 ≤ p < ∞`, the linear span of the monomials `mFourier n` is dense in the `Lᵖ` space
 of functions on `UnitAddTorus d`. -/
 theorem span_mFourierLp_closure_eq_top {p : ℝ≥0∞} [Fact (1 ≤ p)] (hp : p ≠ ∞) :

Mathlib/Analysis/RCLike/Lemmas.lean

@@ -60,8 +60,9 @@ variable [NormedAddCommGroup E] [NormedSpace K E]
 This is not an instance because it would cause a search for `FiniteDimensional ?x E` before
 `RCLike ?x`. -/
 theorem proper_rclike [FiniteDimensional K E] : ProperSpace E := by
-  letI : NormedSpace ℝ E := RestrictScalars.normedSpace ℝ K E
-  letI : FiniteDimensional ℝ E := FiniteDimensional.trans ℝ K E
+  -- Using `have` not `let` since it is only existence of `NormedSpace` structure that we need.
+  have : NormedSpace ℝ E := RestrictScalars.normedSpace ℝ K E
+  have : FiniteDimensional ℝ E := FiniteDimensional.trans ℝ K E
   infer_instance
 
 variable {E}

Mathlib/Topology/Algebra/Module/FiniteDimension.lean

@@ -8,6 +8,7 @@ import Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
 import Mathlib.LinearAlgebra.FreeModule.Finite.Matrix
 import Mathlib.RingTheory.LocalRing.Basic
 import Mathlib.Topology.Algebra.Module.Determinant
+import Mathlib.Topology.Algebra.Module.ModuleTopology
 import Mathlib.Topology.Algebra.Module.Simple
 import Mathlib.Topology.Algebra.SeparationQuotient.FiniteDimensional
 
@@ -238,23 +239,26 @@ private theorem continuous_equivFun_basis_aux [T2Space E] {ι : Type v} [Fintype
     change Continuous (ξ.coord i)
     exact H₂ (ξ.coord i)
 
-/-- Any linear map on a finite dimensional space over a complete field is continuous. -/
-theorem LinearMap.continuous_of_finiteDimensional [T2Space E] [FiniteDimensional 𝕜 E]
-    (f : E →ₗ[𝕜] F') : Continuous f := by
+/-- A finite-dimensional t2 vector space over a complete field must carry the module topology.
+
+Not declared as a global instance only for performance reasons. -/
+@[local instance]
+lemma isModuleTopologyOfFiniteDimensional [T2Space E] [FiniteDimensional 𝕜 E] :
+    IsModuleTopology 𝕜 E :=
   -- for the proof, go to a model vector space `b → 𝕜` thanks to `continuous_equivFun_basis`, and
-  -- argue that all linear maps there are continuous.
+  -- use that it has the module topology
   let b := Basis.ofVectorSpace 𝕜 E
-  have A : Continuous b.equivFun := continuous_equivFun_basis_aux b
-  have B : Continuous (f.comp (b.equivFun.symm : (Basis.ofVectorSpaceIndex 𝕜 E → 𝕜) →ₗ[𝕜] E)) :=
-    LinearMap.continuous_on_pi _
-  have :
-    Continuous
-      (f.comp (b.equivFun.symm : (Basis.ofVectorSpaceIndex 𝕜 E → 𝕜) →ₗ[𝕜] E) ∘ b.equivFun) :=
-    B.comp A
-  convert this
-  ext x
-  dsimp
-  rw [Basis.equivFun_symm_apply, Basis.sum_repr]
+  have continuousEquiv : E ≃L[𝕜] (Basis.ofVectorSpaceIndex 𝕜 E) → 𝕜 :=
+    { __ := b.equivFun
+      continuous_toFun := continuous_equivFun_basis_aux b
+      continuous_invFun := IsModuleTopology.continuous_of_linearMap (R := 𝕜)
+        (A := (Basis.ofVectorSpaceIndex 𝕜 E) → 𝕜) (B := E) b.equivFun.symm }
+  IsModuleTopology.iso continuousEquiv.symm
+
+/-- Any linear map on a finite dimensional space over a complete field is continuous. -/
+theorem LinearMap.continuous_of_finiteDimensional [T2Space E] [FiniteDimensional 𝕜 E]
+    (f : E →ₗ[𝕜] F') : Continuous f :=
+  IsModuleTopology.continuous_of_linearMap f
 
 instance LinearMap.continuousLinearMapClassOfFiniteDimensional [T2Space E] [FiniteDimensional 𝕜 E] :
     ContinuousLinearMapClass (E →ₗ[𝕜] F') 𝕜 E F' :=
@@ -322,15 +326,8 @@ theorem range_toContinuousLinearMap (f : E →ₗ[𝕜] F') :
 
 /-- A surjective linear map `f` with finite dimensional codomain is an open map. -/
 theorem isOpenMap_of_finiteDimensional (f : F →ₗ[𝕜] E) (hf : Function.Surjective f) :
-    IsOpenMap f := by
-  obtain ⟨g, hg⟩ := f.exists_rightInverse_of_surjective (LinearMap.range_eq_top.2 hf)
-  refine IsOpenMap.of_sections fun x => ⟨fun y => g (y - f x) + x, ?_, ?_, fun y => ?_⟩
-  · exact
-      ((g.continuous_of_finiteDimensional.comp <| continuous_id.sub continuous_const).add
-          continuous_const).continuousAt
-  · simp only
-    rw [sub_self, map_zero, zero_add]
-  · simp only [map_sub, map_add, ← comp_apply f g, hg, id_apply, sub_add_cancel]
+    IsOpenMap f :=
+  IsModuleTopology.isOpenMap_of_surjective hf
 
 instance canLiftContinuousLinearMap : CanLift (E →ₗ[𝕜] F) (E →L[𝕜] F) (↑) fun _ => True :=
   ⟨fun f _ => ⟨LinearMap.toContinuousLinearMap f, rfl⟩⟩

Mathlib/Topology/Algebra/Module/ModuleTopology.lean

@@ -6,6 +6,7 @@ Authors: Kevin Buzzard, Will Sawin
 import Mathlib.Topology.Algebra.Module.Equiv
 import Mathlib.RingTheory.Finiteness.Cardinality
 import Mathlib.Algebra.Algebra.Bilinear
+import Mathlib.Algebra.Group.Basic
 
 /-!
 # A "module topology" for modules over a topological ring
@@ -414,13 +415,39 @@ theorem isQuotientMap_of_surjective [τB : TopologicalSpace B] [IsModuleTopology
       rw [← (IsOpenQuotientMap.prodMap hφo hφo).continuous_comp_iff, hφ2]
       exact Continuous.comp hφo.continuous hA
 
+/-- A linear surjection between modules with the module topology is an open quotient map. -/
+theorem isOpenQuotientMap_of_surjective [TopologicalSpace B] [IsModuleTopology R B]
+    {φ : A →ₗ[R] B} (hφ : Function.Surjective φ) :
+    IsOpenQuotientMap φ :=
+  have := toContinuousAdd R A
+  AddMonoidHom.isOpenQuotientMap_of_isQuotientMap <| isQuotientMap_of_surjective hφ
+
+omit [IsModuleTopology R A] in
+/-- A linear surjection to a module with the module topology is open. -/
+theorem isOpenMap_of_surjective [TopologicalSpace B] [IsModuleTopology R B]
+    [ContinuousAdd A] [ContinuousSMul R A] {φ : A →ₗ[R] B} (hφ : Function.Surjective φ) :
+    IsOpenMap φ := by
+  have hOpenMap :=
+    letI : TopologicalSpace A := moduleTopology R A
+    have : IsModuleTopology R A := ⟨rfl⟩
+    isOpenQuotientMap_of_surjective hφ |>.isOpenMap
+  intro U hU
+  exact hOpenMap U <| moduleTopology_le R A U hU
+
 lemma _root_.ModuleTopology.eq_coinduced_of_surjective
     {φ : A →ₗ[R] B} (hφ : Function.Surjective φ) :
     moduleTopology R B = TopologicalSpace.coinduced φ inferInstance := by
   letI : TopologicalSpace B := moduleTopology R B
   haveI : IsModuleTopology R B := ⟨rfl⟩
   exact (isQuotientMap_of_surjective hφ).eq_coinduced
 
+instance instQuot (S : Submodule R A) : IsModuleTopology R (A ⧸ S) := by
+  constructor
+  have := toContinuousAdd R A
+  have quot := (Submodule.isOpenQuotientMap_mkQ S).isQuotientMap.eq_coinduced
+  have module := ModuleTopology.eq_coinduced_of_surjective <| Submodule.mkQ_surjective S
+  rw [quot, module]
+
 end surjection
 
 section Prod