English
There is a group structure on the unit sphere S = { z ∈ 𝕜 : ∥z∥ = 1 }, transported from the unit group of 𝕜 by the injective map x ↦ unitSphereToUnits 𝕜 x. Concretely, for x,y ∈ S there exists a product x * y ∈ S defined by requiring unitSphereToUnits 𝕜 (x * y) = (unitSphereToUnits 𝕜 x)(unitSphereToUnits 𝕜 y). This makes S a group with the usual inverse coming from the ambient ring.
Русский
Существует групповая структура на единичной сфере S = { z ∈ 𝕜 : ∥z∥ = 1}, которая переносит элементарную групповую структуру единиц 𝕜 через инъективное отображение x ↦ unitSphereToUnits 𝕜 x. Конкретно, для x,y ∈ S существует произведение x * y ∈ S такое, что unitSphereToUnits 𝕜 (x * y) = (unitSphereToUnits 𝕜 x)(unitSphereToUnits 𝕜 y). Это задаёт S как группу, а обход обратной операции задаётся в окружении кольца.
LaTeX
$$$$S = \\{ z \\in 𝕜 : \\|z\\| = 1 \\},\\quad \\exists \\;\\cdot_S:\\; S\\times S\\to S\\ \\text{ such that }\\; \\mathrm{unitSphereToUnits}(𝕜)(x\\cdot_S y) = \\mathrm{unitSphereToUnits}(𝕜)(x)\\cdot \\mathrm{unitSphereToUnits}(𝕜)(y).$$$$
Lean4
instance instGroup [NormedDivisionRing 𝕜] : Group (sphere (0 : 𝕜) 1) :=
unitSphereToUnits_injective.group (unitSphereToUnits 𝕜) (Units.ext rfl) (fun _x _y => Units.ext rfl)
(fun _x => Units.ext rfl) (fun _x _y => Units.ext <| div_eq_mul_inv _ _)
(fun x n => Units.ext (Units.val_pow_eq_pow_val (unitSphereToUnits 𝕜 x) n).symm) fun x n =>
Units.ext (Units.val_zpow_eq_zpow_val (unitSphereToUnits 𝕜 x) n).symm
