English
There is a natural equivalence between the set of associates of R and the set of principal ideals of R, given by x mod units ↦ span{x} and its inverse sending a principal ideal to its generator.
Русский
Существует естественная эквивалентность между классами асоциированных элементов R и множеством главных идеалов R: x ↦ (x) и обратное отображение по генератору главного идеала.
LaTeX
$$$\\text{associatesEquivIsPrincipal} : (\\text{Associates }R) \\simeq {I : \\text{Ideal }R \\mid \\text{IsPrincipal } I}.$$$
Lean4
/-- The equivalence between `Associates R` and the principal ideals of `R` defined by sending the
class of `x` to the principal ideal generated by `x`. -/
noncomputable def associatesEquivIsPrincipal : Associates R ≃ { I : Ideal R // IsPrincipal I }
where
toFun := _root_.Quotient.lift (fun x ↦ ⟨span { x }, x, rfl⟩) (fun _ _ _ ↦ by simpa [span_singleton_eq_span_singleton])
invFun I := .mk I.2.generator
left_inv :=
Quotient.ind fun _ ↦ by
simpa using Ideal.span_singleton_eq_span_singleton.mp (@Ideal.span_singleton_generator _ _ _ ⟨_, rfl⟩)
right_inv I := by simp only [_root_.Quotient.lift_mk, span_singleton_generator, Subtype.coe_eta]
