# mathlibdocumentation

ring_theory.ideal.operations

# More operations on modules and ideals #

@[instance]
def submodule.has_scalar' {R : Type u} {M : Type v} [comm_ring R] [ M] :
Equations
def submodule.annihilator {R : Type u} {M : Type v} [comm_ring R] [ M] (N : M) :

`N.annihilator` is the ideal of all elements `r : R` such that `r • N = 0`.

Equations
def submodule.colon {R : Type u} {M : Type v} [comm_ring R] [ M] (N P : M) :

`N.colon P` is the ideal of all elements `r : R` such that `r • P ⊆ N`.

Equations
theorem submodule.mem_annihilator {R : Type u} {M : Type v} [comm_ring R] [ M] {N : M} {r : R} :
r N.annihilator ∀ (n : M), n Nr n = 0
theorem submodule.mem_annihilator' {R : Type u} {M : Type v} [comm_ring R] [ M] {N : M} {r : R} :
theorem submodule.annihilator_bot {R : Type u} {M : Type v} [comm_ring R] [ M] :
theorem submodule.annihilator_eq_top_iff {R : Type u} {M : Type v} [comm_ring R] [ M] {N : M} :
N =
theorem submodule.annihilator_mono {R : Type u} {M : Type v} [comm_ring R] [ M] {N P : M} (h : N P) :
theorem submodule.annihilator_supr {R : Type u} {M : Type v} [comm_ring R] [ M] (ι : Sort w) (f : ι → M) :
(⨆ (i : ι), f i).annihilator = ⨅ (i : ι), (f i).annihilator
theorem submodule.mem_colon {R : Type u} {M : Type v} [comm_ring R] [ M] {N P : M} {r : R} :
r N.colon P ∀ (p : M), p Pr p N
theorem submodule.mem_colon' {R : Type u} {M : Type v} [comm_ring R] [ M] {N P : M} {r : R} :
r N.colon P P
theorem submodule.colon_mono {R : Type u} {M : Type v} [comm_ring R] [ M] {N₁ N₂ P₁ P₂ : M} (hn : N₁ N₂) (hp : P₁ P₂) :
N₁.colon P₂ N₂.colon P₁
theorem submodule.infi_colon_supr {R : Type u} {M : Type v} [comm_ring R] [ M] (ι₁ : Sort w) (f : ι₁ → M) (ι₂ : Sort x) (g : ι₂ → M) :
(⨅ (i : ι₁), f i).colon (⨆ (j : ι₂), g j) = ⨅ (i : ι₁) (j : ι₂), (f i).colon (g j)
theorem submodule.smul_mem_smul {R : Type u} {M : Type v} [comm_ring R] [ M] {I : ideal R} {N : M} {r : R} {n : M} (hr : r I) (hn : n N) :
r n I N
theorem submodule.smul_le {R : Type u} {M : Type v} [comm_ring R] [ M] {I : ideal R} {N P : M} :
I N P ∀ (r : R), r I∀ (n : M), n Nr n P
theorem submodule.smul_induction_on {R : Type u} {M : Type v} [comm_ring R] [ M] {I : ideal R} {N : M} {p : M → Prop} {x : M} (H : x I N) (Hb : ∀ (r : R), r I∀ (n : M), n Np (r n)) (H0 : p 0) (H1 : ∀ (x y : M), p xp yp (x + y)) (H2 : ∀ (c : R) (n : M), p np (c n)) :
p x
theorem submodule.mem_smul_span_singleton {R : Type u} {M : Type v} [comm_ring R] [ M] {I : ideal R} {m x : M} :
x I {m} ∃ (y : R) (H : y I), y m = x
theorem submodule.smul_le_right {R : Type u} {M : Type v} [comm_ring R] [ M] {I : ideal R} {N : M} :
I N N
theorem submodule.smul_mono {R : Type u} {M : Type v} [comm_ring R] [ M] {I J : ideal R} {N P : M} (hij : I J) (hnp : N P) :
I N J P
theorem submodule.smul_mono_left {R : Type u} {M : Type v} [comm_ring R] [ M] {I J : ideal R} {N : M} (h : I J) :
I N J N
theorem submodule.smul_mono_right {R : Type u} {M : Type v} [comm_ring R] [ M] {I : ideal R} {N P : M} (h : N P) :
I N I P
@[simp]
theorem submodule.annihilator_smul {R : Type u} {M : Type v} [comm_ring R] [ M] (N : M) :
@[simp]
theorem submodule.annihilator_mul {R : Type u} [comm_ring R] (I : ideal R) :
@[simp]
theorem submodule.mul_annihilator {R : Type u} [comm_ring R] (I : ideal R) :
@[simp]
theorem submodule.smul_bot {R : Type u} {M : Type v} [comm_ring R] [ M] (I : ideal R) :
@[simp]
theorem submodule.bot_smul {R : Type u} {M : Type v} [comm_ring R] [ M] (N : M) :
@[simp]
theorem submodule.top_smul {R : Type u} {M : Type v} [comm_ring R] [ M] (N : M) :
N = N
theorem submodule.smul_sup {R : Type u} {M : Type v} [comm_ring R] [ M] (I : ideal R) (N P : M) :
I (N P) = I N I P
theorem submodule.sup_smul {R : Type u} {M : Type v} [comm_ring R] [ M] (I J : ideal R) (N : M) :
(I J) N = I N J N
theorem submodule.smul_assoc {R : Type u} {M : Type v} [comm_ring R] [ M] (I J : ideal R) (N : M) :
(I J) N = I J N
theorem submodule.span_smul_span {R : Type u} {M : Type v} [comm_ring R] [ M] (S : set R) (T : set M) :
= (⋃ (s : R) (H : s S) (t : M) (H : t T), {s t})
theorem submodule.map_smul'' {R : Type u} {M : Type v} [comm_ring R] [ M] (I : ideal R) (N : M) {M' : Type w} [add_comm_group M'] [ M'] (f : M →ₗ[R] M') :
(I N) = I
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 : ι → ) :
(⨅ (i : ι), f i).quotient →+* Π (i : ι), (f i).quotient

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 = ) :
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 = ) :
(⨅ (i : ι), f i).quotient ≃+* Π (i : ι), (f i).quotient

