English
The image of the natural injection toProdMulOpposite consists precisely of those pairs (f, g) such that for all x, y in A, unop(g)(x) y = x f(y).
Русский
Образ естественной инъекции toProdMulOpposite состоит ровно из пар (f, g), для которых для всех x, y в A выполнено unop(g)(x) y = x f(y).
LaTeX
$$$\\mathrm{range}(\mathrm{toProdMulOpposite}) = \\{ (f,g) \\in (A \\to_L A) \\times (A \\to_L A)^{\\mathrm{op}} \\mid \\forall x,y\\in A,\\; \\mathrm{unop}(g)(x) \\cdot y = x \\cdot (f(y)) \\}$$$
Lean4
/-- The natural injection from `DoubleCentralizer.toProd` except the second coordinate inherits
`MulOpposite.op`. The ring structure on `𝓜(𝕜, A)` is the pullback under this map. -/
def toProdMulOpposite : 𝓜(𝕜, A) → (A →L[𝕜] A) × (A →L[𝕜] A)ᵐᵒᵖ := fun a => (a.fst, MulOpposite.op a.snd)
