Ideal quotients

This file defines ideal quotients as a special case of submodule quotients and proves some basic results about these quotients.

See Algebra.RingQuot for quotients of non-commutative rings.

Main definitions

• Ideal.instHasQuotient: the quotient of a commutative ring R by an ideal I : Ideal R
• Ideal.Quotient.commRing: the ring structure of the ideal quotient
• Ideal.Quotient.mk: map an element of R to the quotient R ⧸ I
• Ideal.Quotient.lift: turn a map R → S into a map R ⧸ I → S
• Ideal.quotEquivOfEq: quotienting by equal ideals gives isomorphic rings

@[reducible, inline]

instance Ideal.instHasQuotient {R : Type u} [CommRing R] : HasQuotient R (Ideal R)

The quotient R/I of a ring R by an ideal I.

The ideal quotient of I is defined to equal the quotient of I as an R-submodule of R. This definition uses abbrev so that typeclass instances can be shared between Ideal.Quotient I and Submodule.Quotient I.

Equations

• Ideal.instHasQuotient = Submodule.hasQuotient

instance Ideal.Quotient.one {R : Type u} [CommRing R] (I : Ideal R) : One (R ⧸ I)

Equations

• Ideal.Quotient.one I = { one := Submodule.Quotient.mk 1 }

def Ideal.Quotient.ringCon {R : Type u} [CommRing R] (I : Ideal R) : RingCon R

On Ideals, Submodule.quotientRel is a ring congruence.

Equations

• Ideal.Quotient.ringCon I = { toSetoid := (QuotientAddGroup.con (Submodule.toAddSubgroup I)).toSetoid, mul' := ⋯, add' := ⋯ }

instance Ideal.Quotient.commRing {R : Type u} [CommRing R] (I : Ideal R) : CommRing (R ⧸ I)

Equations

• Ideal.Quotient.commRing I = inferInstanceAs (CommRing (Ideal.Quotient.ringCon I).Quotient)

def Ideal.Quotient.mk {R : Type u} [CommRing R] (I : Ideal R) : R →+* R ⧸ I

The ring homomorphism from a ring R to a quotient ring R/I.

Equations

