English
There is a natural embedding of A into 𝓜(𝕜,A) given by a ↦ (L_a, R_a) where L_a and R_a are left and right multiplications by a.
Русский
В 𝓜(𝕜,A) существует естественное вложение A, отправляющее a в пару (L_a, R_a), где L_a и R_a — левое и правое умножения на a.
LaTeX
$$$\\text{coe}: A \\to 𝓜(\\mathbb{K},A),\\ a \\mapsto (L_a, R_a)$ with $L_a(x)=a x$, $R_a(x)=x a$$$
Lean4
/-- The natural coercion of `A` into `𝓜(𝕜, A)` given by sending `a : A` to the pair of linear
maps `Lₐ Rₐ : A →L[𝕜] A` given by left- and right-multiplication by `a`, respectively.
Warning: if `A = 𝕜`, then this is a coercion which is not definitionally equal to the
`algebraMap 𝕜 𝓜(𝕜, 𝕜)` coercion, but these are propositionally equal. See
`DoubleCentralizer.coe_eq_algebraMap` below. -/
@[coe]
protected noncomputable def coe (a : A) : 𝓜(𝕜, A) :=
{ fst := ContinuousLinearMap.mul 𝕜 A a
snd := (ContinuousLinearMap.mul 𝕜 A).flip a
central := fun _x _y => mul_assoc _ _ _ }
