The weak topology and the canonical bidual map

The canonical map from a seminormed space with its weak topology to its weak-star bidual is inducing: the weak topology is the topology pulled back from the weak-star bidual. This holds without assuming that the seminorm separates points.

When the scalar field is proper, a norm-bounded set has weakly compact closure if the weak-star closure of its bidual image lies in the range of the canonical map. This extends Mathlib's NormedSpace.isCompact_closure_of_isBounded to seminormed spaces, using the inducing property to transfer Banach–Alaoglu compactness back to the weak topology. In particular, in a reflexive seminormed space over a proper field, where the canonical map is surjective, every norm-bounded set has weakly compact closure (TauCeti.isCompact_closure_toWeakSpace).

Finally, every linear map from a vector space into the bidual of a normed space lifts into the space on the subspace of vectors sent into the canonical image (LinearMap.exists_lift_doubleDual).

theorem NormedSpace.isInducing_inclusionInDoubleDualWeak (𝕜 : Type u_1) (E : Type u_2) [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] : Topology.IsInducing ⇑(inclusionInDoubleDualWeak 𝕜 E)

The canonical bidual map induces the weak topology from the weak-star topology, including when the seminorm on the source does not separate points.

theorem NormedSpace.toWeakDual_mem_range_inclusionInDoubleDualWeak_iff (𝕜 : Type u_1) (E : Type u_2) [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] (Φ : StrongDual 𝕜 (StrongDual 𝕜 E)) : StrongDual.toWeakDual Φ ∈ Set.range ⇑(inclusionInDoubleDualWeak 𝕜 E) ↔ Φ ∈ Set.range ⇑(inclusionInDoubleDual 𝕜 E)

An element of the bidual lies in the canonical image of E iff it does when viewed in the weak-star bidual.

theorem NormedSpace.isCompact_closure_weakSpace_of_isBounded (𝕜 : Type u_1) (E : Type u_2) [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [ProperSpace 𝕜] (s : Set (WeakSpace 𝕜 E)) (hs : Bornology.IsBounded (⇑(toWeakSpace 𝕜 E) ⁻¹' s)) (hrange : closure (⇑(inclusionInDoubleDualWeak 𝕜 E) '' s) ⊆ Set.range ⇑(inclusionInDoubleDualWeak 𝕜 E)) : IsCompact (closure s)

A norm-bounded set in a seminormed space has weakly compact closure if the weak-star closure of its canonical bidual image lies in the range of the canonical map.

theorem TauCeti.isCompact_closure_toWeakSpace {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [ProperSpace 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] (hE : Function.Surjective ⇑(NormedSpace.inclusionInDoubleDual 𝕜 E)) {s : Set E} (hs : Bornology.IsBounded s) : IsCompact (closure (⇑(toWeakSpace 𝕜 E) '' s))

In a reflexive seminormed space over a proper nontrivially normed field, every norm-bounded set has weakly compact closure.

theorem LinearMap.exists_lift_doubleDual {𝕜 : Type u_1} {E : Type u_2} {V : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [AddCommGroup V] [Module 𝕜 V] (ι : V →ₗ[𝕜] StrongDual 𝕜 (StrongDual 𝕜 E)) : ∃ (F₀ : Submodule 𝕜 V) (A : ↥F₀ →ₗ[𝕜] E), (∀ (φ : ↥F₀), (NormedSpace.inclusionInDoubleDual 𝕜 E) (A φ) = ι ↑φ) ∧ ∀ (v : V) (x : E), ι v = (NormedSpace.inclusionInDoubleDual 𝕜 E) x → v ∈ F₀

A linear map ι : V → E** lifts into E on the subspace F₀ of the vectors that it maps into the canonical image of E: there is a linear map A : F₀ → E whose canonical image is ι, and every v with ι v equal to the canonical image of x lies in F₀.