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.

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

theorem TwoSidedIdeal.mem_span_iff {R : Type u_1} [NonUnitalNonAssocRing R] {s : Set R} {x : R} : x ∈ 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) : span s ≤ span t

theorem TwoSidedIdeal.span_le {R : Type u_1} [NonUnitalNonAssocRing R] {s : Set R} {I : TwoSidedIdeal R} : span s ≤ I ↔ s ⊆ ↑I

theorem TwoSidedIdeal.span_induction {R : Type u_1} [NonUnitalNonAssocRing R] {s : Set R} {p : (x : R) → x ∈ span s → Prop} (mem : ∀ (x : R) (h : x ∈ s), p x ⋯) (zero : p 0 ⋯) (add : ∀ (x y : R) (hx : x ∈ span s) (hy : y ∈ span s), p x hx → p y hy → p (x + y) ⋯) (neg : ∀ (x : R) (hx : x ∈ span s), p x hx → p (-x) ⋯) (left_absorb : ∀ (a x : R) (hx : x ∈ span s), p x hx → p (a * x) ⋯) (right_absorb : ∀ (b x : R) (hx : x ∈ span s), p x hx → p (x * b) ⋯) {x : R} (hx : x ∈ span s) : p x hx

An induction principle for span membership.

If p holds for 0 and all elements of s, and is preserved under addition and left and right multiplication, then p holds for all elements of the span of s.

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.

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) : map f I ≤ 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] : TwoSidedIdeal S →o TwoSidedIdeal R

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

theorem TwoSidedIdeal.comap_le_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 J : TwoSidedIdeal S} (h : I ≤ J) : (comap f) I ≤ (comap f) J

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 ∈ (comap f) I ↔ f x ∈ I

def RingEquiv.mapTwoSidedIdeal {R : Type u_1} {S : Type u_2} [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] (e : R ≃+* S) : TwoSidedIdeal R ≃o TwoSidedIdeal S

If R and S are isomorphic as rings, then two-sided ideals of R and two-sided ideals of S are order isomorphic.

theorem RingEquiv.mapTwoSidedIdeal_apply {R : Type u_1} {S : Type u_2} [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] (e : R ≃+* S) (I : TwoSidedIdeal R) : e.mapTwoSidedIdeal I = (TwoSidedIdeal.comap e.symm) I

theorem RingEquiv.mapTwoSidedIdeal_symm {R : Type u_1} {S : Type u_2} [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] (e : R ≃+* S) : e.mapTwoSidedIdeal.symm = e.symm.mapTwoSidedIdeal

theorem TwoSidedIdeal.comap_comap {R : Type u_1} {S : Type u_2} {T : Type u_3} [NonAssocRing R] [NonAssocRing S] [NonAssocRing T] (I : TwoSidedIdeal T) (f : R →+* S) (g : S →+* T) : (comap f) ((comap g) I) = (comap (g.comp f)) 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 ∈ 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 ∈ 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 ∈ 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

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

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

@[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

@[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

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.

@[simp]

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

theorem TwoSidedIdeal.subtype_injective {R : Type u_1} [Ring R] (I : TwoSidedIdeal R) : Function.Injective ⇑I.subtype

@[simp]

theorem TwoSidedIdeal.coe_subtype {R : Type u_1} [Ring R] (I : TwoSidedIdeal R) : ⇑I.subtype = Subtype.val

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ᵐᵒᵖ.

@[simp]

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

theorem TwoSidedIdeal.subtypeMop_injective {R : Type u_1} [Ring R] (I : TwoSidedIdeal R) : Function.Injective ⇑I.subtypeMop

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.

theorem TwoSidedIdeal.mem_fromIdeal {R : Type u_1} [Ring R] {I : Ideal R} {x : R} : x ∈ fromIdeal I ↔ x ∈ 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.

@[simp]

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

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

@[simp]

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

@[simp]

theorem TwoSidedIdeal.bot_asIdeal {R : Type u_1} [Ring R] : asIdeal ⊥ = ⊥

@[simp]

theorem TwoSidedIdeal.top_asIdeal {R : Type u_1} [Ring R] : asIdeal ⊤ = ⊤

instance TwoSidedIdeal.instIsTwoSidedCoeOrderHomIdealAsIdeal {R : Type u_1} [Ring R] (I : TwoSidedIdeal R) : (asIdeal I).IsTwoSided

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

Every two-sided ideal is also a right ideal.

theorem TwoSidedIdeal.mem_asIdealOpposite {R : Type u_1} [Ring R] {I : TwoSidedIdeal R} {x : Rᵐᵒᵖ} : x ∈ 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.

def Ideal.toTwoSided {R : Type u_1} [Ring R] (I : Ideal R) [I.IsTwoSided] : TwoSidedIdeal R

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

@[simp]

theorem Ideal.mem_toTwoSided {R : Type u_1} [Ring R] {I : Ideal R} [I.IsTwoSided] {x : R} : x ∈ I.toTwoSided ↔ x ∈ I

@[simp]

theorem Ideal.coe_toTwoSided {R : Type u_1} [Ring R] (I : Ideal R) [I.IsTwoSided] : ↑I.toTwoSided = ↑I

@[simp]

theorem Ideal.toTwoSided_asIdeal {R : Type u_1} [Ring R] (I : TwoSidedIdeal R) : (TwoSidedIdeal.asIdeal I).toTwoSided = I

@[simp]

theorem Ideal.asIdeal_toTwoSided {R : Type u_1} [Ring R] (I : Ideal R) [I.IsTwoSided] : TwoSidedIdeal.asIdeal I.toTwoSided = I

instance Ideal.instCanLiftTwoSidedIdealCoeOrderHomAsIdealIsTwoSided {R : Type u_1} [Ring R] : CanLift (Ideal R) (TwoSidedIdeal R) ⇑TwoSidedIdeal.asIdeal fun (x : Ideal R) => x.IsTwoSided

def TwoSidedIdeal.orderIsoIsTwoSided {R : Type u_1} [Ring R] : TwoSidedIdeal R ≃o { I : Ideal R // I.IsTwoSided }

A two-sided ideal is simply a left ideal that is two-sided.

@[simp]

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

@[simp]

theorem TwoSidedIdeal.orderIsoIsTwoSided_symm_apply {R : Type u_1} [Ring R] (I : { I : Ideal R // I.IsTwoSided }) : (RelIso.symm orderIsoIsTwoSided) I = have this := ⋯; (↑I).toTwoSided