# Documentation

Mathlib.RingTheory.Ideal.Operations

# More operations on modules and ideals #

instance Submodule.hasSMul' {R : Type u} {M : Type v} [] [] [Module R M] :
SMul () ()
theorem Ideal.smul_eq_mul {R : Type u} [] (I : ) (J : ) :
I J = I * J

This duplicates the global smul_eq_mul, but doesn't have to unfold anywhere near as much to apply.

def Submodule.annihilator {R : Type u} {M : Type v} [] [] [Module R M] (N : ) :

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

Instances For
theorem Submodule.mem_annihilator {R : Type u} {M : Type v} [] [] [Module R M] {N : } {r : R} :
∀ (n : M), n Nr n = 0
theorem Submodule.mem_annihilator' {R : Type u} {M : Type v} [] [] [Module R M] {N : } {r : R} :
N Submodule.comap (r LinearMap.id)
theorem Submodule.mem_annihilator_span {R : Type u} {M : Type v} [] [] [Module R M] (s : Set M) (r : R) :
∀ (n : s), r n = 0
theorem Submodule.mem_annihilator_span_singleton {R : Type u} {M : Type v} [] [] [Module R M] (g : M) (r : R) :
r r g = 0
theorem Submodule.annihilator_bot {R : Type u} {M : Type v} [] [] [Module R M] :
theorem Submodule.annihilator_eq_top_iff {R : Type u} {M : Type v} [] [] [Module R M] {N : } :
N =
theorem Submodule.annihilator_mono {R : Type u} {M : Type v} [] [] [Module R M] {N : } {P : } (h : N P) :
theorem Submodule.annihilator_iSup {R : Type u} {M : Type v} [] [] [Module R M] (ι : Sort w) (f : ι) :
Submodule.annihilator (⨆ (i : ι), f i) = ⨅ (i : ι),
theorem Submodule.smul_mem_smul {R : Type u} {M : Type v} [] [] [Module R M] {I : } {N : } {r : R} {n : M} (hr : r I) (hn : n N) :
r n I N
theorem Submodule.smul_le {R : Type u} {M : Type v} [] [] [Module R M] {I : } {N : } {P : } :
I N P ∀ (r : R), r I∀ (n : M), n Nr n P
theorem Submodule.smul_induction_on {R : Type u} {M : Type v} [] [] [Module R M] {I : } {N : } {p : MProp} {x : M} (H : x I N) (Hb : (r : R) → r I(n : M) → n Np (r n)) (H1 : (x y : M) → p xp yp (x + y)) :
p x
theorem Submodule.smul_induction_on' {R : Type u} {M : Type v} [] [] [Module R M] {I : } {N : } {x : M} (hx : x I N) {p : (x : M) → x I NProp} (Hb : (r : R) → (hr : r I) → (n : M) → (hn : n N) → p (r n) (_ : r n I N)) (H1 : (x : M) → (hx : x I N) → (y : M) → (hy : y I N) → p x hxp y hyp (x + y) (_ : x + y I N)) :
p x hx

Dependent version of Submodule.smul_induction_on.

theorem Submodule.mem_smul_span_singleton {R : Type u} {M : Type v} [] [] [Module R M] {I : } {m : M} {x : M} :
x I Submodule.span R {m} y, y I y m = x
theorem Submodule.smul_le_right {R : Type u} {M : Type v} [] [] [Module R M] {I : } {N : } :
I N N
theorem Submodule.smul_mono {R : Type u} {M : Type v} [] [] [Module R M] {I : } {J : } {N : } {P : } (hij : I J) (hnp : N P) :
I N J P
theorem Submodule.smul_mono_left {R : Type u} {M : Type v} [] [] [Module R M] {I : } {J : } {N : } (h : I J) :
I N J N
theorem Submodule.smul_mono_right {R : Type u} {M : Type v} [] [] [Module R M] {I : } {N : } {P : } (h : N P) :
I N I P
theorem Submodule.map_le_smul_top {R : Type u} {M : Type v} [] [] [Module R M] (I : ) (f : R →ₗ[R] M) :
@[simp]
theorem Submodule.annihilator_smul {R : Type u} {M : Type v} [] [] [Module R M] (N : ) :
@[simp]
theorem Submodule.annihilator_mul {R : Type u} [] (I : ) :
@[simp]
theorem Submodule.mul_annihilator {R : Type u} [] (I : ) :
@[simp]
theorem Submodule.smul_bot {R : Type u} {M : Type v} [] [] [Module R M] (I : ) :
@[simp]
theorem Submodule.bot_smul {R : Type u} {M : Type v} [] [] [Module R M] (N : ) :
@[simp]
theorem Submodule.top_smul {R : Type u} {M : Type v} [] [] [Module R M] (N : ) :
N = N
theorem Submodule.smul_sup {R : Type u} {M : Type v} [] [] [Module R M] (I : ) (N : ) (P : ) :
I (N P) = I N I P
theorem Submodule.sup_smul {R : Type u} {M : Type v} [] [] [Module R M] (I : ) (J : ) (N : ) :
(I J) N = I N J N
theorem Submodule.smul_assoc {R : Type u} {M : Type v} [] [] [Module R M] (I : ) (J : ) (N : ) :
(I J) N = I J N
theorem Submodule.smul_inf_le {R : Type u} {M : Type v} [] [] [Module R M] (I : ) (M₁ : ) (M₂ : ) :
I (M₁ M₂) I M₁ I M₂
theorem Submodule.smul_iSup {R : Type u} {M : Type v} [] [] [Module R M] {ι : Sort u_3} {I : } {t : ι} :
I iSup t = ⨆ (i : ι), I t i
theorem Submodule.smul_iInf_le {R : Type u} {M : Type v} [] [] [Module R M] {ι : Sort u_3} {I : } {t : ι} :
I iInf t ⨅ (i : ι), I t i
theorem Submodule.span_smul_span {R : Type u} {M : Type v} [] [] [Module R M] (S : Set R) (T : Set M) :
= Submodule.span R (⋃ (s : R) (_ : s S) (t : M) (_ : t T), {s t})
theorem Submodule.ideal_span_singleton_smul {R : Type u} {M : Type v} [] [] [Module R M] (r : R) (N : ) :
Ideal.span {r} N = r N
theorem Submodule.mem_of_span_top_of_smul_mem {R : Type u} {M : Type v} [] [] [Module R M] (M' : ) (s : Set R) (hs : ) (x : M) (H : ∀ (r : s), r x M') :
x M'
theorem Submodule.mem_of_span_eq_top_of_smul_pow_mem {R : Type u} {M : Type v} [] [] [Module R M] (M' : ) (s : Set R) (hs : ) (x : M) (H : ∀ (r : s), n, r ^ n x M') :
x M'

