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 : Set R} {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 : TwoSidedIdeal R} {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

def TwoSidedIdeal.ker {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 R

The kernel of a ring homomorphism, as a two-sided ideal.

Equations

• TwoSidedIdeal.ker f = TwoSidedIdeal.mk' {r : R | f r = 0} ⋯ ⋯ ⋯ ⋯ ⋯

theorem TwoSidedIdeal.mem_ker {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] {x : R} : x ∈ TwoSidedIdeal.ker f ↔ f x = 0

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)

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

• ⋯ = ⋯