# mathlib3documentation

ring_theory.ideal.quotient

# Ideal quotients #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

See algebra.ring_quot 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.quotient_inf_ring_equiv_pi_quotient: the Chinese Remainder Theorem
@[protected, instance, reducible]
def ideal.has_quotient {R : Type u} [comm_ring 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.

Equations
@[protected, instance]
def ideal.quotient.has_one {R : Type u} [comm_ring R] (I : ideal R) :
has_one (R I)
Equations
@[protected]
def ideal.quotient.ring_con {R : Type u} [comm_ring R] (I : ideal R) :

On ideals, submodule.quotient_rel is a ring congruence.

Equations
@[protected, instance]
def ideal.quotient.comm_ring {R : Type u} [comm_ring R] (I : ideal R) :
Equations
@[protected, instance]
def ideal.quotient.is_scalar_tower_right {R : Type u} [comm_ring R] {I : ideal R} {α : Type u_1} [ R] [ R] :
(R I) (R I)
@[protected, instance]
def ideal.quotient.smul_comm_class {R : Type u} [comm_ring R] {I : ideal R} {α : Type u_1} [ R] [ R] [ R] :
(R I) (R I)
@[protected, instance]
def ideal.quotient.smul_comm_class' {R : Type u} [comm_ring R] {I : ideal R} {α : Type u_1} [ R] [ R] [ R] :
smul_comm_class (R I) α (R I)
def ideal.quotient.mk {R : Type u} [comm_ring R] (I : ideal R) :
R →+* R I

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

Equations
Instances for ideal.quotient.mk
@[ext]
theorem ideal.quotient.ring_hom_ext {R : Type u} [comm_ring R] {I : ideal R} {S : Type v} ⦃f g : R I →+* S⦄ (h : f.comp = g.comp ) :
f = g
@[protected, instance]
def ideal.quotient.inhabited {R : Type u} [comm_ring R] {I : ideal R} :
Equations
@[protected]
theorem ideal.quotient.eq {R : Type u} [comm_ring R] {I : ideal R} {x y : R} :
x = y x - y I
@[simp]
theorem ideal.quotient.mk_eq_mk {R : Type u} [comm_ring R] {I : ideal R} (x : R) :
theorem ideal.quotient.eq_zero_iff_mem {R : Type u} [comm_ring R] {a : R} {I : ideal R} :
a = 0 a I
theorem ideal.quotient.zero_eq_one_iff {R : Type u} [comm_ring R] {I : ideal R} :
0 = 1 I =
theorem ideal.quotient.zero_ne_one_iff {R : Type u} [comm_ring R] {I : ideal R} :
0 1 I
@[protected]
theorem ideal.quotient.nontrivial {R : Type u} [comm_ring R] {I : ideal R} (hI : I ) :
theorem ideal.quotient.mk_surjective {R : Type u} [comm_ring R] {I : ideal R} :
@[protected, instance]
theorem ideal.quotient.quotient_ring_saturate {R : Type u} [comm_ring R] (I : ideal R) (s : set R) :
⁻¹' ( '' s) = (x : I), (λ (y : R), x.val + 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.

@[protected, instance]
@[protected, instance]
def ideal.quotient.is_domain {R : Type u} [comm_ring R] (I : ideal R) [hI : I.is_prime] :
theorem ideal.quotient.exists_inv {R : Type u} [comm_ring R] {I : ideal R} [hI : I.is_maximal] {a : R I} :
a 0 ( (b : R I), a * b = 1)
@[protected, reducible]
noncomputable def ideal.quotient.group_with_zero {R : Type u} [comm_ring R] (I : ideal R) [hI : I.is_maximal] :

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.

Equations
@[protected, reducible]
noncomputable def ideal.quotient.field {R : Type u} [comm_ring R] (I : ideal R) [hI : I.is_maximal] :
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.

Equations
theorem ideal.quotient.maximal_of_is_field {R : Type u} [comm_ring R] (I : ideal R) (hqf : is_field (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} [comm_ring R] {S : Type v} [comm_ring 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.

Equations
@[simp]
theorem ideal.quotient.lift_mk {R : Type u} [comm_ring R] {a : R} {S : Type v} [comm_ring S] (I : ideal R) (f : R →+* S) (H : (a : R), a I f a = 0) :
H) ( a) = f a
theorem ideal.quotient.lift_surjective_of_surjective {R : Type u} [comm_ring R] {S : Type v} [comm_ring S] (I : ideal R) {f : R →+* S} (H : (a : R), a I f a = 0) (hf : function.surjective f) :
def ideal.quotient.factor {R : Type u} [comm_ring R] (S 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
@[simp]
theorem ideal.quotient.factor_mk {R : Type u} [comm_ring R] (S T : ideal R) (H : S T) (x : R) :
H) ( x) = x
@[simp]
theorem ideal.quotient.factor_comp_mk {R : Type u} [comm_ring R] (S T : ideal R) (H : S T) :
H).comp =
def ideal.quot_equiv_of_eq {R : Type u_1} [comm_ring R] {I J : ideal R} (h : I = J) :
R I ≃+* R J

Quotienting by equal ideals gives equivalent rings.

See also submodule.quot_equiv_of_eq and ideal.quotient_equiv_alg_of_eq.

Equations
@[simp]
theorem ideal.quot_equiv_of_eq_mk {R : Type u_1} [comm_ring R] {I J : ideal R} (h : I = J) (x : R) :
( x) = x
@[simp]
theorem ideal.quot_equiv_of_eq_symm {R : Type u_1} [comm_ring R] {I J : ideal R} (h : I = J) :
@[protected, instance]
def ideal.module_pi {R : Type u} [comm_ring R] (I : ideal R) (ι : Type v) :
module (R I) ((ι R) I.pi ι)

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

Equations
noncomputable def ideal.pi_quot_equiv {R : Type u} [comm_ring R] (I : ideal R) (ι : Type v) :
((ι R) I.pi ι) ≃ₗ[R I] ι R I

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

Equations
theorem ideal.map_pi {R : Type u} [comm_ring 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} [comm_ring R] {ι : Type v} (s : finset ι) {f : ι } (hf : (i : ι), i s (j : ι), j s i j f i f j = ) (i : ι) (his : i s) :
(r : R), r - 1 f i (j : ι), j s j i r f j
theorem ideal.exists_sub_mem {R : Type u} [comm_ring R] {ι : Type v} [finite ι] {f : ι } (hf : (i j : ι), i j f i f j = ) (g : ι R) :
(r : R), (i : ι), r - g i f i
def ideal.quotient_inf_to_pi_quotient {R : Type u} [comm_ring R] {ι : 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.

Equations
theorem ideal.quotient_inf_to_pi_quotient_bijective {R : Type u} [comm_ring R] {ι : Type v} [finite ι] {f : ι } (hf : (i j : ι), i j f i f j = ) :
noncomputable def ideal.quotient_inf_ring_equiv_pi_quotient {R : Type u} [comm_ring R] {ι : Type v} [finite ι] (f : ι ) (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

Equations
noncomputable def ideal.quotient_inf_equiv_quotient_prod {R : Type u} [comm_ring R] (I J : ideal R) (coprime : I J = ) :
R I J ≃+* (R I) × R J

Chinese remainder theorem, specialized to two ideals.

Equations
@[simp]
theorem ideal.quotient_inf_equiv_quotient_prod_fst {R : Type u} [comm_ring R] (I J : ideal R) (coprime : I J = ) (x : R I J) :
( coprime) x).fst = (ideal.quotient.factor (I J) I inf_le_left) x
@[simp]
theorem ideal.quotient_inf_equiv_quotient_prod_snd {R : Type u} [comm_ring R] (I J : ideal R) (coprime : I J = ) (x : R I J) :
@[simp]
theorem ideal.fst_comp_quotient_inf_equiv_quotient_prod {R : Type u} [comm_ring R] (I J : ideal R) (coprime : I J = ) :
@[simp]
theorem ideal.snd_comp_quotient_inf_equiv_quotient_prod {R : Type u} [comm_ring R] (I J : ideal R) (coprime : I J = ) :