feat: port Topology.VectorBundle.Hom (leanprover-community#4514)

qawbecrdtey · Jul 7, 2023 · 228cd34 · 228cd34
1 parent f3d17f2
commit 228cd34
Show file tree

Hide file tree

Showing 4 changed files with 346 additions and 3 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -3280,6 +3280,7 @@ import Mathlib.Topology.UrysohnsBounded
 import Mathlib.Topology.UrysohnsLemma
 import Mathlib.Topology.VectorBundle.Basic
 import Mathlib.Topology.VectorBundle.Constructions
+import Mathlib.Topology.VectorBundle.Hom
 import Mathlib.Util.AddRelatedDecl
 import Mathlib.Util.AssertExists
 import Mathlib.Util.AssertNoSorry

diff --git a/Mathlib/Analysis/Convolution.lean b/Mathlib/Analysis/Convolution.lean
@@ -1528,7 +1528,7 @@ theorem contDiffOn_convolution_right_with_param {f : G → E} {n : ℕ∞} (L :
     ext1 a
     simp only [(· ∘ ·), ContinuousLinearEquiv.apply_symm_apply, coe_comp',
       ContinuousLinearEquiv.prod_apply, ContinuousLinearEquiv.map_sub,
-      ContinuousLinearEquiv.arrowCongr, ContinuousLinearEquiv.arrowCongrSL_symm_apply_toFun,
+      ContinuousLinearEquiv.arrowCongr, ContinuousLinearEquiv.arrowCongrSL_symm_apply,
       ContinuousLinearEquiv.coe_coe, Function.comp_apply, ContinuousLinearEquiv.apply_symm_apply,
       LinearEquiv.invFun_eq_symm, ContinuousLinearEquiv.arrowCongrₛₗ_symm_apply, eq_self_iff_true]
   simp_rw [this] at A

diff --git a/Mathlib/Topology/Algebra/Module/StrongTopology.lean b/Mathlib/Topology/Algebra/Module/StrongTopology.lean
@@ -59,7 +59,7 @@ uniform convergence, bounded convergence
 -/
 
 
-open Topology UniformConvergence
+open scoped Topology UniformConvergence
 
 namespace ContinuousLinearMap
 
@@ -261,6 +261,8 @@ def arrowCongrₛₗ (e₁₂ : E ≃SL[σ₁₂] F) (e₄₃ : H ≃SL[σ₄₃
     map_add' := fun f g => by simp only [add_comp, comp_add]
     map_smul' := fun t f => by simp only [smul_comp, comp_smulₛₗ] }
 #align continuous_linear_equiv.arrow_congrₛₗ ContinuousLinearEquiv.arrowCongrₛₗ
+#align continuous_linear_equiv.arrow_congrₛₗ_apply ContinuousLinearEquiv.arrowCongrₛₗ_apply
+#align continuous_linear_equiv.arrow_congrₛₗ_symm_apply ContinuousLinearEquiv.arrowCongrₛₗ_symm_apply
 
 variable [RingHomIsometric σ₂₁]
 
@@ -282,13 +284,19 @@ variable [RingHomIsometric σ₁₂]
 
 /-- A pair of continuous (semi)linear equivalences generates a continuous (semi)linear equivalence
 between the spaces of continuous (semi)linear maps. -/
-@[simps!]
+@[simps! apply symm_apply toLinearEquiv]
 def arrowCongrSL (e₁₂ : E ≃SL[σ₁₂] F) (e₄₃ : H ≃SL[σ₄₃] G) : (E →SL[σ₁₄] H) ≃SL[σ₄₃] F →SL[σ₂₃] G :=
   { e₁₂.arrowCongrₛₗ e₄₃ with
     continuous_toFun := e₁₂.arrowCongrₛₗ_continuous e₄₃
     continuous_invFun := e₁₂.symm.arrowCongrₛₗ_continuous e₄₃.symm }
 set_option linter.uppercaseLean3 false in
 #align continuous_linear_equiv.arrow_congrSL ContinuousLinearEquiv.arrowCongrSL
+set_option linter.uppercaseLean3 false in
+#align continuous_linear_equiv.arrow_congrSL_apply ContinuousLinearEquiv.arrowCongrSL_apply
+set_option linter.uppercaseLean3 false in
+#align continuous_linear_equiv.arrow_congrSL_symm_apply ContinuousLinearEquiv.arrowCongrSL_symm_apply
+set_option linter.uppercaseLean3 false in
+#align continuous_linear_equiv.arrow_congrSL_to_linear_equiv ContinuousLinearEquiv.arrowCongrSL_toLinearEquiv
 
 end Semilinear