[Merged by Bors] - feat(Topology/Algebra/Module/ModuleTopology): finite products of modules.

Mathlib/Topology/Algebra/Module/ModuleTopology.lean

@@ -413,4 +413,83 @@ lemma _root_.ModuleTopology.eq_coinduced_of_surjective
 
 end surjection
 
+section Prod
+
+variable {R : Type*} [TopologicalSpace R] [Semiring R]
+variable {M : Type*} [AddCommMonoid M] [Module R M] [TopologicalSpace M] [IsModuleTopology R M]
+variable {N : Type*} [AddCommMonoid N] [Module R N] [TopologicalSpace N] [IsModuleTopology R N]
+
+/-- The product of the module topologies for two modules over a topological ring
+is the module topology. -/
+instance instProd : IsModuleTopology R (M × N) := by
+  constructor
+  have : ContinuousAdd M := toContinuousAdd R M
+  have : ContinuousAdd N := toContinuousAdd R N
+  -- In this proof, `M × N` always denotes the product with its *product* topology.
+  -- Addition `(M × N)² → M × N` and scalar multiplication `R × (M × N) → M × N`
+  -- are continuous for the product topology (by results in the library), so the module topology
+  -- on `M × N` is finer than the product topology (as it's the Inf of such topologies).
+  -- It thus remains to show that the product topology is finer than the module topology.
+  refine le_antisymm ?_ <| sInf_le ⟨Prod.continuousSMul, Prod.continuousAdd⟩
+  -- Or equivalently, if `P` denotes `M × N` with the module topology,
+  let P := M × N
+  let τP : TopologicalSpace P := moduleTopology R P
+  have : IsModuleTopology R P := ⟨rfl⟩
+  have : ContinuousAdd P := ModuleTopology.continuousAdd R P
+  -- and if `i` denotes the identity map from `M × N` to `P`
+  let i : M × N → P := id
+  -- then we need to show that `i` is continuous.
+  rw [← continuous_id_iff_le]
+  change @Continuous (M × N) P instTopologicalSpaceProd τP i
+  -- But `i` can be written as (m, n) ↦ (m, 0) + (0, n)
+  -- or equivalently as i₁ ∘ pr₁ + i₂ ∘ pr₂, where prᵢ are the projections,
+  -- the iⱼ's are linear inclusions M → P and N → P, and the addition is P × P → P.
+  let i₁ : M →ₗ[R] P := LinearMap.inl R M N
+  let i₂ : N →ₗ[R] P := LinearMap.inr R M N
+  rw [show (i : M × N → P) =
+       (fun abcd ↦ abcd.1 + abcd.2 : P × P → P) ∘
+       (fun ab ↦ (i₁ ab.1,i₂ ab.2)) by
+       ext ⟨a, b⟩ <;> aesop]
+  -- and these maps are all continuous, hence `i` is too
+  fun_prop
+
+end Prod
+
+section Pi
+
+variable {R : Type*} [TopologicalSpace R] [Semiring R]
+variable {ι : Type*} [Finite ι] {A : ι → Type*} [∀ i, AddCommMonoid (A i)]
+  [∀ i, Module R (A i)] [∀ i, TopologicalSpace (A i)]
+  [∀ i, IsModuleTopology R (A i)]
+
+/-- The product of the module topologies for a finite family of modules over a topological ring
+is the module topology. -/
+instance instPi : IsModuleTopology R (∀ i, A i) := by
+  -- This is an easy induction on the size of the finite type, given the result
+  -- for binary products above. We use a "decategorified" induction principle for finite types.
+  induction ι using Finite.induction_empty_option
+  · -- invariance under equivalence of the finite type we're taking the product over
+    case of_equiv X Y e _ _ _ _ _ =>
+    exact iso (ContinuousLinearEquiv.piCongrLeft R A e)
+  · -- empty case
+    infer_instance
+  · -- "inductive step" is to check for product over `Option ι` case when known for product over `ι`
+    case h_option ι _ hind _ _ _ _ =>
+    -- `Option ι` is a `Sum` of `ι` and `Unit`
+    let e : Option ι ≃ ι ⊕ Unit := Equiv.optionEquivSumPUnit ι
+    -- so suffices to check for a product of modules over `ι ⊕ Unit`
+    suffices IsModuleTopology R ((i' : ι ⊕ Unit) → A (e.symm i')) from iso (.piCongrLeft R A e.symm)
+    -- but such a product is isomorphic to a binary product
+    -- of (product over `ι`) and (product over `Unit`)
+    suffices IsModuleTopology R
+      (((s : ι) → A (e.symm (Sum.inl s))) × ((t : Unit) → A (e.symm (Sum.inr t)))) from
+      iso (ContinuousLinearEquiv.sumPiEquivProdPi R ι Unit _).symm
+    -- The product over `ι` has the module topology by the inductive hypothesis,
+    -- and the product over `Unit` is just a module which is assumed to have the module topology
+    have := iso (ContinuousLinearEquiv.piUnique R (fun t ↦ A (e.symm (Sum.inr t)))).symm
+    -- so the result follows from the previous lemma (binary products).
+    infer_instance
+
+end Pi
+
 end IsModuleTopology