Operations on two-sided ideals

This file defines operations on two-sided ideals of a ring R.

Main definitions and results

• TwoSidedIdeal.span: the span of s ⊆ R is the smallest two-sided ideal containing the set.

• TwoSidedIdeal.mem_span_iff_mem_addSubgroup_closure_nonunital: in an associative but non-unital ring, an element x is in the two-sided ideal spanned by s if and only if x is in the closure of s ∪ {y * a | y ∈ s, a ∈ R} ∪ {a * y | y ∈ s, a ∈ R} ∪ {a * y * b | y ∈ s, a, b ∈ R} as an additive subgroup.

• TwoSidedIdeal.mem_span_iff_mem_addSubgroup_closure: in a unital and associative ring, an element x is in the two-sided ideal spanned by s if and only if x is in the closure of {a*y*b | a, b ∈ R, y ∈ s} as an additive subgroup.

• TwoSidedIdeal.comap: pullback of a two-sided ideal; defined as the preimage of a two-sided ideal.

• TwoSidedIdeal.map: pushforward of a two-sided ideal; defined as the span of the image of a two-sided ideal.

• TwoSidedIdeal.ker: the kernel of a ring homomorphism as a two-sided ideal.

• TwoSidedIdeal.gc: fromIdeal and asIdeal form a Galois connection where fromIdeal : Ideal R → TwoSidedIdeal R is defined as the smallest two-sided ideal containing an ideal and asIdeal : TwoSidedIdeal R → Ideal R the inclusion map.

@[reducible, inline]

abbrev TwoSidedIdeal.span {R : Type u_1} [NonUnitalNonAssocRing R] (s : Set R) : TwoSidedIdeal R

The smallest two-sided ideal containing a set.

Equations

• TwoSidedIdeal.span s = { ringCon := ringConGen fun (a b : R) => a - b ∈ s }

theorem TwoSidedIdeal.subset_span {R : Type u_1} [NonUnitalNonAssocRing R] {s : Set R} : s ⊆ ↑(TwoSidedIdeal.span s)

theorem TwoSidedIdeal.mem_span_iff {R : Type u_1} [NonUnitalNonAssocRing R] {s : Set R} {x : R} : x ∈ TwoSidedIdeal.span s ↔ ∀ (I : TwoSidedIdeal R), s ⊆ ↑I → x ∈ I

theorem TwoSidedIdeal.span_mono {R : Type u_1} [NonUnitalNonAssocRing R] {s t : Set R} (h : s ⊆ t) : TwoSidedIdeal.span s ≤ TwoSidedIdeal.span t

def TwoSidedIdeal.map {R : Type u_1} {S : Type u_2} [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] {F : Type u_3} [FunLike F R S] (f : F) (I : TwoSidedIdeal R) : TwoSidedIdeal S

Pushout of a two-sided ideal. Defined as the span of the image of a two-sided ideal under a ring homomorphism.

Equations

• TwoSidedIdeal.map f I = TwoSidedIdeal.span (⇑f '' ↑I)

theorem TwoSidedIdeal.map_mono {R : Type u_1} {S : Type u_2} [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] {F : Type u_3} [FunLike F R S] (f : F) {I J : TwoSidedIdeal R} (h : I ≤ J) : TwoSidedIdeal.map f I ≤ TwoSidedIdeal.map f J

def TwoSidedIdeal.comap {R : Type u_1} {S : Type u_2} [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] {F : Type u_3} [FunLike F R S] (f : F) [NonUnitalRingHomClass F R S] (I : TwoSidedIdeal S) : TwoSidedIdeal R

Preimage of a two-sided ideal, as a two-sided ideal.

Equations

• TwoSidedIdeal.comap f I = { ringCon := I.ringCon.comap f }

theorem TwoSidedIdeal.mem_comap {R : Type u_1} {S : Type u_2} [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] {F : Type u_3} [FunLike F R S] (f : F) [NonUnitalRingHomClass F R S] {I : TwoSidedIdeal S} {x : R} : x ∈ TwoSidedIdeal.comap f I ↔ f x ∈ I

theorem TwoSidedIdeal.mem_span_iff_mem_addSubgroup_closure_absorbing {R : Type u_1} [NonUnitalRing R] {s : Set R} (h_left : ∀ (x y : R), y ∈ s → x * y ∈ s) (h_right : ∀ (y x : R), y ∈ s → y * x ∈ s) {z : R} : z ∈ TwoSidedIdeal.span s ↔ z ∈ AddSubgroup.closure s

If s : Set R is absorbing under multiplication, then its TwoSidedIdeal.span coincides with its AddSubgroup.closure, as sets.

theorem TwoSidedIdeal.set_mul_subset {R : Type u_1} [NonUnitalRing R] {s : Set R} {I : TwoSidedIdeal R} (h : s ⊆ ↑I) (t : Set R) : t * s ⊆ ↑I

theorem TwoSidedIdeal.subset_mul_set {R : Type u_1} [NonUnitalRing R] {s : Set R} {I : TwoSidedIdeal R} (h : s ⊆ ↑I) (t : Set R) : s * t ⊆ ↑I

theorem TwoSidedIdeal.mem_span_iff_mem_addSubgroup_closure_nonunital {R : Type u_1} [NonUnitalRing R] {s : Set R} {z : R} : z ∈ TwoSidedIdeal.span s ↔ z ∈ AddSubgroup.closure (s ∪ s * Set.univ ∪ Set.univ * s ∪ Set.univ * s * Set.univ)

