Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - feat: port Topology.VectorBundle.Hom #4514

Closed
wants to merge 6 commits into from
Closed

[Merged by Bors] - feat: port Topology.VectorBundle.Hom #4514

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
d1d8217
feat: port Topology.VectorBundle.Hom
urkud Jul 5, 2023
4d798cf
Initial file copy from mathport
urkud Jul 5, 2023
9d26946
automated fixes
urkud Jul 5, 2023
35b571f
Fix compile
urkud Jul 5, 2023
ee29f32
auto+manual: naming
urkud Jul 5, 2023
41077b9
Long line, fix compile
urkud Jul 5, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions Mathlib.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3279,6 +3279,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
Expand Down
2 changes: 1 addition & 1 deletion Mathlib/Analysis/Convolution.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
12 changes: 10 additions & 2 deletions Mathlib/Topology/Algebra/Module/StrongTopology.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -59,7 +59,7 @@ uniform convergence, bounded convergence
-/


open Topology UniformConvergence
open scoped Topology UniformConvergence

namespace ContinuousLinearMap

Expand Down Expand Up @@ -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 σ₂₁]

Expand All @@ -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

Expand Down
Loading
Loading