Chinese Remainder Theorem. Eisenbud Ex.2.6. Similar to Atiyah-Macdonald 1.10 and Stacks 00DT

Equations
@[instance]
def ideal.has_mul {R : Type u} [comm_ring R] :
Equations
@[simp]
theorem ideal.add_eq_sup {R : Type u} [comm_ring R] {I J : ideal R} :
I + J = I J
@[simp]
theorem ideal.zero_eq_bot {R : Type u} [comm_ring R] :
0 =
@[simp]
theorem ideal.one_eq_top {R : Type u} [comm_ring R] :
1 =
theorem ideal.mul_mem_mul {R : Type u} [comm_ring R] {I J : ideal R} {r s : R} (hr : r I) (hs : s J) :
r * s I * J
theorem ideal.mul_mem_mul_rev {R : Type u} [comm_ring R] {I J : ideal R} {r s : R} (hr : r I) (hs : s J) :
s * r I * J
theorem ideal.pow_mem_pow {R : Type u} [comm_ring R] {I : ideal R} {x : R} (hx : x I) (n : ) :
x ^ n I ^ n
theorem ideal.mul_le {R : Type u} [comm_ring R] {I J K : ideal R} :
I * J K ∀ (r : R), r I∀ (s : R), s Jr * s K
theorem ideal.mul_le_left {R : Type u} [comm_ring R] {I J : ideal R} :
I * J J
theorem ideal.mul_le_right {R : Type u} [comm_ring R] {I J : ideal R} :
I * J I
@[simp]
theorem ideal.sup_mul_right_self {R : Type u} [comm_ring R] {I J : ideal R} :
I I * J = I
@[simp]
theorem ideal.sup_mul_left_self {R : Type u} [comm_ring R] {I J : ideal R} :
I J * I = I
@[simp]
theorem ideal.mul_right_self_sup {R : Type u} [comm_ring R] {I J : ideal R} :
I * J I = I
@[simp]
theorem ideal.mul_left_self_sup {R : Type u} [comm_ring R] {I J : ideal R} :
J * I I = I
theorem ideal.mul_comm {R : Type u} [comm_ring R] (I J : ideal R) :
I * J = J * I
theorem ideal.mul_assoc {R : Type u} [comm_ring R] (I J K : ideal R) :
(I * J) * K = I * J * K
theorem ideal.span_mul_span {R : Type u} [comm_ring R] (S T : set R) :
(ideal.span S) * = ideal.span (⋃ (s : R) (H : s S) (t : R) (H : t T), {s * t})
theorem ideal.span_mul_span' {R : Type u} [comm_ring R] (S T : set R) :
theorem ideal.span_singleton_mul_span_singleton {R : Type u} [comm_ring R] (r s : R) :
theorem ideal.span_singleton_pow {R : Type u} [comm_ring R] (s : R) (n : ) :
ideal.span {s} ^ n = ideal.span {s ^ n}
theorem ideal.mem_mul_span_singleton {R : Type u} [comm_ring R] {x y : R} {I : ideal R} :
x I * ideal.span {y} ∃ (z : R) (H : z I), z * y = x
theorem ideal.mem_span_singleton_mul {R : Type u} [comm_ring R] {x y : R} {I : ideal R} :
x (ideal.span {y}) * I ∃ (z : R) (H : z I), y * z = x
theorem ideal.le_span_singleton_mul_iff {R : Type u} [comm_ring R] {x : R} {I J : ideal R} :
I (ideal.span {x}) * J ∀ (zI : R), zI I(∃ (zJ : R) (H : zJ J), x * zJ = zI)
theorem ideal.span_singleton_mul_le_iff {R : Type u} [comm_ring R] {x : R} {I J : ideal R} :
(ideal.span {x}) * I J ∀ (z : R), z Ix * z J
theorem ideal.span_singleton_mul_le_span_singleton_mul {R : Type u} [comm_ring R] {x y : R} {I J : ideal R} :
(ideal.span {x}) * I (ideal.span {y}) * J ∀ (zI : R), zI I(∃ (zJ : R) (H : zJ J), x * zI = y * zJ)
theorem ideal.eq_span_singleton_mul {R : Type u} [comm_ring R] {x : R} (I J : ideal R) :
I = (ideal.span {x}) * J (∀ (zI : R), zI I(∃ (zJ : R) (H : zJ J), x * zJ = zI)) ∀ (z : R), z Jx * z I
theorem ideal.span_singleton_mul_eq_span_singleton_mul {R : Type u} [comm_ring R] {x y : R} (I J : ideal R) :
(ideal.span {x}) * I = (ideal.span {y}) * J (∀ (zI : R), zI I(∃ (zJ : R) (H : zJ J), x * zI = y * zJ)) ∀ (zJ : R), zJ J(∃ (zI : R) (H : zI I), x * zI = y * zJ)
theorem ideal.mul_le_inf {R : Type u} [comm_ring R] {I J : ideal R} :
I * J I J
theorem ideal.multiset_prod_le_inf {R : Type u} [comm_ring R] {s : multiset (ideal R)} :
theorem ideal.prod_le_inf {R : Type u} {ι : Type u_1} [comm_ring R] {s : finset ι} {f : ι → } :
s.prod f s.inf f
theorem ideal.mul_eq_inf_of_coprime {R : Type u} [comm_ring R] {I J : ideal R} (h : I J = ) :
I * J = I J
theorem ideal.mul_bot {R : Type u} [comm_ring R] (I : ideal R) :
theorem ideal.bot_mul {R : Type u} [comm_ring R] (I : ideal R) :
theorem ideal.mul_top {R : Type u} [comm_ring R] (I : ideal R) :
I * = I
theorem ideal.top_mul {R : Type u} [comm_ring R] (I : ideal R) :
* I = I
theorem ideal.mul_mono {R : Type u} [comm_ring R] {I J K L : ideal R} (hik : I K) (hjl : J L) :
I * J K * L
theorem ideal.mul_mono_left {R : Type u} [comm_ring R] {I J K : ideal R} (h : I J) :
I * K J * K
theorem ideal.mul_mono_right {R : Type u} [comm_ring R] {I J K : ideal R} (h : J K) :
I * J I * K
theorem ideal.mul_sup {R : Type u} [comm_ring R] (I J K : ideal R) :
I * (J K) = I * J I * K
theorem ideal.sup_mul {R : Type u} [comm_ring R] (I J K : ideal R) :
(I J) * K = I * K J * K
theorem ideal.pow_le_pow {R : Type u} [comm_ring R] {I : ideal R} {m n : } (h : m n) :
I ^ n I ^ m
theorem ideal.mul_eq_bot {R : Type u_1} {I J : ideal R} :
I * J = I = J =
@[instance]
def ideal.no_zero_divisors {R : Type u_1}  :
theorem ideal.prod_eq_bot {R : Type u_1} {s : multiset (ideal R)} :
s.prod = ∃ (I : ideal R) (H : I s), I =

