From b916d59f44e28190425c5d227e8114e2b2c0da53 Mon Sep 17 00:00:00 2001 From: Anatole Dedecker Date: Sat, 5 Nov 2022 17:02:37 +0000 Subject: [PATCH] feat(topology/algebra/module/strong_operator, analysis/normed_space/operator_norm): strong operator topology (#16053) --- src/analysis/convolution.lean | 2 +- .../normed_space/bounded_linear_maps.lean | 4 +- src/analysis/normed_space/multilinear.lean | 4 +- src/analysis/normed_space/operator_norm.lean | 97 ++++++++- .../algebra/module/strong_topology.lean | 193 ++++++++++++++++++ src/topology/vector_bundle/hom.lean | 10 +- 6 files changed, 292 insertions(+), 18 deletions(-) create mode 100644 src/topology/algebra/module/strong_topology.lean diff --git a/src/analysis/convolution.lean b/src/analysis/convolution.lean index dd2bc3236db22..124a5916ebe51 100644 --- a/src/analysis/convolution.lean +++ b/src/analysis/convolution.lean @@ -940,7 +940,7 @@ lemma convolution_precompR_apply {g : G β†’ E'' β†’L[π•œ] E'} (hf : locally_integrable f ΞΌ) (hcg : has_compact_support g) (hg : continuous g) (xβ‚€ : G) (x : E'') : (f ⋆[L.precompR E'', ΞΌ] g) xβ‚€ x = (f ⋆[L, ΞΌ] (Ξ» a, g a x)) xβ‚€ := begin - have := hcg.convolution_exists_right (L.precompR E'') hf hg xβ‚€, + have := hcg.convolution_exists_right (L.precompR E'' : _) hf hg xβ‚€, simp_rw [convolution_def, continuous_linear_map.integral_apply this], refl, end diff --git a/src/analysis/normed_space/bounded_linear_maps.lean b/src/analysis/normed_space/bounded_linear_maps.lean index 2c9f6ffffa049..240db4bf7031f 100644 --- a/src/analysis/normed_space/bounded_linear_maps.lean +++ b/src/analysis/normed_space/bounded_linear_maps.lean @@ -242,7 +242,7 @@ argument of `f`. variables {R : Type*} variables {π•œβ‚‚ π•œ' : Type*} [nontrivially_normed_field π•œ'] [nontrivially_normed_field π•œβ‚‚] variables {M : Type*} [topological_space M] -variables {σ₁₂ : π•œ β†’+* π•œβ‚‚} [ring_hom_isometric σ₁₂] +variables {σ₁₂ : π•œ β†’+* π•œβ‚‚} variables {G' : Type*} [normed_add_comm_group G'] [normed_space π•œβ‚‚ G'] [normed_space π•œ' G'] variables [smul_comm_class π•œβ‚‚ π•œ' G'] @@ -544,7 +544,7 @@ begin refine Ξ» e, is_open.mem_nhds _ (mem_range_self _), let O : (E β†’L[π•œ] F) β†’ (E β†’L[π•œ] E) := Ξ» f, (e.symm : F β†’L[π•œ] E).comp f, have h_O : continuous O := is_bounded_bilinear_map_comp.continuous_right, - convert units.is_open.preimage h_O using 1, + convert show is_open (O ⁻¹' {x | is_unit x}), from units.is_open.preimage h_O using 1, ext f', split, { rintros ⟨e', rfl⟩, diff --git a/src/analysis/normed_space/multilinear.lean b/src/analysis/normed_space/multilinear.lean index 1e9533e449436..95163f6eeffea 100644 --- a/src/analysis/normed_space/multilinear.lean +++ b/src/analysis/normed_space/multilinear.lean @@ -882,8 +882,8 @@ def mk_continuous_linear (f : G β†’β‚—[π•œ] multilinear_map π•œ E G') (C : ℝ G β†’L[π•œ] continuous_multilinear_map π•œ E G' := linear_map.mk_continuous { to_fun := Ξ» x, (f x).mk_continuous (C * βˆ₯xβˆ₯) $ H x, - map_add' := Ξ» x y, by { ext1, simp }, - map_smul' := Ξ» c x, by { ext1, simp } } + map_add' := Ξ» x y, by { ext1, simp only [_root_.map_add], refl }, + map_smul' := Ξ» c x, by { ext1, simp only [smul_hom_class.map_smul], refl } } (max C 0) $ Ξ» x, ((f x).mk_continuous_norm_le' _).trans_eq $ by rw [max_mul_of_nonneg _ _ (norm_nonneg x), zero_mul] diff --git a/src/analysis/normed_space/operator_norm.lean b/src/analysis/normed_space/operator_norm.lean index fc6a658ee48c5..20e53e52c177f 100644 --- a/src/analysis/normed_space/operator_norm.lean +++ b/src/analysis/normed_space/operator_norm.lean @@ -7,6 +7,7 @@ import algebra.algebra.tower import analysis.asymptotics.asymptotics import analysis.normed_space.linear_isometry import analysis.normed_space.riesz_lemma +import topology.algebra.module.strong_topology /-! # Operator norm on the space of continuous linear maps @@ -381,14 +382,99 @@ lemma op_norm_smul_le {π•œ' : Type*} [normed_field π•œ'] [normed_space π•œ' F end)) /-- Continuous linear maps themselves form a seminormed space with respect to - the operator norm. -/ -instance to_seminormed_add_comm_group : seminormed_add_comm_group (E β†’SL[σ₁₂] F) := +the operator norm. This is only a temporary definition because we want to replace the topology +with `continuous_linear_map.topological_space` to avoid diamond issues. +See Note [forgetful inheritance] -/ +protected def tmp_seminormed_add_comm_group : seminormed_add_comm_group (E β†’SL[σ₁₂] F) := add_group_seminorm.to_seminormed_add_comm_group { to_fun := norm, map_zero' := op_norm_zero, add_le' := op_norm_add_le, neg' := op_norm_neg } +/-- The `pseudo_metric_space` structure on `E β†’SL[σ₁₂] F` coming from +`continuous_linear_map.tmp_seminormed_add_comm_group`. +See Note [forgetful inheritance] -/ +protected def tmp_pseudo_metric_space : pseudo_metric_space (E β†’SL[σ₁₂] F) := +continuous_linear_map.tmp_seminormed_add_comm_group.to_pseudo_metric_space + +/-- The `uniform_space` structure on `E β†’SL[σ₁₂] F` coming from +`continuous_linear_map.tmp_seminormed_add_comm_group`. +See Note [forgetful inheritance] -/ +protected def tmp_uniform_space : uniform_space (E β†’SL[σ₁₂] F) := +continuous_linear_map.tmp_pseudo_metric_space.to_uniform_space + +/-- The `topological_space` structure on `E β†’SL[σ₁₂] F` coming from +`continuous_linear_map.tmp_seminormed_add_comm_group`. +See Note [forgetful inheritance] -/ +protected def tmp_topological_space : topological_space (E β†’SL[σ₁₂] F) := +continuous_linear_map.tmp_uniform_space.to_topological_space + +section tmp + +local attribute [-instance] continuous_linear_map.topological_space +local attribute [-instance] continuous_linear_map.uniform_space +local attribute [instance] continuous_linear_map.tmp_seminormed_add_comm_group + +protected lemma tmp_topological_add_group : topological_add_group (E β†’SL[σ₁₂] F) := +infer_instance + +protected lemma tmp_closed_ball_div_subset {a b : ℝ} (ha : 0 < a) (hb : 0 < b) : + closed_ball (0 : E β†’SL[σ₁₂] F) (a / b) βŠ† + {f | βˆ€ x ∈ closed_ball (0 : E) b, f x ∈ closed_ball (0 : F) a} := +begin + intros f hf x hx, + rw mem_closed_ball_zero_iff at ⊒ hf hx, + calc βˆ₯f xβˆ₯ + ≀ βˆ₯fβˆ₯ * βˆ₯xβˆ₯ : le_op_norm _ _ + ... ≀ (a/b) * b : mul_le_mul hf hx (norm_nonneg _) (div_pos ha hb).le + ... = a : div_mul_cancel a hb.ne.symm +end + +end tmp + +protected theorem tmp_topology_eq : + (continuous_linear_map.tmp_topological_space : topological_space (E β†’SL[σ₁₂] F)) = + continuous_linear_map.topological_space := +begin + refine continuous_linear_map.tmp_topological_add_group.ext infer_instance + ((@metric.nhds_basis_closed_ball _ continuous_linear_map.tmp_pseudo_metric_space 0).ext + (continuous_linear_map.has_basis_nhds_zero_of_basis metric.nhds_basis_closed_ball) _ _), + { rcases normed_field.exists_norm_lt_one π•œ with ⟨c, hcβ‚€, hcβ‚βŸ©, + refine Ξ» Ξ΅ hΞ΅, ⟨⟨closed_ball 0 (1 / βˆ₯cβˆ₯), Ρ⟩, + ⟨normed_space.is_vonN_bounded_closed_ball _ _ _, hΡ⟩, Ξ» f hf, _⟩, + change βˆ€ x, _ at hf, + simp_rw mem_closed_ball_zero_iff at hf, + rw @mem_closed_ball_zero_iff _ seminormed_add_comm_group.to_seminormed_add_group, + refine op_norm_le_of_shell' (div_pos one_pos hcβ‚€) hΞ΅.le hc₁ (Ξ» x hx₁ hxc, _), + rw div_mul_cancel 1 hcβ‚€.ne.symm at hx₁, + exact (hf x hxc.le).trans (le_mul_of_one_le_right hΞ΅.le hx₁) }, + { rintros ⟨S, Ρ⟩ ⟨hS, hΡ⟩, + rw [normed_space.is_vonN_bounded_iff, ← bounded_iff_is_bounded] at hS, + rcases hS.subset_ball_lt 0 0 with ⟨δ, hΞ΄, hSδ⟩, + exact ⟨Ρ/Ξ΄, div_pos hΞ΅ hΞ΄, (continuous_linear_map.tmp_closed_ball_div_subset hΞ΅ hΞ΄).trans $ + Ξ» f hf x hx, hf x $ hSΞ΄ hx⟩ } +end + +protected theorem tmp_uniform_space_eq : + (continuous_linear_map.tmp_uniform_space : uniform_space (E β†’SL[σ₁₂] F)) = + continuous_linear_map.uniform_space := +begin + rw [← @uniform_add_group.to_uniform_space_eq _ continuous_linear_map.tmp_uniform_space, + ← @uniform_add_group.to_uniform_space_eq _ continuous_linear_map.uniform_space], + congr' 1, + exact continuous_linear_map.tmp_topology_eq +end + +instance to_pseudo_metric_space : pseudo_metric_space (E β†’SL[σ₁₂] F) := +continuous_linear_map.tmp_pseudo_metric_space.replace_uniformity + (congr_arg _ continuous_linear_map.tmp_uniform_space_eq.symm) + +/-- Continuous linear maps themselves form a seminormed space with respect to + the operator norm. -/ +instance to_seminormed_add_comm_group : seminormed_add_comm_group (E β†’SL[σ₁₂] F) := +{ dist_eq := continuous_linear_map.tmp_seminormed_add_comm_group.dist_eq } + lemma nnnorm_def (f : E β†’SL[σ₁₂] F) : βˆ₯fβˆ₯β‚Š = Inf {c | βˆ€ x, βˆ₯f xβˆ₯β‚Š ≀ c * βˆ₯xβˆ₯β‚Š} := begin ext, @@ -1302,12 +1388,7 @@ instance norm_one_class [nontrivial E] : norm_one_class (E β†’L[π•œ] E) := ⟨n /-- Continuous linear maps themselves form a normed space with respect to the operator norm. -/ instance to_normed_add_comm_group [ring_hom_isometric σ₁₂] : normed_add_comm_group (E β†’SL[σ₁₂] F) := -add_group_norm.to_normed_add_comm_group -{ to_fun := norm, - map_zero' := op_norm_zero, - neg' := op_norm_neg, - add_le' := op_norm_add_le, - eq_zero_of_map_eq_zero' := Ξ» f, (op_norm_zero_iff f).1 } +normed_add_comm_group.of_separation (Ξ» f, (op_norm_zero_iff f).mp) /-- Continuous linear maps form a normed ring with respect to the operator norm. -/ instance to_normed_ring : normed_ring (E β†’L[π•œ] E) := diff --git a/src/topology/algebra/module/strong_topology.lean b/src/topology/algebra/module/strong_topology.lean new file mode 100644 index 0000000000000..a1a9c4df48916 --- /dev/null +++ b/src/topology/algebra/module/strong_topology.lean @@ -0,0 +1,193 @@ +/- +Copyright (c) 2022 Anatole Dedecker. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Anatole Dedecker +-/ +import topology.algebra.uniform_convergence + +/-! +# Strong topologies on the space of continuous linear maps + +In this file, we define the strong topologies on `E β†’L[π•œ] F` associated with a family +`𝔖 : set (set E)` to be the topology of uniform convergence on the elements of `𝔖` (also called +the topology of `𝔖`-convergence). + +The lemma `uniform_convergence_on.has_continuous_smul_of_image_bounded` tells us that this is a +vector space topology if the continuous linear image of any element of `𝔖` is bounded (in the sense +of `bornology.is_vonN_bounded`). + +We then declare an instance for the case where `𝔖` is exactly the set of all bounded subsets of +`E`, giving us the so-called "topology of uniform convergence on bounded sets" (or "topology of +bounded convergence"), which coincides with the operator norm topology in the case of +`normed_space`s. + +Other useful examples include the weak-* topology (when `𝔖` is the set of finite sets or the set +of singletons) and the topology of compact convergence (when `𝔖` is the set of relatively compact +sets). + +## Main definitions + +* `continuous_linear_map.strong_topology` is the topology mentioned above for an arbitrary `𝔖`. +* `continuous_linear_map.topological_space` is the topology of bounded convergence. This is + declared as an instance. + +## Main statements + +* `continuous_linear_map.strong_topology.topological_add_group` and + `continuous_linear_map.strong_topology.has_continuous_smul` show that the strong topology + makes `E β†’L[π•œ] F` a topological vector space, with the assumptions on `𝔖` mentioned above. +* `continuous_linear_map.topological_add_group` and + `continuous_linear_map.has_continuous_smul` register these facts as instances for the special + case of bounded convergence. + +## References + +* [N. Bourbaki, *Topological Vector Spaces*][bourbaki1987] + +## TODO + +* show that these topologies are Tβ‚‚ and locally convex if the topology on `F` is + +## Tags + +uniform convergence, bounded convergence +-/ + +open_locale topological_space + +namespace continuous_linear_map + +section general + +variables {π•œβ‚ π•œβ‚‚ : Type*} [normed_field π•œβ‚] [normed_field π•œβ‚‚] (Οƒ : π•œβ‚ β†’+* π•œβ‚‚) + {E : Type*} (F : Type*) [add_comm_group E] [module π•œβ‚ E] + [add_comm_group F] [module π•œβ‚‚ F] [topological_space E] + +/-- Given `E` and `F` two topological vector spaces and `𝔖 : set (set E)`, then +`strong_topology Οƒ F 𝔖` is the "topology of uniform convergence on the elements of `𝔖`" on +`E β†’L[π•œ] F`. + +If the continuous linear image of any element of `𝔖` is bounded, this makes `E β†’L[π•œ] F` a +topological vector space. -/ +def strong_topology [topological_space F] [topological_add_group F] + (𝔖 : set (set E)) : topological_space (E β†’SL[Οƒ] F) := +(@uniform_convergence_on.topological_space E F + (topological_add_group.to_uniform_space F) 𝔖).induced coe_fn + +/-- The uniform structure associated with `continuous_linear_map.strong_topology`. We make sure +that this has nice definitional properties. -/ +def strong_uniformity [uniform_space F] [uniform_add_group F] + (𝔖 : set (set E)) : uniform_space (E β†’SL[Οƒ] F) := +@uniform_space.replace_topology _ (strong_topology Οƒ F 𝔖) + ((uniform_convergence_on.uniform_space E F 𝔖).comap coe_fn) + (by rw [strong_topology, uniform_add_group.to_uniform_space_eq]; refl) + +@[simp] lemma strong_uniformity_topology_eq [uniform_space F] [uniform_add_group F] + (𝔖 : set (set E)) : + (strong_uniformity Οƒ F 𝔖).to_topological_space = strong_topology Οƒ F 𝔖 := +rfl + +lemma strong_uniformity.uniform_add_group [uniform_space F] [uniform_add_group F] + (𝔖 : set (set E)) : @uniform_add_group (E β†’SL[Οƒ] F) (strong_uniformity Οƒ F 𝔖) _ := +begin + letI : uniform_space (E β†’ F) := uniform_convergence_on.uniform_space E F 𝔖, + letI : uniform_space (E β†’SL[Οƒ] F) := strong_uniformity Οƒ F 𝔖, + haveI : uniform_add_group (E β†’ F) := uniform_convergence_on.uniform_add_group, + rw [strong_uniformity, uniform_space.replace_topology_eq], + let Ο† : (E β†’SL[Οƒ] F) β†’+ E β†’ F := ⟨(coe_fn : (E β†’SL[Οƒ] F) β†’ E β†’ F), rfl, Ξ» _ _, rfl⟩, + exact uniform_add_group_comap Ο† +end + +lemma strong_topology.topological_add_group [topological_space F] [topological_add_group F] + (𝔖 : set (set E)) : @topological_add_group (E β†’SL[Οƒ] F) (strong_topology Οƒ F 𝔖) _ := +begin + letI : uniform_space F := topological_add_group.to_uniform_space F, + haveI : uniform_add_group F := topological_add_comm_group_is_uniform, + letI : uniform_space (E β†’SL[Οƒ] F) := strong_uniformity Οƒ F 𝔖, + haveI : uniform_add_group (E β†’SL[Οƒ] F) := strong_uniformity.uniform_add_group Οƒ F 𝔖, + apply_instance +end + +lemma strong_topology.has_continuous_smul [ring_hom_surjective Οƒ] [ring_hom_isometric Οƒ] + [topological_space F] [topological_add_group F] [has_continuous_smul π•œβ‚‚ F] (𝔖 : set (set E)) + (h𝔖₁ : 𝔖.nonempty) (h𝔖₂ : directed_on (βŠ†) 𝔖) (h𝔖₃ : βˆ€ S ∈ 𝔖, bornology.is_vonN_bounded π•œβ‚ S) : + @has_continuous_smul π•œβ‚‚ (E β†’SL[Οƒ] F) _ _ (strong_topology Οƒ F 𝔖) := +begin + letI : uniform_space F := topological_add_group.to_uniform_space F, + haveI : uniform_add_group F := topological_add_comm_group_is_uniform, + letI : topological_space (E β†’ F) := uniform_convergence_on.topological_space E F 𝔖, + letI : topological_space (E β†’SL[Οƒ] F) := strong_topology Οƒ F 𝔖, + let Ο† : (E β†’SL[Οƒ] F) β†’β‚—[π•œβ‚‚] E β†’ F := ⟨(coe_fn : (E β†’SL[Οƒ] F) β†’ E β†’ F), Ξ» _ _, rfl, Ξ» _ _, rfl⟩, + exact uniform_convergence_on.has_continuous_smul_induced_of_image_bounded π•œβ‚‚ E F (E β†’SL[Οƒ] F) + h𝔖₁ h𝔖₂ Ο† ⟨rfl⟩ (Ξ» u s hs, (h𝔖₃ s hs).image u) +end + +lemma strong_topology.has_basis_nhds_zero_of_basis [topological_space F] [topological_add_group F] + {ΞΉ : Type*} (𝔖 : set (set E)) (h𝔖₁ : 𝔖.nonempty) (h𝔖₂ : directed_on (βŠ†) 𝔖) {p : ΞΉ β†’ Prop} + {b : ΞΉ β†’ set F} (h : (𝓝 0 : filter F).has_basis p b) : + (@nhds (E β†’SL[Οƒ] F) (strong_topology Οƒ F 𝔖) 0).has_basis + (Ξ» Si : set E Γ— ΞΉ, Si.1 ∈ 𝔖 ∧ p Si.2) + (Ξ» Si, {f : E β†’SL[Οƒ] F | βˆ€ x ∈ Si.1, f x ∈ b Si.2}) := +begin + letI : uniform_space F := topological_add_group.to_uniform_space F, + haveI : uniform_add_group F := topological_add_comm_group_is_uniform, + rw nhds_induced, + exact (uniform_convergence_on.has_basis_nhds_zero_of_basis 𝔖 h𝔖₁ h𝔖₂ h).comap coe_fn +end + +lemma strong_topology.has_basis_nhds_zero [topological_space F] [topological_add_group F] + (𝔖 : set (set E)) (h𝔖₁ : 𝔖.nonempty) (h𝔖₂ : directed_on (βŠ†) 𝔖) : + (@nhds (E β†’SL[Οƒ] F) (strong_topology Οƒ F 𝔖) 0).has_basis + (Ξ» SV : set E Γ— set F, SV.1 ∈ 𝔖 ∧ SV.2 ∈ (𝓝 0 : filter F)) + (Ξ» SV, {f : E β†’SL[Οƒ] F | βˆ€ x ∈ SV.1, f x ∈ SV.2}) := +strong_topology.has_basis_nhds_zero_of_basis Οƒ F 𝔖 h𝔖₁ h𝔖₂ (𝓝 0).basis_sets + +end general + +section bounded_sets + +variables {π•œβ‚ π•œβ‚‚ : Type*} [normed_field π•œβ‚] [normed_field π•œβ‚‚] {Οƒ : π•œβ‚ β†’+* π•œβ‚‚} {E F : Type*} + [add_comm_group E] [module π•œβ‚ E] [add_comm_group F] [module π•œβ‚‚ F] [topological_space E] + +/-- The topology of bounded convergence on `E β†’L[π•œ] F`. This coincides with the topology induced by +the operator norm when `E` and `F` are normed spaces. -/ +instance [topological_space F] [topological_add_group F] : topological_space (E β†’SL[Οƒ] F) := +strong_topology Οƒ F {S | bornology.is_vonN_bounded π•œβ‚ S} + +instance [topological_space F] [topological_add_group F] : topological_add_group (E β†’SL[Οƒ] F) := +strong_topology.topological_add_group Οƒ F _ + +instance [ring_hom_surjective Οƒ] [ring_hom_isometric Οƒ] [topological_space F] + [topological_add_group F] [has_continuous_smul π•œβ‚‚ F] : + has_continuous_smul π•œβ‚‚ (E β†’SL[Οƒ] F) := +strong_topology.has_continuous_smul Οƒ F {S | bornology.is_vonN_bounded π•œβ‚ S} + βŸ¨βˆ…, bornology.is_vonN_bounded_empty π•œβ‚ E⟩ + (directed_on_of_sup_mem $ Ξ» _ _, bornology.is_vonN_bounded.union) + (Ξ» s hs, hs) + +instance [uniform_space F] [uniform_add_group F] : uniform_space (E β†’SL[Οƒ] F) := +strong_uniformity Οƒ F {S | bornology.is_vonN_bounded π•œβ‚ S} + +instance [uniform_space F] [uniform_add_group F] : uniform_add_group (E β†’SL[Οƒ] F) := +strong_uniformity.uniform_add_group Οƒ F _ + +protected lemma has_basis_nhds_zero_of_basis [topological_space F] + [topological_add_group F] {ΞΉ : Type*} {p : ΞΉ β†’ Prop} {b : ΞΉ β†’ set F} + (h : (𝓝 0 : filter F).has_basis p b) : + (𝓝 (0 : E β†’SL[Οƒ] F)).has_basis + (Ξ» Si : set E Γ— ΞΉ, bornology.is_vonN_bounded π•œβ‚ Si.1 ∧ p Si.2) + (Ξ» Si, {f : E β†’SL[Οƒ] F | βˆ€ x ∈ Si.1, f x ∈ b Si.2}) := +strong_topology.has_basis_nhds_zero_of_basis Οƒ F + {S | bornology.is_vonN_bounded π•œβ‚ S} βŸ¨βˆ…, bornology.is_vonN_bounded_empty π•œβ‚ E⟩ + (directed_on_of_sup_mem $ Ξ» _ _, bornology.is_vonN_bounded.union) h + +protected lemma has_basis_nhds_zero [topological_space F] + [topological_add_group F] : + (𝓝 (0 : E β†’SL[Οƒ] F)).has_basis + (Ξ» SV : set E Γ— set F, bornology.is_vonN_bounded π•œβ‚ SV.1 ∧ SV.2 ∈ (𝓝 0 : filter 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 + +end bounded_sets + +end continuous_linear_map diff --git a/src/topology/vector_bundle/hom.lean b/src/topology/vector_bundle/hom.lean index a21c54f6ffe81..b2ef1236087a4 100644 --- a/src/topology/vector_bundle/hom.lean +++ b/src/topology/vector_bundle/hom.lean @@ -85,7 +85,6 @@ variables (Fβ‚‚ : Type*) [normed_add_comm_group Fβ‚‚][normed_space π•œβ‚‚ Fβ‚‚] namespace topological_vector_bundle variables {F₁ E₁ Fβ‚‚ Eβ‚‚} (e₁ e₁' : trivialization π•œβ‚ F₁ E₁) (eβ‚‚ eβ‚‚' : trivialization π•œβ‚‚ Fβ‚‚ Eβ‚‚) -variables [ring_hom_isometric Οƒ] namespace pretrivialization @@ -94,7 +93,8 @@ namespace pretrivialization function between the two induced (pre)trivializations `pretrivialization.continuous_linear_map Οƒ e₁ eβ‚‚` and `pretrivialization.continuous_linear_map Οƒ e₁' eβ‚‚'` of `bundle.continuous_linear_map`. -/ -def continuous_linear_map_coord_change (b : B) : (F₁ β†’SL[Οƒ] Fβ‚‚) β†’L[π•œβ‚‚] F₁ β†’SL[Οƒ] Fβ‚‚ := +def continuous_linear_map_coord_change [ring_hom_isometric Οƒ] (b : B) : + (F₁ β†’SL[Οƒ] Fβ‚‚) β†’L[π•œβ‚‚] F₁ β†’SL[Οƒ] Fβ‚‚ := ((e₁'.coord_change e₁ b).symm.arrow_congrSL (eβ‚‚.coord_change eβ‚‚' b) : (F₁ β†’SL[Οƒ] Fβ‚‚) ≃L[π•œβ‚‚] F₁ β†’SL[Οƒ] Fβ‚‚) @@ -102,7 +102,7 @@ variables {Οƒ e₁ e₁' eβ‚‚ eβ‚‚'} variables [Ξ  x : B, topological_space (E₁ x)] [topological_vector_bundle π•œβ‚ F₁ E₁] variables [Ξ  x : B, topological_space (Eβ‚‚ x)] [topological_vector_bundle π•œβ‚‚ Fβ‚‚ Eβ‚‚] -lemma continuous_on_continuous_linear_map_coord_change +lemma continuous_on_continuous_linear_map_coord_change [ring_hom_isometric Οƒ] (he₁ : e₁ ∈ trivialization_atlas π•œβ‚ F₁ E₁) (he₁' : e₁' ∈ trivialization_atlas π•œβ‚ F₁ E₁) (heβ‚‚ : eβ‚‚ ∈ trivialization_atlas π•œβ‚‚ Fβ‚‚ Eβ‚‚) (heβ‚‚' : eβ‚‚' ∈ trivialization_atlas π•œβ‚‚ Fβ‚‚ Eβ‚‚) : continuous_on (continuous_linear_map_coord_change Οƒ e₁ e₁' eβ‚‚ eβ‚‚') @@ -178,7 +178,7 @@ begin rw [symm_apply], refl, exact hb end -lemma continuous_linear_map_coord_change_apply (b : B) +lemma continuous_linear_map_coord_change_apply [ring_hom_isometric Οƒ] (b : B) (hb : b ∈ (e₁.base_set ∩ eβ‚‚.base_set) ∩ (e₁'.base_set ∩ eβ‚‚'.base_set)) (L : F₁ β†’SL[Οƒ] Fβ‚‚) : continuous_linear_map_coord_change Οƒ e₁ e₁' eβ‚‚ eβ‚‚' b L = (continuous_linear_map Οƒ e₁' eβ‚‚' @@ -199,7 +199,7 @@ end end pretrivialization open pretrivialization -variables (F₁ E₁ Fβ‚‚ Eβ‚‚) +variables (F₁ E₁ Fβ‚‚ Eβ‚‚) [ring_hom_isometric Οƒ] variables [Ξ  x : B, topological_space (E₁ x)] [topological_vector_bundle π•œβ‚ F₁ E₁] variables [Ξ  x : B, topological_space (Eβ‚‚ x)] [topological_vector_bundle π•œβ‚‚ Fβ‚‚ Eβ‚‚] variables [Ξ  x, has_continuous_add (Eβ‚‚ x)] [Ξ  x, has_continuous_smul π•œβ‚‚ (Eβ‚‚ x)]