feat(topology/algebra/module/strong_topology): golf arrow_congrSL introduced in #19107 (#19128)

ADedecker · ADedecker · commit 8905e5ed9085 · 2023-07-06T13:05:39.000Z
I added more general definitions `precomp` and `postcomp` for expressing that (pre/post)-composing by a *fixed* continuous linear maps is continuous. These were planned about a year ago when I defined the strong topology and follow from [uniform_on_fun.precomp_uniform_continuous](https://leanprover-community.github.io/mathlib_docs/topology/uniform_space/uniform_convergence_topology.html#uniform_on_fun.precomp_uniform_continuous) and [uniform_on_fun.postcomp_uniform_continuous](https://leanprover-community.github.io/mathlib_docs/topology/uniform_space/uniform_convergence_topology.html#uniform_on_fun.postcomp_uniform_continuous). The proof of continuity of `arrow_congrSL` is a direct consequence of these, so we don't have to do it by hand. This is not really a "golf" since I added more lines than I removed, but these more general constructions will be needed at some point anyway (my use case was distribution theory) so I'm doing some proactive golfing 😄.
diff --git a/src/analysis/convolution.lean b/src/analysis/convolution.lean
@@ -1500,9 +1500,7 @@ begin
     simp only [ef, eg, comp_app, continuous_linear_equiv.apply_symm_apply, coe_comp',
       continuous_linear_equiv.prod_apply, continuous_linear_equiv.map_sub,
       continuous_linear_equiv.arrow_congr, continuous_linear_equiv.arrow_congrSL_symm_apply,
-      continuous_linear_equiv.coe_coe, comp_app, continuous_linear_equiv.apply_symm_apply,
-      linear_equiv.inv_fun_eq_symm, continuous_linear_equiv.arrow_congrₛₗ_symm_apply,
-      eq_self_iff_true] },
+      continuous_linear_equiv.coe_coe, comp_app, continuous_linear_equiv.apply_symm_apply ] },
   simp_rw [this] at A,
   exact A,
 end