A product of ideals in an integral domain is zero if and only if one of the terms is zero.

def ideal.radical {R : Type u} [comm_ring R] (I : ideal R) :

The radical of an ideal `I` consists of the elements `r` such that `r^n ∈ I` for some `n`.

Equations
theorem ideal.le_radical {R : Type u} [comm_ring R] {I : ideal R} :
theorem ideal.radical_top (R : Type u) [comm_ring R] :
theorem ideal.radical_mono {R : Type u} [comm_ring R] {I J : ideal R} (H : I J) :
@[simp]
theorem ideal.radical_idem {R : Type u} [comm_ring R] (I : ideal R) :
theorem ideal.radical_le_radical_iff {R : Type u} [comm_ring R] {I J : ideal R} :
theorem ideal.radical_eq_top {R : Type u} [comm_ring R] {I : ideal R} :
I =
theorem ideal.is_prime.radical {R : Type u} [comm_ring R] {I : ideal R} (H : I.is_prime) :
theorem ideal.radical_sup {R : Type u} [comm_ring R] (I J : ideal R) :
theorem ideal.radical_inf {R : Type u} [comm_ring R] (I J : ideal R) :
theorem ideal.radical_mul {R : Type u} [comm_ring R] (I J : ideal R) :
theorem ideal.is_prime.radical_le_iff {R : Type u} [comm_ring R] {I J : ideal R} (hj : J.is_prime) :
theorem ideal.radical_eq_Inf {R : Type u} [comm_ring R] (I : ideal R) :
I.radical = Inf {J : | I J J.is_prime}
@[simp]
theorem ideal.radical_bot_of_integral_domain {R : Type u}  :
@[instance]
def ideal.comm_semiring {R : Type u} [comm_ring R] :
Equations
theorem ideal.top_pow (R : Type u) [comm_ring R] (n : ) :
theorem ideal.radical_pow {R : Type u} [comm_ring R] (I : ideal R) (n : ) (H : n > 0) :
theorem ideal.is_prime.mul_le {R : Type u} [comm_ring R] {I J P : ideal R} (hp : P.is_prime) :
I * J P I P J P
theorem ideal.is_prime.inf_le {R : Type u} [comm_ring R] {I J P : ideal R} (hp : P.is_prime) :
I J P I P J P
theorem ideal.is_prime.multiset_prod_le {R : Type u} [comm_ring R] {s : multiset (ideal R)} {P : ideal R} (hp : P.is_prime) (hne : s 0) :
s.prod P ∃ (I : ideal R) (H : I s), I P
theorem ideal.is_prime.multiset_prod_map_le {R : Type u} {ι : Type u_1} [comm_ring R] {s : multiset ι} (f : ι → ) {P : ideal R} (hp : P.is_prime) (hne : s 0) :
s).prod P ∃ (i : ι) (H : i s), f i P
theorem ideal.is_prime.prod_le {R : Type u} {ι : Type u_1} [comm_ring R] {s : finset ι} {f : ι → } {P : ideal R} (hp : P.is_prime) (hne : s.nonempty) :
s.prod f P ∃ (i : ι) (H : i s), f i P
theorem ideal.is_prime.inf_le' {R : Type u} {ι : Type u_1} [comm_ring R] {s : finset ι} {f : ι → } {P : ideal R} (hp : P.is_prime) (hsne : s.nonempty) :
s.inf f P ∃ (i : ι) (H : i s), f i P
theorem ideal.subset_union {R : Type u} [comm_ring R] {I J K : ideal R} :
I J K I J I K
theorem ideal.subset_union_prime' {R : Type u} {ι : Type u_1} [comm_ring R] {s : finset ι} {f : ι → } {a b : ι} (hp : ∀ (i : ι), i s(f i).is_prime) {I : ideal R} :
(I (f a) (f b) ⋃ (i : ι) (H : i s), (f i)) I f a I f b ∃ (i : ι) (H : i s), I f i
theorem ideal.subset_union_prime {R : Type u} {ι : Type u_1} [comm_ring R] {s : finset ι} {f : ι → } (a b : ι) (hp : ∀ (i : ι), i si ai b(f i).is_prime) {I : ideal R} :
(I ⋃ (i : ι) (H : i s), (f i)) ∃ (i : ι) (H : i s), I f i

Prime avoidance. Atiyah-Macdonald 1.11, Eisenbud 3.3, Stacks 00DS, Matsumura Ex.1.6.

theorem ideal.le_of_dvd {R : Type u} [comm_ring R] {I J : ideal R} :
I JJ I

If `I` divides `J`, then `I` contains `J`.

In a Dedekind domain, to divide and contain are equivalent, see `ideal.dvd_iff_le`.

theorem ideal.is_unit_iff {R : Type u} [comm_ring R] {I : ideal R} :
I =
@[instance]
def ideal.unique_units {R : Type u} [comm_ring R] :
Equations
def ideal.map {R : Type u} {S : Type v} [ring R] [ring S] (f : R →+* S) (I : ideal R) :

`I.map f` is the span of the image of the ideal `I` under `f`, which may be bigger than the image itself.

Equations
def ideal.comap {R : Type u} {S : Type v} [ring R] [ring S] (f : R →+* S) (I : ideal S) :

`I.comap f` is the preimage of `I` under `f`.

