refactor(LocallyConvex,Topology): split WeakDual/WeakSpace and rename WeakBilin

Mathlib.lean

@@ -1997,7 +1997,7 @@ public import Mathlib.Analysis.LocallyConvex.Polar
 public import Mathlib.Analysis.LocallyConvex.SeparatingDual
 public import Mathlib.Analysis.LocallyConvex.Separation
 public import Mathlib.Analysis.LocallyConvex.StrongTopology
-public import Mathlib.Analysis.LocallyConvex.WeakDual
+public import Mathlib.Analysis.LocallyConvex.WeakBilin
 public import Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
 public import Mathlib.Analysis.LocallyConvex.WeakSpace
 public import Mathlib.Analysis.LocallyConvex.WithSeminorms
@@ -7317,6 +7317,7 @@ public import Mathlib.Topology.Algebra.Module.Spaces.PointwiseConvergenceCLM
 public import Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
 public import Mathlib.Topology.Algebra.Module.Spaces.WeakBilin
 public import Mathlib.Topology.Algebra.Module.Spaces.WeakDual
+public import Mathlib.Topology.Algebra.Module.Spaces.WeakSpace
 public import Mathlib.Topology.Algebra.Module.Star
 public import Mathlib.Topology.Algebra.Module.StrongTopology
 public import Mathlib.Topology.Algebra.Module.TopDualPairing

Mathlib/Analysis/LocallyConvex/WeakDual.lean → Mathlib/Analysis/LocallyConvex/WeakBilin.lean

@@ -12,7 +12,7 @@ public import Mathlib.LinearAlgebra.Finsupp.Span
 public import Mathlib.Topology.Algebra.Module.Spaces.WeakBilin
 
 /-!
-# Weak Dual in Topological Vector Spaces
+# Weak Bilinear Topologies in Topological Vector Spaces
 
 We prove that the weak topology induced by a bilinear form `B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜` is locally
 convex and we explicitly give a neighborhood basis in terms of the family of seminorms
@@ -28,7 +28,7 @@ convex and we explicitly give a neighborhood basis in terms of the family of sem
 
 * `LinearMap.hasBasis_weakBilin`: the seminorm balls of `B.toSeminormFamily` form a
   neighborhood basis of `0` in the weak topology.
-* `LinearMap.toSeminormFamily.withSeminorms`: the topology of a weak space is induced by the
+* `LinearMap.weakBilin_withSeminorms`: the topology of a weak space is induced by the
   family of seminorms `B.toSeminormFamily`.
 * `WeakBilin.locallyConvexSpace`: a space endowed with a weak topology is locally convex.
 * `LinearMap.rightDualEquiv`: When `B` is right-separating, `F` is linearly equivalent to the
@@ -43,7 +43,7 @@ convex and we explicitly give a neighborhood basis in terms of the family of sem
 
 ## Tags
 
-weak dual, seminorm
+weak bilinear, seminorm
 -/
 
 @[expose] public section

Mathlib/Analysis/LocallyConvex/WeakSpace.lean

@@ -1,26 +1,66 @@
 /-
 Copyright (c) 2024 Jireh Loreaux. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Jireh Loreaux
+Authors: Jireh Loreaux, Michał Świętek
 -/
 module
 
 public import Mathlib.Analysis.LocallyConvex.Separation
 public import Mathlib.Analysis.LocallyConvex.SeparatingDual
+public import Mathlib.Analysis.LocallyConvex.WeakBilin
 public import Mathlib.LinearAlgebra.Dual.Defs
-public import Mathlib.Topology.Algebra.Module.Spaces.WeakDual
+public import Mathlib.Topology.Algebra.Module.Spaces.WeakSpace
 
-/-! # Closures of convex sets in locally convex spaces
+/-! # Weak topology on normed spaces: seminorm family and convex closures
 
-This file contains the standard result that if `E` is a vector space with two locally convex
+## Seminorm family
+
+The weak topology on `WeakSpace 𝕜 E` is generated by the seminorm family `fun f x ↦ ‖f x‖`
+indexed by `StrongDual 𝕜 E`. This follows from the general `LinearMap.weakBilin_withSeminorms`
+applied to the flipped `topDualPairing`.
+
+## Closures of convex sets
+
+This file also contains the standard result that if `E` is a vector space with two locally convex
 topologies, then the closure of a convex set is the same in either topology, provided they have the
 same collection of continuous linear functionals. In particular, the weak closure of a convex set
 in a locally convex space coincides with the closure in the original topology.
 Of course, we phrase this in terms of linear maps between locally convex spaces, rather than
 creating two separate topologies on the same space.
 -/
 
