English
For a fixed base field 𝕜' ⊆ 𝕜 and any ι, the restriction of scalars map from the space of ι‑variable continuous alternating 𝕜‑multilinear maps to the analogous space but viewed over 𝕜' is a uniform embedding. In particular, it is injective and induces the uniform structure of the target space.
Русский
При фиксированном подполе 𝕜' ⊆ 𝕜 и для любых ι отображение ограничения скаляров из пространства непрерывных чередующихся ι‑арных линейных отображений над 𝕜 в аналогичное пространство над 𝕜' является равномерно вложением: инъективно сохраняет униформную структуру.
LaTeX
$$$\\text{IsUniformEmbedding}(\\operatorname{restrictScalars}_{\\mathsf{ }\\!\\mathbb{k}'})$$$
Lean4
theorem isUniformEmbedding_restrictScalars :
IsUniformEmbedding (restrictScalars 𝕜' : E [⋀^ι]→L[𝕜] F → E [⋀^ι]→L[𝕜'] F) :=
by
rw [← isUniformEmbedding_toContinuousMultilinearMap.of_comp_iff]
exact
(ContinuousMultilinearMap.isUniformEmbedding_restrictScalars 𝕜').comp isUniformEmbedding_toContinuousMultilinearMap
