mathlib3 documentation

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 #

Main results #

source
@[protected, instance, reducible]
def ideal.has_quotient {R : Type u} [comm_ring R] :
has_quotient 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
source
@[protected, instance]
def ideal.quotient.has_one {R : Type u} [comm_ring R] (I : ideal R) :
has_one (R ⧸ I)
Equations
source
@[protected]
def ideal.quotient.ring_con {R : Type u} [comm_ring R] (I : ideal R) :
ring_con R

On ideals, submodule.quotient_rel is a ring congruence.

Equations
source
@[protected, instance]
def ideal.quotient.comm_ring {R : Type u} [comm_ring R] (I : ideal R) :
comm_ring (R ⧸ I)
Equations
source
@[protected, instance]
def ideal.quotient.is_scalar_tower_right {R : Type u} [comm_ring R] {I : ideal R} {α : Type u_1} [has_smul α R] [is_scalar_tower α R R] :
is_scalar_tower α (R ⧸ I) (R ⧸ I)
source
@[protected, instance]
def ideal.quotient.smul_comm_class {R : Type u} [comm_ring R] {I : ideal R} {α : Type u_1} [has_smul α R] [is_scalar_tower α R R] [smul_comm_class α R R] :
smul_comm_class α (R ⧸ I) (R ⧸ I)
source
@[protected, instance]
def ideal.quotient.smul_comm_class' {R : Type u} [comm_ring R] {I : ideal R} {α : Type u_1} [has_smul α R] [is_scalar_tower α R R] [smul_comm_class R α R] :
smul_comm_class (R ⧸ I) α (R ⧸ I)
source
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
source
@[ext]
theorem ideal.quotient.ring_hom_ext {R : Type u} [comm_ring R] {I : ideal R} {S : Type v} [non_assoc_semiring S] ⦃f g : R ⧸ I →+* S⦄ (h : f.comp (ideal.quotient.mk I) = g.comp (ideal.quotient.mk I)) :
f = g
source
@[protected, instance]
def ideal.quotient.inhabited {R : Type u} [comm_ring R] {I : ideal R} :
inhabited (R ⧸ I)
Equations
source
@[protected]
theorem ideal.quotient.eq {R : Type u} [comm_ring R] {I : ideal R} {x y : R} :
⇑(ideal.quotient.mk I) x = ⇑(ideal.quotient.mk I) y ↔ x - y ∈ I
source
@[simp]
theorem ideal.quotient.mk_eq_mk {R : Type u} [comm_ring R] {I : ideal R} (x : R) :
submodule.quotient.mk x = ⇑(ideal.quotient.mk I) x
source
theorem ideal.quotient.eq_zero_iff_mem {R : Type u} [comm_ring R] {a : R} {I : ideal R} :
⇑(ideal.quotient.mk I) a = 0 ↔ a ∈ I
source
theorem ideal.quotient.zero_eq_one_iff {R : Type u} [comm_ring R] {I : ideal R} :
0 = 1 ↔ I = ⊤
source
theorem ideal.quotient.zero_ne_one_iff {R : Type u} [comm_ring R] {I : ideal R} :
0 ≠ 1 ↔ I ≠ ⊤
source
@[protected]
theorem ideal.quotient.nontrivial {R : Type u} [comm_ring R] {I : ideal R} (hI : I ≠ ⊤) :
nontrivial (R ⧸ I)
source
theorem ideal.quotient.subsingleton_iff {R : Type u} [comm_ring R] {I : ideal R} :
subsingleton (R ⧸ I) ↔ I = ⊤
source
@[protected, instance]
def ideal.quotient.has_quotient.quotient.unique {R : Type u} [comm_ring R] :
unique (R ⧸ ⊤)
Equations
source
theorem ideal.quotient.mk_surjective {R : Type u} [comm_ring R] {I : ideal R} :
function.surjective ⇑(ideal.quotient.mk I)
source
@[protected, instance]
def ideal.quotient.mk.ring_hom_surjective {R : Type u} [comm_ring R] {I : ideal R} :
ring_hom_surjective (ideal.quotient.mk I)
source
theorem ideal.quotient.quotient_ring_saturate {R : Type u} [comm_ring R] (I : ideal R) (s : set R) :
⇑(ideal.quotient.mk I) ⁻¹' (⇑(ideal.quotient.mk I) '' 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.

