English
If G is a finite cyclic group, then the group homomorphisms G →* G′ are (noncanonically) in bijection with the nth roots of unity in G′, where n is the order of G.
Русский
Если G — конечная циклическая группа, то множество гомоморфизмов G →* G′ не канонически эр в биективном соответствии с n-ми корнями единицы в G′, где n — порядок G.
LaTeX
$$$\exists\text{ Nonempty } (G \to^* G') \cong\operatorname{rootsOfUnity}(\lvert G \rvert)G'$$$
Lean4
/-- The isomorphism from the group of group homomorphisms from a finite cyclic group `G` of order
`n` into another group `G'` to the group of `n`th roots of unity in `G'` determined by a generator
`g` of `G`. It sends `φ : G →* G'` to `φ g`. -/
noncomputable def monoidHomMulEquivRootsOfUnityOfGenerator {G : Type*} [CommGroup G] {g : G}
(hg : ∀ (x : G), x ∈ Subgroup.zpowers g) (G' : Type*) [CommGroup G'] : (G →* G') ≃* rootsOfUnity (Nat.card G) G'
where
toFun
φ :=
⟨(IsUnit.map φ <| Group.isUnit g).unit, by
simp only [mem_rootsOfUnity, Units.ext_iff, Units.val_pow_eq_pow_val, IsUnit.unit_spec, ← map_pow,
pow_card_eq_one', map_one, Units.val_one]⟩
invFun
ζ :=
monoidHomOfForallMemZpowers hg (g' := (ζ.val : G')) <| by
simpa only [orderOf_eq_card_of_forall_mem_zpowers hg, orderOf_dvd_iff_pow_eq_one, ← Units.val_pow_eq_pow_val,
Units.val_eq_one] using ζ.prop
left_inv
φ :=
(MonoidHom.eq_iff_eq_on_generator hg _ φ).mpr <| by
simp only [IsUnit.unit_spec, monoidHomOfForallMemZpowers_apply_gen]
right_inv φ := Subtype.ext <| by simp only [monoidHomOfForallMemZpowers_apply_gen, IsUnit.unit_of_val_units]
map_mul' x
y := by
simp only [MonoidHom.mul_apply, MulMemClass.mk_mul_mk, Subtype.mk.injEq, Units.ext_iff, IsUnit.unit_spec,
Units.val_mul]
