English
If I and J come from integral ideals I' and J' respectively, then mk I = mk J iff there exist x,y in R with xy ≠ 0 such that span{x}·I' = span{y}·J'.
Русский
Если I и J получены из интегральных идеалов I' и J' соответственно, то mk I = mk J тогда и только тогда существуют x,y∈R с xy ≠ 0 такие, что span{x}·I' = span{y}·J'.
LaTeX
$$$\mathrm{ClassGroup.mk}(I) = \mathrm{ClassGroup.mk}(J) \iff \exists x,y\in R,\; x\neq 0 \land y \neq 0 \land \mathrm{Ideal.span}\{x\} \cdot I' = \mathrm{Ideal.span}\{y\} \cdot J'.$$$
Lean4
theorem mk_eq_mk_of_coe_ideal {I J : (FractionalIdeal R⁰ <| FractionRing R)ˣ} {I' J' : Ideal R}
(hI : (I : FractionalIdeal R⁰ <| FractionRing R) = I') (hJ : (J : FractionalIdeal R⁰ <| FractionRing R) = J') :
ClassGroup.mk I = ClassGroup.mk J ↔ ∃ x y : R, x ≠ 0 ∧ y ≠ 0 ∧ Ideal.span { x } * I' = Ideal.span { y } * J' :=
by
rw [ClassGroup.mk_eq_mk]
constructor
· rintro ⟨x, rfl⟩
rw [Units.val_mul, hI, coe_toPrincipalIdeal, mul_comm, spanSingleton_mul_coeIdeal_eq_coeIdeal] at hJ
exact ⟨_, _, sec_fst_ne_zero x.ne_zero, sec_snd_ne_zero (R := R) le_rfl (x : FractionRing R), hJ⟩
· rintro ⟨x, y, hx, hy, h⟩
have : IsUnit (mk' (FractionRing R) x ⟨y, mem_nonZeroDivisors_of_ne_zero hy⟩) := by
simpa only [isUnit_iff_ne_zero, ne_eq, mk'_eq_zero_iff_eq_zero] using hx
refine ⟨this.unit, ?_⟩
rw [mul_comm, ← Units.val_inj, Units.val_mul, coe_toPrincipalIdeal]
convert (mk'_mul_coeIdeal_eq_coeIdeal (FractionRing R) <| mem_nonZeroDivisors_of_ne_zero hy).2 h
