English
For every class C in the class group of 𝓞_K there exists a representative I in that class with absNorm(I) ≤ M(K).
Русский
Для каждого класса C в группе классов 𝓞_K существует представитель I этого класса с absNorm(I) ≤ M(K).
LaTeX
$$$\exists I \in (\mathrm{Ideal}(\mathcal{O}_K))^{\circ},\; \mathrm{ClassGroup.mk0}(I)=C \land \mathrm{absNorm}(I) \le M(K)$$$
Lean4
theorem exists_ideal_in_class_of_norm_le (C : ClassGroup (𝓞 K)) :
∃ I : (Ideal (𝓞 K))⁰, ClassGroup.mk0 I = C ∧ absNorm (I : Ideal (𝓞 K)) ≤ M K :=
by
obtain ⟨J, hJ⟩ := ClassGroup.mk0_surjective C⁻¹
obtain ⟨_, ⟨a, ha, rfl⟩, h_nz, h_nm⟩ := exists_ne_zero_mem_ideal_of_norm_le_mul_sqrt_discr K (FractionalIdeal.mk0 K J)
obtain ⟨I₀, hI⟩ := dvd_iff_le.mpr ((span_singleton_le_iff_mem J).mpr (by exact ha))
have : I₀ ≠ 0 := by
contrapose! h_nz
rw [h_nz, mul_zero, zero_eq_bot, span_singleton_eq_bot] at hI
rw [Algebra.linearMap_apply, hI, map_zero]
let I := (⟨I₀, mem_nonZeroDivisors_iff_ne_zero.mpr this⟩ : (Ideal (𝓞 K))⁰)
refine ⟨I, ?_, ?_⟩
· suffices ClassGroup.mk0 I = (ClassGroup.mk0 J)⁻¹ by rw [this, hJ, inv_inv]
exact ClassGroup.mk0_eq_mk0_inv_iff.mpr ⟨a, Subtype.coe_ne_coe.1 h_nz, by rw [mul_comm, hI]⟩
· rw [← FractionalIdeal.absNorm_span_singleton (𝓞 K), Algebra.linearMap_apply, ←
FractionalIdeal.coeIdeal_span_singleton, FractionalIdeal.coeIdeal_absNorm, hI, map_mul, cast_mul, Rat.cast_mul,
absNorm_apply, Rat.cast_natCast, Rat.cast_natCast, FractionalIdeal.coe_mk0, FractionalIdeal.coeIdeal_absNorm,
Rat.cast_natCast, mul_div_assoc, mul_assoc, mul_assoc] at h_nm
refine le_of_mul_le_mul_of_pos_left h_nm ?_
exact cast_pos.mpr <| pos_of_ne_zero <| absNorm_ne_zero_of_nonZeroDivisors J
