English
Given a ring homomorphism σ from R to S, one can restrict σ to act on nth roots of unity: any nth root of unity in R maps to an nth root of unity in S, and this restriction is a monoid homomorphism between the corresponding root-of-unity subgroups.
Русский
Пусть существуют кольцевые гомоморфизмы σ: R → S; ограничивая σ на корни единицы порядка n, получаем гомоморфизм между подгруппами корней единицы в R и корней единицы в S.
LaTeX
$$$\exists \text{MonoidHom } (\operatorname{rootsOfUnity}_n(R) \to \operatorname{rootsOfUnity}_n(S)).$$$
Lean4
/-- Restrict a ring homomorphism to the nth roots of unity. -/
def restrictRootsOfUnity [MonoidHomClass F R S] (σ : F) (n : ℕ) : rootsOfUnity n R →* rootsOfUnity n S :=
{ toFun := fun ξ ↦
⟨Units.map σ (ξ : Rˣ),
by
rw [mem_rootsOfUnity, ← map_pow, Units.ext_iff, Units.coe_map, ξ.prop]
exact map_one σ⟩
map_one' := by ext1; simp only [OneMemClass.coe_one, map_one]
map_mul' := fun ξ₁ ξ₂ ↦ by ext1; simp only [Subgroup.coe_mul, map_mul, MulMemClass.mk_mul_mk] }