-public section
+@[expose] public section
+
+section Seminorms
+
+variable {𝕜 : Type*} [NormedField 𝕜] {E : Type*} [AddCommGroup E] [Module 𝕜 E]
+  [TopologicalSpace E] [ContinuousAdd E] [ContinuousConstSMul 𝕜 E]
+
+namespace WeakSpace
+
+set_option backward.isDefEq.respectTransparency false in
+variable (𝕜 E) in
+/-- The family of seminorms on `WeakSpace 𝕜 E` given by `fun f x ↦ ‖f x‖`, indexed by
+`StrongDual 𝕜 E`. This is the seminorm family associated to the weak topology via the
+flipped `topDualPairing`. -/
+def seminormFamily : SeminormFamily 𝕜 (WeakSpace 𝕜 E) (StrongDual 𝕜 E) :=
+  (topDualPairing 𝕜 E).flip.toSeminormFamily
+
+set_option backward.isDefEq.respectTransparency false in
+omit [ContinuousAdd E] [ContinuousConstSMul 𝕜 E] in
+@[simp]
+lemma seminormFamily_apply (f : StrongDual 𝕜 E) (x : WeakSpace 𝕜 E) :
+    seminormFamily 𝕜 E f x = ‖f x‖ := rfl
+
+set_option backward.isDefEq.respectTransparency false in
+omit [ContinuousAdd E] [ContinuousConstSMul 𝕜 E] in
+variable (𝕜 E) in
+lemma withSeminorms : WithSeminorms (seminormFamily 𝕜 E) :=
+  (topDualPairing 𝕜 E).flip.weakBilin_withSeminorms
+
+end WeakSpace
+
+end Seminorms
 
 variable {𝕜 E F : Type*}
 variable [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F]

Mathlib/Analysis/Normed/Module/WeakDual.lean

@@ -10,7 +10,7 @@ public import Mathlib.Analysis.Normed.Operator.Completeness
 public import Mathlib.Topology.Algebra.Module.Spaces.WeakDual
 public import Mathlib.Topology.MetricSpace.PiNat
 public import Mathlib.Analysis.Normed.Operator.BanachSteinhaus
-public import Mathlib.Analysis.LocallyConvex.WeakDual
+public import Mathlib.Analysis.LocallyConvex.WeakBilin
 
 /-!
 # Weak dual of normed space

Mathlib/Topology/Algebra/Module/Spaces/WeakDual.lean

@@ -12,28 +12,15 @@ public import Mathlib.Topology.Algebra.Module.Spaces.WeakBilin
 /-!
 # Weak dual topology
 
-We continue in the setting of `Mathlib/Topology/Algebra/Module/WeakBilin.lean`,
-which defines the weak topology given two vector spaces `E` and `F` over a commutative semiring
-`𝕜` and a bilinear form `B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜`. The weak topology on `E` is the coarsest topology
-such that for all `y : F` every map `fun x => B x y` is continuous.
-
-In this file, we consider two special cases.
-In the case that `F = E →L[𝕜] 𝕜` and `B` being the canonical pairing, we obtain the weak-* topology,
-`WeakDual 𝕜 E := (E →L[𝕜] 𝕜)`. Interchanging the arguments in the bilinear form yields the
-weak topology `WeakSpace 𝕜 E := E`.
+This file defines the weak-* (weak dual) topology on the continuous dual `E →L[𝕜] 𝕜`.
+It is the coarsest topology such that for all `z : E` every evaluation map
+`fun v => v z` is continuous.
 
 ## Main definitions
 
-The main definitions are the types `WeakDual 𝕜 E` and `WeakSpace 𝕜 E`,
-with the respective topology instances on it.
-
-* `WeakDual 𝕜 E` is a type synonym for `Dual 𝕜 E` (when the latter is defined): both are equal to
-  the type `E →L[𝕜] 𝕜` of continuous linear maps from a module `E` over `𝕜` to the ring `𝕜`.
+* `WeakDual 𝕜 E` is a type synonym for `E →L[𝕜] 𝕜` (equal to `Dual 𝕜 E`).
 * The instance `WeakDual.instTopologicalSpace` is the weak-* topology on `WeakDual 𝕜 E`, i.e., the
   coarsest topology making the evaluation maps at all `z : E` continuous.
