feat(topology/algebra/*, analysis/normed_space/operator_norm): constr…

…uct bundled {monoid_hom, linear_map} from limits of such maps (#10700)

Given a function which is a pointwise limit of {`monoid_hom`, `add_monoid_hom`, `linear_map`} maps, construct a bundled version of the corresponding type with that function as its `to_fun`. Then this construction is used to replace the existing in-proof construction that the continuous linear maps into a banach space is itself complete. 



Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>

src/analysis/normed_space/operator_norm.lean

@@ -1198,20 +1198,7 @@ begin
   -- into a function which we call `G`.
   choose G hG using λv, cauchy_seq_tendsto_of_complete (cau v),
   -- Next, we show that this `G` is linear,
-  let Glin : E →ₛₗ[σ₁₂] F :=
-  { to_fun := G,
-    map_add' := λ v w, begin
-      have A := hG (v + w),
-      have B := (hG v).add (hG w),
-      simp only [map_add] at A B,
-      exact tendsto_nhds_unique A B,
-    end,
-    map_smul' := λ c v, begin
-      have A := hG (c • v),
-      have B := filter.tendsto.smul (@tendsto_const_nhds _ ℕ _ (σ₁₂ c) _) (hG v),
-      simp only [map_smulₛₗ] at A B,
-      exact tendsto_nhds_unique A B
-    end },
+  let Glin : E →ₛₗ[σ₁₂] F := linear_map_of_tendsto _ (tendsto_pi_nhds.mpr hG),
   -- and that `G` has norm at most `(b 0 + ∥f 0∥)`.
   have Gnorm : ∀ v, ∥G v∥ ≤ (b 0 + ∥f 0∥) * ∥v∥,
   { assume v,

src/topology/algebra/module.lean

@@ -250,6 +250,27 @@ notation M ` ≃SL[`:50 σ `] ` M₂ := continuous_linear_equiv σ M M₂
 notation M ` ≃L[`:50 R `] ` M₂ := continuous_linear_equiv (ring_hom.id R) M M₂
 notation M ` ≃L⋆[`:50 R `] ` M₂ := continuous_linear_equiv (@star_ring_aut R _ _ : R →+* R) M M₂
 
+section pointwise_limits
+
+variables
+{M₁ M₂ α R S : Type*}
+[topological_space M₂] [t2_space M₂] [semiring R] [semiring S]
+[add_comm_monoid M₁] [add_comm_monoid M₂] [module R M₁] [module S M₂]
+[topological_space S] [has_continuous_smul S M₂] [has_continuous_add M₂]
+{σ : R →+* S} {l : filter α} {f : M₁ → M₂}
+
+/-- Construct a bundled linear map from a pointwise limit of linear maps -/
+@[simps] def linear_map_of_tendsto (g : α → M₁ →ₛₗ[σ] M₂) [l.ne_bot]
+  (h : tendsto (λ a x, g a x) l (𝓝 f)) : M₁ →ₛₗ[σ] M₂ :=
+{ to_fun := f,
+  map_smul' := λ r x, by
+    { rw tendsto_pi_nhds at h,
+      refine tendsto_nhds_unique (h (r • x)) _,
+      simpa only [linear_map.map_smulₛₗ] using tendsto.smul tendsto_const_nhds (h x) },
+  .. add_monoid_hom_of_tendsto (λ a, (g a).to_add_monoid_hom) h }
+
+end pointwise_limits
+
 namespace continuous_linear_map
 
 section semiring

src/topology/algebra/monoid.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Mario Carneiro
 -/
 import topology.continuous_on
+import topology.separation
 import group_theory.submonoid.operations
 import algebra.group.prod
 import algebra.pointwise
@@ -159,6 +160,28 @@ end
 
 end has_continuous_mul
 
+section pointwise_limits
+
+variables {M₁ M₂ : Type*} [topological_space M₂] [t2_space M₂] {l : filter α} {f : M₁ → M₂}
+
+/-- Construct a bundled monoid homomorphism from a pointwise limit of
+monoid homomorphisms -/
+@[to_additive "Construct a bundled additive monoid homomorphism from
+a pointwise limit of monoid homomorphisms", simps]
+def monoid_hom_of_tendsto [monoid M₁] [monoid M₂]
+  [has_continuous_mul M₂] (g : α → M₁ →* M₂) [l.ne_bot]
+  (h : tendsto (λ a x, g a x) l (𝓝 f)) : M₁ →* M₂ :=
+{ to_fun := f,
+  map_one' := by
+    { refine tendsto_nhds_unique (tendsto_pi_nhds.mp h 1) _,
+      simpa only [monoid_hom.map_one] using tendsto_const_nhds },
+  map_mul' := λ x y, by
+    { rw tendsto_pi_nhds at h,
+      refine tendsto_nhds_unique (h (x * y)) _,
+      simpa only [monoid_hom.map_mul] using (h x).mul (h y) } }
+
+end pointwise_limits
+
 namespace submonoid
 
 @[to_additive] instance [topological_space α] [monoid α] [has_continuous_mul α] (S : submonoid α) :