English
The multiplier algebra 𝓜(𝕜,A) carries a normed ring structure obtained by pulling back the norm along the injective map toProdMulOppositeHom into the product of operator spaces; hence 𝓜(𝕜,A) is a normed ring.
Русский
У мультипликаторной алгебры 𝓜(𝕜,A) задаётся норма как обратная инъекции в произведение пространств операторов, и таким образом 𝓜(𝕜,A) является нормированной кольцевой структурой.
LaTeX
$$$\text{NormedRing}(\mathcal{M}(\mathbb{K},A))$ via $\text{NormedRing.induced}$ from $toProdMulOppositeHom$.$$
Lean4
/-- The normed group structure is inherited as the pullback under the ring monomorphism
`DoubleCentralizer.toProdMulOppositeHom : 𝓜(𝕜, A) →+* (A →L[𝕜] A) × (A →L[𝕜] A)ᵐᵒᵖ`. -/
noncomputable instance : NormedRing 𝓜(𝕜, A) :=
NormedRing.induced _ _ (toProdMulOppositeHom : 𝓜(𝕜, A) →+* (A →L[𝕜] A) × (A →L[𝕜] A)ᵐᵒᵖ)
(by simpa using toProdMulOpposite_injective)
-- even though the definition is actually in terms of `DoubleCentralizer.toProdMulOpposite`, we
-- choose to see through that here to avoid `MulOpposite.op` appearing.
