Documentation

Mathlib.RingTheory.TwoSidedIdeal.Operations

Operations on two-sided ideals #

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

Main definitions and results #

@[reducible, inline]

The smallest two-sided ideal containing a set.

Equations
theorem TwoSidedIdeal.mem_span_iff {R : Type u_1} [NonUnitalNonAssocRing R] {s : Set R} {x : R} :
x TwoSidedIdeal.span s ∀ (I : TwoSidedIdeal R), s Ix I
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) :

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

Equations
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) :
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) :

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

Equations
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} :
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] :

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

Equations
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} :
theorem TwoSidedIdeal.mem_span_iff_mem_addSubgroup_closure_absorbing {R : Type u_1} [NonUnitalRing R] {s : Set R} (h_left : ∀ (x y : R), y sx * y s) (h_right : ∀ (y x : R), y sy * x s) {z : R} :

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)

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

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

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

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

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 Ix * y I) :

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

Equations
@[simp]
theorem Ideal.mem_toTwoSided {R : Type u_1} [Ring R] {I : Ideal R} {h : ∀ {x y : R}, x Ix * 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 Ix * 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 Ix * 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 Ix * 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 Ix * y I
Equations
  • =