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.Quotient: the quotient of a commutative ring R by an ideal I : Ideal R

Main results

• Ideal.quotientInfRingEquivPiQuotient: the Chinese Remainder Theorem

@[reducible]

instance Ideal.instHasQuotientIdealToSemiringToCommSemiring {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 is marked reducible so that typeclass instances can be shared between Ideal.Quotient I and Submodule.Quotient I.

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

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

On Ideals, Submodule.quotientRel is a ring congruence.

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

instance Ideal.Quotient.isScalarTower_right {R : Type u} [CommRing R] {I : Ideal R} {α : Type u_1} [SMul α R] [IsScalarTower α R R] : IsScalarTower α (R ⧸ I) (R ⧸ I)

instance Ideal.Quotient.smulCommClass {R : Type u} [CommRing R] {I : Ideal R} {α : Type u_1} [SMul α R] [IsScalarTower α R R] [SMulCommClass α R R] : SMulCommClass α (R ⧸ I) (R ⧸ I)

instance Ideal.Quotient.smulCommClass' {R : Type u} [CommRing R] {I : Ideal R} {α : Type u_1} [SMul α R] [IsScalarTower α R R] [SMulCommClass R α R] : SMulCommClass (R ⧸ I) α (R ⧸ I)

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.

instance Ideal.Quotient.instCoeQuotientIdealToSemiringToCommSemiringInstHasQuotientIdealToSemiringToCommSemiring {R : Type u} [CommRing R] {I : Ideal R} : Coe R (R ⧸ 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 : RingHom.comp f (Ideal.Quotient.mk I) = RingHom.comp g (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)

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.zero_eq_one_iff {R : Type u} [CommRing R] {I : Ideal R} : 0 = 1 ↔ I = ⊤

theorem Ideal.Quotient.zero_ne_one_iff {R : Type u} [CommRing R] {I : Ideal R} : 0 ≠ 1 ↔ I ≠ ⊤

theorem Ideal.Quotient.nontrivial {R : Type u} [CommRing R] {I : Ideal R} (hI : I ≠ ⊤) : Nontrivial (R ⧸ I)

theorem Ideal.Quotient.subsingleton_iff {R : Type u} [CommRing R] {I : Ideal R} : Subsingleton (R ⧸ I) ↔ I = ⊤

instance Ideal.Quotient.instUniqueQuotientIdealToSemiringToCommSemiringInstHasQuotientIdealToSemiringToCommSemiringTopInstTopSubmoduleToAddCommMonoidToNonUnitalNonAssocSemiringToNonAssocSemiringToModule {R : Type u} [CommRing R] : Unique (R ⧸ ⊤)

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

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

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 : { x // x ∈ I }), (fun y => ↑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.

instance Ideal.Quotient.noZeroDivisors {R : Type u} [CommRing R] (I : Ideal R) [hI : Ideal.IsPrime I] : NoZeroDivisors (R ⧸ I)

instance Ideal.Quotient.isDomain {R : Type u} [CommRing R] (I : Ideal R) [hI : Ideal.IsPrime I] : IsDomain (R ⧸ I)

theorem Ideal.Quotient.isDomain_iff_prime {R : Type u} [CommRing R] (I : Ideal R) : IsDomain (R ⧸ I) ↔ Ideal.IsPrime I

theorem Ideal.Quotient.exists_inv {R : Type u} [CommRing R] {I : Ideal R} [hI : Ideal.IsMaximal I] {a : R ⧸ I} : a ≠ 0 → ∃ b, a * b = 1

@[reducible]

noncomputable def Ideal.Quotient.groupWithZero {R : Type u} [CommRing R] (I : Ideal R) [hI : Ideal.IsMaximal I] : GroupWithZero (R ⧸ I)

The quotient by a maximal ideal is a group with zero. This is a def rather than instance, since users will have computable inverses in some applications.

See note [reducible non-instances].

@[reducible]

noncomputable def Ideal.Quotient.field {R : Type u} [CommRing R] (I : Ideal R) [hI : Ideal.IsMaximal I] : Field (R ⧸ I)

The quotient by a maximal ideal is a field. This is a def rather than instance, since users will have computable inverses (and qsmul, rat_cast) in some applications.

See note [reducible non-instances].

theorem Ideal.Quotient.maximal_of_isField {R : Type u} [CommRing R] (I : Ideal R) (hqf : IsField (R ⧸ I)) : Ideal.IsMaximal I

If the quotient by an ideal is a field, then the ideal is maximal.

theorem Ideal.Quotient.maximal_ideal_iff_isField_quotient {R : Type u} [CommRing R] (I : Ideal R) : Ideal.IsMaximal I ↔ IsField (R ⧸ I)

The quotient of a ring by an ideal is a field iff the ideal is maximal.

def Ideal.Quotient.lift {R : Type u} [CommRing R] {S : Type v} [CommRing S] (I : Ideal R) (f : R →+* S) (H : ∀ (a : R), 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.

@[simp]

theorem Ideal.Quotient.lift_mk {R : Type u} [CommRing R] {a : R} {S : Type v} [CommRing S] (I : Ideal R) (f : R →+* S) (H : ∀ (a : R), 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} [CommRing S] (I : Ideal R) {f : R →+* S} (H : ∀ (a : R), 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

@[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) : RingHom.comp (Ideal.Quotient.factor S T H) (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.

@[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) : RingEquiv.symm (Ideal.quotEquivOfEq h) = Ideal.quotEquivOfEq (_ : J = I)

instance Ideal.modulePi {R : Type u} [CommRing R] (I : Ideal R) (ι : Type v) : Module (R ⧸ I) ((ι → R) ⧸ Ideal.pi I ι)

R^n/I^n is a R/I-module.

noncomputable def Ideal.piQuotEquiv {R : Type u} [CommRing R] (I : Ideal R) (ι : Type v) : ((ι → R) ⧸ Ideal.pi I ι) ≃ₗ[R ⧸ I] ι → R ⧸ I

R^n/I^n is isomorphic to (R/I)^n as an R/I-module.

theorem Ideal.map_pi {R : Type u} [CommRing R] (I : Ideal R) {ι : Type u_1} [Finite ι] {ι' : Type w} (x : ι → R) (hi : ∀ (i : ι), x i ∈ I) (f : (ι → R) →ₗ[R] ι' → R) (i : ι') : ↑f x i ∈ I

If f : R^n → R^m is an R-linear map and I ⊆ R is an ideal, then the image of I^n is contained in I^m.

theorem Ideal.exists_sub_one_mem_and_mem {R : Type u} [CommRing R] {ι : Type v} (s : Finset ι) {f : ι → Ideal R} (hf : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → f i ⊔ f j = ⊤) (i : ι) (his : i ∈ s) : ∃ r, r - 1 ∈ f i ∧ ∀ (j : ι), j ∈ s → j ≠ i → r ∈ f j

theorem Ideal.exists_sub_mem {R : Type u} [CommRing R] {ι : Type v} [Finite ι] {f : ι → Ideal R} (hf : ∀ (i j : ι), i ≠ j → f i ⊔ f j = ⊤) (g : ι → R) : ∃ r, ∀ (i : ι), r - g i ∈ f i

def Ideal.quotientInfToPiQuotient {R : Type u} [CommRing R] {ι : Type v} (f : ι → Ideal R) : R ⧸ ⨅ (i : ι), f i →+* (i : ι) → R ⧸ f i

The homomorphism from R/(⋂ i, f i) to ∏ i, (R / f i) featured in the Chinese Remainder Theorem. It is bijective if the ideals f i are comaximal.

theorem Ideal.quotientInfToPiQuotient_bijective {R : Type u} [CommRing R] {ι : Type v} [Finite ι] {f : ι → Ideal R} (hf : ∀ (i j : ι), i ≠ j → f i ⊔ f j = ⊤) : Function.Bijective ↑(Ideal.quotientInfToPiQuotient f)

noncomputable def Ideal.quotientInfRingEquivPiQuotient {R : Type u} [CommRing R] {ι : Type v} [Finite ι] (f : ι → Ideal R) (hf : ∀ (i j : ι), i ≠ j → f i ⊔ f j = ⊤) : R ⧸ ⨅ (i : ι), f i ≃+* ((i : ι) → R ⧸ f i)

Chinese Remainder Theorem. Eisenbud Ex.2.6. Similar to Atiyah-Macdonald 1.10 and Stacks 00DT

noncomputable def Ideal.quotientInfEquivQuotientProd {R : Type u} [CommRing R] (I : Ideal R) (J : Ideal R) (coprime : I ⊔ J = ⊤) : R ⧸ I ⊓ J ≃+* (R ⧸ I) × R ⧸ J

Chinese remainder theorem, specialized to two ideals.

@[simp]

theorem Ideal.quotientInfEquivQuotientProd_fst {R : Type u} [CommRing R] (I : Ideal R) (J : Ideal R) (coprime : I ⊔ J = ⊤) (x : R ⧸ I ⊓ J) : (↑(Ideal.quotientInfEquivQuotientProd I J coprime) x).fst = ↑(Ideal.Quotient.factor (I ⊓ J) I (_ : I ⊓ J ≤ I)) x

@[simp]

theorem Ideal.quotientInfEquivQuotientProd_snd {R : Type u} [CommRing R] (I : Ideal R) (J : Ideal R) (coprime : I ⊔ J = ⊤) (x : R ⧸ I ⊓ J) : (↑(Ideal.quotientInfEquivQuotientProd I J coprime) x).snd = ↑(Ideal.Quotient.factor (I ⊓ J) J (_ : I ⊓ J ≤ J)) x

@[simp]

theorem Ideal.fst_comp_quotientInfEquivQuotientProd {R : Type u} [CommRing R] (I : Ideal R) (J : Ideal R) (coprime : I ⊔ J = ⊤) : RingHom.comp (RingHom.fst (R ⧸ I) (R ⧸ J)) ↑(Ideal.quotientInfEquivQuotientProd I J coprime) = Ideal.Quotient.factor (I ⊓ J) I (_ : I ⊓ J ≤ I)

@[simp]

theorem Ideal.snd_comp_quotientInfEquivQuotientProd {R : Type u} [CommRing R] (I : Ideal R) (J : Ideal R) (coprime : I ⊔ J = ⊤) : RingHom.comp (RingHom.snd (R ⧸ I) (R ⧸ J)) ↑(Ideal.quotientInfEquivQuotientProd I J coprime) = Ideal.Quotient.factor (I ⊓ J) J (_ : I ⊓ J ≤ J)