# 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.

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

Instances For

source
theorem TwoSidedIdeal.subset_span {R : Type u_1} [NonUnitalNonAssocRing R] {s : Set R} :
s ⊆ ↑(span s)
source
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
source
theorem TwoSidedIdeal.span_mono {R : Type u_1} [NonUnitalNonAssocRing R] {s t : Set R} (h : s ⊆ t) :
span s ≤ span t
source
theorem TwoSidedIdeal.span_le {R : Type u_1} [NonUnitalNonAssocRing R] {s : Set R} {I : TwoSidedIdeal R} :
span s ≤ I ↔ s ⊆ ↑I
source
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`.

source
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)

Instances For

source
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
source
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.

Equations

- TwoSidedIdeal.comap f = { toFun := fun (I : TwoSidedIdeal S) => { ringCon := I.ringCon.comap f }, monotone' := ⋯ }

Instances For

source
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
source
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
source
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.

Equations

- e.mapTwoSidedIdeal = OrderIso.ofHomInv (TwoSidedIdeal.comap e.symm) (TwoSidedIdeal.comap e) ⋯ ⋯

Instances For

source
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
source
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
source
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
source
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.

source
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
source
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
source
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)
source
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)
source
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, ⋯⟩ }

source
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, ⋯⟩ }

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

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

source
@[simp]
theorem TwoSidedIdeal.coe_smul {R : Type u_1} [Ring R] (I : TwoSidedIdeal R) {r : R} {x : ↥I} :
r • ↑x = r * ↑x
source
instance TwoSidedIdeal.rightModule {R : Type u_1} [Ring R] (I : TwoSidedIdeal R) :
Module R ᵐᵒᵖ ↥I
Equations

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

source
@[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
source
instance TwoSidedIdeal.instSMulCommClassMulOppositeSubtypeMem {R : Type u_1} [Ring R] (I : TwoSidedIdeal R) :
SMulCommClass R R ᵐᵒᵖ ↥I
source
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' := ⋯ }

Instances For

source
@[simp]
theorem TwoSidedIdeal.subtype_apply {R : Type u_1} [Ring R] (I : TwoSidedIdeal R) (x : ↥I) :
I.subtype x = ↑x
source
theorem TwoSidedIdeal.subtype_injective {R : Type u_1} [Ring R] (I : TwoSidedIdeal R) :
Function.Injective ⇑I.subtype
source
@[simp]
theorem TwoSidedIdeal.coe_subtype {R : Type u_1} [Ring R] (I : TwoSidedIdeal R) :
⇑I.subtype = Subtype.val
source
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' := ⋯ }

Instances For

source
@[simp]
theorem TwoSidedIdeal.subtypeMop_apply {R : Type u_1} [Ring R] (I : TwoSidedIdeal R) (x : ↥I) :
I.subtypeMop x = MulOpposite.op ↑x
source
theorem TwoSidedIdeal.subtypeMop_injective {R : Type u_1} [Ring R] (I : TwoSidedIdeal R) :
Function.Injective ⇑I.subtypeMop
source
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' := ⋯ }

Instances For

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

Instances For

source
@[simp]
theorem TwoSidedIdeal.mem_asIdeal {R : Type u_1} [Ring R] {I : TwoSidedIdeal R} {x : R} :
x ∈ asIdeal I ↔ x ∈ I
source
theorem TwoSidedIdeal.gc {R : Type u_1} [Ring R] :
GaloisConnection ⇑fromIdeal ⇑asIdeal
source
@[simp]
theorem TwoSidedIdeal.coe_asIdeal {R : Type u_1} [Ring R] {I : TwoSidedIdeal R} :
↑(asIdeal I) = ↑I
source
@[simp]
theorem TwoSidedIdeal.bot_asIdeal {R : Type u_1} [Ring R] :
asIdeal ⊥ = ⊥
source
@[simp]
theorem TwoSidedIdeal.top_asIdeal {R : Type u_1} [Ring R] :
asIdeal ⊤ = ⊤
source
instance TwoSidedIdeal.instIsTwoSidedCoeOrderHomIdealAsIdeal {R : Type u_1} [Ring R] (I : TwoSidedIdeal R) :
(asIdeal I).IsTwoSided
source
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' := ⋯ }

Instances For

source
theorem TwoSidedIdeal.mem_asIdealOpposite {R : Type u_1} [Ring R] {I : TwoSidedIdeal R} {x : R ᵐᵒᵖ} :
x ∈ asIdealOpposite I ↔ MulOpposite.unop x ∈ I
source
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' := ⋯ }

Instances For

source
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`.

Equations

- I.toTwoSided = TwoSidedIdeal.mk' ↑I ⋯ ⋯ ⋯ ⋯ ⋯

Instances For

source
@[simp]
theorem Ideal.mem_toTwoSided {R : Type u_1} [Ring R] {I : Ideal R} [I.IsTwoSided] {x : R} :
x ∈ I.toTwoSided ↔ x ∈ I
source
@[simp]
theorem Ideal.coe_toTwoSided {R : Type u_1} [Ring R] (I : Ideal R) [I.IsTwoSided] :
↑I.toTwoSided = ↑I
source
@[simp]
theorem Ideal.toTwoSided_asIdeal {R : Type u_1} [Ring R] (I : TwoSidedIdeal R) :
(TwoSidedIdeal.asIdeal I).toTwoSided = I
source
@[simp]
theorem Ideal.asIdeal_toTwoSided {R : Type u_1} [Ring R] (I : Ideal R) [I.IsTwoSided] :
TwoSidedIdeal.asIdeal I.toTwoSided = I
source
instance Ideal.instCanLiftTwoSidedIdealCoeOrderHomAsIdealIsTwoSided {R : Type u_1} [Ring R] :
CanLift (Ideal R) (TwoSidedIdeal R) ⇑TwoSidedIdeal.asIdeal fun (x : Ideal R) => x.IsTwoSided
source
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.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[simp]
theorem TwoSidedIdeal.orderIsoIsTwoSided_apply_coe {R : Type u_1} [Ring R] (I : TwoSidedIdeal R) :
↑(orderIsoIsTwoSided I) = asIdeal I
source
@[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