English
If I and J are units corresponding to ideals I' and J' respectively, then mk I = mk J is equivalent to the existence of x,y in R satisfying I' and J' relation via principal spans.
Русский
Если I и J — единичные дробные идеалы, соответствующие идеалам I' и J', тогда mk I = mk J эквивалентно существованию x,y из R, удовлетворяющих условию отношения через принципы порожденные идеалами.
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_one_of_coe_ideal {I : (FractionalIdeal R⁰ <| FractionRing R)ˣ} {I' : Ideal R}
(hI : (I : FractionalIdeal R⁰ <| FractionRing R) = I') :
ClassGroup.mk I = 1 ↔ ∃ x : R, x ≠ 0 ∧ I' = Ideal.span { x } :=
by
rw [← map_one (ClassGroup.mk (R := R) (K := FractionRing R)), ClassGroup.mk_eq_mk_of_coe_ideal hI]
any_goals rfl
constructor
· rintro ⟨x, y, hx, hy, h⟩
rw [Ideal.mul_top] at h
rcases Ideal.mem_span_singleton_mul.mp ((Ideal.span_singleton_le_iff_mem _).mp h.ge) with ⟨i, _hi, rfl⟩
rw [← Ideal.span_singleton_mul_span_singleton, Ideal.span_singleton_mul_right_inj hx] at h
exact ⟨i, by grobner, h⟩
· rintro ⟨x, hx, rfl⟩
exact ⟨1, x, one_ne_zero, hx, by rw [Ideal.span_singleton_one, Ideal.top_mul, Ideal.mul_top]⟩
