English
Equivalent principal-span condition expressed via mk0 for units representing fractional ideals.
Русский
Эквивалентность через условие, выраженное через mk0 для единичных дробных идеалов в терминах порождающих через FractionRing.
LaTeX
$$$\mathrm{mk0\_eq\_mk0\_iff}(I,J) \iff \exists x,y\in R, x\neq 0 \land y\neq 0 \land \text{(principal relations between } I',J').$$$
Lean4
theorem mk0_eq_mk0_iff [IsDedekindDomain R] {I J : (Ideal R)⁰} :
ClassGroup.mk0 I = ClassGroup.mk0 J ↔
∃ (x y : R) (_hx : x ≠ 0) (_hy : y ≠ 0), Ideal.span { x } * (I : Ideal R) = Ideal.span { y } * J :=
by
refine (ClassGroup.mk0_eq_mk0_iff_exists_fraction_ring (FractionRing R)).trans ⟨?_, ?_⟩
· rintro ⟨z, hz, h⟩
obtain ⟨x, ⟨y, hy⟩, rfl⟩ := IsLocalization.mk'_surjective R⁰ z
refine ⟨x, y, ?_, mem_nonZeroDivisors_iff_ne_zero.mp hy, ?_⟩
· rintro hx; apply hz
rw [hx, IsFractionRing.mk'_eq_div, map_zero, zero_div]
· exact (FractionalIdeal.mk'_mul_coeIdeal_eq_coeIdeal _ hy).mp h
· rintro ⟨x, y, hx, hy, h⟩
have hy' : y ∈ R⁰ := mem_nonZeroDivisors_iff_ne_zero.mpr hy
refine ⟨IsLocalization.mk' _ x ⟨y, hy'⟩, ?_, ?_⟩
· contrapose! hx
rwa [mk'_eq_iff_eq_mul, zero_mul, ← (algebraMap R (FractionRing R)).map_zero,
(IsFractionRing.injective R (FractionRing R)).eq_iff] at hx
· exact (FractionalIdeal.mk'_mul_coeIdeal_eq_coeIdeal _ hy').mpr h