theorem TwoSidedIdeal.mem_span_iff_mem_addSubgroup_closure {R : Type u_1} [Ring R] {s : Set R} {z : R} : z ∈ TwoSidedIdeal.span s ↔ z ∈ AddSubgroup.closure (Set.univ * s * Set.univ)

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

• ⋯ = ⋯

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.subtype_apply {R : Type u_1} [Ring R] (I : TwoSidedIdeal R) (x : ↥I) : I.subtype x = ↑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' := ⋯ }

@[simp]

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

def TwoSidedIdeal.fromIdeal {R : Type u_1} [Ring R] : Ideal R →o TwoSidedIdeal R

Given an ideal I, span I is the smallest two-sided ideal containing I.

Equations

• TwoSidedIdeal.fromIdeal = { toFun := fun (I : Ideal R) => TwoSidedIdeal.span ↑I, monotone' := ⋯ }

theorem TwoSidedIdeal.mem_fromIdeal {R : Type u_1} [Ring R] {I : Ideal R} {x : R} : x ∈ TwoSidedIdeal.fromIdeal I ↔ x ∈ TwoSidedIdeal.span ↑I

def TwoSidedIdeal.asIdeal {R : Type u_1} [Ring R] : TwoSidedIdeal R →o Ideal R

Every two-sided ideal is also a left ideal.

Equations

• TwoSidedIdeal.asIdeal = { toFun := fun (I : TwoSidedIdeal R) => { carrier := ↑I, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }, monotone' := ⋯ }

@[simp]

theorem TwoSidedIdeal.mem_asIdeal {R : Type u_1} [Ring R] {I : TwoSidedIdeal R} {x : R} : x ∈ TwoSidedIdeal.asIdeal I ↔ x ∈ I

theorem TwoSidedIdeal.gc {R : Type u_1} [Ring R] : GaloisConnection ⇑TwoSidedIdeal.fromIdeal ⇑TwoSidedIdeal.asIdeal

@[simp]

theorem TwoSidedIdeal.coe_asIdeal {R : Type u_1} [Ring R] {I : TwoSidedIdeal R} : ↑(TwoSidedIdeal.asIdeal I) = ↑I

def TwoSidedIdeal.asIdealOpposite {R : Type u_1} [Ring R] : TwoSidedIdeal R →o Ideal Rᵐᵒᵖ

Every two-sided ideal is also a right ideal.

Equations

• TwoSidedIdeal.asIdealOpposite = { toFun := fun (I : TwoSidedIdeal R) => TwoSidedIdeal.asIdeal { ringCon := I.ringCon.op }, monotone' := ⋯ }

theorem TwoSidedIdeal.mem_asIdealOpposite {R : Type u_1} [Ring R] {I : TwoSidedIdeal R} {x : Rᵐᵒᵖ} : x ∈ TwoSidedIdeal.asIdealOpposite I ↔ MulOpposite.unop x ∈ I

def TwoSidedIdeal.orderIsoIdeal {R : Type u_1} [CommRing R] : TwoSidedIdeal R ≃o Ideal R

When the ring is commutative, two-sided ideals are exactly the same as left ideals.

Equations

• TwoSidedIdeal.orderIsoIdeal = { toFun := ⇑TwoSidedIdeal.asIdeal, invFun := ⇑TwoSidedIdeal.fromIdeal, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }

def Ideal.toTwoSided {R : Type u_1} [Ring R] (I : Ideal R) (mul_mem_right : ∀ {x y : R}, x ∈ I → x * y ∈ I) : TwoSidedIdeal R

Bundle an Ideal that is already two-sided as a TwoSidedIdeal.

Equations

• I.toTwoSided mul_mem_right = TwoSidedIdeal.mk' ↑I ⋯ ⋯ ⋯ ⋯ ⋯

@[simp]

theorem Ideal.mem_toTwoSided {R : Type u_1} [Ring R] {I : Ideal R} {h : ∀ {x y : R}, x ∈ I → x * y ∈ I} {x : R} : x ∈ I.toTwoSided h ↔ x ∈ I

@[simp]

theorem Ideal.coe_toTwoSided {R : Type u_1} [Ring R] (I : Ideal R) (h : ∀ {x y : R}, x ∈ I → x * y ∈ I) : ↑(I.toTwoSided h) = ↑I

@[simp]

theorem Ideal.toTwoSided_asIdeal {R : Type u_1} [Ring R] (I : TwoSidedIdeal R) (h : ∀ {x y : R}, x ∈ TwoSidedIdeal.asIdeal I → x * y ∈ TwoSidedIdeal.asIdeal I) : (TwoSidedIdeal.asIdeal I).toTwoSided h = I

@[simp]

theorem Ideal.asIdeal_toTwoSided {R : Type u_1} [Ring R] (I : Ideal R) (h : ∀ {x y : R}, x ∈ I → x * y ∈ I) : TwoSidedIdeal.asIdeal (I.toTwoSided h) = I

instance Ideal.instCanLiftTwoSidedIdealCoeOrderHomAsIdealForallForallForallMemHMul {R : Type u_1} [Ring R] : CanLift (Ideal R) (TwoSidedIdeal R) ⇑TwoSidedIdeal.asIdeal fun (I : Ideal R) => ∀ {x y : R}, x ∈ I → x * y ∈ I

Equations

• ⋯ = ⋯