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.

• ringCon : RingCon R

  every two-sided-ideal is induced by a congruence relation on the ring.

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

Equations

• ⋯ = ⋯

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' := ⋯ }

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

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

@[simp]

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

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' := ⋯ }

theorem TwoSidedIdeal.le_iff {R : Type u_1} [NonUnitalNonAssocRing R] {I : TwoSidedIdeal R} {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.mk, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }

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

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

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

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

theorem TwoSidedIdeal.lt_iff {R : Type u_1} [NonUnitalNonAssocRing R] (I : TwoSidedIdeal R) (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 : R} {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

Equations

• ⋯ = ⋯

theorem TwoSidedIdeal.sub_mem {R : Type u_1} [NonUnitalNonAssocRing R] (I : TwoSidedIdeal R) {x : R} {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 : R) (y : R) (hy : y ∈ I) : x * y ∈ I

theorem TwoSidedIdeal.mul_mem_right {R : Type u_1} [NonUnitalNonAssocRing R] (I : TwoSidedIdeal R) (x : R) (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 ∈ TwoSidedIdeal.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) : ↑(TwoSidedIdeal.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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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' := ⋯ }

instance TwoSidedIdeal.instSMulSubtypeMem {R : Type u_1} [Ring R] (I : TwoSidedIdeal R) : SMul R ↥I

Equations

• I.instSMulSubtypeMem = { smul := fun (r : R) (x : ↥I) => ⟨r • ↑x, ⋯⟩ }

instance TwoSidedIdeal.instSMulMulOppositeSubtypeMem {R : Type u_1} [Ring R] (I : TwoSidedIdeal R) : SMul Rᵐᵒᵖ ↥I

Equations

• I.instSMulMulOppositeSubtypeMem = { smul := fun (r : Rᵐᵒᵖ) (x : ↥I) => ⟨r • ↑x, ⋯⟩ }

instance TwoSidedIdeal.leftModule {R : Type u_1} [Ring R] (I : TwoSidedIdeal R) : Module R ↥I

Equations

• I.leftModule = Function.Injective.module R I.coeAddMonoidHom ⋯ ⋯

@[simp]

theorem TwoSidedIdeal.coe_smul {R : Type u_1} [Ring R] (I : TwoSidedIdeal R) {r : R} {x : ↥I} : r • ↑x = r * ↑x

instance TwoSidedIdeal.rightModule {R : Type u_1} [Ring R] (I : TwoSidedIdeal R) : Module Rᵐᵒᵖ ↥I

Equations

• I.rightModule = Function.Injective.module Rᵐᵒᵖ I.coeAddMonoidHom ⋯ ⋯

@[simp]

theorem TwoSidedIdeal.coe_mop_smul {R : Type u_1} [Ring R] (I : TwoSidedIdeal R) {r : Rᵐᵒᵖ} {x : ↥I} : r • ↑x = ↑x * MulOpposite.unop r

instance TwoSidedIdeal.instSMulCommClassMulOppositeSubtypeMem {R : Type u_1} [Ring R] (I : TwoSidedIdeal R) : SMulCommClass R Rᵐᵒᵖ ↥I

Equations

• ⋯ = ⋯

@[simp]

theorem TwoSidedIdeal.subtype_apply {R : Type u_1} [Ring R] (I : TwoSidedIdeal R) (x : ↥I) : I.subtype x = ↑x

def TwoSidedIdeal.subtype {R : Type u_1} [Ring R] (I : TwoSidedIdeal R) : ↥I →ₗ[R] R

For any I : RingCon R, when we view it as an ideal, I.subtype is the injective R-linear map I → R.

Equations

• I.subtype = { toFun := fun (x : ↥I) => ↑x, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem TwoSidedIdeal.subtypeMop_apply {R : Type u_1} [Ring R] (I : TwoSidedIdeal R) (x : ↥I) : I.subtypeMop x = MulOpposite.op ↑x

def TwoSidedIdeal.subtypeMop {R : Type u_1} [Ring R] (I : TwoSidedIdeal R) : ↥I →ₗ[Rᵐᵒᵖ] Rᵐᵒᵖ

For any RingCon R, when we view it as an ideal in Rᵒᵖ, subtype is the injective Rᵐᵒᵖ-linear map I → Rᵐᵒᵖ.

Equations

• I.subtypeMop = { toFun := fun (x : ↥I) => MulOpposite.op ↑x, map_add' := ⋯, map_smul' := ⋯ }