English
When R is commutative, the lattice of two-sided ideals is order-isomorphic to the lattice of ideals; the isomorphism is given by I ↦ I.asIdeal and its inverse by J ↦ J.fromIdeal.
Русский
При коммутативном кольце R равенство между двумя зколами: двусторонние идеалы и идеалы образуют единообразные решетки, связь задаётся посредством I ↦ I.asIdeal и обратное через J ↦ J.fromIdeal.
LaTeX
$$$\text{orderIsoIdeal} : TwoSidedIdeal(R) \simeq_{\mathrm{o}} \mathrm{Ideal}(R)$$$
Lean4
/-- When the ring is commutative, two-sided ideals are exactly the same as left ideals.
-/
def orderIsoIdeal : TwoSidedIdeal R ≃o Ideal R where
toFun := asIdeal
invFun := fromIdeal
map_rel_iff' := ⟨fun h _ hx ↦ h hx, fun h ↦ asIdeal.monotone' h⟩
left_inv _ := SetLike.ext fun _ ↦ mem_span_iff.trans <| by aesop
right_inv
J :=
SetLike.ext fun x ↦
mem_span_iff.trans
⟨fun h ↦
mem_mk' _ _ _ _ _ _ _ |>.1 <|
h (mk' J J.zero_mem J.add_mem J.neg_mem (J.mul_mem_left _) (J.mul_mem_right _)) (fun x => by simp),
by aesop⟩
