English
Let M be a commutative monoid containing an element ξ that is a primitive n-th root of unity, and let a ∈ ZMod n be nonzero. Then there exists a monoid homomorphism φ from the multiplicative monoid of ZMod n to the unit group Mˣ such that φ(ofAdd a) ≠ 1.
Русский
Пусть M — коммутативный моноид, содержащий элемент ξ, являющийся примитивным n-й корнем единства, и пусть a ∈ ZMod n так что a ≠ 0. Тогда существует моноидный гомоморфизм φ: Multiplicative(ZMod n) →* Mˣ с φ(Multiplicative.ofAdd a) ≠ 1.
LaTeX
$$$\\exists \\phi: \\mathrm{Multiplicative}(\\mathbb{Z}/n\\mathbb{Z}) \\to^* (M)^{\\times}, \\ \\phi(\\mathrm{Multiplicative.ofAdd}(a)) \\neq 1.$$$
Lean4
/-- If `M` is a commutative group that contains a primitive `n`th root of unity
and `a : ZMod n` is nonzero, then there exists a group homomorphism `φ` from the
additive group `ZMod n` to the multiplicative group `Mˣ` such that `φ a ≠ 1`. -/
theorem exists_monoidHom_apply_ne_one {M : Type*} [CommMonoid M] {n : ℕ} [NeZero n] (hG : ∃ ζ : M, IsPrimitiveRoot ζ n)
{a : ZMod n} (ha : a ≠ 0) : ∃ φ : Multiplicative (ZMod n) →* Mˣ, φ (Multiplicative.ofAdd a) ≠ 1 :=
by
obtain ⟨ζ, hζ⟩ := hG
have hc : n = Nat.card (Multiplicative (ZMod n)) := by
simp only [Nat.card_eq_fintype_card, Fintype.card_multiplicative, card]
exact
IsCyclic.exists_apply_ne_one (hc ▸ ⟨hζ.toRootsOfUnity.val, IsPrimitiveRoot.coe_units_iff.mp hζ⟩) <| by
simp only [ne_eq, ofAdd_eq_one, ha, not_false_eq_true]