source
@[protected, instance]
def ideal.quotient.no_zero_divisors {R : Type u} [comm_ring R] (I : ideal R) [hI : I.is_prime] :
no_zero_divisors (R ⧸ I)
source
@[protected, instance]
def ideal.quotient.is_domain {R : Type u} [comm_ring R] (I : ideal R) [hI : I.is_prime] :
is_domain (R ⧸ I)
source
theorem ideal.quotient.is_domain_iff_prime {R : Type u} [comm_ring R] (I : ideal R) :
is_domain (R ⧸ I) ↔ I.is_prime
source
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)
source
@[protected, reducible]
noncomputable def ideal.quotient.group_with_zero {R : Type u} [comm_ring R] (I : ideal R) [hI : I.is_maximal] :
group_with_zero (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].

Equations
source
@[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.

See note [reducible non-instances].

Equations
source
theorem ideal.quotient.maximal_of_is_field {R : Type u} [comm_ring R] (I : ideal R) (hqf : is_field (R ⧸ I)) :
I.is_maximal

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

source
theorem ideal.quotient.maximal_ideal_iff_is_field_quotient {R : Type u} [comm_ring R] (I : ideal R) :
I.is_maximal ↔ is_field (R ⧸ I)

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

source
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
source
@[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) :
⇑(ideal.quotient.lift I f H) (⇑(ideal.quotient.mk I) a) = ⇑f a
source
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) :
function.surjective ⇑(ideal.quotient.lift I f H)
source
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
source
@[simp]
theorem ideal.quotient.factor_mk {R : Type u} [comm_ring R] (S T : ideal R) (H : S ≤ T) (x : R) :
⇑(ideal.quotient.factor S T H) (⇑(ideal.quotient.mk S) x) = ⇑(ideal.quotient.mk T) x
source
@[simp]
theorem ideal.quotient.factor_comp_mk {R : Type u} [comm_ring R] (S T : ideal R) (H : S ≤ T) :
(ideal.quotient.factor S T H).comp (ideal.quotient.mk S) = ideal.quotient.mk T
source
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
source
@[simp]
theorem ideal.quot_equiv_of_eq_mk {R : Type u_1} [comm_ring R] {I J : ideal R} (h : I = J) (x : R) :
⇑(ideal.quot_equiv_of_eq h) (⇑(ideal.quotient.mk I) x) = ⇑(ideal.quotient.mk J) x
source
@[simp]
theorem ideal.quot_equiv_of_eq_symm {R : Type u_1} [comm_ring R] {I J : ideal R} (h : I = J) :
(ideal.quot_equiv_of_eq h).symm = ideal.quot_equiv_of_eq _
source
@[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
source
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
source
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.

source
theorem ideal.exists_sub_one_mem_and_mem {R : Type u} [comm_ring 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), r - 1 ∈ f i ∧ ∀ (j : ι), j ∈ s → j ≠ i → r ∈ f j
source
theorem ideal.exists_sub_mem {R : Type u} [comm_ring R] {ι : Type v} [finite ι] {f : ι → ideal R} (hf : ∀ (i j : ι), i ≠ j → f i ⊔ f j = ⊤) (g : ι → R) :
∃ (r : R), ∀ (i : ι), r - g i ∈ f i
source
def ideal.quotient_inf_to_pi_quotient {R : Type u} [comm_ring 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.

Equations
source
theorem ideal.quotient_inf_to_pi_quotient_bijective {R : Type u} [comm_ring R] {ι : Type v} [finite ι] {f : ι → ideal R} (hf : ∀ (i j : ι), i ≠ j → f i ⊔ f j = ⊤) :
function.bijective ⇑(ideal.quotient_inf_to_pi_quotient f)
source
noncomputable def ideal.quotient_inf_ring_equiv_pi_quotient {R : Type u} [comm_ring 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

Equations
source
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
source
@[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) :
(⇑(I.quotient_inf_equiv_quotient_prod J coprime) x).fst = ⇑(ideal.quotient.factor (I ⊓ J) I inf_le_left) x
source
@[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) :
(⇑(I.quotient_inf_equiv_quotient_prod J coprime) x).snd = ⇑(ideal.quotient.factor (I ⊓ J) J inf_le_right) x
source
@[simp]
theorem ideal.fst_comp_quotient_inf_equiv_quotient_prod {R : Type u} [comm_ring R] (I J : ideal R) (coprime : I ⊔ J = ⊤) :
(ring_hom.fst (R ⧸ I) (R ⧸ J)).comp ↑(I.quotient_inf_equiv_quotient_prod J coprime) = ideal.quotient.factor (I ⊓ J) I inf_le_left
source
@[simp]
theorem ideal.snd_comp_quotient_inf_equiv_quotient_prod {R : Type u} [comm_ring R] (I J : ideal R) (coprime : I ⊔ J = ⊤) :
(ring_hom.snd (R ⧸ I) (R ⧸ J)).comp ↑(I.quotient_inf_equiv_quotient_prod J coprime) = ideal.quotient.factor (I ⊓ J) J inf_le_right