# Documentation

Mathlib.RingTheory.Ideal.Quotient

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

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} [] (I : ) :
One (R I)
def Ideal.Quotient.ringCon {R : Type u} [] (I : ) :

On Ideals, Submodule.quotientRel is a ring congruence.

Instances For
instance Ideal.Quotient.commRing {R : Type u} [] (I : ) :
instance Ideal.Quotient.isScalarTower_right {R : Type u} [] {I : } {α : Type u_1} [SMul α R] [] :
IsScalarTower α (R I) (R I)
instance Ideal.Quotient.smulCommClass {R : Type u} [] {I : } {α : Type u_1} [SMul α R] [] [] :
SMulCommClass α (R I) (R I)
instance Ideal.Quotient.smulCommClass' {R : Type u} [] {I : } {α : Type u_1} [SMul α R] [] [] :
SMulCommClass (R I) α (R I)
def Ideal.Quotient.mk {R : Type u} [] (I : ) :
R →+* R I

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

Instances For
theorem Ideal.Quotient.ringHom_ext {R : Type u} [] {I : } {S : Type v} [] ⦃f : R I →+* S ⦃g : R I →+* S (h : ) :
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} [] {I : } :
theorem Ideal.Quotient.eq {R : Type u} [] {I : } {x : R} {y : R} :
↑() x = ↑() y x - y I
@[simp]
theorem Ideal.Quotient.mk_eq_mk {R : Type u} [] {I : } (x : R) :
theorem Ideal.Quotient.eq_zero_iff_mem {R : Type u} [] {a : R} {I : } :
↑() a = 0 a I
theorem Ideal.Quotient.mk_eq_mk_iff_sub_mem {R : Type u} [] {I : } (x : R) (y : R) :
↑() x = ↑() y x - y I
theorem Ideal.Quotient.zero_eq_one_iff {R : Type u} [] {I : } :
0 = 1 I =
theorem Ideal.Quotient.zero_ne_one_iff {R : Type u} [] {I : } :
0 1 I
theorem Ideal.Quotient.nontrivial {R : Type u} [] {I : } (hI : I ) :
theorem Ideal.Quotient.mk_surjective {R : Type u} [] {I : } :
theorem Ideal.Quotient.quotient_ring_saturate {R : Type u} [] (I : ) (s : Set R) :
↑() ⁻¹' (↑() '' 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} [] (I : ) [hI : ] :
instance Ideal.Quotient.isDomain {R : Type u} [] (I : ) [hI : ] :
theorem Ideal.Quotient.isDomain_iff_prime {R : Type u} [] (I : ) :
theorem Ideal.Quotient.exists_inv {R : Type u} [] {I : } [hI : ] {a : R I} :
a 0b, a * b = 1
@[reducible]
noncomputable def Ideal.Quotient.groupWithZero {R : Type u} [] (I : ) [hI : ] :

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

Instances For
@[reducible]
noncomputable def Ideal.Quotient.field {R : Type u} [] (I : ) [hI : ] :
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].

Instances For
theorem Ideal.Quotient.maximal_of_isField {R : Type u} [] (I : ) (hqf : IsField (R I)) :

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

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

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

Instances For
@[simp]
theorem Ideal.Quotient.lift_mk {R : Type u} [] {a : R} {S : Type v} [] (I : ) (f : R →+* S) (H : ∀ (a : R), a If a = 0) :
↑() (↑() a) = f a
theorem Ideal.Quotient.lift_surjective_of_surjective {R : Type u} [] {S : Type v} [] (I : ) {f : R →+* S} (H : ∀ (a : R), a If a = 0) (hf : ) :
def Ideal.Quotient.factor {R : Type u} [] (S : ) (T : ) (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

Instances For
@[simp]
theorem Ideal.Quotient.factor_mk {R : Type u} [] (S : ) (T : ) (H : S T) (x : R) :
↑() (↑() x) = ↑() x
@[simp]
theorem Ideal.Quotient.factor_comp_mk {R : Type u} [] (S : ) (T : ) (H : S T) :
def Ideal.quotEquivOfEq {R : Type u_1} [] {I : } {J : } (h : I = J) :
R I ≃+* R J

Quotienting by equal ideals gives equivalent rings.

See also Submodule.quotEquivOfEq and Ideal.quotientEquivAlgOfEq.

Instances For
@[simp]
theorem Ideal.quotEquivOfEq_mk {R : Type u_1} [] {I : } {J : } (h : I = J) (x : R) :
↑() (↑() x) = ↑() x
@[simp]
theorem Ideal.quotEquivOfEq_symm {R : Type u_1} [] {I : } {J : } (h : I = J) :
instance Ideal.modulePi {R : Type u} [] (I : ) (ι : 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} [] (I : ) (ι : 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.

Instances For
theorem Ideal.map_pi {R : Type u} [] (I : ) {ι : Type u_1} [] {ι' : 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} [] {ι : Type v} (s : ) {f : ι} (hf : ∀ (i : ι), i s∀ (j : ι), j si jf i f j = ) (i : ι) (his : i s) :
r, r - 1 f i ∀ (j : ι), j sj ir f j
theorem Ideal.exists_sub_mem {R : Type u} [] {ι : Type v} [] {f : ι} (hf : ∀ (i j : ι), i jf i f j = ) (g : ιR) :
r, ∀ (i : ι), r - g i f i
def Ideal.quotientInfToPiQuotient {R : Type u} [] {ι : Type v} (f : ι) :
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.

Instances For
theorem Ideal.quotientInfToPiQuotient_bijective {R : Type u} [] {ι : Type v} [] {f : ι} (hf : ∀ (i j : ι), i jf i f j = ) :
noncomputable def Ideal.quotientInfRingEquivPiQuotient {R : Type u} [] {ι : Type v} [] (f : ι) (hf : ∀ (i j : ι), i jf 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

Instances For
noncomputable def Ideal.quotientInfEquivQuotientProd {R : Type u} [] (I : ) (J : ) (coprime : I J = ) :
R I J ≃+* (R I) × R J

Chinese remainder theorem, specialized to two ideals.

Instances For
@[simp]
theorem Ideal.quotientInfEquivQuotientProd_fst {R : Type u} [] (I : ) (J : ) (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} [] (I : ) (J : ) (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} [] (I : ) (J : ) (coprime : I J = ) :
@[simp]
theorem Ideal.snd_comp_quotientInfEquivQuotientProd {R : Type u} [] (I : ) (J : ) (coprime : I J = ) :