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

Main definitions

• Ideal.Quotient.Ring: the quotient of a ring R by a two-sided ideal I : Ideal R

@[simp]

theorem Ideal.Quotient.mk_span_range {ι : Type u_1} {R : Type u_3} [Ring R] (f : ι → R) [(span (Set.range f)).IsTwoSided] (i : ι) : (mk (span (Set.range f))) (f i) = 0

theorem Ideal.Quotient.zero_eq_one_iff {R : Type u_3} [Ring R] {I : Ideal R} : 0 = 1 ↔ I = ⊤

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

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

theorem Ideal.Quotient.nontrivial_iff {R : Type u_3} [Ring R] {I : Ideal R} : Nontrivial (R ⧸ I) ↔ I ≠ ⊤

@[deprecated Ideal.Quotient.nontrivial_iff (since := "2025-11-02")]

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

instance Ideal.Quotient.instUniqueQuotientTop {R : Type u_3} [Ring R] : Unique (R ⧸ ⊤)

@[instance 100]

instance Ideal.Quotient.isScalarTower_right {R : Type u_3} [Ring R] {I : Ideal R} [I.IsTwoSided] {α : Type u_5} [SMul α R] [IsScalarTower α R R] : IsScalarTower α (R ⧸ I) (R ⧸ I)

instance Ideal.Quotient.smulCommClass {R : Type u_3} [Ring R] {I : Ideal R} [I.IsTwoSided] {α : Type u_5} [SMul α R] [IsScalarTower α R R] [SMulCommClass α R R] : SMulCommClass α (R ⧸ I) (R ⧸ I)

instance Ideal.Quotient.smulCommClass' {R : Type u_3} [Ring R] {I : Ideal R} [I.IsTwoSided] {α : Type u_5} [SMul α R] [IsScalarTower α R R] [SMulCommClass R α R] : SMulCommClass (R ⧸ I) α (R ⧸ I)

theorem Ideal.Quotient.eq_zero_iff_dvd {R : Type u_5} [CommRing R] (x y : R) : (mk (span {x})) y = 0 ↔ x ∣ y

@[simp]

theorem Ideal.Quotient.mk_singleton_self {R : Type u_3} [Ring R] (x : R) [(span {x}).IsTwoSided] : (mk (span {x})) x = 0

instance Ideal.Quotient.noZeroDivisors {R : Type u_3} [Ring R] (I : Ideal R) [I.IsTwoSided] [hI : I.IsPrime] : NoZeroDivisors (R ⧸ I)

instance Ideal.Quotient.isDomain {R : Type u_3} [Ring R] (I : Ideal R) [I.IsTwoSided] [hI : I.IsPrime] : IsDomain (R ⧸ I)

theorem Ideal.Quotient.isDomain_iff_prime {R : Type u_3} [Ring R] (I : Ideal R) [I.IsTwoSided] : IsDomain (R ⧸ I) ↔ I.IsPrime

theorem Ideal.Quotient.exists_inv {R : Type u_3} [Ring R] {I : Ideal R} [I.IsTwoSided] [hI : I.IsMaximal] {a : R ⧸ I} : a ≠ 0 → ∃ (b : R ⧸ I), a * b = 1

@[reducible, inline]

noncomputable abbrev Ideal.Quotient.groupWithZero {R : Type u_3} [Ring R] (I : Ideal R) [I.IsTwoSided] [hI : I.IsMaximal] : 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, inline]

noncomputable abbrev Ideal.Quotient.divisionRing {R : Type u_3} [Ring R] (I : Ideal R) [I.IsTwoSided] [I.IsMaximal] : DivisionRing (R ⧸ I)

The quotient by a two-sided ideal that is maximal as a left ideal is a division ring. This is a def rather than instance, since users will have computable inverses (and qsmul, ratCast) in some applications.

See note [reducible non-instances].

@[reducible, inline]

noncomputable abbrev Ideal.Quotient.field {R : Type u_5} [CommRing R] (I : Ideal R) [I.IsMaximal] : Field (R ⧸ I)

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

See note [reducible non-instances].

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

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_5} [CommRing R] (I : Ideal R) : I.IsMaximal ↔ IsField (R ⧸ I)

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

instance Ideal.modulePi {ι : Type u_1} {R : Type u_3} [Ring R] (I : Ideal R) [I.IsTwoSided] : Module (R ⧸ I) ((ι → R) ⧸ pi fun (x : ι) => I)

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

noncomputable def Ideal.piQuotEquiv (ι : Type u_1) {R : Type u_3} [Ring R] (I : Ideal R) [I.IsTwoSided] : ((ι → R) ⧸ pi fun (x : ι) => I) ≃ₗ[R ⧸ I] ι → R ⧸ I

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

theorem Ideal.map_pi {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} [Ring R] (I : Ideal R) [I.IsTwoSided] [Finite ι] (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.univ_eq_iUnion_image_add {R : Type u_3} [Ring R] (I : Ideal R) : Set.univ = ⋃ (x : R ⧸ I), Quotient.out x +ᵥ ↑I

A ring is made up of a disjoint union of cosets of an ideal.

theorem finite_iff_ideal_quotient {R : Type u_3} [Ring R] (I : Ideal R) : Finite R ↔ Finite ↥I ∧ Finite (R ⧸ I)

theorem Finite.of_ideal_quotient {R : Type u_3} [Ring R] (I : Ideal R) [Finite ↥I] [Finite (R ⧸ I)] : Finite R

@[deprecated Finite.of_ideal_quotient (since := "2025-11-11")]

theorem Finite.of_finite_quot_finite_ideal {R : Type u_3} [Ring R] (I : Ideal R) [Finite ↥I] [Finite (R ⧸ I)] : Finite R

Alias of Finite.of_ideal_quotient.