# mathlibdocumentation

ring_theory.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.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, instance]
def ideal.quotient.has_mul {R : Type u} [comm_ring R] (I : ideal R) :
has_mul (R I)
Equations
@[protected, instance]
def ideal.quotient.comm_ring {R : Type u} [comm_ring R] (I : ideal R) :
Equations
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
@[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.subsingleton_iff {R : Type u} [comm_ring R] {I : ideal R} :
theorem ideal.quotient.mk_surjective {R : Type u} [comm_ring R] {I : ideal R} :
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]
def ideal.quotient.is_domain {R : Type u} [comm_ring R] (I : ideal R) [hI : I.is_prime] :
theorem ideal.quotient.is_domain_iff_prime {R : Type u} [comm_ring R] (I : ideal R) :
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.field {R : Type u} [comm_ring R] (I : ideal R) [hI : I.is_maximal] :
field (R I)

quotient by maximal ideal is a field. def rather than instance, since users will have computable inverses in some applications. See note [reducible non-instances].

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

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 If a = 0) :
H) ( a) = f a
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.

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} [fintype ι] {ι' : 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 si jf i f j = ) (i : ι) (his : i s) :
∃ (r : R), r - 1 f i ∀ (j : ι), j sj ir f j
theorem ideal.exists_sub_mem {R : Type u} [comm_ring R] {ι : Type v} [fintype ι] {f : ι → } (hf : ∀ (i j : ι), i jf 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} [fintype ι] {f : ι → } (hf : ∀ (i j : ι), i jf i f j = ) :
noncomputable def ideal.quotient_inf_ring_equiv_pi_quotient {R : Type u} [comm_ring R] {ι : Type v} [fintype ι] (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

Equations