Given s, a generating set of R, to check that an x : M falls in a submodule M' of x, we only need to show that r ^ n • x ∈ M' for some n for each r : s.

theorem Submodule.map_smul'' {R : Type u} {M : Type v} [] [] [Module R M] (I : ) (N : ) {M' : Type w} [] [Module R M'] (f : M →ₗ[R] M') :
Submodule.map f (I N) = I
theorem Submodule.mem_smul_span {R : Type u} {M : Type v} [] [] [Module R M] {I : } {s : Set M} {x : M} :
x I x Submodule.span R (⋃ (a : R) (_ : a I) (b : M) (_ : b s), {a b})
theorem Submodule.mem_ideal_smul_span_iff_exists_sum {R : Type u} {M : Type v} [] [] [Module R M] (I : ) {ι : Type u_3} (f : ιM) (x : M) :
x I a x, (Finsupp.sum a fun i c => c f i) = x

If x is an I-multiple of the submodule spanned by f '' s, then we can write x as an I-linear combination of the elements of f '' s.

theorem Submodule.mem_ideal_smul_span_iff_exists_sum' {R : Type u} {M : Type v} [] [] [Module R M] (I : ) {ι : Type u_3} (s : Set ι) (f : ιM) (x : M) :
x I Submodule.span R (f '' s) a x, (Finsupp.sum a fun i c => c f i) = x
theorem Submodule.mem_smul_top_iff {R : Type u} {M : Type v} [] [] [Module R M] (I : ) (N : ) (x : { x // x N }) :
x I x I N
@[simp]
theorem Submodule.smul_comap_le_comap_smul {R : Type u} {M : Type v} [] [] [Module R M] {M' : Type w} [] [Module R M'] (f : M →ₗ[R] M') (S : Submodule R M') (I : ) :
def Submodule.colon {R : Type u} {M : Type v} [] [] [Module R M] (N : ) (P : ) :

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

Instances For
theorem Submodule.mem_colon {R : Type u} {M : Type v} [] [] [Module R M] {N : } {P : } {r : R} :
r ∀ (p : M), p Pr p N
theorem Submodule.mem_colon' {R : Type u} {M : Type v} [] [] [Module R M] {N : } {P : } {r : R} :
r P Submodule.comap (r LinearMap.id) N
theorem Submodule.colon_mono {R : Type u} {M : Type v} [] [] [Module R M] {N₁ : } {N₂ : } {P₁ : } {P₂ : } (hn : N₁ N₂) (hp : P₁ P₂) :
Submodule.colon N₁ P₂ Submodule.colon N₂ P₁
theorem Submodule.iInf_colon_iSup {R : Type u} {M : Type v} [] [] [Module R M] (ι₁ : Sort w) (f : ι₁) (ι₂ : Sort x) (g : ι₂) :
Submodule.colon (⨅ (i : ι₁), f i) (⨆ (j : ι₂), g j) = ⨅ (i : ι₁) (j : ι₂), Submodule.colon (f i) (g j)
@[simp]
theorem Submodule.mem_colon_singleton {R : Type u} {M : Type v} [] [] [Module R M] {N : } {x : M} {r : R} :
@[simp]
theorem Ideal.mem_colon_singleton {R : Type u} [] {I : } {x : R} {r : R} :
@[simp]
theorem Ideal.add_eq_sup {R : Type u} [] {I : } {J : } :
I + J = I J
@[simp]
theorem Ideal.zero_eq_bot {R : Type u} [] :
0 =
@[simp]
theorem Ideal.sum_eq_sup {R : Type u} [] {ι : Type u_1} (s : ) (f : ι) :
=
@[simp]
theorem Ideal.one_eq_top {R : Type u} [] :
1 =
theorem Ideal.mul_mem_mul {R : Type u} [] {I : } {J : } {r : R} {s : R} (hr : r I) (hs : s J) :
r * s I * J
theorem Ideal.mul_mem_mul_rev {R : Type u} [] {I : } {J : } {r : R} {s : R} (hr : r I) (hs : s J) :
s * r I * J
theorem Ideal.pow_mem_pow {R : Type u} [] {I : } {x : R} (hx : x I) (n : ) :
x ^ n I ^ n
theorem Ideal.prod_mem_prod {R : Type u} [] {ι : Type u_2} {s : } {I : ι} {x : ιR} :
(∀ (i : ι), i sx i I i) → (Finset.prod s fun i => x i) Finset.prod s fun i => I i
theorem Ideal.mul_le {R : Type u} [] {I : } {J : } {K : } :
I * J K ∀ (r : R), r I∀ (s : R), s Jr * s K
theorem Ideal.mul_le_left {R : Type u} [] {I : } {J : } :
I * J J
theorem Ideal.mul_le_right {R : Type u} [] {I : } {J : } :
I * J I
@[simp]
theorem Ideal.sup_mul_right_self {R : Type u} [] {I : } {J : } :
I I * J = I
@[simp]
theorem Ideal.sup_mul_left_self {R : Type u} [] {I : } {J : } :
I J * I = I
@[simp]
theorem Ideal.mul_right_self_sup {R : Type u} [] {I : } {J : } :
I * J I = I
@[simp]
theorem Ideal.mul_left_self_sup {R : Type u} [] {I : } {J : } :
J * I I = I
theorem Ideal.mul_comm {R : Type u} [] (I : ) (J : ) :
I * J = J * I
theorem Ideal.mul_assoc {R : Type u} [] (I : ) (J : ) (K : ) :
I * J * K = I * (J * K)
theorem Ideal.span_mul_span {R : Type u} [] (S : Set R) (T : Set R) :
= Ideal.span (⋃ (s : R) (_ : s S) (t : R) (_ : t T), {s * t})
theorem Ideal.span_mul_span' {R : Type u} [] (S : Set R) (T : Set R) :
= Ideal.span (S * T)
theorem Ideal.span_singleton_mul_span_singleton {R : Type u} [] (r : R) (s : R) :
theorem Ideal.span_singleton_pow {R : Type u} [] (s : R) (n : ) :
Ideal.span {s} ^ n = Ideal.span {s ^ n}
theorem Ideal.mem_mul_span_singleton {R : Type u} [] {x : R} {y : R} {I : } :
x I * Ideal.span {y} z, z I z * y = x
theorem Ideal.mem_span_singleton_mul {R : Type u} [] {x : R} {y : R} {I : } :
x Ideal.span {y} * I z, z I y * z = x
theorem Ideal.le_span_singleton_mul_iff {R : Type u} [] {x : R} {I : } {J : } :
I Ideal.span {x} * J ∀ (zI : R), zI IzJ, zJ J x * zJ = zI
theorem Ideal.span_singleton_mul_le_iff {R : Type u} [] {x : R} {I : } {J : } :
Ideal.span {x} * I J ∀ (z : R), z Ix * z J
theorem Ideal.span_singleton_mul_le_span_singleton_mul {R : Type u} [] {x : R} {y : R} {I : } {J : } :
Ideal.span {x} * I Ideal.span {y} * J ∀ (zI : R), zI IzJ, zJ J x * zI = y * zJ
theorem Ideal.span_singleton_mul_right_mono {R : Type u} [] {I : } {J : } [] {x : R} (hx : x 0) :
Ideal.span {x} * I Ideal.span {x} * J I J
theorem Ideal.span_singleton_mul_left_mono {R : Type u} [] {I : } {J : } [] {x : R} (hx : x 0) :
I * Ideal.span {x} J * Ideal.span {x} I J
theorem Ideal.span_singleton_mul_right_inj {R : Type u} [] {I : } {J : } [] {x : R} (hx : x 0) :
Ideal.span {x} * I = Ideal.span {x} * J I = J
theorem Ideal.span_singleton_mul_left_inj {R : Type u} [] {I : } {J : } [] {x : R} (hx : x 0) :
I * Ideal.span {x} = J * Ideal.span {x} I = J
theorem Ideal.span_singleton_mul_right_injective {R : Type u} [] [] {x : R} (hx : x 0) :
Function.Injective ((fun x x_1 => x * x_1) (Ideal.span {x}))
theorem Ideal.span_singleton_mul_left_injective {R : Type u} [] [] {x : R} (hx : x 0) :
theorem Ideal.eq_span_singleton_mul {R : Type u} [] {x : R} (I : ) (J : ) :
I = Ideal.span {x} * J (∀ (zI : R), zI IzJ, zJ J x * zJ = zI) ∀ (z : R), z Jx * z I
theorem Ideal.span_singleton_mul_eq_span_singleton_mul {R : Type u} [] {x : R} {y : R} (I : ) (J : ) :
Ideal.span {x} * I = Ideal.span {y} * J (∀ (zI : R), zI IzJ, zJ J x * zI = y * zJ) ∀ (zJ : R), zJ JzI, zI I x * zI = y * zJ
theorem Ideal.prod_span {R : Type u} [] {ι : Type u_2} (s : ) (I : ιSet R) :
(Finset.prod s fun i => Ideal.span (I i)) = Ideal.span (Finset.prod s fun i => I i)
theorem Ideal.prod_span_singleton {R : Type u} [] {ι : Type u_2} (s : ) (I : ιR) :
(Finset.prod s fun i => Ideal.span {I i}) = Ideal.span {Finset.prod s fun i => I i}
@[simp]
theorem Ideal.multiset_prod_span_singleton {R : Type u} [] (m : ) :
theorem Ideal.finset_inf_span_singleton {R : Type u} [] {ι : Type u_2} (s : ) (I : ιR) (hI : Set.Pairwise (s) (IsCoprime on I)) :
(Finset.inf s fun i => Ideal.span {I i}) = Ideal.span {Finset.prod s fun i => I i}
theorem Ideal.iInf_span_singleton {R : Type u} [] {ι : Type u_2} [] (I : ιR) (hI : ∀ (i j : ι), i jIsCoprime (I i) (I j)) :
⨅ (i : ι), Ideal.span {I i} = Ideal.span {Finset.prod Finset.univ fun i => I i}
theorem Ideal.sup_eq_top_iff_isCoprime {R : Type u_2} [] (x : R) (y : R) :
theorem Ideal.mul_le_inf {R : Type u} [] {I : } {J : } :
I * J I J
theorem Ideal.multiset_prod_le_inf {R : Type u} [] {s : Multiset ()} :
theorem Ideal.prod_le_inf {R : Type u} {ι : Type u_1} [] {s : } {f : ι} :
theorem Ideal.mul_eq_inf_of_coprime {R : Type u} [] {I : } {J : } (h : I J = ) :
I * J = I J
theorem Ideal.sup_mul_eq_of_coprime_left {R : Type u} [] {I : } {J : } {K : } (h : I J = ) :
I J * K = I K
theorem Ideal.sup_mul_eq_of_coprime_right {R : Type u} [] {I : } {J : } {K : } (h : I K = ) :
I J * K = I J
theorem Ideal.mul_sup_eq_of_coprime_left {R : Type u} [] {I : } {J : } {K : } (h : I J = ) :
I * K J = K J
theorem Ideal.mul_sup_eq_of_coprime_right {R : Type u} [] {I : } {J : } {K : } (h : K J = ) :
I * K J = I J
theorem Ideal.sup_prod_eq_top {R : Type u} {ι : Type u_1} [] {I : } {s : } {J : ι} (h : ∀ (i : ι), i sI J i = ) :
(I Finset.prod s fun i => J i) =
theorem Ideal.sup_iInf_eq_top {R : Type u} {ι : Type u_1} [] {I : } {s : } {J : ι} (h : ∀ (i : ι), i sI J i = ) :
I ⨅ (i : ι) (_ : i s), J i =
theorem Ideal.prod_sup_eq_top {R : Type u} {ι : Type u_1} [] {I : } {s : } {J : ι} (h : ∀ (i : ι), i sJ i I = ) :
(Finset.prod s fun i => J i) I =
theorem Ideal.iInf_sup_eq_top {R : Type u} {ι : Type u_1} [] {I : } {s : } {J : ι} (h : ∀ (i : ι), i sJ i I = ) :
(⨅ (i : ι) (_ : i s), J i) I =
theorem Ideal.sup_pow_eq_top {R : Type u} [] {I : } {J : } {n : } (h : I J = ) :
I J ^ n =
theorem Ideal.pow_sup_eq_top {R : Type u} [] {I : } {J : } {n : } (h : I J = ) :
I ^ n J =
theorem Ideal.pow_sup_pow_eq_top {R : Type u} [] {I : } {J : } {m : } {n : } (h : I J = ) :
I ^ m J ^ n =
theorem Ideal.mul_bot {R : Type u} [] (I : ) :
theorem Ideal.bot_mul {R : Type u} [] (I : ) :
@[simp]
theorem Ideal.mul_top {R : Type u} [] (I : ) :
I * = I
@[simp]
theorem Ideal.top_mul {R : Type u} [] (I : ) :
* I = I
theorem Ideal.mul_mono {R : Type u} [] {I : } {J : } {K : } {L : } (hik : I K) (hjl : J L) :
I * J K * L
theorem Ideal.mul_mono_left {R : Type u} [] {I : } {J : } {K : } (h : I J) :
I * K J * K
theorem Ideal.mul_mono_right {R : Type u} [] {I : } {J : } {K : } (h : J K) :
I * J I * K
theorem Ideal.mul_sup {R : Type u} [] (I : ) (J : ) (K : ) :
I * (J K) = I * J I * K
theorem Ideal.sup_mul {R : Type u} [] (I : ) (J : ) (K : ) :
(I J) * K = I * K J * K
theorem Ideal.pow_le_pow {R : Type u} [] {I : } {m : } {n : } (h : m n) :
I ^ n I ^ m
theorem Ideal.pow_le_self {R : Type u} [] {I : } {n : } (hn : n 0) :
I ^ n I
theorem Ideal.pow_mono {R : Type u} [] {I : } {J : } (e : I J) (n : ) :
I ^ n J ^ n
theorem Ideal.mul_eq_bot {R : Type u_2} [] [] {I : } {J : } :
I * J = I = J =
theorem Ideal.prod_eq_bot {R : Type u_2} [] [] {s : Multiset ()} :
I, I s I =

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

theorem Ideal.span_pair_mul_span_pair {R : Type u} [] (w : R) (x : R) (y : R) (z : R) :
Ideal.span {w, x} * Ideal.span {y, z} = Ideal.span {w * y, w * z, x * y, x * z}
def Ideal.radical {R : Type u} [] (I : ) :

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

Instances For
def Ideal.IsRadical {R : Type u} [] (I : ) :

Instances For
theorem Ideal.le_radical {R : Type u} [] {I : } :
theorem Ideal.radical_eq_iff {R : Type u} [] {I : } :

Alias of the reverse direction of Ideal.radical_eq_iff.

theorem Ideal.radical_top (R : Type u) [] :
theorem Ideal.radical_mono {R : Type u} [] {I : } {J : } (H : I J) :
@[simp]
theorem Ideal.radical_idem {R : Type u} [] (I : ) :
theorem Ideal.IsRadical.radical_le_iff {R : Type u} [] {I : } {J : } (hJ : ) :
I J
theorem Ideal.radical_le_radical_iff {R : Type u} [] {I : } {J : } :
theorem Ideal.radical_eq_top {R : Type u} [] {I : } :
I =
theorem Ideal.IsPrime.isRadical {R : Type u} [] {I : } (H : ) :
theorem Ideal.IsPrime.radical {R : Type u} [] {I : } (H : ) :
theorem Ideal.radical_sup {R : Type u} [] (I : ) (J : ) :
theorem Ideal.radical_inf {R : Type u} [] (I : ) (J : ) :
theorem Ideal.radical_mul {R : Type u} [] (I : ) (J : ) :
theorem Ideal.IsPrime.radical_le_iff {R : Type u} [] {I : } {J : } (hJ : ) :
I J
theorem Ideal.radical_eq_sInf {R : Type u} [] (I : ) :
= sInf {J | I J }
@[simp]
theorem Ideal.top_pow (R : Type u) [] (n : ) :
theorem Ideal.radical_pow {R : Type u} [] (I : ) (n : ) (H : n > 0) :
theorem Ideal.IsPrime.mul_le {R : Type u} [] {I : } {J : } {P : } (hp : ) :
I * J P I P J P
theorem Ideal.IsPrime.inf_le {R : Type u} [] {I : } {J : } {P : } (hp : ) :
I J P I P J P
theorem Ideal.IsPrime.multiset_prod_le {R : Type u} [] {s : Multiset ()} {P : } (hp : ) (hne : s 0) :
I, I s I P
theorem Ideal.IsPrime.multiset_prod_map_le {R : Type u} {ι : Type u_1} [] {s : } (f : ι) {P : } (hp : ) (hne : s 0) :
P i, i s f i P
theorem Ideal.IsPrime.prod_le {R : Type u} {ι : Type u_1} [] {s : } {f : ι} {P : } (hp : ) (hne : ) :
P i, i s f i P
theorem Ideal.IsPrime.inf_le' {R : Type u} {ι : Type u_1} [] {s : } {f : ι} {P : } (hp : ) (hsne : ) :
P i, i s f i P
theorem Ideal.subset_union {R : Type u} [Ring R] {I : } {J : } {K : } :
I J K I J I K
theorem Ideal.subset_union_prime' {ι : Type u_1} {R : Type u} [] {s : } {f : ι} {a : ι} {b : ι} (hp : ∀ (i : ι), i sIdeal.IsPrime (f i)) {I : } :
I ↑(f a) ↑(f b) ⋃ (i : ι) (_ : i s), ↑(f i) I f a I f b i, i s I f i
theorem Ideal.subset_union_prime {ι : Type u_1} {R : Type u} [] {s : } {f : ι} (a : ι) (b : ι) (hp : ∀ (i : ι), i si ai bIdeal.IsPrime (f i)) {I : } :
I ⋃ (i : ι) (_ : i s), ↑(f i) i, 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} [] {I : } {J : } :
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.isUnit_iff {R : Type u} [] {I : } :
I =
instance Ideal.uniqueUnits {R : Type u} [] :
def Ideal.map {R : Type u} {S : Type v} {F : Type u_1} [] [] [rc : RingHomClass F R S] (f : F) (I : ) :

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

Instances For
def Ideal.comap {R : Type u} {S : Type v} {F : Type u_1} [] [] [rc : RingHomClass F R S] (f : F) (I : ) :

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

Instances For
theorem Ideal.coe_comap {R : Type u} {S : Type v} {F : Type u_1} [] [] [rc : RingHomClass F R S] (f : F) (I : ) :
↑() = f ⁻¹' I
theorem Ideal.map_mono {R : Type u} {S : Type v} {F : Type u_1} [] [] [rc : RingHomClass F R S] {f : F} {I : } {J : } (h : I J) :
theorem Ideal.mem_map_of_mem {R : Type u} {S : Type v} {F : Type u_1} [] [] [rc : RingHomClass F R S] (f : F) {I : } {x : R} (h : x I) :
f x
theorem Ideal.apply_coe_mem_map {R : Type u} {S : Type v} {F : Type u_1} [] [] [rc : RingHomClass F R S] (f : F) (I : ) (x : { x // x I }) :
f x
theorem Ideal.map_le_iff_le_comap {R : Type u} {S : Type v} {F : Type u_1} [] [] [rc : RingHomClass F R S] {f : F} {I : } {K : } :
K I
@[simp]
theorem Ideal.mem_comap {R : Type u} {S : Type v} {F : Type u_1} [] [] [rc : RingHomClass F R S] {f : F} {K : } {x : R} :
x f x K
theorem Ideal.comap_mono {R : Type u} {S : Type v} {F : Type u_1} [] [] [rc : RingHomClass F R S] {f : F} {K : } {L : } (h : K L) :
theorem Ideal.comap_ne_top {R : Type u} {S : Type v} {F : Type u_1} [] [] [rc : RingHomClass F R S] (f : F) {K : } (hK : K ) :
theorem Ideal.map_le_comap_of_inv_on {R : Type u} {S : Type v} {F : Type u_1} [] [] [rc : RingHomClass F R S] (f : F) {G : Type u_2} [rcg : RingHomClass G S R] (g : G) (I : ) (hf : Set.LeftInvOn g f I) :
theorem Ideal.comap_le_map_of_inv_on {R : Type u} {S : Type v} {F : Type u_1} [] [] [rc : RingHomClass F R S] (f : F) {G : Type u_2} [rcg : RingHomClass G S R] (g : G) (I : ) (hf : Set.LeftInvOn (g) (f) (f ⁻¹' I)) :
theorem Ideal.map_le_comap_of_inverse {R : Type u} {S : Type v} {F : Type u_1} [] [] [rc : RingHomClass F R S] (f : F) {G : Type u_2} [rcg : RingHomClass G S R] (g : G) (I : ) (h : ) :

The Ideal version of Set.image_subset_preimage_of_inverse.

theorem Ideal.comap_le_map_of_inverse {R : Type u} {S : Type v} {F : Type u_1} [] [] [rc : RingHomClass F R S] (f : F) {G : Type u_2} [rcg : RingHomClass G S R] (g : G) (I : ) (h : ) :

The Ideal version of Set.preimage_subset_image_of_inverse.

instance Ideal.IsPrime.comap {R : Type u} {S : Type v} {F : Type u_1} [] [] [rc : RingHomClass F R S] (f : F) {K : } [hK : ] :
theorem Ideal.map_top {R : Type u} {S : Type v} {F : Type u_1} [] [] [rc : RingHomClass F R S] (f : F) :
theorem Ideal.gc_map_comap {R : Type u} {S : Type v} {F : Type u_1} [] [] [rc : RingHomClass F R S] (f : F) :
@[simp]
theorem Ideal.comap_id {R : Type u} [] (I : ) :
= I
@[simp]
theorem Ideal.map_id {R : Type u} [] (I : ) :
Ideal.map () I = I
theorem Ideal.comap_comap {R : Type u} {S : Type v} [] [] {T : Type u_3} [] {I : } (f : R →+* S) (g : S →+* T) :
theorem Ideal.map_map {R : Type u} {S : Type v} [] [] {T : Type u_3} [] {I : } (f : R →+* S) (g : S →+* T) :
theorem Ideal.map_span {R : Type u} {S : Type v} {F : Type u_1} [] [] [rc : RingHomClass F R S] (f : F) (s : Set R) :
Ideal.map f () = Ideal.span (f '' s)
theorem Ideal.map_le_of_le_comap {R : Type u} {S : Type v} {F : Type u_1} [] [] [rc : RingHomClass F R S] {f : F} {I : } {K : } :
I K
theorem Ideal.le_comap_of_map_le {R : Type u} {S : Type v} {F : Type u_1} [] [] [rc : RingHomClass F R S] {f : F} {I : } {K : } :
KI
theorem Ideal.le_comap_map {R : Type u} {S : Type v} {F : Type u_1} [] [] [rc : RingHomClass F R S] {f : F} {I : } :
theorem Ideal.map_comap_le {R : Type u} {S : Type v} {F : Type u_1} [] [] [rc : RingHomClass F R S] {f : F} {K : } :
Ideal.map f () K
@[simp]
theorem Ideal.comap_top {R : Type u} {S : Type v} {F : Type u_1} [] [] [rc : RingHomClass F R S] {f : F} :
@[simp]
theorem Ideal.comap_eq_top_iff {R : Type u} {S : Type v} {F : Type u_1} [] [] [rc : RingHomClass F R S] {f : F} {I : } :
@[simp]
theorem Ideal.map_bot {R : Type u} {S : Type v} {F : Type u_1} [] [] [rc : RingHomClass F R S] {f : F} :
@[simp]
theorem Ideal.map_comap_map {R : Type u} {S : Type v} {F : Type u_1} [] [] [rc : RingHomClass F R S] (f : F) (I : ) :
@[simp]
theorem Ideal.comap_map_comap {R : Type u} {S : Type v} {F : Type u_1} [] [] [rc : RingHomClass F R S] (f : F) (K : ) :
theorem Ideal.map_sup {R : Type u} {S : Type v} {F : Type u_1} [] [] [rc : RingHomClass F R S] (f : F) (I : ) (J : ) :
Ideal.map f (I J) =
theorem Ideal.comap_inf {R : Type u} {S : Type v} {F : Type u_1} [] [] [rc : RingHomClass F R S] (f : F) (K : ) (L : ) :
Ideal.comap f (K L) =
theorem Ideal.map_iSup {R : Type u} {S : Type v} {F : Type u_1} [] [] [rc : RingHomClass F R S] (f : F) {ι : Sort u_3} (K : ι) :
Ideal.map f (iSup K) = ⨆ (i : ι), Ideal.map f (K i)
theorem Ideal.comap_iInf {R : Type u} {S : Type v} {F : Type u_1} [] [] [rc : RingHomClass F R S] (f : F) {ι : Sort u_3} (K : ι) :
Ideal.comap f (iInf K) = ⨅ (i : ι), Ideal.comap f (K i)
theorem Ideal.map_sSup {R : Type u} {S : Type v} {F : Type u_1} [] [] [rc : RingHomClass F R S] (f : F) (s : Set ()) :
Ideal.map f (sSup s) = ⨆ (I : ) (_ : I s),
theorem Ideal.comap_sInf {R : Type u} {S : Type v} {F : Type u_1} [] [] [rc : RingHomClass F R S] (f : F) (s : Set ()) :
Ideal.comap f (sInf s) = ⨅ (I : ) (_ : I s),
theorem Ideal.comap_sInf' {R : Type u} {S : Type v} {F : Type u_1} [] [] [rc : RingHomClass F R S] (f : F) (s : Set ()) :
Ideal.comap f (sInf s) = ⨅ (I : ) (_ : I ), I
theorem Ideal.comap_isPrime {R : Type u} {S : Type v} {F : Type u_1} [] [] [rc : RingHomClass F R S] (f : F) (K : ) [H : ] :
theorem Ideal.map_inf_le {R : Type u} {S : Type v} {F : Type u_1} [] [] [rc : RingHomClass F R S] (f : F) {I : } {J : } :
Ideal.map f (I J)
theorem Ideal.le_comap_sup {R : Type u} {S : Type v} {F : Type u_1} [] [] [rc : RingHomClass F R S] (f : F) {K : } {L : } :
@[simp]
theorem Ideal.smul_top_eq_map {R : Type u_4} {S : Type u_5} [] [] [Algebra R S] (I : ) :
@[simp]
theorem Ideal.coe_restrictScalars {R : Type u_4} {S : Type u_5} [] [] [Algebra R S] (I : ) :
↑() = I
@[simp]
theorem Ideal.restrictScalars_mul {R : Type u_4} {S : Type u_5} [] [] [Algebra R S] (I : ) (J : ) :

The smallest S-submodule that contains all x ∈ I * y ∈ J is also the smallest R-submodule that does so.

theorem Ideal.map_comap_of_surjective {R : Type u} {S : Type v} {F : Type u_1} [] [] [rc : RingHomClass F R S] (f : F) (hf : ) (I : ) :
Ideal.map f () = I
def Ideal.giMapComap {R : Type u} {S : Type v} {F : Type u_1} [] [] [rc : RingHomClass F R S] (f : F) (hf : ) :

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

Instances For
theorem Ideal.map_surjective_of_surjective {R : Type u} {S : Type v} {F : Type u_1} [] [] [rc : RingHomClass F R S] (f : F) (hf : ) :
theorem Ideal.comap_injective_of_surjective {R : Type u} {S : Type v} {F : Type u_1} [] [] [rc : RingHomClass F R S] (f : F) (hf : ) :
theorem Ideal.map_sup_comap_of_surjective {R : Type u} {S : Type v} {F : Type u_1} [] [] [rc : RingHomClass F R S] (f : F) (hf : ) (I : ) (J : ) :
Ideal.map f ( ) = I J
theorem Ideal.map_iSup_comap_of_surjective {R : Type u} {S : Type v} {F : Type u_1} [] [] [rc : RingHomClass F R S] (f : F) {ι : Sort u_3} (hf : ) (K : ι) :
Ideal.map f (⨆ (i : ι), Ideal.comap f (K i)) = iSup K
theorem Ideal.map_inf_comap_of_surjective {R : Type u} {S : Type v} {F : Type u_1} [] [] [rc : RingHomClass F R S] (f : F) (hf : ) (I : ) (J : ) :
Ideal.map f ( ) = I J
theorem Ideal.map_iInf_comap_of_surjective {R : Type u} {S : Type v} {F : Type u_1} [] [] [rc : RingHomClass F R S] (f : F) {ι : Sort u_3} (hf : ) (K : ι) :
Ideal.map f (⨅ (i : ι), Ideal.comap f (K i)) = iInf K
theorem Ideal.mem_image_of_mem_map_of_surjective {R : Type u} {S : Type v} {F : Type u_1} [] [] [rc : RingHomClass F R S] (f : F) (hf : ) {I : } {y : S} (H : y ) :
y f '' I
theorem Ideal.mem_map_iff_of_surjective {R : Type u} {S : Type v} {F : Type u_1} [] [] [rc : RingHomClass F R S] (f : F) (hf : ) {I : } {y : S} :
y x, x I f x = y
theorem Ideal.le_map_of_comap_le_of_surjective {R : Type u} {S : Type v} {F : Type u_1} [] [] [rc : RingHomClass F R S] (f : F) {I : } {K : } (hf : ) :
IK
theorem Ideal.map_eq_submodule_map {R : Type u} {S : Type v} [] [] (f : R →+* S) [h : ] (I : ) :
theorem Ideal.comap_bot_le_of_injective {R : Type u} {S : Type v} {F : Type u_1} [] [] [rc : RingHomClass F R S] (f : F) {I : } (hf : ) :
I
theorem Ideal.comap_bot_of_injective {R : Type u} {S : Type v} {F : Type u_1} [] [] [rc : RingHomClass F R S] (f : F) (hf : ) :
theorem Ideal.comap_map_of_surjective {R : Type u} {S : Type v} {F : Type u_1} [Ring R] [Ring S] [RingHomClass F R S] (f : F) (hf : ) (I : ) :
Ideal.comap f () = I
def Ideal.relIsoOfSurjective {R : Type u} {S : Type v} {F : Type u_1} [Ring R] [Ring S] [RingHomClass F R S] (f : F) (hf : ) :
≃o { p // p }

Correspondence theorem

Instances For
def Ideal.orderEmbeddingOfSurjective {R : Type u} {S : Type v} {F : Type u_1} [Ring R] [Ring S] [RingHomClass F R S] (f : F) (hf : ) :

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

Instances For
theorem Ideal.map_eq_top_or_isMaximal_of_surjective {R : Type u} {S : Type v} {F : Type u_1} [Ring R] [Ring S] [RingHomClass F R S] (f : F) (hf : ) {I : } (H : ) :
theorem Ideal.comap_isMaximal_of_surjective {R : Type u} {S : Type v} {F : Type u_1} [Ring R] [Ring S] [RingHomClass F R S] (f : F) (hf : ) {K : } [H : ] :
theorem Ideal.comap_le_comap_iff_of_surjective {R : Type u} {S : Type v} {F : Type u_1} [Ring R] [Ring S] [RingHomClass F R S] (f : F) (hf : ) (I : ) (J : ) :
I J
@[simp]
theorem Ideal.map_of_equiv {R : Type u} {S : Type v} [Ring R] [Ring S] (I : ) (f : R ≃+* S) :
Ideal.map (↑()) (Ideal.map (f) I) = I

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 : ) (f : R ≃+* S) :
Ideal.comap (f) (Ideal.comap (↑()) 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 : ) (f : R ≃+* S) :
Ideal.map (f) I =

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

def Ideal.relIsoOfBijective {R : Type u} {S : Type v} {F : Type u_1} [Ring R] [Ring S] [RingHomClass F R S] (f : F) (hf : ) :

Special case of the correspondence theorem for isomorphic rings

Instances For
theorem Ideal.comap_le_iff_le_map {R : Type u} {S : Type v} {F : Type u_1} [Ring R] [Ring S] [RingHomClass F R S] (f : F) (hf : ) {I : } {K : } :
I K
theorem Ideal.map.isMaximal {R : Type u} {S : Type v} {F : Type u_1} [Ring R] [Ring S] [RingHomClass F R S] (f : F) (hf : ) {I : } (H : ) :
theorem Ideal.RingEquiv.bot_maximal_iff {R : Type u} {S : Type v} [Ring R] [Ring S] (e : R ≃+* S) :
theorem Ideal.map_mul {R : Type u} {S : Type v} {F : Type u_1} [] [] [rc : RingHomClass F R S] (f : F) (I : ) (J : ) :
Ideal.map f (I * J) = *
@[simp]
theorem Ideal.mapHom_apply {R : Type u} {S : Type v} {F : Type u_1} [] [] [rc : RingHomClass F R S] (f : F) (I : ) :
↑() I =
def Ideal.mapHom {R : Type u} {S : Type v} {F : Type u_1} [] [] [rc : RingHomClass F R S] (f : F) :

The pushforward Ideal.map as a monoid-with-zero homomorphism.

Instances For
theorem Ideal.map_pow {R : Type u} {S : Type v} {F : Type u_1} [] [] [rc : RingHomClass F R S] (f : F) (I : ) (n : ) :
Ideal.map f (I ^ n) = ^ n
theorem Ideal.comap_radical {R : Type u} {S : Type v} {F : Type u_1} [] [] [rc : RingHomClass F R S] (f : F) (K : ) :
theorem Ideal.IsRadical.comap {R : Type u} {S : Type v} {F : Type u_1} [] [] [rc : RingHomClass F R S] (f : F) {K : } (hK : ) :
theorem Ideal.map_radical_le {R : Type u} {S : Type v} {F : Type u_1} [] [] [rc : RingHomClass F R S] (f : F) {I : } :
theorem Ideal.le_comap_mul {R : Type u} {S : Type v} {F : Type u_1} [] [] [rc : RingHomClass F R S] (f : F) {K : } {L : } :
* Ideal.comap f (K * L)
theorem Ideal.le_comap_pow {R : Type u} {S : Type v} {F : Type u_1} [] [] [rc : RingHomClass F R S] (f : F) {K : } (n : ) :
^ n Ideal.comap f (K ^ n)
def Ideal.IsPrimary {R : Type u} [] (I : ) :

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

Instances For
theorem Ideal.IsPrime.isPrimary {R : Type u} [] {I : } (hi : ) :
theorem Ideal.mem_radical_of_pow_mem {R : Type u} [] {I : } {x : R} {m : } (hx : x ^ m ) :
theorem Ideal.isPrime_radical {R : Type u} [] {I : } (hi : ) :
theorem Ideal.isPrimary_inf {R : Type u} [] {I : } {J : } (hi : ) (hj : ) (hij : ) :
noncomputable def Ideal.finsuppTotal (ι : Type u_1) (M : Type u_2) [] {R : Type u_3} [] [Module R M] (I : ) (v : ιM) :
(ι →₀ { x // x I }) →ₗ[R] M

A variant of Finsupp.total that takes in vectors valued in I.

Instances For
theorem Ideal.finsuppTotal_apply {ι : Type u_1} {M : Type u_2} [] {R : Type u_3} [] [Module R M] (I : ) {v : ιM} (f : ι →₀ { x // x I }) :
↑() f = Finsupp.sum f fun i x => x v i
theorem Ideal.finsuppTotal_apply_eq_of_fintype {ι : Type u_1} {M : Type u_2} [] {R : Type u_3} [] [Module R M] (I : ) {v : ιM} [] (f : ι →₀ { x // x I }) :
↑() f = Finset.sum Finset.univ fun i => ↑(f i) v i
theorem Ideal.range_finsuppTotal {ι : Type u_1} {M : Type u_2} [] {R : Type u_3} [] [Module R M] (I : ) {v : ιM} :
noncomputable def Ideal.basisSpanSingleton {ι : Type u_1} {R : Type u_2} {S : Type u_3} [] [] [] [Algebra R S] (b : Basis ι R S) {x : S} (hx : x 0) :
Basis ι R { x // x Ideal.span {x} }

A basis on S gives a basis on Ideal.span {x}, by multiplying everything by x.

Instances For
@[simp]
theorem Ideal.basisSpanSingleton_apply {ι : Type u_1} {R : Type u_2} {S : Type u_3} [] [] [] [Algebra R S] (b : Basis ι R S) {x : S} (hx : x 0) (i : ι) :
↑(↑() i) = x * b i
@[simp]
theorem Ideal.constr_basisSpanSingleton {ι : Type u_1} {R : Type u_2} {S : Type u_3} [] [] [] [Algebra R S] {N : Type u_4} [] [Module N S] [] (b : Basis ι R S) {x : S} (hx : x 0) :
theorem Associates.mk_ne_zero' {R : Type u_1} [] {r : R} :
theorem Basis.mem_ideal_iff {ι : Type u_1} {R : Type u_2} {S : Type u_3} [] [] [Algebra R S] {I : } (b : Basis ι R { x // x I }) {x : S} :
x I c, x = Finsupp.sum c fun i x => x ↑(b i)

If I : Ideal S has a basis over R, x ∈ I iff it is a linear combination of basis vectors.

theorem Basis.mem_ideal_iff' {ι : Type u_1} {R : Type u_2} {S : Type u_3} [] [] [] [Algebra R S] {I : } (b : Basis ι R { x // x I }) {x : S} :
x I c, x = Finset.sum Finset.univ fun i => c i ↑(b i)

If I : Ideal S has a finite basis over R, x ∈ I iff it is a linear combination of basis vectors.

def RingHom.ker {R : Type u} {S : Type v} {F : Type u_1} [] [] [rcf : RingHomClass F R S] (f : F) :

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

Instances For
theorem RingHom.mem_ker {R : Type u} {S : Type v} {F : Type u_1} [] [] [rcf : RingHomClass F R S] (f : F) {r : R} :
r f r = 0

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

theorem RingHom.ker_eq {R : Type u} {S : Type v} {F : Type u_1} [] [] [rcf : RingHomClass F R S] (f : F) :
↑() = f ⁻¹' {0}
theorem RingHom.ker_eq_comap_bot {R : Type u} {S : Type v} {F : Type u_1} [] [] [rcf : RingHomClass F R S] (f : F) :
theorem RingHom.comap_ker {R : Type u} {S : Type v} {T : Type w} [] [] [] (f : S →+* R) (g : T →+* S) :
theorem RingHom.not_one_mem_ker {R : Type u} {S : Type v} {F : Type u_1} [] [] [rcf : RingHomClass F R S] [] (f : F) :

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

theorem RingHom.ker_ne_top {R : Type u} {S : Type v} {F : Type u_1} [] [] [rcf : RingHomClass F R S] [] (f : F) :
theorem RingHom.injective_iff_ker_eq_bot {R : Type u} {S : Type v} {F : Type u_1} [Ring R] [] [rc : RingHomClass F R S] (f : F) :
theorem RingHom.ker_eq_bot_iff_eq_zero {R : Type u} {S : Type v} {F : Type u_1} [Ring R] [] [rc : RingHomClass F R S] (f : F) :
∀ (x : R), f x = 0x = 0
@[simp]
theorem RingHom.ker_coe_equiv {R : Type u} {S : Type v} [Ring R] [] (f : R ≃+* S) :
@[simp]
theorem RingHom.ker_equiv {R : Type u} {S : Type v} [Ring R] [] {F' : Type u_2} [RingEquivClass F' R S] (f : F') :
theorem RingHom.sub_mem_ker_iff {R : Type u} {S : Type v} {F : Type u_1} [Ring R] [Ring S] [rc : RingHomClass F R S] (f : F) {x : R} {y : R} :
x - y f x = f y
theorem RingHom.ker_isPrime {R : Type u} {S : Type v} {F : Type u_1} [Ring R] [Ring S] [] [RingHomClass F R S] (f : F) :

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

theorem RingHom.ker_isMaximal_of_surjective {R : Type u_1} {K : Type u_2} {F : Type u_3} [Ring R] [] [RingHomClass F R K] (f : F) (hf : ) :

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} {F : Type u_3} [] [] [rc : RingHomClass F R S] {I : } (f : F) :
= I
theorem Ideal.ker_le_comap {R : Type u_1} {S : Type u_2} {F : Type u_3} [] [] [rc : RingHomClass F R S] {K : } (f : F) :
theorem Ideal.map_sInf {R : Type u_1} {S : Type u_2} {F : Type u_3} [Ring R] [Ring S] [rc : RingHomClass F R S] {A : Set ()} {f : F} (hf : ) :
(∀ (J : ), J A J) → Ideal.map f (sInf A) = sInf ( '' A)
theorem Ideal.map_isPrime_of_surjective {R : Type u_1} {S : Type u_2} {F : Type u_3} [Ring R] [Ring S] [rc : RingHomClass F R S] {f : F} (hf : ) {I : } [H : ] (hk : I) :
theorem Ideal.map_eq_bot_iff_of_injective {R : Type u_1} {S : Type u_2} {F : Type u_3} [Ring R] [Ring S] [rc : RingHomClass F R S] {I : } {f : F} (hf : ) :
theorem Ideal.map_isPrime_of_equiv {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] {F' : Type u_4} [RingEquivClass F' R S] (f : F') {I : } [] :
theorem Ideal.map_eq_iff_sup_ker_eq_of_surjective {R : Type u_1} {S : Type u_2} [] [] {I : } {J : } (f : R →+* S) (hf : ) :
= I = J
theorem Ideal.map_radical_of_surjective {R : Type u_1} {S : Type u_2} [] [] {f : R →+* S} (hf : ) {I : } (h : I) :
instance Submodule.moduleSubmodule {R : Type u} {M : Type v} [] [] [Module R M] :
Module () ()
def RingHom.liftOfRightInverseAux {A : Type u_1} {B : Type u_2} {C : Type u_3} [Ring A] [Ring B] [Ring C] (f : A →+* B) (f_inv : BA) (hf : Function.RightInverse f_inv f) (g : A →+* C) (hg : ) :
B →+* C

Auxiliary definition used to define liftOfRightInverse

Instances For
@[simp]
theorem RingHom.liftOfRightInverseAux_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 : BA) (hf : Function.RightInverse f_inv f) (g : A →+* C) (hg : ) (a : A) :
↑(RingHom.liftOfRightInverseAux f f_inv hf g hg) (f a) = g a
def RingHom.liftOfRightInverse {A : Type u_1} {B : Type u_2} {C : Type u_3} [Ring A] [Ring B] [Ring C] (f : A →+* B) (f_inv : BA) (hf : Function.RightInverse f_inv f) :
{ g // } (B →+* C)

liftOfRightInverse f hf g hg is the unique ring homomorphism φ

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

See RingHom.eq_liftOfRightInverse for the uniqueness lemma.

   A .
|  \
f |   \ g
|    \
v     \⌟
B ----> C
∃!φ

Instances For
@[inline, reducible]
noncomputable abbrev RingHom.liftOfSurjective {A : Type u_1} {B : Type u_2} {C : Type u_3} [Ring A] [Ring B] [Ring C] (f : A →+* B) (hf : ) :
{ g // } (B →+* C)

A non-computable version of RingHom.liftOfRightInverse for when no computable right inverse is available, that uses Function.surjInv.

Instances For
theorem RingHom.liftOfRightInverse_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 : BA) (hf : Function.RightInverse f_inv f) (g : { g // }) (x : A) :
↑(↑(RingHom.liftOfRightInverse f f_inv hf) g) (f x) = g x
theorem RingHom.liftOfRightInverse_comp {A : Type u_1} {B : Type u_2} {C : Type u_3} [Ring A] [Ring B] [Ring C] (f : A →+* B) (f_inv : BA) (hf : Function.RightInverse f_inv f) (g : { g // }) :
RingHom.comp (↑(RingHom.liftOfRightInverse f f_inv hf) g) f = g
theorem RingHom.eq_liftOfRightInverse {A : Type u_1} {B : Type u_2} {C : Type u_3} [Ring A] [Ring B] [Ring C] (f : A →+* B) (f_inv : BA) (hf : Function.RightInverse f_inv f) (g : A →+* C) (hg : ) (h : B →+* C) (hh : = g) :
h = ↑(RingHom.liftOfRightInverse f f_inv hf) { val := g, property := hg }