English
Let M be a commutative monoid. The nth roots of unity inside the unit group M× are canonically isomorphic, as a multiplicative group, to the nth roots of unity inside M. Concretely there is a natural isomorphism between the subgroup of all ζ ∈ M× with ζ^n = 1 and the subgroup of elements x ∈ M with x^n = 1, given by forgetting the unit structure of ζ.
Русский
Пусть M — коммутативное моноидальное множество. Относительно n-й степени корней единицы внутри группы единиц M× существует каноническое мультиоднородное отображение на группу между корнями единицы в M× и корнями единицы в M; то есть существует канонический изоморфизм между двумя подгруппами: ζ^n = 1 в M× и x^n = 1 в M.
LaTeX
$$$\operatorname{RootsOfUnity}_n(M^{\times}) \cong_* \operatorname{RootsOfUnity}_n(M)$$$
Lean4
/-- The canonical isomorphism from the `n`th roots of unity in `Mˣ`
to the `n`th roots of unity in `M`. -/
def rootsOfUnityUnitsMulEquiv (M : Type*) [CommMonoid M] (n : ℕ) : rootsOfUnity n Mˣ ≃* rootsOfUnity n M
where
toFun ζ := ⟨ζ.val, (mem_rootsOfUnity ..).mpr <| (mem_rootsOfUnity' ..).mp ζ.prop⟩
invFun
ζ :=
⟨toUnits ζ.val, by
simp only [mem_rootsOfUnity, ← map_pow, EmbeddingLike.map_eq_one_iff]
exact (mem_rootsOfUnity ..).mp ζ.prop⟩
left_inv ζ := by simp only [toUnits_val_apply, Subtype.coe_eta]
right_inv ζ := by simp only [val_toUnits_apply, Subtype.coe_eta]
map_mul' ζ ζ' := by simp only [Subgroup.coe_mul, Units.val_mul, MulMemClass.mk_mul_mk]
