English
Let G be a finite cyclic group of order n, and let G' be a commutative group containing a primitive n-th root of unity. Then for every element a in G with a ≠ 1 there exists a group homomorphism φ: G → G' such that φ(a) ≠ 1.
Русский
Пусть G — конечная циклическая группа порядка n, а G' — коммутативная группа, содержащая примитивный корень n-й степени единицы. Тогда для каждого элемента a ∈ G с a ≠ 1 существует гомоморфизм φ: G → G', такой что φ(a) ≠ 1.
LaTeX
$$$\\forall G\\,\\forall G'\\,\\text{with } G \\text{ finite cyclic of order } n, \\ G' \\text{ has a primitive } n\\text{-th root of unity} \\,\\Rightarrow \\, \\forall a \\in G\\ (a \\neq 1), \\exists \\phi: G \\to G', \\phi(a) \\neq 1.$$$
Lean4
/-- If `G` is cyclic of order `n` and `G'` contains a primitive `n`th root of unity,
then for each `a : G` with `a ≠ 1` there is a homomorphism `φ : G →* G'` such that `φ a ≠ 1`. -/
theorem exists_apply_ne_one {G G' : Type*} [Group G] [IsCyclic G] [Finite G] [CommGroup G']
(hG' : ∃ ζ : G', IsPrimitiveRoot ζ (Nat.card G)) ⦃a : G⦄ (ha : a ≠ 1) : ∃ φ : G →* G', φ a ≠ 1 :=
by
let inst : Fintype G := Fintype.ofFinite _
obtain ⟨ζ, hζ⟩ := hG'
obtain ⟨g, hg⟩ := IsCyclic.exists_generator (α := G)
have hζg : orderOf ζ ∣ orderOf g := by
rw [← hζ.eq_orderOf, orderOf_eq_card_of_forall_mem_zpowers hg, Nat.card_eq_fintype_card]
-- use the homomorphism `φ` given by `g ↦ ζ`
let φ := monoidHomOfForallMemZpowers hg hζg
have hφg : IsPrimitiveRoot (φ g) (Nat.card G) := by rwa [monoidHomOfForallMemZpowers_apply_gen hg hζg]
use φ
contrapose! ha
specialize hg a
rw [← mem_powers_iff_mem_zpowers, Submonoid.mem_powers_iff] at hg
obtain ⟨k, hk⟩ := hg
rw [← hk, map_pow] at ha
obtain ⟨l, rfl⟩ := (hφg.pow_eq_one_iff_dvd k).mp ha
rw [← hk, pow_mul, Nat.card_eq_fintype_card, pow_card_eq_one, one_pow]
