English
Let K be a CM-field. The index of the subgroup of the units of the ring of integers generated by the real units together with the roots of unity is equal to 2 if and only if there exists a unit u in the ring of integers of K such that the subgroup generated by the image of u under the complex-conjugation twist generates the torsion (roots of unity) subgroup of K.
Русский
Пусть K является полем CM. Индукция подгруппы единиц кольца целых O_K, порождаемая действительными единицами и корнями тождества, равна 2 тогда и только тогда существует единица u ∈ O_K^× такая, что порождаемая образом u под преобразованием через комплексного сопряжения подгруппа содержит всю torsion-подгруппу K (множество корней тождества).
LaTeX
$$$\\text{indexRealUnits}(K)=2 \\;\\iff\\; \\exists u \\in (\\mathcal{O}_K)^{\\times},\\; \\operatorname{zpowers}(\\mathrm{unitsMulComplexConjInv}(K,u))=\\top,$$$
Lean4
/-- The index of the subgroup of `(𝓞 K)ˣ` generated by the real units and the roots of unity is equal
to `2` iff there exists a unit whose image by `unitsMulComplexConjInv` generates the torsion
subgroup of `K`.
-/
theorem indexRealUnits_eq_two_iff :
indexRealUnits K = 2 ↔ ∃ u : (𝓞 K)ˣ, Subgroup.zpowers (unitsMulComplexConjInv K u) = ⊤ :=
by
suffices
(∃ u : (𝓞 K)ˣ, Subgroup.zpowers (unitsMulComplexConjInv K u) = ⊤) ↔ (unitsMulComplexConjInv K).range.index = 1
by
rw [this]
have h_eq := indexRealUnits_mul_eq K
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
· rwa [h, Nat.mul_eq_left two_ne_zero] at h_eq
· rwa [h, mul_one] at h_eq
refine ⟨fun ⟨u, hu⟩ ↦ Subgroup.index_eq_one.mpr (top_le_iff.mp ?_), fun h ↦ ?_⟩
· refine le_of_eq_of_le ?_ ((Subgroup.zpowers u).map_le_range (unitsMulComplexConjInv K))
rw [MonoidHom.map_zpowers, ← hu]
· obtain ⟨ζ, hζ⟩ := exists_zpow_surjective (torsion K)
rw [Subgroup.index_eq_one, MonoidHom.range_eq_top] at h
obtain ⟨u, rfl⟩ := h ζ
exact ⟨u, (Subgroup.eq_top_iff' _).mpr hζ⟩
