English
There is a canonical monoid hom from the units of α to α × αᵐᵒᵖ given by x ↦ (x, x^{-1}).
Русский
Существуют канонические моноид-гомоморфизм из единиц α в α × α^{op}, отправляющий x ↦ (x, x^{-1}).
LaTeX
$$$\\mathrm{embedProduct}: \\alpha^{\\times} \\to^* \\alpha \\times \\alpha^{\\mathrm{op}},\\quad \\mathrm{embedProduct}(x) = (x, x^{-1}).$$$
Lean4
/-- Canonical homomorphism of monoids from `αˣ` into `α × αᵐᵒᵖ`.
Used mainly to define the natural topology of `αˣ`. -/
@[to_additive (attr := simps) /-- Canonical homomorphism of additive monoids from `AddUnits α` into `α × αᵃᵒᵖ`.
Used mainly to define the natural topology of `AddUnits α`. -/
]
def embedProduct (α : Type*) [Monoid α] : αˣ →* α × αᵐᵒᵖ
where
toFun x := ⟨x, op ↑x⁻¹⟩
map_one' := by simp only [inv_one, Units.val_one, op_one, Prod.mk_eq_one, and_self_iff]
map_mul' x y := by simp only [mul_inv_rev, op_mul, Units.val_mul, Prod.mk_mul_mk]