diff --git a/src/geometry/manifold/vector_bundle/hom.lean b/src/geometry/manifold/vector_bundle/hom.lean
@@ -70,7 +70,7 @@ begin
     simp only [continuous_linear_map_coord_change, continuous_linear_equiv.coe_coe,
       continuous_linear_equiv.arrow_congrSL_apply, comp_apply, function.comp, compL_apply,
       flip_apply, continuous_linear_equiv.symm_symm, linear_equiv.to_fun_eq_coe,
-      continuous_linear_equiv.arrow_congrₛₗ_apply, continuous_linear_map.coe_comp'] },
+      continuous_linear_map.coe_comp'] },
 end
 
 include _i₁ _i₂
diff --git a/src/topology/algebra/module/strong_topology.lean b/src/topology/algebra/module/strong_topology.lean
@@ -175,9 +175,12 @@ end general
 
 section bounded_sets
 
-variables {𝕜₁ 𝕜₂ : Type*} [normed_field 𝕜₁] [normed_field 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E E' F F' : Type*}
+variables {𝕜₁ 𝕜₂ 𝕜₃ : Type*} [normed_field 𝕜₁] [normed_field 𝕜₂] [normed_field 𝕜₃]
+  {σ : 𝕜₁ →+* 𝕜₂} {τ : 𝕜₂ →+* 𝕜₃} {ρ : 𝕜₁ →+* 𝕜₃} [ring_hom_comp_triple σ τ ρ]
+  {E E' F F' G : Type*}
   [add_comm_group E] [module 𝕜₁ E] [add_comm_group E'] [module ℝ E']
   [add_comm_group F] [module 𝕜₂ F] [add_comm_group F'] [module ℝ F']
+  [add_comm_group G] [module 𝕜₃ G]
   [topological_space E]
 
 /-- The topology of bounded convergence on `E →L[𝕜] F`. This coincides with the topology induced by
@@ -224,6 +227,49 @@ protected lemma has_basis_nhds_zero [topological_space F]
     (λ SV, {f : E →SL[σ] F | ∀ x ∈ SV.1, f x ∈ SV.2}) :=
 continuous_linear_map.has_basis_nhds_zero_of_basis (𝓝 0).basis_sets
 
+variables (G) [topological_space F] [topological_space G]
+
+/-- Pre-composition by a *fixed* continuous linear map as a continuous linear map.
+Note that in non-normed space it is not always true that composition is continuous
+in both variables, so we have to fix one of them. -/
+@[simps] def precomp [topological_add_group G] [has_continuous_const_smul 𝕜₃ G]
+  [ring_hom_surjective σ] [ring_hom_isometric σ] (L : E →SL[σ] F) :
+  (F →SL[τ] G) →L[𝕜₃] (E →SL[ρ] G) :=
+{ to_fun := λ f, f.comp L,
+  map_add' := λ f g, add_comp f g L,
+  map_smul' := λ a f, smul_comp a f L,
+  cont :=
+  begin
+    letI : uniform_space G := topological_add_group.to_uniform_space G,
+    haveI : uniform_add_group G := topological_add_comm_group_is_uniform,
+    rw (strong_topology.embedding_coe_fn _ _ _).continuous_iff,
+    refine (uniform_on_fun.precomp_uniform_continuous _).continuous.comp
+      (strong_topology.embedding_coe_fn _ _ _).continuous,
+    exact λ S hS, hS.image L,
+  end }
+
+variables (E) {G}
+
+/-- Post-composition by a *fixed* continuous linear map as a continuous linear map.
+Note that in non-normed space it is not always true that composition is continuous
+in both variables, so we have to fix one of them. -/
+@[simps] def postcomp [topological_add_group F] [topological_add_group G]
+  [has_continuous_const_smul 𝕜₃ G] [has_continuous_const_smul 𝕜₂ F] (L : F →SL[τ] G) :
+  (E →SL[σ] F) →SL[τ] (E →SL[ρ] G) :=
+{ to_fun := λ f, L.comp f,
+  map_add' := comp_add L,
+  map_smul' := comp_smulₛₗ L,
+  cont :=
+  begin
+    letI : uniform_space G := topological_add_group.to_uniform_space G,
+    haveI : uniform_add_group G := topological_add_comm_group_is_uniform,
+    letI : uniform_space F := topological_add_group.to_uniform_space F,
+    haveI : uniform_add_group F := topological_add_comm_group_is_uniform,
+    rw (strong_topology.embedding_coe_fn _ _ _).continuous_iff,
+    exact (uniform_on_fun.postcomp_uniform_continuous L.uniform_continuous).continuous.comp
+      (strong_topology.embedding_coe_fn _ _ _).continuous
+  end }
+
 end bounded_sets
 
 end continuous_linear_map
@@ -249,49 +295,29 @@ variables {𝕜 : Type*} {𝕜₂ : Type*} {𝕜₃ : Type*} {𝕜₄ : Type*}
     [ring_hom_inv_pair σ₄₃ σ₃₄]
   [ring_hom_comp_triple σ₂₁ σ₁₄ σ₂₄] [ring_hom_comp_triple σ₂₄ σ₄₃ σ₂₃]
     [ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃] [ring_hom_comp_triple σ₁₃ σ₃₄ σ₁₄]
+    [ring_hom_comp_triple σ₂₃ σ₃₄ σ₂₄] [ring_hom_comp_triple σ₁₂ σ₂₄ σ₁₄]
+  [ring_hom_isometric σ₁₂] [ring_hom_isometric σ₂₁]
 
 include σ₁₄ σ₂₄ σ₁₃ σ₃₄ σ₂₁ σ₂₃
 
 /-- A pair of continuous (semi)linear equivalences generates a (semi)linear equivalence between the
 spaces of continuous (semi)linear maps. -/
-@[simps] def arrow_congrₛₗ (e₁₂ : E ≃SL[σ₁₂] F) (e₄₃ : H ≃SL[σ₄₃] G) :
-  (E →SL[σ₁₄] H) ≃ₛₗ[σ₄₃] (F →SL[σ₂₃] G) :=
+@[simps] def arrow_congrSL (e₁₂ : E ≃SL[σ₁₂] F) (e₄₃ : H ≃SL[σ₄₃] G) :
+  (E →SL[σ₁₄] H) ≃SL[σ₄₃] (F →SL[σ₂₃] G) :=
 { -- given explicitly to help `simps`
   to_fun := λ L, (e₄₃ : H →SL[σ₄₃] G).comp (L.comp (e₁₂.symm : F →SL[σ₂₁] E)),
   -- given explicitly to help `simps`
   inv_fun := λ L, (e₄₃.symm : G →SL[σ₃₄] H).comp (L.comp (e₁₂ : E →SL[σ₁₂] F)),
   map_add' := λ f g, by rw [add_comp, comp_add],
   map_smul' := λ t f, by rw [smul_comp, comp_smulₛₗ],
+  continuous_to_fun :=
+    ((postcomp F e₄₃.to_continuous_linear_map).comp
+      (precomp H e₁₂.symm.to_continuous_linear_map)).continuous,
+  continuous_inv_fun :=
+    ((precomp H e₁₂.to_continuous_linear_map).comp
+      (postcomp F e₄₃.symm.to_continuous_linear_map)).continuous,
   .. e₁₂.arrow_congr_equiv e₄₃, }
 
-variables [ring_hom_isometric σ₂₁]
-
-lemma arrow_congrₛₗ_continuous (e₁₂ : E ≃SL[σ₁₂] F) (e₄₃ : H ≃SL[σ₄₃] G) :
-  continuous (id (e₁₂.arrow_congrₛₗ e₄₃ : (E →SL[σ₁₄] H) ≃ₛₗ[σ₄₃] (F →SL[σ₂₃] G))) :=
-begin
-  apply continuous_of_continuous_at_zero,
-  show filter.tendsto _ _ _,
-  simp_rw [(e₁₂.arrow_congrₛₗ e₄₃).map_zero],
-  rw continuous_linear_map.has_basis_nhds_zero.tendsto_iff
-    continuous_linear_map.has_basis_nhds_zero,
-  rintros ⟨sF, sG⟩ ⟨h1 : bornology.is_vonN_bounded 𝕜₂ sF, h2 : sG ∈ nhds (0:G)⟩,
-  dsimp,
-  refine ⟨(e₁₂.symm '' sF, e₄₃ ⁻¹' sG), ⟨h1.image (e₁₂.symm : F →SL[σ₂₁] E), _⟩,
-    λ _ h _ hx, h _ (set.mem_image_of_mem _ hx)⟩,
-  apply e₄₃.continuous.continuous_at,
-  simpa using h2,
-end
-
-variables [ring_hom_isometric σ₁₂]
-
-/-- A pair of continuous (semi)linear equivalences generates an continuous (semi)linear equivalence
-between the spaces of continuous (semi)linear maps. -/
-@[simps] def arrow_congrSL (e₁₂ : E ≃SL[σ₁₂] F) (e₄₃ : H ≃SL[σ₄₃] G) :
-  (E →SL[σ₁₄] H) ≃SL[σ₄₃] (F →SL[σ₂₃] G) :=
-{ continuous_to_fun := e₁₂.arrow_congrₛₗ_continuous e₄₃,
-  continuous_inv_fun := e₁₂.symm.arrow_congrₛₗ_continuous e₄₃.symm,
-  .. e₁₂.arrow_congrₛₗ e₄₃, }
-
 end semilinear
 
 section linear
diff --git a/src/topology/vector_bundle/hom.lean b/src/topology/vector_bundle/hom.lean
@@ -110,9 +110,8 @@ begin
   { mfld_set_tac },
   { intros b hb, ext L v,
     simp only [continuous_linear_map_coord_change, continuous_linear_equiv.coe_coe,
-      continuous_linear_equiv.arrow_congrₛₗ_apply, linear_equiv.to_fun_eq_coe, coe_comp',
-      continuous_linear_equiv.arrow_congrSL_apply, comp_apply, function.comp, compSL_apply,
-      flip_apply, continuous_linear_equiv.symm_symm] },
+      continuous_linear_equiv.arrow_congrSL_apply,
+      comp_apply, function.comp, compSL_apply, flip_apply, continuous_linear_equiv.symm_symm] },
 end
 
 omit iσ
@@ -206,8 +205,7 @@ lemma continuous_linear_map_coord_change_apply (b : B)
 begin
   ext v,
   simp_rw [continuous_linear_map_coord_change, continuous_linear_equiv.coe_coe,
-    continuous_linear_equiv.arrow_congrSL_apply, linear_equiv.to_fun_eq_coe,
-    continuous_linear_equiv.arrow_congrₛₗ_apply,
+    continuous_linear_equiv.arrow_congrSL_apply,
     continuous_linear_map_apply, continuous_linear_map_symm_apply' σ e₁ e₂ hb.1,
     comp_apply, continuous_linear_equiv.coe_coe, continuous_linear_equiv.symm_symm,
     trivialization.continuous_linear_map_at_apply, trivialization.symmL_apply],