Equations
theorem ideal.map_mono {R : Type u} {S : Type v} [ring R] [ring S] {f : R →+* S} {I J : ideal R} (h : I J) :
I J
theorem ideal.mem_map_of_mem {R : Type u} {S : Type v} [ring R] [ring S] (f : R →+* S) {I : ideal R} {x : R} (h : x I) :
f x I
theorem ideal.apply_coe_mem_map {R : Type u} {S : Type v} [ring R] [ring S] (f : R →+* S) (I : ideal R) (x : I) :
f x I
theorem ideal.map_le_iff_le_comap {R : Type u} {S : Type v} [ring R] [ring S] {f : R →+* S} {I : ideal R} {K : ideal S} :
I K I K
@[simp]
theorem ideal.mem_comap {R : Type u} {S : Type v} [ring R] [ring S] {f : R →+* S} {K : ideal S} {x : R} :
x K f x K
theorem ideal.comap_mono {R : Type u} {S : Type v} [ring R] [ring S] {f : R →+* S} {K L : ideal S} (h : K L) :
K L
theorem ideal.comap_ne_top {R : Type u} {S : Type v} [ring R] [ring S] (f : R →+* S) {K : ideal S} (hK : K ) :
K
@[instance]
def ideal.is_prime.comap {R : Type u} {S : Type v} [ring R] [ring S] (f : R →+* S) {K : ideal S} [hK : K.is_prime] :
theorem ideal.map_top {R : Type u} {S : Type v} [ring R] [ring S] (f : R →+* S) :
theorem ideal.gc_map_comap {R : Type u} {S : Type v} [ring R] [ring S] (f : R →+* S) :
@[simp]
theorem ideal.comap_id {R : Type u} [ring R] (I : ideal R) :
I = I
@[simp]
theorem ideal.map_id {R : Type u} [ring R] (I : ideal R) :
I = I
theorem ideal.comap_comap {R : Type u} {S : Type v} [ring R] [ring S] {T : Type u_1} [ring T] {I : ideal T} (f : R →+* S) (g : S →+* T) :
I) = ideal.comap (g.comp f) I
theorem ideal.map_map {R : Type u} {S : Type v} [ring R] [ring S] {T : Type u_1} [ring T] {I : ideal R} (f : R →+* S) (g : S →+* T) :
I) = ideal.map (g.comp f) I
theorem ideal.map_span {R : Type u} {S : Type v} [ring R] [ring S] (f : R →+* S) (s : set R) :
theorem ideal.map_le_of_le_comap {R : Type u} {S : Type v} [ring R] [ring S] {f : R →+* S} {I : ideal R} {K : ideal S} :
I K I K
theorem ideal.le_comap_of_map_le {R : Type u} {S : Type v} [ring R] [ring S] {f : R →+* S} {I : ideal R} {K : ideal S} :
I KI K
theorem ideal.le_comap_map {R : Type u} {S : Type v} [ring R] [ring S] {f : R →+* S} {I : ideal R} :
I I)
theorem ideal.map_comap_le {R : Type u} {S : Type v} [ring R] [ring S] {f : R →+* S} {K : ideal S} :
K) K
@[simp]
theorem ideal.comap_top {R : Type u} {S : Type v} [ring R] [ring S] {f : R →+* S} :
@[simp]
theorem ideal.comap_eq_top_iff {R : Type u} {S : Type v} [ring R] [ring S] {f : R →+* S} {I : ideal S} :
I = I =
@[simp]
theorem ideal.map_bot {R : Type u} {S : Type v} [ring R] [ring S] {f : R →+* S} :
@[simp]
theorem ideal.map_comap_map {R : Type u} {S : Type v} [ring R] [ring S] (f : R →+* S) (I : ideal R) :
I)) = I
@[simp]
theorem ideal.comap_map_comap {R : Type u} {S : Type v} [ring R] [ring S] (f : R →+* S) (K : ideal S) :
K)) = K
theorem ideal.map_sup {R : Type u} {S : Type v} [ring R] [ring S] (f : R →+* S) (I J : ideal R) :
(I J) = I J
theorem ideal.comap_inf {R : Type u} {S : Type v} [ring R] [ring S] (f : R →+* S) (K L : ideal S) :
(K L) = K L
theorem ideal.map_supr {R : Type u} {S : Type v} [ring R] [ring S] (f : R →+* S) {ι : Sort u_1} (K : ι → ) :
(supr K) = ⨆ (i : ι), (K i)
theorem ideal.comap_infi {R : Type u} {S : Type v} [ring R] [ring S] (f : R →+* S) {ι : Sort u_1} (K : ι → ) :
(infi K) = ⨅ (i : ι), (K i)
theorem ideal.map_Sup {R : Type u} {S : Type v} [ring R] [ring S] (f : R →+* S) (s : set (ideal R)) :
(Sup s) = ⨆ (I : ideal R) (H : I s), I
theorem ideal.comap_Inf {R : Type u} {S : Type v} [ring R] [ring S] (f : R →+* S) (s : set (ideal S)) :
(Inf s) = ⨅ (I : ideal S) (H : I s), I
theorem ideal.comap_Inf' {R : Type u} {S : Type v} [ring R] [ring S] (f : R →+* S) (s : set (ideal S)) :
(Inf s) = ⨅ (I : ideal R) (H : I '' s), I
theorem ideal.comap_is_prime {R : Type u} {S : Type v} [ring R] [ring S] (f : R →+* S) (K : ideal S) [H : K.is_prime] :
theorem ideal.map_inf_le {R : Type u} {S : Type v} [ring R] [ring S] (f : R →+* S) {I J : ideal R} :
(I J) I J
theorem ideal.le_comap_sup {R : Type u} {S : Type v} [ring R] [ring S] (f : R →+* S) {K L : ideal S} :
K L (K L)
theorem ideal.map_comap_of_surjective {R : Type u} {S : Type v} [ring R] [ring S] (f : R →+* S) (hf : function.surjective f) (I : ideal S) :
I) = I
def ideal.gi_map_comap {R : Type u} {S : Type v} [ring R] [ring S] (f : R →+* S) (hf : function.surjective f) :

`map` and `comap` are adjoint, and the composition `map f ∘ comap f` is the identity

