English
The map mkMMem from the class group of S to the class group of S is surjective; i.e., every class has a representative coming from mkMMem.
Русский
Отображение mkMMem в класс-группу S сюръективно: каждый класс имеет представитель, приходящий через mkMMem.
LaTeX
$$Function.Surjective (ClassGroup.mkMMem bS adm)$$
Lean4
/-- Each class in the class group contains an ideal `J`
such that `M := Π m ∈ finsetApprox` is in `J`. -/
theorem exists_mk0_eq_mk0 [IsDedekindDomain S] [Algebra.IsAlgebraic R S] (I : (Ideal S)⁰) :
∃ J : (Ideal S)⁰,
ClassGroup.mk0 I = ClassGroup.mk0 J ∧ algebraMap _ _ (∏ m ∈ finsetApprox bS adm, m) ∈ (J : Ideal S) :=
by
set M := ∏ m ∈ finsetApprox bS adm, m
have hM : algebraMap R S M ≠ 0 := prod_finsetApprox_ne_zero bS adm
obtain ⟨b, b_mem, b_ne_zero, b_min⟩ := exists_min abv I
suffices Ideal.span { b } ∣ Ideal.span {algebraMap _ _ M} * I.1
by
obtain ⟨J, hJ⟩ := this
refine ⟨⟨J, ?_⟩, ?_, ?_⟩
· rw [mem_nonZeroDivisors_iff_ne_zero]
rintro rfl
rw [Ideal.zero_eq_bot, Ideal.mul_bot] at hJ
exact hM (Ideal.span_singleton_eq_bot.mp (I.2.2 _ hJ))
· rw [ClassGroup.mk0_eq_mk0_iff]
exact ⟨algebraMap _ _ M, b, hM, b_ne_zero, hJ⟩
rw [← SetLike.mem_coe, ← Set.singleton_subset_iff, ← Ideal.span_le, ← Ideal.dvd_iff_le]
apply (mul_dvd_mul_iff_left _).mp _
swap; · exact mt Ideal.span_singleton_eq_bot.mp b_ne_zero
rw [Subtype.coe_mk, Ideal.dvd_iff_le, ← hJ, mul_comm]
apply Ideal.mul_mono le_rfl
rw [Ideal.span_le, Set.singleton_subset_iff]
exact b_mem
rw [Ideal.dvd_iff_le, Ideal.mul_le]
intro r' hr' a ha
rw [Ideal.mem_span_singleton] at hr' ⊢
obtain ⟨q, r, r_mem, lt⟩ := exists_mem_finset_approx' bS adm a b_ne_zero
apply @dvd_of_mul_left_dvd _ _ q
simp only [Algebra.smul_def] at lt
rw [← sub_eq_zero.mp (b_min _ (I.1.sub_mem (I.1.mul_mem_left _ ha) (I.1.mul_mem_left _ b_mem)) lt)]
refine mul_dvd_mul_right (dvd_trans (map_dvd _ ?_) hr') _
exact Multiset.dvd_prod (Multiset.mem_map.mpr ⟨_, r_mem, rfl⟩)
