English
The image of the torsion subgroup under a complex embedding equals the group of complex roots of unity of order torsionOrder(K).
Русский
Образ торсионной подгруппы единиц при комплексном вложении равен группе корней единицы комплексного числа порядка torsionOrder(K).
LaTeX
$$$(\mathrm{torsion}(K))^{\varphi} = \mathrm{rootsOfUnity}(\mathrm{torsionOrder}(K), \mathbb{C})$$$
Lean4
/-- The image of `torsion K` by a complex embedding is the group of complex roots of unity of
order `torsionOrder K`.
-/
theorem map_complexEmbedding_torsion (φ : K →+* ℂ) :
(torsion K).map (Units.complexEmbedding φ) = rootsOfUnity (torsionOrder K) ℂ :=
by
apply Subgroup.eq_of_le_of_card_ge
· rw [← rootsOfUnity_eq_torsion]
exact map_rootsOfUnity _ (torsionOrder K)
· let e :=
((torsion K).equivMapOfInjective (Units.complexEmbedding φ) (Units.complexEmbedding_injective φ)).symm.toEquiv
rw [Nat.card_eq_fintype_card, Complex.card_rootsOfUnity, Nat.card_congr e, torsionOrder, Nat.card_eq_fintype_card]
