English
The forgetful restriction of scalars is a continuous map between spaces of continuous linear maps.
Русский
Переход по ограничениям скаляров — непрерывный переход между пространствами непрерывных линейных отображений.
LaTeX
$$$Continuous(\\mathrm{restrictScalars}_{𝕜'})$$$
Lean4
/-- Let `E` be a topological vector space over a normed field `𝕜`, let `α` be any type.
Let `H` be a submodule of `α →ᵤ E` such that the range of each `f ∈ H` is von Neumann bounded.
Then `H` is a topological vector space over `𝕜`,
i.e., the pointwise scalar multiplication is continuous in both variables.
For convenience we require that `H` is a vector space over `𝕜`
with a topology induced by `UniformFun.ofFun ∘ φ`, where `φ : H →ₗ[𝕜] (α → E)`. -/
theorem continuousSMul_induced_of_range_bounded (φ : hom) (hφ : IsInducing (ofFun ∘ φ))
(h : ∀ u : H, Bornology.IsVonNBounded 𝕜 (Set.range (φ u))) : ContinuousSMul 𝕜 H :=
by
have : IsTopologicalAddGroup H :=
let ofFun' : (α → E) →+ (α →ᵤ E) := AddMonoidHom.id _
IsInducing.topologicalAddGroup (ofFun'.comp (φ : H →+ (α → E))) hφ
have hb : (𝓝 (0 : H)).HasBasis (· ∈ 𝓝 (0 : E)) fun V ↦ {u | ∀ x, φ u x ∈ V} :=
by
simp only [hφ.nhds_eq_comap, Function.comp_apply, map_zero]
exact UniformFun.hasBasis_nhds_zero.comap _
apply ContinuousSMul.of_basis_zero hb
· intro U hU
have : Tendsto (fun x : 𝕜 × E ↦ x.1 • x.2) (𝓝 0) (𝓝 0) := continuous_smul.tendsto' _ _ (zero_smul _ _)
rcases ((Filter.basis_sets _).prod_nhds (Filter.basis_sets _)).tendsto_left_iff.1 this U hU with
⟨⟨V, W⟩, ⟨hV, hW⟩, hVW⟩
refine ⟨V, hV, W, hW, Set.smul_subset_iff.2 fun a ha u hu x ↦ ?_⟩
rw [map_smul]
exact hVW (Set.mk_mem_prod ha (hu x))
· intro c U hU
have : Tendsto (c • · : E → E) (𝓝 0) (𝓝 0) := (continuous_const_smul c).tendsto' _ _ (smul_zero _)
refine ⟨_, this hU, fun u hu x ↦ ?_⟩
simpa only [map_smul] using hu x
· intro u U hU
simp only [Set.mem_setOf_eq, map_smul, Pi.smul_apply]
simpa only [Set.mapsTo_range_iff] using (h u hU).eventually_nhds_zero (mem_of_mem_nhds hU)