• Ideal.Quotient.mk I = { toFun := fun (a : R) => Submodule.Quotient.mk a, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

instance Ideal.Quotient.instCoeQuotient {R : Type u} [CommRing R] {I : Ideal R} : Coe R (R ⧸ I)

Equations

• Ideal.Quotient.instCoeQuotient = { coe := ⇑(Ideal.Quotient.mk I) }

theorem Ideal.Quotient.ringHom_ext_iff {R : Type u} [CommRing R] {I : Ideal R} {S : Type v} [NonAssocSemiring S] {f : R ⧸ I →+* S} {g : R ⧸ I →+* S} : f = g ↔ f.comp (Ideal.Quotient.mk I) = g.comp (Ideal.Quotient.mk I)

theorem Ideal.Quotient.ringHom_ext {R : Type u} [CommRing R] {I : Ideal R} {S : Type v} [NonAssocSemiring S] ⦃f : R ⧸ I →+* S⦄ ⦃g : R ⧸ I →+* S⦄ (h : f.comp (Ideal.Quotient.mk I) = g.comp (Ideal.Quotient.mk I)) : f = g

Two RingHoms from the quotient by an ideal are equal if their compositions with Ideal.Quotient.mk' are equal.

See note [partially-applied ext lemmas].

instance Ideal.Quotient.inhabited {R : Type u} [CommRing R] {I : Ideal R} : Inhabited (R ⧸ I)

Equations

• Ideal.Quotient.inhabited = { default := (Ideal.Quotient.mk I) 37 }

theorem Ideal.Quotient.eq {R : Type u} [CommRing R] {I : Ideal R} {x : R} {y : R} : (Ideal.Quotient.mk I) x = (Ideal.Quotient.mk I) y ↔ x - y ∈ I

@[simp]

theorem Ideal.Quotient.mk_eq_mk {R : Type u} [CommRing R] {I : Ideal R} (x : R) : Submodule.Quotient.mk x = (Ideal.Quotient.mk I) x

theorem Ideal.Quotient.eq_zero_iff_mem {R : Type u} [CommRing R] {a : R} {I : Ideal R} : (Ideal.Quotient.mk I) a = 0 ↔ a ∈ I

theorem Ideal.Quotient.mk_eq_mk_iff_sub_mem {R : Type u} [CommRing R] {I : Ideal R} (x : R) (y : R) : (Ideal.Quotient.mk I) x = (Ideal.Quotient.mk I) y ↔ x - y ∈ I

theorem Ideal.Quotient.mk_surjective {R : Type u} [CommRing R] {I : Ideal R} : Function.Surjective ⇑(Ideal.Quotient.mk I)

instance Ideal.Quotient.instRingHomSurjectiveQuotientMk {R : Type u} [CommRing R] {I : Ideal R} : RingHomSurjective (Ideal.Quotient.mk I)

Equations

• ⋯ = ⋯

theorem Ideal.Quotient.quotient_ring_saturate {R : Type u} [CommRing R] (I : Ideal R) (s : Set R) : ⇑(Ideal.Quotient.mk I) ⁻¹' (⇑(Ideal.Quotient.mk I) '' s) = ⋃ (x : ↥I), (fun (y : R) => ↑x + y) '' s

If I is an ideal of a commutative ring R, if q : R → R/I is the quotient map, and if s ⊆ R is a subset, then q⁻¹(q(s)) = ⋃ᵢ(i + s), the union running over all i ∈ I.

def Ideal.Quotient.lift {R : Type u} [CommRing R] {S : Type v} [Semiring S] (I : Ideal R) (f : R →+* S) (H : ∀ a ∈ I, f a = 0) : R ⧸ I →+* S

Given a ring homomorphism f : R →+* S sending all elements of an ideal to zero, lift it to the quotient by this ideal.

Equations

• Ideal.Quotient.lift I f H = { toFun := (↑(QuotientAddGroup.lift (Submodule.toAddSubgroup I) f.toAddMonoidHom H)).toFun, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem Ideal.Quotient.lift_mk {R : Type u} [CommRing R] {a : R} {S : Type v} [Semiring S] (I : Ideal R) (f : R →+* S) (H : ∀ a ∈ I, f a = 0) : (Ideal.Quotient.lift I f H) ((Ideal.Quotient.mk I) a) = f a

theorem Ideal.Quotient.lift_surjective_of_surjective {R : Type u} [CommRing R] {S : Type v} [Semiring S] (I : Ideal R) {f : R →+* S} (H : ∀ a ∈ I, f a = 0) (hf : Function.Surjective ⇑f) : Function.Surjective ⇑(Ideal.Quotient.lift I f H)

def Ideal.Quotient.factor {R : Type u} [CommRing R] (S : Ideal R) (T : Ideal R) (H : S ≤ T) : R ⧸ S →+* R ⧸ T

The ring homomorphism from the quotient by a smaller ideal to the quotient by a larger ideal.

This is the Ideal.Quotient version of Quot.Factor

Equations

• Ideal.Quotient.factor S T H = Ideal.Quotient.lift S (Ideal.Quotient.mk T) ⋯

@[simp]

theorem Ideal.Quotient.factor_mk {R : Type u} [CommRing R] (S : Ideal R) (T : Ideal R) (H : S ≤ T) (x : R) : (Ideal.Quotient.factor S T H) ((Ideal.Quotient.mk S) x) = (Ideal.Quotient.mk T) x

@[simp]

theorem Ideal.Quotient.factor_comp_mk {R : Type u} [CommRing R] (S : Ideal R) (T : Ideal R) (H : S ≤ T) : (Ideal.Quotient.factor S T H).comp (Ideal.Quotient.mk S) = Ideal.Quotient.mk T

def Ideal.quotEquivOfEq {R : Type u_1} [CommRing R] {I : Ideal R} {J : Ideal R} (h : I = J) : R ⧸ I ≃+* R ⧸ J

Quotienting by equal ideals gives equivalent rings.

See also Submodule.quotEquivOfEq and Ideal.quotientEquivAlgOfEq.

Equations

• Ideal.quotEquivOfEq h = { toFun := (↑(Submodule.quotEquivOfEq I J h)).toFun, invFun := (Submodule.quotEquivOfEq I J h).invFun, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯ }

@[simp]

theorem Ideal.quotEquivOfEq_mk {R : Type u_1} [CommRing R] {I : Ideal R} {J : Ideal R} (h : I = J) (x : R) : (Ideal.quotEquivOfEq h) ((Ideal.Quotient.mk I) x) = (Ideal.Quotient.mk J) x

@[simp]

theorem Ideal.quotEquivOfEq_symm {R : Type u_1} [CommRing R] {I : Ideal R} {J : Ideal R} (h : I = J) : (Ideal.quotEquivOfEq h).symm = Ideal.quotEquivOfEq ⋯