The topology of pointwise convergence is locally convex

We prove that the topology of pointwise convergence is induced by a family of seminorms and that it is locally convex in the topological sense

• PointwiseConvergenceCLM.seminorm: the seminorms on E →SLₚₜ[σ] F given by A ↦ ‖A x‖ for fixed x : E.
• PointwiseConvergenceCLM.withSeminorm: the topology is induced by the seminorms.
• PointwiseConvergenceCLM.instLocallyConvexSpace: E →SLₚₜ[σ] F is locally convex.

def PointwiseConvergenceCLM.seminorm {𝕜₁ : Type u_2} {𝕜₂ : Type u_3} [NormedField 𝕜₁] [NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_4} {F : Type u_5} [AddCommGroup E] [TopologicalSpace E] [Module 𝕜₁ E] [NormedAddCommGroup F] [NormedSpace 𝕜₂ F] (x : E) : Seminorm 𝕜₂ (E →SLₚₜ[σ] F)

The family of seminorms that induce the topology of pointwise convergence, namely ‖A x‖ for all x : E.

Equations

• PointwiseConvergenceCLM.seminorm x = { toFun := fun (A : E →SLₚₜ[σ] F) => ‖A x‖, map_zero' := ⋯, add_le' := ⋯, neg' := ⋯, smul' := ⋯ }

@[reducible, inline]

abbrev PointwiseConvergenceCLM.seminormFamily {𝕜₁ : Type u_2} {𝕜₂ : Type u_3} [NormedField 𝕜₁] [NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) (E : Type u_4) (F : Type u_5) [AddCommGroup E] [TopologicalSpace E] [Module 𝕜₁ E] [NormedAddCommGroup F] [NormedSpace 𝕜₂ F] : SeminormFamily 𝕜₂ (E →SLₚₜ[σ] F) E

The family of seminorms that induce the topology of pointwise convergence, namely ‖A x‖ for all x : E.

Equations

• PointwiseConvergenceCLM.seminormFamily σ E F = PointwiseConvergenceCLM.seminorm

def PointwiseConvergenceCLM.inducingFn {𝕜₁ : Type u_2} {𝕜₂ : Type u_3} [NormedField 𝕜₁] [NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) (E : Type u_4) (F : Type u_5) [AddCommGroup E] [TopologicalSpace E] [Module 𝕜₁ E] [NormedAddCommGroup F] [NormedSpace 𝕜₂ F] : (E →SLₚₜ[σ] F) →ₗ[𝕜₂] E → F

The coercion E →SLₚₜ[σ] F to E → F as a linear map.

The topology on E →SLₚₜ[σ] F is induced by this map.

Equations

• PointwiseConvergenceCLM.inducingFn σ E F = { toFun := fun (f : E →SLₚₜ[σ] F) => ⇑f, map_add' := ⋯, map_smul' := ⋯ }

theorem PointwiseConvergenceCLM.isInducing_inducingFn {𝕜₁ : Type u_2} {𝕜₂ : Type u_3} [NormedField 𝕜₁] [NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) (E : Type u_4) (F : Type u_5) [AddCommGroup E] [TopologicalSpace E] [Module 𝕜₁ E] [NormedAddCommGroup F] [NormedSpace 𝕜₂ F] : Topology.IsInducing ⇑(inducingFn σ E F)

theorem PointwiseConvergenceCLM.withSeminorms {𝕜₁ : Type u_2} {𝕜₂ : Type u_3} [NormedField 𝕜₁] [NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_4} {F : Type u_5} [AddCommGroup E] [TopologicalSpace E] [Module 𝕜₁ E] [NormedAddCommGroup F] [NormedSpace 𝕜₂ F] : WithSeminorms (PointwiseConvergenceCLM.seminormFamily σ E F)

instance PointwiseConvergenceCLM.instLocallyConvexSpace {R : Type u_1} {𝕜₁ : Type u_2} {𝕜₂ : Type u_3} [NormedField 𝕜₁] [NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_4} {F : Type u_5} [AddCommGroup E] [TopologicalSpace E] [Module 𝕜₁ E] [AddCommGroup F] [TopologicalSpace F] [IsTopologicalAddGroup F] [Module 𝕜₂ F] [Semiring R] [PartialOrder R] [Module R F] [ContinuousConstSMul R F] [LocallyConvexSpace R F] [SMulCommClass 𝕜₂ R F] : LocallyConvexSpace R (E →SLₚₜ[σ] F)