Two Sided Ideals

In this file, for any Ring R, we reinterpret I : RingCon R as a two-sided-ideal of a ring.

Main definitions and results

• TwoSidedIdeal: For any NonUnitalNonAssocRing R, TwoSidedIdeal R is a wrapper around RingCon R.
• TwoSidedIdeal.setLike: Every I : TwoSidedIdeal R can be interpreted as a set of R where x ∈ I if and only if I.ringCon x 0.
• TwoSidedIdeal.addCommGroup: Every I : TwoSidedIdeal R is an abelian group.

structure TwoSidedIdeal (R : Type u_1) [NonUnitalNonAssocRing R] : Type u_1

A two-sided ideal of a ring R is a subset of R that contains 0 and is closed under addition, negation, and absorbs multiplication on both sides.

• ofRingCon :: (
• ringCon : RingCon R

  The congruence relation induced by this ideal.

• )

instance TwoSidedIdeal.instNontrivial {R : Type u_1} [NonUnitalNonAssocRing R] [Nontrivial R] : Nontrivial (TwoSidedIdeal R)

@[implicit_reducible]

instance TwoSidedIdeal.setLike {R : Type u_1} [NonUnitalNonAssocRing R] : SetLike (TwoSidedIdeal R) R

Equations

• TwoSidedIdeal.setLike = { coe := fun (t : TwoSidedIdeal R) => {r : R | t.ringCon r 0}, coe_injective := ⋯ }

@[implicit_reducible]

instance TwoSidedIdeal.instPartialOrder {R : Type u_1} [NonUnitalNonAssocRing R] : PartialOrder (TwoSidedIdeal R)

Equations

• TwoSidedIdeal.instPartialOrder = PartialOrder.ofSetLike (TwoSidedIdeal R) R

theorem TwoSidedIdeal.mem_iff {R : Type u_1} [NonUnitalNonAssocRing R] (I : TwoSidedIdeal R) (x : R) : x ∈ I ↔ I.ringCon x 0

@[simp]

theorem TwoSidedIdeal.mem_ofRingCon {R : Type u_1} [NonUnitalNonAssocRing R] {x : R} {c : RingCon R} : x ∈ { ringCon := c } ↔ c x 0

@[simp]

theorem TwoSidedIdeal.coe_ofRingCon {R : Type u_1} [NonUnitalNonAssocRing R] {c : RingCon R} : ↑{ ringCon := c } = {x : R | c x 0}

@[reducible, inline, deprecated TwoSidedIdeal.mk (since := "2026-06-18")]

abbrev TwoSidedIdeal.mk {R : Type u_1} [NonUnitalNonAssocRing R] (c : RingCon R) : TwoSidedIdeal R

A deprecated alias for ofRingCon.

Equations

• TwoSidedIdeal.mk c = { ringCon := c }

@[deprecated TwoSidedIdeal.mem_ofRingCon (since := "2026-06-18")]

theorem TwoSidedIdeal.mem_mk {R : Type u_1} [NonUnitalNonAssocRing R] {x : R} {c : RingCon R} : x ∈ mk c ↔ c x 0

@[deprecated TwoSidedIdeal.coe_ofRingCon (since := "2026-06-18")]

theorem TwoSidedIdeal.coe_mk {R : Type u_1} [NonUnitalNonAssocRing R] {c : RingCon R} : ↑(mk c) = {x : R | c x 0}

theorem TwoSidedIdeal.rel_iff {R : Type u_1} [NonUnitalNonAssocRing R] (I : TwoSidedIdeal R) (x y : R) : I.ringCon x y ↔ x - y ∈ I

def TwoSidedIdeal.coeOrderEmbedding {R : Type u_1} [NonUnitalNonAssocRing R] : TwoSidedIdeal R ↪o Set R

the coercion from two-sided-ideals to sets is an order embedding

Equations

• TwoSidedIdeal.coeOrderEmbedding = { toFun := SetLike.coe, inj' := ⋯, map_rel_iff' := ⋯ }

@[simp]

theorem TwoSidedIdeal.coeOrderEmbedding_apply {R : Type u_1} [NonUnitalNonAssocRing R] (a✝ : TwoSidedIdeal R) : coeOrderEmbedding a✝ = ↑a✝

theorem TwoSidedIdeal.le_iff {R : Type u_1} [NonUnitalNonAssocRing R] {I J : TwoSidedIdeal R} : I ≤ J ↔ ↑I ⊆ ↑J

