English
Under the same hypotheses as the injectivity lemma, the map from the torsion of K to (𝓞K/I)× is injective.
Русский
При тех же условиях, что и лемма инъекции, отображение отtorsion(K) в (𝓞K/I)× инъективно.
LaTeX
$$Same as 152097: injectivity of torsionMapQuot.$$
Lean4
theorem torsionMapQuot_injective (hI₁ : absNorm I ≠ 1) (hI₂ : (absNorm I).Coprime (torsionOrder K)) :
Function.Injective (torsionMapQuot I) :=
by
refine (injective_iff_map_eq_one _).mpr fun ⟨ζ, hζ⟩ h ↦ ?_
rw [← rootsOfUnity_eq_torsion] at hζ
obtain ⟨t, ht₀, ht, hζ⟩ := isPrimitiveRoot_of_mem_rootsOfUnity hζ
suffices ¬(2 ≤ t) by simpa [show t = 1 by grind] using hζ
intro ht'
let μ : K := ζ.val
have hμ : IsPrimitiveRoot μ t := (IsPrimitiveRoot.coe_units_iff.mpr hζ).map_of_injective RingOfIntegers.coe_injective
rw [Units.ext_iff, torsionMapQuot_apply, Units.val_one] at h
refine hμ.not_coprime_norm_of_mk_eq_one hI₁ ht' h ?_
exact Nat.dvd_one.mp (hI₂ ▸ Nat.gcd_dvd_gcd_of_dvd_right (absNorm I) ht)