Equations
theorem ideal.map_surjective_of_surjective {R : Type u} {S : Type v} [ring R] [ring S] (f : R →+* S) (hf : function.surjective f) :
theorem ideal.comap_injective_of_surjective {R : Type u} {S : Type v} [ring R] [ring S] (f : R →+* S) (hf : function.surjective f) :
theorem ideal.map_sup_comap_of_surjective {R : Type u} {S : Type v} [ring R] [ring S] (f : R →+* S) (hf : function.surjective f) (I J : ideal S) :
I J) = I J
theorem ideal.map_supr_comap_of_surjective {R : Type u} {S : Type v} [ring R] [ring S] (f : R →+* S) {ι : Sort u_1} (hf : function.surjective f) (K : ι → ) :
(⨆ (i : ι), (K i)) = supr K
theorem ideal.map_inf_comap_of_surjective {R : Type u} {S : Type v} [ring R] [ring S] (f : R →+* S) (hf : function.surjective f) (I J : ideal S) :
I J) = I J
theorem ideal.map_infi_comap_of_surjective {R : Type u} {S : Type v} [ring R] [ring S] (f : R →+* S) {ι : Sort u_1} (hf : function.surjective f) (K : ι → ) :
(⨅ (i : ι), (K i)) = infi K
theorem ideal.mem_image_of_mem_map_of_surjective {R : Type u} {S : Type v} [ring R] [ring S] (f : R →+* S) (hf : function.surjective f) {I : ideal R} {y : S} (H : y I) :
theorem ideal.mem_map_iff_of_surjective {R : Type u} {S : Type v} [ring R] [ring S] (f : R →+* S) (hf : function.surjective f) {I : ideal R} {y : S} :
y I ∃ (x : R), x I f x = y
theorem ideal.comap_map_of_surjective {R : Type u} {S : Type v} [ring R] [ring S] (f : R →+* S) (hf : function.surjective f) (I : ideal R) :
I) = I
theorem ideal.le_map_of_comap_le_of_surjective {R : Type u} {S : Type v} [ring R] [ring S] (f : R →+* S) {I : ideal R} {K : ideal S} (hf : function.surjective f) :
K IK I
def ideal.rel_iso_of_surjective {R : Type u} {S : Type v} [ring R] [ring S] (f : R →+* S) (hf : function.surjective f) :
≃o {p // p}

Correspondence theorem

Equations
def ideal.order_embedding_of_surjective {R : Type u} {S : Type v} [ring R] [ring S] (f : R →+* S) (hf : function.surjective f) :

The map on ideals induced by a surjective map preserves inclusion.

Equations
theorem ideal.map_eq_top_or_is_maximal_of_surjective {R : Type u} {S : Type v} [ring R] [ring S] (f : R →+* S) {I : ideal R} (hf : function.surjective f) (H : I.is_maximal) :
theorem ideal.comap_is_maximal_of_surjective {R : Type u} {S : Type v} [ring R] [ring S] (f : R →+* S) {K : ideal S} (hf : function.surjective f) [H : K.is_maximal] :
@[simp]
theorem ideal.map_of_equiv {R : Type u} {S : Type v} [ring R] [ring S] (I : ideal R) (f : R ≃+* S) :

If `f : R ≃+* S` is a ring isomorphism and `I : ideal R`, then `map f (map f.symm) = I`.

@[simp]
theorem ideal.comap_of_equiv {R : Type u} {S : Type v} [ring R] [ring S] (I : ideal R) (f : R ≃+* S) :
(ideal.comap (f.symm) I) = I

If `f : R ≃+* S` is a ring isomorphism and `I : ideal R`, then `comap f.symm (comap f) = I`.

theorem ideal.map_comap_of_equiv {R : Type u} {S : Type v} [ring R] [ring S] (I : ideal R) (f : R ≃+* S) :

If `f : R ≃+* S` is a ring isomorphism and `I : ideal R`, then `map f I = comap f.symm I`.

theorem ideal.comap_bot_le_of_injective {R : Type u} {S : Type v} [ring R] [ring S] (f : R →+* S) {I : ideal R} (hf : function.injective f) :
I
def ideal.rel_iso_of_bijective {R : Type u} {S : Type v} [ring R] [ring S] (f : R →+* S) (hf : function.bijective f) :

Special case of the correspondence theorem for isomorphic rings

Equations
theorem ideal.comap_le_iff_le_map {R : Type u} {S : Type v} [ring R] [ring S] (f : R →+* S) {I : ideal R} {K : ideal S} (hf : function.bijective f) :
K I K I
theorem ideal.map.is_maximal {R : Type u} {S : Type v} [ring R] [ring S] (f : R →+* S) {I : ideal R} (hf : function.bijective f) (H : I.is_maximal) :
theorem ideal.ring_equiv.bot_maximal_iff {R : Type u} {S : Type v} [ring R] [ring S] (e : R ≃+* S) :
theorem ideal.mem_quotient_iff_mem {R : Type u} [comm_ring R] {I J : ideal R} (hIJ : I J) {x : R} :
x x J
theorem ideal.map_mul {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) (I J : ideal R) :
(I * J) = I) * J
theorem ideal.comap_radical {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) (K : ideal S) :
@[simp]
theorem ideal.map_quotient_self {R : Type u} [comm_ring R] (I : ideal R) :
theorem ideal.map_radical_le {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) {I : ideal R} :
theorem ideal.le_comap_mul {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) {K L : ideal S} :
K) * L (K * L)
def ideal.is_primary {R : Type u} [comm_ring R] (I : ideal R) :
Prop

A proper ideal `I` is primary iff `xy ∈ I` implies `x ∈ I` or `y ∈ radical I`.

Equations
theorem ideal.is_primary.to_is_prime {R : Type u} [comm_ring R] (I : ideal R) (hi : I.is_prime) :
theorem ideal.mem_radical_of_pow_mem {R : Type u} [comm_ring R] {I : ideal R} {x : R} {m : } (hx : x ^ m I.radical) :
theorem ideal.is_prime_radical {R : Type u} [comm_ring R] {I : ideal R} (hi : I.is_primary) :
theorem ideal.is_primary_inf {R : Type u} [comm_ring R] {I J : ideal R} (hi : I.is_primary) (hj : J.is_primary) (hij : I.radical = J.radical) :
def ring_hom.ker {R : Type u} {S : Type v} [ring R] [ring S] (f : R →+* S) :