def TwoSidedIdeal.orderIsoRingCon {R : Type u_1} [NonUnitalNonAssocRing R] : TwoSidedIdeal R ≃o RingCon R

Two-sided-ideals corresponds to congruence relations on a ring.

Equations

• TwoSidedIdeal.orderIsoRingCon = { toFun := TwoSidedIdeal.ringCon, invFun := TwoSidedIdeal.ofRingCon, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }

@[simp]

theorem TwoSidedIdeal.orderIsoRingCon_apply {R : Type u_1} [NonUnitalNonAssocRing R] (self : TwoSidedIdeal R) : orderIsoRingCon self = self.ringCon

@[simp]

theorem TwoSidedIdeal.orderIsoRingCon_symm_apply {R : Type u_1} [NonUnitalNonAssocRing R] (ringCon : RingCon R) : (RelIso.symm orderIsoRingCon) ringCon = { ringCon := ringCon }

theorem TwoSidedIdeal.ringCon_injective {R : Type u_1} [NonUnitalNonAssocRing R] : Function.Injective ringCon

theorem TwoSidedIdeal.ringCon_le_iff {R : Type u_1} [NonUnitalNonAssocRing R] {I J : TwoSidedIdeal R} : I ≤ J ↔ I.ringCon ≤ J.ringCon

theorem TwoSidedIdeal.ext {R : Type u_1} [NonUnitalNonAssocRing R] {I J : TwoSidedIdeal R} (h : ∀ (x : R), x ∈ I ↔ x ∈ J) : I = J

theorem TwoSidedIdeal.ext_iff {R : Type u_1} [NonUnitalNonAssocRing R] {I J : TwoSidedIdeal R} : I = J ↔ ∀ (x : R), x ∈ I ↔ x ∈ J

theorem TwoSidedIdeal.lt_iff {R : Type u_1} [NonUnitalNonAssocRing R] (I J : TwoSidedIdeal R) : I < J ↔ ↑I ⊂ ↑J

theorem TwoSidedIdeal.zero_mem {R : Type u_1} [NonUnitalNonAssocRing R] (I : TwoSidedIdeal R) : 0 ∈ I

theorem TwoSidedIdeal.add_mem {R : Type u_1} [NonUnitalNonAssocRing R] (I : TwoSidedIdeal R) {x y : R} (hx : x ∈ I) (hy : y ∈ I) : x + y ∈ I

theorem TwoSidedIdeal.neg_mem {R : Type u_1} [NonUnitalNonAssocRing R] (I : TwoSidedIdeal R) {x : R} (hx : x ∈ I) : -x ∈ I

instance TwoSidedIdeal.instAddSubgroupClass {R : Type u_1} [NonUnitalNonAssocRing R] : AddSubgroupClass (TwoSidedIdeal R) R

theorem TwoSidedIdeal.sub_mem {R : Type u_1} [NonUnitalNonAssocRing R] (I : TwoSidedIdeal R) {x y : R} (hx : x ∈ I) (hy : y ∈ I) : x - y ∈ I

theorem TwoSidedIdeal.mul_mem_left {R : Type u_1} [NonUnitalNonAssocRing R] (I : TwoSidedIdeal R) (x y : R) (hy : y ∈ I) : x * y ∈ I

theorem TwoSidedIdeal.mul_mem_right {R : Type u_1} [NonUnitalNonAssocRing R] (I : TwoSidedIdeal R) (x y : R) (hx : x ∈ I) : x * y ∈ I

theorem TwoSidedIdeal.nsmul_mem {R : Type u_1} [NonUnitalNonAssocRing R] (I : TwoSidedIdeal R) {x : R} (n : ℕ) (hx : x ∈ I) : n • x ∈ I

theorem TwoSidedIdeal.zsmul_mem {R : Type u_1} [NonUnitalNonAssocRing R] (I : TwoSidedIdeal R) {x : R} (n : ℤ) (hx : x ∈ I) : n • x ∈ I

def TwoSidedIdeal.mk' {R : Type u_1} [NonUnitalNonAssocRing R] (carrier : Set R) (zero_mem : 0 ∈ carrier) (add_mem : ∀ {x y : R}, x ∈ carrier → y ∈ carrier → x + y ∈ carrier) (neg_mem : ∀ {x : R}, x ∈ carrier → -x ∈ carrier) (mul_mem_left : ∀ {x y : R}, y ∈ carrier → x * y ∈ carrier) (mul_mem_right : ∀ {x y : R}, x ∈ carrier → x * y ∈ carrier) : TwoSidedIdeal R

