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] - chore(analysis/locally_convex/strong_topology): generalize to semilinear maps #18679

Closed
wants to merge 4 commits into from
Closed

[Merged by Bors] - chore(analysis/locally_convex/strong_topology): generalize to semilinear maps #18679

Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
63702c0
generalize to semilinear maps
mcdoll Mar 28, 2023
dbec8ed
variable names
mcdoll Mar 28, 2023
8b0f233
unused instance
mcdoll Mar 28, 2023
29dd038
generalize from `real` to an arbitrary ring too
eric-wieser Mar 31, 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
32 changes: 19 additions & 13 deletions src/analysis/locally_convex/strong_topology.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -27,25 +27,30 @@ locally convex, bounded convergence

open_locale topology uniform_convergence

variables {E F : Type*}
variables {R 𝕜₁ 𝕜₂ 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 (R)
variables [ordered_semiring R]
variables [normed_field 𝕜₁] [normed_field 𝕜₂] [module 𝕜₁ E] [module 𝕜₂ 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 →L[ℝ] F) _ _ _ (strong_topology (ring_hom.id ℝ) F 𝔖) :=
@locally_convex_space R (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)) _,
(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
Expand All @@ -54,12 +59,13 @@ 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 [ordered_semiring R]
variables [normed_field 𝕜₁] [normed_field 𝕜₂] [module 𝕜₁ E] [module 𝕜₂ 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 →L[ℝ] 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
Expand Down