Kernel of a ring homomorphism as an ideal of the domain.

Equations
theorem ring_hom.mem_ker {R : Type u} {S : Type v} [ring R] [ring S] (f : R →+* S) {r : R} :
r f.ker f r = 0

An element is in the kernel if and only if it maps to zero.

theorem ring_hom.ker_eq {R : Type u} {S : Type v} [ring R] [ring S] (f : R →+* S) :
(f.ker) = f ⁻¹' {0}
theorem ring_hom.ker_eq_comap_bot {R : Type u} {S : Type v} [ring R] [ring S] (f : R →+* S) :
f.ker =
theorem ring_hom.injective_iff_ker_eq_bot {R : Type u} {S : Type v} [ring R] [ring S] (f : R →+* S) :
theorem ring_hom.ker_eq_bot_iff_eq_zero {R : Type u} {S : Type v} [ring R] [ring S] (f : R →+* S) :
f.ker = ∀ (x : R), f x = 0x = 0
theorem ring_hom.not_one_mem_ker {R : Type u} {S : Type v} [ring R] [ring S] [nontrivial S] (f : R →+* S) :
1 f.ker

If the target is not the zero ring, then one is not in the kernel.

@[simp]
theorem ring_hom.ker_coe_equiv {R : Type u} {S : Type v} [ring R] [ring S] (f : R ≃+* S) :
def ring_hom.ker_lift {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) :

The induced map from the quotient by the kernel to the codomain.

This is an isomorphism if `f` has a right inverse (`quotient_ker_equiv_of_right_inverse`) / is surjective (`quotient_ker_equiv_of_surjective`).

Equations
@[simp]
theorem ring_hom.ker_lift_mk {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) (r : R) :
(f.ker_lift) ( r) = f r
theorem ring_hom.ker_lift_injective {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) :

The induced map from the quotient by the kernel is injective.

def ring_hom.quotient_ker_equiv_of_right_inverse {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] {f : R →+* S} {g : S → R} (hf : f) :

The first isomorphism theorem for commutative rings, computable version.

Equations
@[simp]
theorem ring_hom.quotient_ker_equiv_of_right_inverse.apply {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] {f : R →+* S} {g : S → R} (hf : f) (x : f.ker.quotient) :
@[simp]
theorem ring_hom.quotient_ker_equiv_of_right_inverse.symm.apply {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] {f : R →+* S} {g : S → R} (hf : f) (x : S) :
= (g x)
def ring_hom.quotient_ker_equiv_of_surjective {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] {f : R →+* S} (hf : function.surjective f) :

The first isomorphism theorem for commutative rings.

Equations
theorem ring_hom.ker_is_prime {R : Type u} {S : Type v} [ring R] (f : R →+* S) :

The kernel of a homomorphism to an integral domain is a prime ideal.

theorem ring_hom.ker_is_maximal_of_surjective {R : Type u_1} {K : Type u_2} [ring R] [field K] (f : R →+* K) (hf : function.surjective f) :

The kernel of a homomorphism to a field is a maximal ideal.

theorem ideal.map_eq_bot_iff_le_ker {R : Type u_1} {S : Type u_2} [ring R] [ring S] {I : ideal R} (f : R →+* S) :
I = I f.ker
theorem ideal.ker_le_comap {R : Type u_1} {S : Type u_2} [ring R] [ring S] {K : ideal S} (f : R →+* S) :
f.ker K
theorem ideal.map_Inf {R : Type u_1} {S : Type u_2} [ring R] [ring S] {A : set (ideal R)} {f : R →+* S} (hf : function.surjective f) :
(∀ (J : ideal R), J Af.ker J) (Inf A) = Inf '' A)
theorem ideal.map_is_prime_of_surjective {R : Type u_1} {S : Type u_2} [ring R] [ring S] {f : R →+* S} (hf : function.surjective f) {I : ideal R} [H : I.is_prime] (hk : f.ker I) :
theorem ideal.map_is_prime_of_equiv {R : Type u_1} {S : Type u_2} [ring R] [ring S] (f : R ≃+* S) {I : ideal R} [I.is_prime] :
@[simp]
theorem ideal.mk_ker {R : Type u_1} [comm_ring R] {I : ideal R} :
.ker = I
theorem ideal.map_mk_eq_bot_of_le {R : Type u_1} [comm_ring R] {I J : ideal R} (h : I J) :
theorem ideal.ker_quotient_lift {R : Type u_1} [comm_ring R] {S : Type v} [comm_ring S] {I : ideal R} (f : R →+* S) (H : I f.ker) :
H).ker =
theorem ideal.map_eq_iff_sup_ker_eq_of_surjective {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] {I J : ideal R} (f : R →+* S) (hf : function.surjective f) :
I = J I f.ker = J f.ker
theorem ideal.map_radical_of_surjective {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] {f : R →+* S} (hf : function.surjective f) {I : ideal R} (h : f.ker I) :
@[simp]
theorem ideal.bot_quotient_is_maximal_iff {R : Type u_1} [comm_ring R] (I : ideal R) :
@[instance]
def ideal.quotient.algebra (R : Type u_1) [comm_ring R] {A : Type u_3} [comm_ring A] [ A] {I : ideal A} :

The `R`-algebra structure on `A/I` for an `R`-algebra `A`

Equations
def ideal.quotient.mkₐ (R : Type u_1) [comm_ring R] {A : Type u_3} [comm_ring A] [ A] (I : ideal A) :

The canonical morphism `A →ₐ[R] I.quotient` as morphism of `R`-algebras, for `I` an ideal of `A`, where `A` is an `R`-algebra.

Equations
theorem ideal.quotient.alg_map_eq (R : Type u_1) [comm_ring R] {A : Type u_3} [comm_ring A] [ A] (I : ideal A) :
= I.quotient).comp A)
@[instance]
def ideal.quotient.is_scalar_tower (R : Type u_1) {S : Type u_2} [comm_ring R] [comm_ring S] {A : Type u_3} [comm_ring A] [ A] [ A] [ R] [ A] {I : ideal A} :
theorem ideal.quotient.mkₐ_to_ring_hom (R : Type u_1) [comm_ring R] {A : Type u_3} [comm_ring A] [ A] (I : ideal A) :
@[simp]
theorem ideal.quotient.mkₐ_eq_mk (R : Type u_1) [comm_ring R] {A : Type u_3} [comm_ring A] [ A] (I : ideal A) :
I) =
theorem ideal.quotient.mkₐ_surjective (R : Type u_1) [comm_ring R] {A : Type u_3} [comm_ring A] [ A] (I : ideal A) :