-* `WeakSpace 𝕜 E` is a type synonym for `E` (when the latter is defined).
-* The instance `WeakSpace.instTopologicalSpace` is the weak topology on `E`, i.e., the
-  coarsest topology such that all `v : dual 𝕜 E` remain continuous.
 
 ## References
 
@@ -165,103 +152,16 @@ end Ring
 
 end WeakDual
 
-/-- The weak topology is the topology coarsest topology on `E` such that all functionals
-`fun x => v x` are continuous. -/
-def WeakSpace (𝕜 E) [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜]
-    [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] :=
-  WeakBilin (topDualPairing 𝕜 E).flip
-deriving AddCommMonoid, Module 𝕜, TopologicalSpace, ContinuousAdd
-
 section Semiring
 
 variable [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜]
 variable [ContinuousConstSMul 𝕜 𝕜]
 variable [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E]
 
-namespace WeakSpace
-
-instance instModule' [CommSemiring 𝕝] [Module 𝕝 E] : Module 𝕝 (WeakSpace 𝕜 E) :=
-  inferInstanceAs <| Module 𝕝 (WeakBilin (topDualPairing 𝕜 E).flip)
-
-instance instIsScalarTower [CommSemiring 𝕝] [Module 𝕝 𝕜] [Module 𝕝 E] [IsScalarTower 𝕝 𝕜 E] :
-    IsScalarTower 𝕝 𝕜 (WeakSpace 𝕜 E) :=
-  WeakBilin.instIsScalarTower (topDualPairing 𝕜 E).flip
-
-instance instContinuousSMul [ContinuousSMul 𝕜 𝕜] : ContinuousSMul 𝕜 (WeakSpace 𝕜 E) :=
-  WeakBilin.instContinuousSMul _
-
-variable [AddCommMonoid F] [Module 𝕜 F] [TopologicalSpace F]
-
-/-- A continuous linear map from `E` to `F` is still continuous when `E` and `F` are equipped with
-their weak topologies. -/
-def map (f : E →L[𝕜] F) : WeakSpace 𝕜 E →L[𝕜] WeakSpace 𝕜 F :=
-  { f with
-    cont :=
-      WeakBilin.continuous_of_continuous_eval _ fun l => WeakBilin.eval_continuous _ (l ∘L f) }
-
-theorem map_apply (f : E →L[𝕜] F) (x : E) : WeakSpace.map f x = f x :=
-  rfl
-
-@[simp]
-theorem coe_map (f : E →L[𝕜] F) : (WeakSpace.map f : E → F) = f :=
-  rfl
-
-end WeakSpace
-
-variable (𝕜 E) in
-/-- There is a canonical map `E → WeakSpace 𝕜 E` (the "identity"
-mapping). It is a linear equivalence. -/
-def toWeakSpace : E ≃ₗ[𝕜] WeakSpace 𝕜 E := LinearEquiv.refl 𝕜 E
-
-variable (𝕜 E) in
-/-- For a topological vector space `E`, "identity mapping" `E → WeakSpace 𝕜 E` is continuous.
-This definition implements it as a continuous linear map. -/
-def toWeakSpaceCLM : E →L[𝕜] WeakSpace 𝕜 E where
-  __ := toWeakSpace 𝕜 E
-  cont := by
-    apply WeakBilin.continuous_of_continuous_eval
-    exact ContinuousLinearMap.continuous
-
-variable (𝕜 E) in
-@[simp]
-theorem toWeakSpaceCLM_eq_toWeakSpace (x : E) :
-    toWeakSpaceCLM 𝕜 E x = toWeakSpace 𝕜 E x := by rfl
-
-theorem toWeakSpaceCLM_bijective :
-    Function.Bijective (toWeakSpaceCLM 𝕜 E) :=
-  (toWeakSpace 𝕜 E).bijective
-
-/-- The canonical map from `WeakSpace 𝕜 E` to `E` is an open map. -/
-theorem isOpenMap_toWeakSpace_symm : IsOpenMap (toWeakSpace 𝕜 E).symm :=
-  IsOpenMap.of_inverse (toWeakSpaceCLM 𝕜 E).cont
-    (toWeakSpace 𝕜 E).left_inv (toWeakSpace 𝕜 E).right_inv
-
-/-- A set in `E` which is open in the weak topology is open. -/
-theorem WeakSpace.isOpen_of_isOpen (V : Set E)
-    (hV : IsOpen ((toWeakSpaceCLM 𝕜 E) '' V : Set (WeakSpace 𝕜 E))) : IsOpen V := by
-  simpa [Set.image_image] using isOpenMap_toWeakSpace_symm _ hV
-
 theorem tendsto_iff_forall_eval_tendsto_topDualPairing {l : Filter α} {f : α → WeakDual 𝕜 E}
     {x : WeakDual 𝕜 E} :
     Tendsto f l (𝓝 x) ↔
       ∀ y, Tendsto (fun i => topDualPairing 𝕜 E (f i) y) l (𝓝 (topDualPairing 𝕜 E x y)) :=
   WeakBilin.tendsto_iff_forall_eval_tendsto _ ContinuousLinearMap.coe_injective
 
 end Semiring
