From 22a9066dbd977d5b1122d23975b0bb9e6cd9f6c6 Mon Sep 17 00:00:00 2001
From: Anatole Dedecker <anatolededecker@gmail.com>
Date: Fri, 9 Sep 2022 16:10:08 +0000
Subject: [PATCH] feat(topology/algebra/module/weak_dual): `weak_space` is
 functorial (#16441)

---
 src/topology/algebra/module/weak_dual.lean | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)

diff --git a/src/topology/algebra/module/weak_dual.lean b/src/topology/algebra/module/weak_dual.lean
index 122106d3c27f9..627aa29f3062c 100644
--- a/src/topology/algebra/module/weak_dual.lean
+++ b/src/topology/algebra/module/weak_dual.lean
@@ -248,6 +248,22 @@ def weak_space (𝕜 E) [comm_semiring 𝕜] [topological_space 𝕜] [has_conti
   [has_continuous_const_smul 𝕜 𝕜] [add_comm_monoid E] [module 𝕜 E] [topological_space E] :=
 weak_bilin (top_dual_pairing 𝕜 E).flip
 
+namespace weak_space
+
+variables {𝕜 E F} [add_comm_monoid F] [module 𝕜 F] [topological_space F]
+
+/-- A continuous linear map from `E` to `F` is still continuous when `E` and `F` are equipped with
+their weak topologies. -/
+def map (f : E →L[𝕜] F) :
+  weak_space 𝕜 E →L[𝕜] weak_space 𝕜 F :=
+{ cont := weak_bilin.continuous_of_continuous_eval _ (λ l, weak_bilin.eval_continuous _ (l ∘L f)),
+  ..f }
+
+lemma map_apply (f : E →L[𝕜] F) (x : E) : weak_space.map f x = f x := rfl
+@[simp] lemma coe_map (f : E →L[𝕜] F) : (weak_space.map f : E → F) = f := rfl
+
+end weak_space
+
 theorem tendsto_iff_forall_eval_tendsto_top_dual_pairing
   {l : filter α} {f : α → weak_dual 𝕜 E} {x : weak_dual 𝕜 E} :
   tendsto f l (𝓝 x) ↔