From 63702c043a52b66f7f64e069a307f6d11afd0a9d Mon Sep 17 00:00:00 2001 From: Moritz Doll Date: Tue, 28 Mar 2023 13:57:39 +1100 Subject: [PATCH 1/4] generalize to semilinear maps --- .../locally_convex/strong_topology.lean | 27 ++++++++++--------- 1 file changed, 15 insertions(+), 12 deletions(-) diff --git a/src/analysis/locally_convex/strong_topology.lean b/src/analysis/locally_convex/strong_topology.lean index 79306e7a3b0ac..2dbb2d4419350 100644 --- a/src/analysis/locally_convex/strong_topology.lean +++ b/src/analysis/locally_convex/strong_topology.lean @@ -27,22 +27,25 @@ locally convex, bounded convergence open_locale topology uniform_convergence -variables {E F : Type*} +variables {π•œ π•œβ‚‚ E F : Type*} namespace continuous_linear_map +variables [add_comm_group E] [topological_space E] + [add_comm_group F] [topological_space F] [topological_add_group F] + section general -variables [add_comm_group E] [module ℝ E] [topological_space E] - [add_comm_group F] [module ℝ F] [topological_space F] [topological_add_group F] - [has_continuous_const_smul ℝ F] [locally_convex_space ℝ F] +variables [normed_field π•œ] [normed_field π•œβ‚‚] [module π•œ E] [module π•œβ‚‚ F] {σ₁₂ : π•œ β†’+* π•œβ‚‚} +variables [module ℝ E] [module ℝ F] [has_continuous_const_smul ℝ F] [locally_convex_space ℝ F] + [smul_comm_class π•œβ‚‚ ℝ F] lemma strong_topology.locally_convex_space (𝔖 : set (set E)) (h𝔖₁ : 𝔖.nonempty) (h𝔖₂ : directed_on (βŠ†) 𝔖) : - @locally_convex_space ℝ (E β†’L[ℝ] F) _ _ _ (strong_topology (ring_hom.id ℝ) F 𝔖) := + @locally_convex_space ℝ (E β†’SL[σ₁₂] F) _ _ _ (strong_topology σ₁₂ F 𝔖) := begin - letI : topological_space (E β†’L[ℝ] F) := strong_topology (ring_hom.id ℝ) F 𝔖, - haveI : topological_add_group (E β†’L[ℝ] F) := strong_topology.topological_add_group _ _ _, + letI : topological_space (E β†’SL[σ₁₂] F) := strong_topology σ₁₂ F 𝔖, + haveI : topological_add_group (E β†’SL[σ₁₂] F) := strong_topology.topological_add_group _ _ _, refine locally_convex_space.of_basis_zero _ _ _ _ (strong_topology.has_basis_nhds_zero_of_basis _ _ _ h𝔖₁ h𝔖₂ (locally_convex_space.convex_basis_zero ℝ F)) _, @@ -54,12 +57,12 @@ end general section bounded_sets -variables [add_comm_group E] [module ℝ E] [topological_space E] - [add_comm_group F] [module ℝ F] [topological_space F] [topological_add_group F] - [has_continuous_const_smul ℝ F] [locally_convex_space ℝ F] +variables [normed_field π•œ] [normed_field π•œβ‚‚] [module π•œ E] [module π•œβ‚‚ F] {σ₁₂ : π•œ β†’+* π•œβ‚‚} +variables [module ℝ E] [module ℝ F] [has_continuous_const_smul ℝ F] [locally_convex_space ℝ F] + [smul_comm_class π•œβ‚‚ ℝ F] -instance : locally_convex_space ℝ (E β†’L[ℝ] F) := -strong_topology.locally_convex_space _ βŸ¨βˆ…, bornology.is_vonN_bounded_empty ℝ E⟩ +instance : locally_convex_space ℝ (E β†’SL[σ₁₂] F) := +strong_topology.locally_convex_space _ βŸ¨βˆ…, bornology.is_vonN_bounded_empty π•œ E⟩ (directed_on_of_sup_mem $ Ξ» _ _, bornology.is_vonN_bounded.union) end bounded_sets From dbec8ed06fb8a0672549a9d5038c7394a520dcd9 Mon Sep 17 00:00:00 2001 From: Moritz Doll Date: Tue, 28 Mar 2023 14:14:53 +1100 Subject: [PATCH 2/4] variable names --- src/analysis/locally_convex/strong_topology.lean | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/src/analysis/locally_convex/strong_topology.lean b/src/analysis/locally_convex/strong_topology.lean index 2dbb2d4419350..49d10b7920373 100644 --- a/src/analysis/locally_convex/strong_topology.lean +++ b/src/analysis/locally_convex/strong_topology.lean @@ -27,7 +27,7 @@ locally convex, bounded convergence open_locale topology uniform_convergence -variables {π•œ π•œβ‚‚ E F : Type*} +variables {π•œβ‚ π•œβ‚‚ E F : Type*} namespace continuous_linear_map @@ -36,16 +36,16 @@ variables [add_comm_group E] [topological_space E] section general -variables [normed_field π•œ] [normed_field π•œβ‚‚] [module π•œ E] [module π•œβ‚‚ F] {σ₁₂ : π•œ β†’+* π•œβ‚‚} +variables [normed_field π•œβ‚] [normed_field π•œβ‚‚] [module π•œβ‚ E] [module π•œβ‚‚ F] {Οƒ : π•œβ‚ β†’+* π•œβ‚‚} variables [module ℝ E] [module ℝ F] [has_continuous_const_smul ℝ F] [locally_convex_space ℝ F] [smul_comm_class π•œβ‚‚ ℝ F] lemma strong_topology.locally_convex_space (𝔖 : set (set E)) (h𝔖₁ : 𝔖.nonempty) (h𝔖₂ : directed_on (βŠ†) 𝔖) : - @locally_convex_space ℝ (E β†’SL[σ₁₂] F) _ _ _ (strong_topology σ₁₂ F 𝔖) := + @locally_convex_space ℝ (E β†’SL[Οƒ] F) _ _ _ (strong_topology Οƒ F 𝔖) := begin - letI : topological_space (E β†’SL[σ₁₂] F) := strong_topology σ₁₂ F 𝔖, - haveI : topological_add_group (E β†’SL[σ₁₂] F) := strong_topology.topological_add_group _ _ _, + letI : topological_space (E β†’SL[Οƒ] F) := strong_topology Οƒ F 𝔖, + haveI : topological_add_group (E β†’SL[Οƒ] F) := strong_topology.topological_add_group _ _ _, refine locally_convex_space.of_basis_zero _ _ _ _ (strong_topology.has_basis_nhds_zero_of_basis _ _ _ h𝔖₁ h𝔖₂ (locally_convex_space.convex_basis_zero ℝ F)) _, @@ -57,12 +57,12 @@ end general section bounded_sets -variables [normed_field π•œ] [normed_field π•œβ‚‚] [module π•œ E] [module π•œβ‚‚ F] {σ₁₂ : π•œ β†’+* π•œβ‚‚} +variables [normed_field π•œβ‚] [normed_field π•œβ‚‚] [module π•œβ‚ E] [module π•œβ‚‚ F] {Οƒ : π•œβ‚ β†’+* π•œβ‚‚} variables [module ℝ E] [module ℝ F] [has_continuous_const_smul ℝ F] [locally_convex_space ℝ F] [smul_comm_class π•œβ‚‚ ℝ F] -instance : locally_convex_space ℝ (E β†’SL[σ₁₂] F) := -strong_topology.locally_convex_space _ βŸ¨βˆ…, bornology.is_vonN_bounded_empty π•œ E⟩ +instance : locally_convex_space ℝ (E β†’SL[Οƒ] F) := +strong_topology.locally_convex_space _ βŸ¨βˆ…, bornology.is_vonN_bounded_empty π•œβ‚ E⟩ (directed_on_of_sup_mem $ Ξ» _ _, bornology.is_vonN_bounded.union) end bounded_sets From 8b0f2339ddd3c823ad3b812e09521b7481bda82d Mon Sep 17 00:00:00 2001 From: Moritz Doll Date: Tue, 28 Mar 2023 16:05:45 +1100 Subject: [PATCH 3/4] unused instance --- src/analysis/locally_convex/strong_topology.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/analysis/locally_convex/strong_topology.lean b/src/analysis/locally_convex/strong_topology.lean index 49d10b7920373..c119a8be2190b 100644 --- a/src/analysis/locally_convex/strong_topology.lean +++ b/src/analysis/locally_convex/strong_topology.lean @@ -37,7 +37,7 @@ variables [add_comm_group E] [topological_space E] section general variables [normed_field π•œβ‚] [normed_field π•œβ‚‚] [module π•œβ‚ E] [module π•œβ‚‚ F] {Οƒ : π•œβ‚ β†’+* π•œβ‚‚} -variables [module ℝ E] [module ℝ F] [has_continuous_const_smul ℝ F] [locally_convex_space ℝ F] +variables [module ℝ F] [has_continuous_const_smul ℝ F] [locally_convex_space ℝ F] [smul_comm_class π•œβ‚‚ ℝ F] lemma strong_topology.locally_convex_space (𝔖 : set (set E)) (h𝔖₁ : 𝔖.nonempty) @@ -58,7 +58,7 @@ end general section bounded_sets variables [normed_field π•œβ‚] [normed_field π•œβ‚‚] [module π•œβ‚ E] [module π•œβ‚‚ F] {Οƒ : π•œβ‚ β†’+* π•œβ‚‚} -variables [module ℝ E] [module ℝ F] [has_continuous_const_smul ℝ F] [locally_convex_space ℝ F] +variables [module ℝ F] [has_continuous_const_smul ℝ F] [locally_convex_space ℝ F] [smul_comm_class π•œβ‚‚ ℝ F] instance : locally_convex_space ℝ (E β†’SL[Οƒ] F) := From 29dd038641826c83ea6baf6511dd2f2ddf836edb Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Fri, 31 Mar 2023 11:34:29 +0000 Subject: [PATCH 4/4] generalize from `real` to an arbitrary ring too --- .../locally_convex/strong_topology.lean | 21 +++++++++++-------- 1 file changed, 12 insertions(+), 9 deletions(-) diff --git a/src/analysis/locally_convex/strong_topology.lean b/src/analysis/locally_convex/strong_topology.lean index c119a8be2190b..a5e444a5729da 100644 --- a/src/analysis/locally_convex/strong_topology.lean +++ b/src/analysis/locally_convex/strong_topology.lean @@ -27,7 +27,7 @@ locally convex, bounded convergence open_locale topology uniform_convergence -variables {π•œβ‚ π•œβ‚‚ E F : Type*} +variables {R π•œβ‚ π•œβ‚‚ E F : Type*} namespace continuous_linear_map @@ -36,19 +36,21 @@ variables [add_comm_group E] [topological_space E] section general +variables (R) +variables [ordered_semiring R] variables [normed_field π•œβ‚] [normed_field π•œβ‚‚] [module π•œβ‚ E] [module π•œβ‚‚ F] {Οƒ : π•œβ‚ β†’+* π•œβ‚‚} -variables [module ℝ F] [has_continuous_const_smul ℝ F] [locally_convex_space ℝ F] - [smul_comm_class π•œβ‚‚ ℝ F] +variables [module R F] [has_continuous_const_smul R F] [locally_convex_space R F] + [smul_comm_class π•œβ‚‚ R F] lemma strong_topology.locally_convex_space (𝔖 : set (set E)) (h𝔖₁ : 𝔖.nonempty) (h𝔖₂ : directed_on (βŠ†) 𝔖) : - @locally_convex_space ℝ (E β†’SL[Οƒ] F) _ _ _ (strong_topology Οƒ F 𝔖) := + @locally_convex_space R (E β†’SL[Οƒ] F) _ _ _ (strong_topology Οƒ F 𝔖) := begin letI : topological_space (E β†’SL[Οƒ] F) := strong_topology Οƒ F 𝔖, haveI : topological_add_group (E β†’SL[Οƒ] F) := strong_topology.topological_add_group _ _ _, refine locally_convex_space.of_basis_zero _ _ _ _ (strong_topology.has_basis_nhds_zero_of_basis _ _ _ h𝔖₁ h𝔖₂ - (locally_convex_space.convex_basis_zero ℝ F)) _, + (locally_convex_space.convex_basis_zero R F)) _, rintros ⟨S, V⟩ ⟨hS, hVmem, hVconvex⟩ f hf g hg a b ha hb hab x hx, exact hVconvex (hf x hx) (hg x hx) ha hb hab, end @@ -57,12 +59,13 @@ end general section bounded_sets +variables [ordered_semiring R] variables [normed_field π•œβ‚] [normed_field π•œβ‚‚] [module π•œβ‚ E] [module π•œβ‚‚ F] {Οƒ : π•œβ‚ β†’+* π•œβ‚‚} -variables [module ℝ F] [has_continuous_const_smul ℝ F] [locally_convex_space ℝ F] - [smul_comm_class π•œβ‚‚ ℝ F] +variables [module R F] [has_continuous_const_smul R F] [locally_convex_space R F] + [smul_comm_class π•œβ‚‚ R F] -instance : locally_convex_space ℝ (E β†’SL[Οƒ] F) := -strong_topology.locally_convex_space _ βŸ¨βˆ…, bornology.is_vonN_bounded_empty π•œβ‚ E⟩ +instance : locally_convex_space R (E β†’SL[Οƒ] F) := +strong_topology.locally_convex_space R _ βŸ¨βˆ…, bornology.is_vonN_bounded_empty π•œβ‚ E⟩ (directed_on_of_sup_mem $ Ξ» _ _, bornology.is_vonN_bounded.union) end bounded_sets