-
-section Ring
-
-namespace WeakSpace
-
-variable [CommRing 𝕜] [TopologicalSpace 𝕜] [IsTopologicalAddGroup 𝕜] [ContinuousConstSMul 𝕜 𝕜]
-variable [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [IsTopologicalAddGroup E]
-
-instance instAddCommGroup : AddCommGroup (WeakSpace 𝕜 E) :=
-  inferInstanceAs <| AddCommGroup (WeakBilin (topDualPairing 𝕜 E).flip)
-
-instance instIsTopologicalAddGroup : IsTopologicalAddGroup (WeakSpace 𝕜 E) :=
-  WeakBilin.instIsTopologicalAddGroup (topDualPairing 𝕜 E).flip
-
-end WeakSpace
-
-end Ring

Mathlib/Topology/Algebra/Module/Spaces/WeakSpace.lean

@@ -0,0 +1,137 @@
+/-
+Copyright (c) 2021 Kalle Kytölä. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kalle Kytölä, Moritz Doll
+-/
+module
+
+public import Mathlib.LinearAlgebra.BilinearMap
+public import Mathlib.Topology.Algebra.Module.LinearMap
+public import Mathlib.Topology.Algebra.Module.Spaces.WeakBilin
+
+/-!
+# Weak topology
+
+This file defines the weak topology on a topological vector space `E`.
+It is the coarsest topology on `E` such that all continuous linear functionals
+`fun x => v x` for `v : E →L[𝕜] 𝕜` remain continuous.
+
+## Main definitions
+
+* `WeakSpace 𝕜 E` is a type synonym for `E`.
+* The instance `WeakSpace.instTopologicalSpace` is the weak topology on `E`, i.e., the
+  coarsest topology such that all `v : E →L[𝕜] 𝕜` remain continuous.
+* `toWeakSpace`: The canonical linear equivalence `E ≃ₗ[𝕜] WeakSpace 𝕜 E`.
+* `toWeakSpaceCLM`: The identity mapping as a continuous linear map `E →L[𝕜] WeakSpace 𝕜 E`.
+
+## References
+
+* [H. H. Schaefer, *Topological Vector Spaces*][schaefer1966]
+
+## Tags
+
+weak topology, duality
+-/
+
+@[expose] public section
+
+noncomputable section
+
+open Filter Topology
+
+variable {α 𝕜 𝕝 E F : Type*}
+
+/-- The weak topology is the topology coarsest topology on `E` such that all functionals
+`fun x => v x` are continuous. -/
+def WeakSpace (𝕜 E) [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜]
+    [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] :=
+  WeakBilin (topDualPairing 𝕜 E).flip
+deriving AddCommMonoid, Module 𝕜, TopologicalSpace, ContinuousAdd
+
+section Semiring
+
+variable [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜]
+variable [ContinuousConstSMul 𝕜 𝕜]
+variable [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E]
+
+namespace WeakSpace
+
+instance instModule' [CommSemiring 𝕝] [Module 𝕝 E] : Module 𝕝 (WeakSpace 𝕜 E) :=
+  inferInstanceAs <| Module 𝕝 (WeakBilin (topDualPairing 𝕜 E).flip)
+
+instance instIsScalarTower [CommSemiring 𝕝] [Module 𝕝 𝕜] [Module 𝕝 E] [IsScalarTower 𝕝 𝕜 E] :
+    IsScalarTower 𝕝 𝕜 (WeakSpace 𝕜 E) :=
+  WeakBilin.instIsScalarTower (topDualPairing 𝕜 E).flip
+
+instance instContinuousSMul [ContinuousSMul 𝕜 𝕜] : ContinuousSMul 𝕜 (WeakSpace 𝕜 E) :=
+  WeakBilin.instContinuousSMul _
+
+variable [AddCommMonoid F] [Module 𝕜 F] [TopologicalSpace F]
+
+/-- A continuous linear map from `E` to `F` is still continuous when `E` and `F` are equipped with
+their weak topologies. -/
+def map (f : E →L[𝕜] F) : WeakSpace 𝕜 E →L[𝕜] WeakSpace 𝕜 F :=
+  { f with
+    cont :=
+      WeakBilin.continuous_of_continuous_eval _ fun l => WeakBilin.eval_continuous _ (l ∘L f) }
+
+theorem map_apply (f : E →L[𝕜] F) (x : E) : WeakSpace.map f x = f x :=
+  rfl
+
+@[simp]
+theorem coe_map (f : E →L[𝕜] F) : (WeakSpace.map f : E → F) = f :=
+  rfl
+
+end WeakSpace
+
+variable (𝕜 E) in
+/-- There is a canonical map `E → WeakSpace 𝕜 E` (the "identity"
+mapping). It is a linear equivalence. -/
+def toWeakSpace : E ≃ₗ[𝕜] WeakSpace 𝕜 E := LinearEquiv.refl 𝕜 E
+
+variable (𝕜 E) in
+/-- For a topological vector space `E`, "identity mapping" `E → WeakSpace 𝕜 E` is continuous.
+This definition implements it as a continuous linear map. -/
+def toWeakSpaceCLM : E →L[𝕜] WeakSpace 𝕜 E where
+  __ := toWeakSpace 𝕜 E
+  cont := by
+    apply WeakBilin.continuous_of_continuous_eval
+    exact ContinuousLinearMap.continuous
+
+variable (𝕜 E) in
+@[simp]
+theorem toWeakSpaceCLM_eq_toWeakSpace (x : E) :
+    toWeakSpaceCLM 𝕜 E x = toWeakSpace 𝕜 E x := by rfl
+
+theorem toWeakSpaceCLM_bijective :
+    Function.Bijective (toWeakSpaceCLM 𝕜 E) :=
+  (toWeakSpace 𝕜 E).bijective
+
+/-- The canonical map from `WeakSpace 𝕜 E` to `E` is an open map. -/
+theorem isOpenMap_toWeakSpace_symm : IsOpenMap (toWeakSpace 𝕜 E).symm :=
+  IsOpenMap.of_inverse (toWeakSpaceCLM 𝕜 E).cont
+    (toWeakSpace 𝕜 E).left_inv (toWeakSpace 𝕜 E).right_inv
+
+/-- A set in `E` which is open in the weak topology is open. -/
+theorem WeakSpace.isOpen_of_isOpen (V : Set E)
+    (hV : IsOpen ((toWeakSpaceCLM 𝕜 E) '' V : Set (WeakSpace 𝕜 E))) : IsOpen V := by
+  simpa [Set.image_image] using isOpenMap_toWeakSpace_symm _ hV
+
+end Semiring
+
+section Ring
+
+namespace WeakSpace
+
+variable [CommRing 𝕜] [TopologicalSpace 𝕜] [IsTopologicalAddGroup 𝕜] [ContinuousConstSMul 𝕜 𝕜]
+variable [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [IsTopologicalAddGroup E]
+
+instance instAddCommGroup : AddCommGroup (WeakSpace 𝕜 E) :=
+  inferInstanceAs <| AddCommGroup (WeakBilin (topDualPairing 𝕜 E).flip)
+
+instance instIsTopologicalAddGroup : IsTopologicalAddGroup (WeakSpace 𝕜 E) :=
+  WeakBilin.instIsTopologicalAddGroup (topDualPairing 𝕜 E).flip
+
+end WeakSpace
+
+end Ring