The canonical morphism `A →ₐ[R] I.quotient` is surjective.

@[simp]
theorem ideal.quotient.mkₐ_ker (R : Type u_1) [comm_ring R] {A : Type u_3} [comm_ring A] [ A] (I : ideal A) :
I).ker = I

The kernel of `A →ₐ[R] I.quotient` is `I`.

theorem ideal.ker_lift.map_smul {R : Type u_1} [comm_ring R] {A : Type u_3} [comm_ring A] [ A] {B : Type u_4} [comm_ring B] [ B] (f : A →ₐ[R] B) (r : R) (x : f.to_ring_hom.ker.quotient) :
def ideal.ker_lift_alg {R : Type u_1} [comm_ring R] {A : Type u_3} [comm_ring A] [ A] {B : Type u_4} [comm_ring B] [ B] (f : A →ₐ[R] B) :

The induced algebras morphism from the quotient by the kernel to the codomain.

This is an isomorphism if `f` has a right inverse (`quotient_ker_alg_equiv_of_right_inverse`) / is surjective (`quotient_ker_alg_equiv_of_surjective`).

Equations
@[simp]
theorem ideal.ker_lift_alg_mk {R : Type u_1} [comm_ring R] {A : Type u_3} [comm_ring A] [ A] {B : Type u_4} [comm_ring B] [ B] (f : A →ₐ[R] B) (a : A) :
a) = f a
@[simp]
theorem ideal.ker_lift_alg_to_ring_hom {R : Type u_1} [comm_ring R] {A : Type u_3} [comm_ring A] [ A] {B : Type u_4} [comm_ring B] [ B] (f : A →ₐ[R] B) :
theorem ideal.ker_lift_alg_injective {R : Type u_1} [comm_ring R] {A : Type u_3} [comm_ring A] [ A] {B : Type u_4} [comm_ring B] [ B] (f : A →ₐ[R] B) :

The induced algebra morphism from the quotient by the kernel is injective.

def ideal.quotient_ker_alg_equiv_of_right_inverse {R : Type u_1} [comm_ring R] {A : Type u_3} [comm_ring A] [ A] {B : Type u_4} [comm_ring B] [ B] {f : A →ₐ[R] B} {g : B → A} (hf : f) :

The first isomorphism theorem for agebras, computable version.

Equations
@[simp]
theorem ideal.quotient_ker_alg_equiv_of_right_inverse.apply {R : Type u_1} [comm_ring R] {A : Type u_3} [comm_ring A] [ A] {B : Type u_4} [comm_ring B] [ B] {f : A →ₐ[R] B} {g : B → A} (hf : f) (x : f.to_ring_hom.ker.quotient) :
@[simp]
theorem ideal.quotient_ker_alg_equiv_of_right_inverse_symm.apply {R : Type u_1} [comm_ring R] {A : Type u_3} [comm_ring A] [ A] {B : Type u_4} [comm_ring B] [ B] {f : A →ₐ[R] B} {g : B → A} (hf : f) (x : B) :
= (g x)
def ideal.quotient_ker_alg_equiv_of_surjective {R : Type u_1} [comm_ring R] {A : Type u_3} [comm_ring A] [ A] {B : Type u_4} [comm_ring B] [ B] {f : A →ₐ[R] B} (hf : function.surjective f) :

The first isomorphism theorem for algebras.

Equations
def ideal.quotient_map {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] {I : ideal R} (J : ideal S) (f : R →+* S) (hIJ : I J) :

The ring hom `R/I →+* S/J` induced by a ring hom `f : R →+* S` with `I ≤ f⁻¹(J)`

Equations
@[simp]
theorem ideal.quotient_map_mk {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] {J : ideal R} {I : ideal S} {f : R →+* S} {H : J I} {x : R} :
(I.quotient_map f H) ( x) = (f x)
theorem ideal.quotient_map_comp_mk {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] {J : ideal R} {I : ideal S} {f : R →+* S} (H : J I) :
(I.quotient_map f H).comp = f
@[simp]
theorem ideal.quotient_equiv_symm_apply {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] (I : ideal R) (J : ideal S) (f : R ≃+* S) (hIJ : J = I) (ᾰ : J.quotient) :
((I.quotient_equiv J f hIJ).symm) = (I.quotient_map (f.symm) _)
def ideal.quotient_equiv {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] (I : ideal R) (J : ideal S) (f : R ≃+* S) (hIJ : J = I) :

The ring equiv `R/I ≃+* S/J` induced by a ring equiv `f : R ≃+** S`, where `J = f(I)`.

Equations
@[simp]
theorem ideal.quotient_equiv_apply {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] (I : ideal R) (J : ideal S) (f : R ≃+* S) (hIJ : J = I) (ᾰ : I.quotient) :
(I.quotient_equiv J f hIJ) = (J.quotient_map f _).to_fun
theorem ideal.quotient_map_injective' {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] {J : ideal R} {I : ideal S} {f : R →+* S} {H : J I} (h : I J) :

`H` and `h` are kept as separate hypothesis since H is used in constructing the quotient map.

theorem ideal.quotient_map_injective {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] {I : ideal S} {f : R →+* S} :

If we take `J = I.comap f` then `quotient_map` is injective automatically.

