English
Let G be a finite commutative group of exponent n, and let M be a commutative monoid with enough n-th roots of unity. Then for every element a in G with a ≠ 1 (the identity), there exists a group homomorphism φ from G to the group of units of M such that φ(a) ≠ 1.
Русский
Пусть G — конечная коммутативная группа экспонента n, а M — коммутативный моноид, в котором достаточно n-й корней единства. Тогда для любого элемента a ∈ G, отличного от единицы, существует гомоморфизм φ: G → Mˣ такой, что φ(a) ≠ 1.
LaTeX
$$$\\forall a \\in G,\\ a \\neq 1 \\Rightarrow \\exists \\varphi \\in \\operatorname{Hom}(G, M^{\\times}),\\ \\varphi(a) \\neq 1$$$
Lean4
/-- If `G` is a finite commutative group of exponent `n` and `M` is a commutative monoid
with enough `n`th roots of unity, then for each `a ≠ 1` in `G`, there exists a
group homomorphism `φ : G → Mˣ` such that `φ a ≠ 1`. -/
theorem exists_apply_ne_one_of_hasEnoughRootsOfUnity {a : G} (ha : a ≠ 1) : ∃ φ : G →* Mˣ, φ a ≠ 1 :=
by
refine exists_apply_ne_one_aux G Mˣ (fun n hn a ha₀ ↦ ?_) ha
have : NeZero n := ⟨fun H ↦ NeZero.ne _ <| Nat.eq_zero_of_zero_dvd (H ▸ hn)⟩
have := HasEnoughRootsOfUnity.of_dvd M hn
exact ZMod.exists_monoidHom_apply_ne_one (HasEnoughRootsOfUnity.exists_primitiveRoot M n) ha₀
