orderIsoRingCon — Mathlib

English

There is an order isomorphism between the lattice of two-sided ideals and the lattice of ring congruences, given by the ring-construction map I ↦ I.ringCon.

Русский

Существует изоморфизм по порядку между решетками двусторонних идеалов и кольцевых конгруэнций, задаваемый I ↦ I.ringCon.

LaTeX

$$TwoSidedIdeal R ≃o RingCon R$$

Lean4

/-- Two-sided-ideals corresponds to congruence relations on a ring. -/
@[simps apply symm_apply]
def orderIsoRingCon : TwoSidedIdeal R ≃o RingCon R
    where
  toFun := TwoSidedIdeal.ringCon
  invFun := .mk
  map_rel_iff'
    {I
      J} :=
    Iff.symm <|
      le_iff.trans
        ⟨fun h x y r => by rw [rel_iff] at r ⊢; exact h r, fun h x hx => by rw [SetLike.mem_coe, mem_iff] at hx ⊢;
          exact h hx⟩

Похожие утверждения