Locally convex topological modules

A LocallyConvexSpace is a topological semimodule over an ordered semiring in which any point admits a neighborhood basis made of convex sets, or equivalently, in which convex neighborhoods of a point form a neighborhood basis at that point.

In a module, this is equivalent to 0 satisfying such properties.

Main results

• locallyConvexSpace_iff_zero : in a module, local convexity at zero gives local convexity everywhere
• WithSeminorms.locallyConvexSpace : a topology generated by a family of seminorms is locally convex (in Analysis.LocallyConvex.WithSeminorms)
• NormedSpace.locallyConvexSpace : a normed space is locally convex (in Analysis.LocallyConvex.WithSeminorms)

TODO

• define a structure LocallyConvexFilterBasis, extending ModuleFilterBasis, for filter bases generating a locally convex topology

class LocallyConvexSpace (𝕜 : Type u_1) (E : Type u_2) [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] : Prop

• convex_basis : ∀ (x : E), Filter.HasBasis (nhds x) (fun s => s ∈ nhds x ∧ Convex 𝕜 s) id

A LocallyConvexSpace is a topological semimodule over an ordered semiring in which convex neighborhoods of a point form a neighborhood basis at that point.

theorem locallyConvexSpace_iff (𝕜 : Type u_1) (E : Type u_2) [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] : LocallyConvexSpace 𝕜 E ↔ ∀ (x : E), Filter.HasBasis (nhds x) (fun s => s ∈ nhds x ∧ Convex 𝕜 s) id

theorem LocallyConvexSpace.ofBases (𝕜 : Type u_1) (E : Type u_2) [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] {ι : Type u_3} (b : E → ι → Set E) (p : E → ι → Prop) (hbasis : ∀ (x : E), Filter.HasBasis (nhds x) (p x) (b x)) (hconvex : ∀ (x : E) (i : ι), p x i → Convex 𝕜 (b x i)) : LocallyConvexSpace 𝕜 E

theorem LocallyConvexSpace.convex_basis_zero (𝕜 : Type u_1) (E : Type u_2) [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] [LocallyConvexSpace 𝕜 E] : Filter.HasBasis (nhds 0) (fun s => s ∈ nhds 0 ∧ Convex 𝕜 s) id

theorem locallyConvexSpace_iff_exists_convex_subset (𝕜 : Type u_1) (E : Type u_2) [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] : LocallyConvexSpace 𝕜 E ↔ ∀ (x : E) (U : Set E), U ∈ nhds x → ∃ S, S ∈ nhds x ∧ Convex 𝕜 S ∧ S ⊆ U

theorem LocallyConvexSpace.ofBasisZero (𝕜 : Type u_1) (E : Type u_2) [OrderedSemiring 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [TopologicalAddGroup E] {ι : Type u_3} (b : ι → Set E) (p : ι → Prop) (hbasis : Filter.HasBasis (nhds 0) p b) (hconvex : ∀ (i : ι), p i → Convex 𝕜 (b i)) : LocallyConvexSpace 𝕜 E

theorem locallyConvexSpace_iff_zero (𝕜 : Type u_1) (E : Type u_2) [OrderedSemiring 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [TopologicalAddGroup E] : LocallyConvexSpace 𝕜 E ↔ Filter.HasBasis (nhds 0) (fun s => s ∈ nhds 0 ∧ Convex 𝕜 s) id

theorem locallyConvexSpace_iff_exists_convex_subset_zero (𝕜 : Type u_1) (E : Type u_2) [OrderedSemiring 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [TopologicalAddGroup E] : LocallyConvexSpace 𝕜 E ↔ ∀ (U : Set E), U ∈ nhds 0 → ∃ S, S ∈ nhds 0 ∧ Convex 𝕜 S ∧ S ⊆ U

instance LocallyConvexSpace.toLocallyConnectedSpace (E : Type u_2) [AddCommGroup E] [TopologicalSpace E] [TopologicalAddGroup E] [Module ℝ E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] : LocallyConnectedSpace E

Equations

• LocallyConvexSpace.toLocallyConnectedSpace = LocallyConvexSpace.toLocallyConnectedSpace.proof_1

theorem LocallyConvexSpace.convex_open_basis_zero (𝕜 : Type u_1) (E : Type u_2) [LinearOrderedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousConstSMul 𝕜 E] [LocallyConvexSpace 𝕜 E] : Filter.HasBasis (nhds 0) (fun s => 0 ∈ s ∧ IsOpen s ∧ Convex 𝕜 s) id

theorem Disjoint.exists_open_convexes {𝕜 : Type u_1} {E : Type u_2} [LinearOrderedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousConstSMul 𝕜 E] [LocallyConvexSpace 𝕜 E] {s : Set E} {t : Set E} (disj : Disjoint s t) (hs₁ : Convex 𝕜 s) (hs₂ : IsCompact s) (ht₁ : Convex 𝕜 t) (ht₂ : IsClosed t) : ∃ u v, IsOpen u ∧ IsOpen v ∧ Convex 𝕜 u ∧ Convex 𝕜 v ∧ s ⊆ u ∧ t ⊆ v ∧ Disjoint u v

In a locally convex space, if s, t are disjoint convex sets, s is compact and t is closed, then we can find open disjoint convex sets containing them.

theorem locallyConvexSpace_sInf {𝕜 : Type u_2} {E : Type u_3} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] {ts : Set (TopologicalSpace E)} (h : ∀ (t : TopologicalSpace E), t ∈ ts → LocallyConvexSpace 𝕜 E) : LocallyConvexSpace 𝕜 E

theorem locallyConvexSpace_iInf {ι : Sort u_1} {𝕜 : Type u_2} {E : Type u_3} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] {ts' : ι → TopologicalSpace E} (h' : ∀ (i : ι), LocallyConvexSpace 𝕜 E) : LocallyConvexSpace 𝕜 E

theorem locallyConvexSpace_inf {𝕜 : Type u_2} {E : Type u_3} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] {t₁ : TopologicalSpace E} {t₂ : TopologicalSpace E} (h₁ : LocallyConvexSpace 𝕜 E) (h₂ : LocallyConvexSpace 𝕜 E) : LocallyConvexSpace 𝕜 E

theorem locallyConvexSpace_induced {𝕜 : Type u_2} {E : Type u_3} {F : Type u_4} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [AddCommMonoid F] [Module 𝕜 F] {t : TopologicalSpace F} [LocallyConvexSpace 𝕜 F] (f : E →ₗ[𝕜] F) : LocallyConvexSpace 𝕜 E

instance Pi.locallyConvexSpace {𝕜 : Type u_2} [OrderedSemiring 𝕜] {ι : Type u_5} {X : ι → Type u_6} [(i : ι) → AddCommMonoid (X i)] [(i : ι) → TopologicalSpace (X i)] [(i : ι) → Module 𝕜 (X i)] [∀ (i : ι), LocallyConvexSpace 𝕜 (X i)] : LocallyConvexSpace 𝕜 ((i : ι) → X i)

Equations

• @Pi.locallyConvexSpace = @Pi.locallyConvexSpace.proof_1

instance Prod.locallyConvexSpace {𝕜 : Type u_2} {E : Type u_3} {F : Type u_4} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [AddCommMonoid F] [Module 𝕜 F] [TopologicalSpace E] [TopologicalSpace F] [LocallyConvexSpace 𝕜 E] [LocallyConvexSpace 𝕜 F] : LocallyConvexSpace 𝕜 (E × F)

Equations

• @Prod.locallyConvexSpace = @Prod.locallyConvexSpace.proof_1