toContinuousLinearMap — Mathlib

English

There is a natural way to view an algebra homomorphism A →𝕜 as a continuous linear functional on A by associating it to its induced linear map.

Русский

Существуют естественные отображения алгебраического гомоморфизма $A \\to 𝕜$ в непрерывное линейное функциональное отображение на A через индуцированную линейную карту.

LaTeX

$$$\\text{toContinuousLinearMap}: (A \\to_{𝕜} 𝕜) \\to\\text{StrongDual}_{𝕜} A$$$

Lean4

/-- An algebra homomorphism into the base field, as a continuous linear map (since it is
automatically bounded). -/
def toContinuousLinearMap (φ : A →ₐ[𝕜] 𝕜) : StrongDual 𝕜 A :=
  { φ.toLinearMap with cont := map_continuous φ }

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