The "set-theoretic-way" of constructing a two-sided ideal by providing:

• the underlying set S;
• a proof that 0 ∈ S;
• a proof that x + y ∈ S if x ∈ S and y ∈ S;
• a proof that -x ∈ S if x ∈ S;
• a proof that x * y ∈ S if y ∈ S;
• a proof that x * y ∈ S if x ∈ S.

Equations

• TwoSidedIdeal.mk' carrier zero_mem add_mem neg_mem mul_mem_left mul_mem_right = { ringCon := { r := fun (x y : R) => x - y ∈ carrier, iseqv := ⋯, mul' := ⋯, add' := ⋯ } }

@[simp]

theorem TwoSidedIdeal.mem_mk' {R : Type u_1} [NonUnitalNonAssocRing R] (carrier : Set R) (zero_mem : 0 ∈ carrier) (add_mem : ∀ {x y : R}, x ∈ carrier → y ∈ carrier → x + y ∈ carrier) (neg_mem : ∀ {x : R}, x ∈ carrier → -x ∈ carrier) (mul_mem_left : ∀ {x y : R}, y ∈ carrier → x * y ∈ carrier) (mul_mem_right : ∀ {x y : R}, x ∈ carrier → x * y ∈ carrier) (x : R) : x ∈ mk' carrier zero_mem add_mem neg_mem mul_mem_left mul_mem_right ↔ x ∈ carrier

@[simp]

theorem TwoSidedIdeal.coe_mk' {R : Type u_1} [NonUnitalNonAssocRing R] (carrier : Set R) (zero_mem : 0 ∈ carrier) (add_mem : ∀ {x y : R}, x ∈ carrier → y ∈ carrier → x + y ∈ carrier) (neg_mem : ∀ {x : R}, x ∈ carrier → -x ∈ carrier) (mul_mem_left : ∀ {x y : R}, y ∈ carrier → x * y ∈ carrier) (mul_mem_right : ∀ {x y : R}, x ∈ carrier → x * y ∈ carrier) : ↑(mk' carrier zero_mem add_mem neg_mem mul_mem_left mul_mem_right) = carrier

instance TwoSidedIdeal.instSMulMemClass {R : Type u_1} [NonUnitalNonAssocRing R] : SMulMemClass (TwoSidedIdeal R) R R

instance TwoSidedIdeal.instSMulMemClassMulOpposite {R : Type u_1} [NonUnitalNonAssocRing R] : SMulMemClass (TwoSidedIdeal R) Rᵐᵒᵖ R

@[implicit_reducible]

instance TwoSidedIdeal.instAddSubtypeMem {R : Type u_1} [NonUnitalNonAssocRing R] (I : TwoSidedIdeal R) : Add ↥I

Equations

• I.instAddSubtypeMem = { add := fun (x y : ↥I) => ⟨↑x + ↑y, ⋯⟩ }

@[implicit_reducible]

instance TwoSidedIdeal.instZeroSubtypeMem {R : Type u_1} [NonUnitalNonAssocRing R] (I : TwoSidedIdeal R) : Zero ↥I

Equations

• I.instZeroSubtypeMem = { zero := ⟨0, ⋯⟩ }

@[implicit_reducible]

instance TwoSidedIdeal.instSMulNatSubtypeMem {R : Type u_1} [NonUnitalNonAssocRing R] (I : TwoSidedIdeal R) : SMul ℕ ↥I

Equations

• I.instSMulNatSubtypeMem = { smul := fun (n : ℕ) (x : ↥I) => ⟨n • ↑x, ⋯⟩ }

@[implicit_reducible]

instance TwoSidedIdeal.instNegSubtypeMem {R : Type u_1} [NonUnitalNonAssocRing R] (I : TwoSidedIdeal R) : Neg ↥I

Equations

• I.instNegSubtypeMem = { neg := fun (x : ↥I) => ⟨-↑x, ⋯⟩ }

@[implicit_reducible]

instance TwoSidedIdeal.instSubSubtypeMem {R : Type u_1} [NonUnitalNonAssocRing R] (I : TwoSidedIdeal R) : Sub ↥I

Equations

• I.instSubSubtypeMem = { sub := fun (x y : ↥I) => ⟨↑x - ↑y, ⋯⟩ }

@[implicit_reducible]

