English
In a domain R, there is a canonical bijection (as a multiplicative structure) between the nonzero-divisors associates of R and the principal ideals of R (viewed as a subset of (Ideal R)⁰).
Русский
В домене R существует каноническая биекция (как по структуре умножения) между ассоциатами не нулевых делителей R и главными идеалами R (считанными внутри (Ideal R)⁰).
LaTeX
$$$\mathrm{Associates}(R)^{0} \cong_* \{ I \in (\mathrm{Ideal}(R))^{0} \mid \mathrm{IsPrincipal}(I) \}$$$
Lean4
/-- A version of `Ideal.associatesEquivIsPrincipal` for non-zero-divisors generators. -/
noncomputable def associatesNonZeroDivisorsEquivIsPrincipal :
Associates R⁰ ≃ { I : (Ideal R)⁰ // IsPrincipal (I : Ideal R) } :=
calc
Associates R⁰ ≃ (Associates R)⁰ := associatesNonZeroDivisorsEquiv.toEquiv.symm
_ ≃ { I : { I : Ideal R // IsPrincipal I } // I.1 ∈ (Ideal R)⁰ } :=
(Equiv.subtypeEquiv (associatesEquivIsPrincipal R)
(fun x ↦ by
rw [← quot_out x, mk_mem_nonZeroDivisors_associates, associatesEquivIsPrincipal_apply,
span_singleton_nonZeroDivisors]))
_ ≃ { I : Ideal R // IsPrincipal I ∧ I ∈ (Ideal R)⁰ } :=
(Equiv.subtypeSubtypeEquivSubtypeInter (fun I ↦ IsPrincipal I) (fun I ↦ I ∈ (Ideal R)⁰))
_ ≃ { I : Ideal R // I ∈ (Ideal R)⁰ ∧ IsPrincipal I } := (Equiv.setCongr (by simp_rw [and_comm]))
_ ≃ { I : (Ideal R)⁰ // IsPrincipal I.1 } := (Equiv.subtypeSubtypeEquivSubtypeInter _ _).symm
