English
Let R be a Dedekind domain. For nonzero fractional ideals I, J of R, the class of I equals the inverse of the class of J in the class group if and only if I J is principal, generated by a nonzero element x ∈ R.
Русский
Пусть R — дискретная норма, т. е. Дедекиндово кольцо. Пусть I и J — ненулевые дробные идеалы R. Элемент класса I равен обратному классу J в классовой группе тогда и только тогда, когда произведение I J является главен (principal), то есть порождено ненуленным элементом x ∈ R, как (x).
LaTeX
$$$[I] = [J]^{-1} \iff \exists x \neq 0 \in R,\; I J = (x).$$$
Lean4
theorem mk0_eq_mk0_inv_iff [IsDedekindDomain R] {I J : (Ideal R)⁰} :
ClassGroup.mk0 I = (ClassGroup.mk0 J)⁻¹ ↔ ∃ x ≠ (0 : R), I * J = Ideal.span { x } :=
by
rw [eq_inv_iff_mul_eq_one, ← map_mul, ClassGroup.mk0_eq_one_iff, Submodule.isPrincipal_iff, Submonoid.coe_mul]
refine ⟨fun ⟨a, ha⟩ ↦ ⟨a, ?_, ha⟩, fun ⟨a, _, ha⟩ ↦ ⟨a, ha⟩⟩
by_contra!
rw [this, Submodule.span_zero_singleton] at ha
exact nonZeroDivisors.coe_ne_zero _ <| J.prop.2 _ ha