instance TwoSidedIdeal.instSMulIntSubtypeMem {R : Type u_1} [NonUnitalNonAssocRing R] (I : TwoSidedIdeal R) : SMul ℤ ↥I

Equations

• I.instSMulIntSubtypeMem = { smul := fun (n : ℤ) (x : ↥I) => ⟨n • ↑x, ⋯⟩ }

@[implicit_reducible]

instance TwoSidedIdeal.addCommGroup {R : Type u_1} [NonUnitalNonAssocRing R] (I : TwoSidedIdeal R) : AddCommGroup ↥I

Equations

• I.addCommGroup = Function.Injective.addCommGroup (fun (a : ↥I) => ↑a) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

def TwoSidedIdeal.coeAddMonoidHom {R : Type u_1} [NonUnitalNonAssocRing R] (I : TwoSidedIdeal R) : ↥I →+ R

The coercion into the ring as a AddMonoidHom

Equations

• I.coeAddMonoidHom = { toFun := Subtype.val, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem TwoSidedIdeal.coeAddMonoidHom_apply {R : Type u_1} [NonUnitalNonAssocRing R] (I : TwoSidedIdeal R) (self : ↥I) : I.coeAddMonoidHom self = ↑self

def TwoSidedIdeal.op {R : Type u_1} [NonUnitalNonAssocRing R] (I : TwoSidedIdeal R) : TwoSidedIdeal Rᵐᵒᵖ

If I is a two-sided ideal of R, then {op x | x ∈ I} is a two-sided ideal in Rᵐᵒᵖ.

Equations

• I.op = { ringCon := I.ringCon.op }

@[simp]

theorem TwoSidedIdeal.op_ringCon {R : Type u_1} [NonUnitalNonAssocRing R] (I : TwoSidedIdeal R) : I.op.ringCon = I.ringCon.op

@[simp]

theorem TwoSidedIdeal.mem_op_iff {R : Type u_1} [NonUnitalNonAssocRing R] {I : TwoSidedIdeal R} {x : Rᵐᵒᵖ} : x ∈ I.op ↔ MulOpposite.unop x ∈ I

@[simp]

theorem TwoSidedIdeal.coe_op {R : Type u_1} [NonUnitalNonAssocRing R] {I : TwoSidedIdeal R} : ↑I.op = MulOpposite.unop ⁻¹' ↑I

def TwoSidedIdeal.unop {R : Type u_1} [NonUnitalNonAssocRing R] (I : TwoSidedIdeal Rᵐᵒᵖ) : TwoSidedIdeal R

If I is a two-sided ideal of Rᵐᵒᵖ, then {x.unop | x ∈ I} is a two-sided ideal in R.

Equations

• I.unop = { ringCon := I.ringCon.unop }

@[simp]

theorem TwoSidedIdeal.unop_ringCon {R : Type u_1} [NonUnitalNonAssocRing R] (I : TwoSidedIdeal Rᵐᵒᵖ) : I.unop.ringCon = I.ringCon.unop

@[simp]

theorem TwoSidedIdeal.mem_unop_iff {R : Type u_1} [NonUnitalNonAssocRing R] {I : TwoSidedIdeal Rᵐᵒᵖ} {x : R} : x ∈ I.unop ↔ MulOpposite.op x ∈ I

@[simp]

theorem TwoSidedIdeal.coe_unop {R : Type u_1} [NonUnitalNonAssocRing R] {I : TwoSidedIdeal Rᵐᵒᵖ} : ↑I.unop = MulOpposite.op ⁻¹' ↑I

def TwoSidedIdeal.opOrderIso {R : Type u_1} [NonUnitalNonAssocRing R] : TwoSidedIdeal R ≃o TwoSidedIdeal Rᵐᵒᵖ

Two-sided-ideals of A and that of Aᵒᵖ corresponds bijectively to each other.

Equations

• TwoSidedIdeal.opOrderIso = { toFun := TwoSidedIdeal.op, invFun := TwoSidedIdeal.unop, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }

@[simp]

theorem TwoSidedIdeal.opOrderIso_apply {R : Type u_1} [NonUnitalNonAssocRing R] (I : TwoSidedIdeal R) : opOrderIso I = I.op

@[simp]

theorem TwoSidedIdeal.opOrderIso_symm_apply {R : Type u_1} [NonUnitalNonAssocRing R] (I : TwoSidedIdeal Rᵐᵒᵖ) : (RelIso.symm opOrderIso) I = I.unop