theorem ideal.quotient_map_surjective {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] {J : ideal R} {I : ideal S} {f : R →+* S} {H : J I} (hf : function.surjective f) :
theorem ideal.comp_quotient_map_eq_of_comp_eq {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] {R' : Type u_3} {S' : Type u_4} [comm_ring R'] [comm_ring S'] {f : R →+* S} {f' : R' →+* S'} {g : R →+* R'} {g' : S →+* S'} (hfg : f'.comp g = g'.comp f) (I : ideal S') :

Commutativity of a square is preserved when taking quotients by an ideal.

def ideal.quotient_mapₐ {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] {A : Type u_3} [comm_ring A] [ A] [ S] {I : ideal A} (J : ideal S) (f : A →ₐ[R] S) (hIJ : I J) :

The algebra hom `A/I →+* S/J` induced by an algebra hom `f : A →ₐ[R] S` with `I ≤ f⁻¹(J)`.

Equations
@[simp]
theorem ideal.quotient_map_mkₐ {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] {A : Type u_3} [comm_ring A] [ A] [ S] {I : ideal A} (J : ideal S) (f : A →ₐ[R] S) (H : I J) {x : A} :
(J.quotient_mapₐ f H) ( x) = J) (f x)
theorem ideal.quotient_map_comp_mkₐ {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] {A : Type u_3} [comm_ring A] [ A] [ S] {I : ideal A} (J : ideal S) (f : A →ₐ[R] S) (H : I J) :
(J.quotient_mapₐ f H).comp I) = J).comp f
def ideal.quotient_equiv_alg {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] {A : Type u_3} [comm_ring A] [ A] [ S] (I : ideal A) (J : ideal S) (f : A ≃ₐ[R] S) (hIJ : J = I) :

The algebra equiv `A/I ≃ₐ[R] S/J` induced by an algebra equiv `f : A ≃ₐ[R] S`, where`J = f(I)`.

Equations
@[instance]
def ideal.quotient_algebra {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] {J : ideal S} [ S] :
Equations
theorem ideal.algebra_map_quotient_injective {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] {J : ideal S} [ S] :
@[instance]
def submodule.module_submodule {R : Type u} {M : Type v} [comm_ring R] [ M] :
module (ideal R) M)
Equations
def ring_hom.lift_of_right_inverse_aux {A : Type u_1} {B : Type u_2} {C : Type u_3} [ring A] [ring B] [ring C] (f : A →+* B) (f_inv : B → A) (hf : f) (g : A →+* C) (hg : f.ker g.ker) :
B →+* C

Auxiliary definition used to define `lift_of_right_inverse`

Equations
@[simp]
theorem ring_hom.lift_of_right_inverse_aux_comp_apply {A : Type u_1} {B : Type u_2} {C : Type u_3} [ring A] [ring B] [ring C] (f : A →+* B) (f_inv : B → A) (hf : f) (g : A →+* C) (hg : f.ker g.ker) (a : A) :
(f.lift_of_right_inverse_aux f_inv hf g hg) (f a) = g a
def ring_hom.lift_of_right_inverse {A : Type u_1} {B : Type u_2} {C : Type u_3} [ring A] [ring B] [ring C] (f : A →+* B) (f_inv : B → A) (hf : f) :
{g // f.ker g.ker} (B →+* C)

`lift_of_right_inverse f hf g hg` is the unique ring homomorphism `φ`

• such that `φ.comp f = g` (`ring_hom.lift_of_right_inverse_comp`),
• where `f : A →+* B` is has a right_inverse `f_inv` (`hf`),
• and `g : B →+* C` satisfies `hg : f.ker ≤ g.ker`.

See `ring_hom.eq_lift_of_right_inverse` for the uniqueness lemma.

``````   A .
|  \
f |   \ g
|    \
v     \⌟
B ----> C
∃!φ
``````
Equations
@[simp]
def ring_hom.lift_of_surjective {A : Type u_1} {B : Type u_2} {C : Type u_3} [ring A] [ring B] [ring C] (f : A →+* B) (hf : function.surjective f) :
{g // f.ker g.ker} (B →+* C)

A non-computable version of `ring_hom.lift_of_right_inverse` for when no computable right inverse is available, that uses `function.surj_inv`.

theorem ring_hom.lift_of_right_inverse_comp_apply {A : Type u_1} {B : Type u_2} {C : Type u_3} [ring A] [ring B] [ring C] (f : A →+* B) (f_inv : B → A) (hf : f) (g : {g // f.ker g.ker}) (x : A) :
((f.lift_of_right_inverse f_inv hf) g) (f x) = g x
theorem ring_hom.lift_of_right_inverse_comp {A : Type u_1} {B : Type u_2} {C : Type u_3} [ring A] [ring B] [ring C] (f : A →+* B) (f_inv : B → A) (hf : f) (g : {g // f.ker g.ker}) :
((f.lift_of_right_inverse f_inv hf) g).comp f = g
theorem ring_hom.eq_lift_of_right_inverse {A : Type u_1} {B : Type u_2} {C : Type u_3} [ring A] [ring B] [ring C] (f : A →+* B) (f_inv : B → A) (hf : f) (g : A →+* C) (hg : f.ker g.ker) (h : B →+* C) (hh : h.comp f = g) :
h = (f.lift_of_right_inverse f_inv hf) g, hg⟩
def double_quot.quot_left_to_quot_sup {R : Type u} [comm_ring R] (I J : ideal R) :

The obvious ring hom `R/I → R/(I ⊔ J)`

Equations
theorem double_quot.ker_quot_left_to_quot_sup {R : Type u} [comm_ring R] (I J : ideal R) :

The kernel of `quot_left_to_quot_sup`

def double_quot.quot_quot_to_quot_sup {R : Type u} [comm_ring R] (I J : ideal R) :

The ring homomorphism `(R/I)/J' -> R/(I ⊔ J)` induced by `quot_left_to_quot_sup` where `J'` is the image of `J` in `R/I`

Equations
def double_quot.quot_quot_mk {R : Type u} [comm_ring R] (I J : ideal R) :

The composite of the maps `R → (R/I)` and `(R/I) → (R/I)/J'`

Equations
theorem double_quot.ker_quot_quot_mk {R : Type u} [comm_ring R] (I J : ideal R) :
.ker = I J

The kernel of `quot_quot_mk`

def double_quot.lift_sup_quot_quot_mk {R : Type u} [comm_ring R] (I J : ideal R) :

The ring homomorphism `R/(I ⊔ J) → (R/I)/J'`induced by `quot_quot_mk`

Equations
def double_quot.quot_quot_equiv_quot_sup {R : Type u} [comm_ring R] (I J : ideal R) :

`quot_quot_to_quot_add` and `lift_sup_double_qot_mk` are inverse isomorphisms

Equations