Skip to content

Commit ce6df01

Browse files
committed
feat: port Topology.VectorBundle.Hom (#4514)
1 parent 99ec98e commit ce6df01

File tree

4 files changed

+346
-3
lines changed

4 files changed

+346
-3
lines changed

Mathlib.lean

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3279,6 +3279,7 @@ import Mathlib.Topology.UrysohnsBounded
32793279
import Mathlib.Topology.UrysohnsLemma
32803280
import Mathlib.Topology.VectorBundle.Basic
32813281
import Mathlib.Topology.VectorBundle.Constructions
3282+
import Mathlib.Topology.VectorBundle.Hom
32823283
import Mathlib.Util.AddRelatedDecl
32833284
import Mathlib.Util.AssertExists
32843285
import Mathlib.Util.AssertNoSorry

Mathlib/Analysis/Convolution.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1528,7 +1528,7 @@ theorem contDiffOn_convolution_right_with_param {f : G → E} {n : ℕ∞} (L :
15281528
ext1 a
15291529
simp only [(· ∘ ·), ContinuousLinearEquiv.apply_symm_apply, coe_comp',
15301530
ContinuousLinearEquiv.prod_apply, ContinuousLinearEquiv.map_sub,
1531-
ContinuousLinearEquiv.arrowCongr, ContinuousLinearEquiv.arrowCongrSL_symm_apply_toFun,
1531+
ContinuousLinearEquiv.arrowCongr, ContinuousLinearEquiv.arrowCongrSL_symm_apply,
15321532
ContinuousLinearEquiv.coe_coe, Function.comp_apply, ContinuousLinearEquiv.apply_symm_apply,
15331533
LinearEquiv.invFun_eq_symm, ContinuousLinearEquiv.arrowCongrₛₗ_symm_apply, eq_self_iff_true]
15341534
simp_rw [this] at A

Mathlib/Topology/Algebra/Module/StrongTopology.lean

Lines changed: 10 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -59,7 +59,7 @@ uniform convergence, bounded convergence
5959
-/
6060

6161

62-
open Topology UniformConvergence
62+
open scoped Topology UniformConvergence
6363

6464
namespace ContinuousLinearMap
6565

@@ -261,6 +261,8 @@ def arrowCongrₛₗ (e₁₂ : E ≃SL[σ₁₂] F) (e₄₃ : H ≃SL[σ₄₃
261261
map_add' := fun f g => by simp only [add_comp, comp_add]
262262
map_smul' := fun t f => by simp only [smul_comp, comp_smulₛₗ] }
263263
#align continuous_linear_equiv.arrow_congrₛₗ ContinuousLinearEquiv.arrowCongrₛₗ
264+
#align continuous_linear_equiv.arrow_congrₛₗ_apply ContinuousLinearEquiv.arrowCongrₛₗ_apply
265+
#align continuous_linear_equiv.arrow_congrₛₗ_symm_apply ContinuousLinearEquiv.arrowCongrₛₗ_symm_apply
264266

265267
variable [RingHomIsometric σ₂₁]
266268

@@ -282,13 +284,19 @@ variable [RingHomIsometric σ₁₂]
282284

283285
/-- A pair of continuous (semi)linear equivalences generates a continuous (semi)linear equivalence
284286
between the spaces of continuous (semi)linear maps. -/
285-
@[simps!]
287+
@[simps! apply symm_apply toLinearEquiv]
286288
def arrowCongrSL (e₁₂ : E ≃SL[σ₁₂] F) (e₄₃ : H ≃SL[σ₄₃] G) : (E →SL[σ₁₄] H) ≃SL[σ₄₃] F →SL[σ₂₃] G :=
287289
{ e₁₂.arrowCongrₛₗ e₄₃ with
288290
continuous_toFun := e₁₂.arrowCongrₛₗ_continuous e₄₃
289291
continuous_invFun := e₁₂.symm.arrowCongrₛₗ_continuous e₄₃.symm }
290292
set_option linter.uppercaseLean3 false in
291293
#align continuous_linear_equiv.arrow_congrSL ContinuousLinearEquiv.arrowCongrSL
294+
set_option linter.uppercaseLean3 false in
295+
#align continuous_linear_equiv.arrow_congrSL_apply ContinuousLinearEquiv.arrowCongrSL_apply
296+
set_option linter.uppercaseLean3 false in
297+
#align continuous_linear_equiv.arrow_congrSL_symm_apply ContinuousLinearEquiv.arrowCongrSL_symm_apply
298+
set_option linter.uppercaseLean3 false in
299+
#align continuous_linear_equiv.arrow_congrSL_to_linear_equiv ContinuousLinearEquiv.arrowCongrSL_toLinearEquiv
292300

293301
end Semilinear
294302

0 commit comments

Comments
 (0)