toDualContinuousMultilinearMap — Mathlib

English

The injective seminorm on the tensor product of a family of normed spaces is defined by embedding into all possible dual targets and taking the supremum of the induced seminorms.

Русский

Инъективная полуубыточная нормируемость на тензорном произведении семейства ньормированных пространств задаётся через вложение в все возможные двойственные пространства и взятие супремума индуцированных полунорм.

LaTeX

$$$\\text{injectiveSeminorm}: \\PiTensorProduct 𝕜 (E_i) \\to Seminorm$ определяется как верхняя грань над семинормами, получаемыми через toDualContinuousMultilinearMap и их композиции.$$

Lean4

/-- The linear map from `⨂[𝕜] i, Eᵢ` to `ContinuousMultilinearMap 𝕜 E F →L[𝕜] F` sending
`x` in `⨂[𝕜] i, Eᵢ` to the map `f ↦ f.lift x`.
-/
@[simps!]
noncomputable def toDualContinuousMultilinearMap : (⨂[𝕜] i, E i) →ₗ[𝕜] ContinuousMultilinearMap 𝕜 E F →L[𝕜] F
    where
  toFun
    x :=
    LinearMap.mkContinuous
      ((LinearMap.flip (lift (R := 𝕜) (s := E) (E := F)).toLinearMap x) ∘ₗ
        ContinuousMultilinearMap.toMultilinearMapLinear)
      (projectiveSeminorm x)
      (fun _ ↦
        by
        simp only [LinearMap.coe_comp, Function.comp_apply, ContinuousMultilinearMap.toMultilinearMapLinear_apply,
          LinearMap.flip_apply, LinearEquiv.coe_coe]
        exact norm_eval_le_projectiveSeminorm _ _ _)
  map_add' x
    y := by
    ext _
    simp only [map_add, LinearMap.mkContinuous_apply, LinearMap.coe_comp, Function.comp_apply,
      ContinuousMultilinearMap.toMultilinearMapLinear_apply, LinearMap.add_apply, LinearMap.flip_apply,
      LinearEquiv.coe_coe, ContinuousLinearMap.add_apply]
  map_smul' a
    x := by
    ext _
    simp only [map_smul, LinearMap.mkContinuous_apply, LinearMap.coe_comp, Function.comp_apply,
      ContinuousMultilinearMap.toMultilinearMapLinear_apply, LinearMap.smul_apply, LinearMap.flip_apply,
      LinearEquiv.coe_coe, RingHom.id_apply, ContinuousLinearMap.coe_smul', Pi.smul_apply]

Похожие утверждения