More operations on modules and ideals

theorem Submodule.coe_span_smul {R' : Type u_1} {M' : Type u_2} [CommSemiring R'] [AddCommMonoid M'] [Module R' M'] (s : Set R') (N : Submodule R' M') : ↑(Ideal.span s) • N = s • N

theorem Submodule.span_singleton_toAddSubgroup_eq_zmultiples (a : ℤ) : (ℤ ∙ a).toAddSubgroup = AddSubgroup.zmultiples a

@[simp]

theorem Ideal.span_singleton_toAddSubgroup_eq_zmultiples (a : ℤ) : Submodule.toAddSubgroup (span {a}) = AddSubgroup.zmultiples a

theorem Ideal.smul_eq_mul {R : Type u} [Semiring R] (I J : Ideal R) : I • J = I * J

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

theorem Submodule.smul_le_right {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] {I : Ideal R} {N : Submodule R M} : I • N ≤ N

theorem Submodule.map_le_smul_top {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] (I : Ideal R) (f : R →ₗ[R] M) : map f I ≤ I • ⊤

@[simp]

theorem Submodule.top_smul {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] (N : Submodule R M) : ⊤ • N = N

theorem Submodule.mul_smul {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] (I J : Ideal R) (N : Submodule R M) : (I * J) • N = I • J • N

theorem Submodule.mem_of_span_top_of_smul_mem {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] (M' : Submodule R M) (s : Set R) (hs : Ideal.span s = ⊤) (x : M) (H : ∀ (r : ↑s), ↑r • x ∈ M') : x ∈ M'

@[simp]

theorem Submodule.map_smul'' {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] (I : Ideal R) (N : Submodule R M) {M' : Type w} [AddCommMonoid M'] [Module R M'] (f : M →ₗ[R] M') : map f (I • N) = I • map f N

theorem Submodule.mem_smul_top_iff {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] (I : Ideal R) (N : Submodule R M) (x : ↥N) : x ∈ I • ⊤ ↔ ↑x ∈ I • N

@[simp]

theorem Submodule.smul_comap_le_comap_smul {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] {M' : Type w} [AddCommMonoid M'] [Module R M'] (f : M →ₗ[R] M') (S : Submodule R M') (I : Ideal R) : I • comap f S ≤ comap f (I • S)

theorem Submodule.comap_smul'' {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] {M' : Type w} [AddCommMonoid M'] [Module R M'] {f : M →ₗ[R] M'} (hf : Function.Injective ⇑f) {p : Submodule R M'} (hp : p ≤ f.range) {I : Ideal R} : comap f (I • p) = I • comap f p

theorem Submodule.mem_smul_span_singleton {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] {I : Ideal R} [I.IsTwoSided] {m x : M} : x ∈ I • (R ∙ m) ↔ ∃ y ∈ I, y • m = x

theorem Submodule.span_smul_span {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] (S : Set R) (T : Set M) [(Ideal.span S).IsTwoSided] : Ideal.span S • span R T = span R (S • T)

theorem Submodule.mem_smul_span {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] {I : Ideal R} [I.IsTwoSided] {s : Set M} {x : M} : x ∈ I • span R s ↔ x ∈ span R (↑I • s)

theorem Submodule.mem_ideal_smul_span_iff_exists_sum {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] (I : Ideal R) [I.IsTwoSided] {ι : Type u_4} (f : ι → M) (x : M) : x ∈ I • span R (Set.range f) ↔ ∃ (a : ι →₀ R) (_ : ∀ (i : ι), a i ∈ I), (a.sum fun (i : ι) (c : R) => 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} [Semiring R] [AddCommMonoid M] [Module R M] (I : Ideal R) [I.IsTwoSided] {ι : Type u_4} (s : Set ι) (f : ι → M) (x : M) : x ∈ I • span R (f '' s) ↔ ∃ (a : ↑s →₀ R) (_ : ∀ (i : ↑s), a i ∈ I), (a.sum fun (i : ↑s) (c : R) => c • f ↑i) = x

theorem Submodule.smul_eq_map₂ {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] {I : Ideal R} {N : Submodule R M} : I • N = map₂ (LinearMap.lsmul R M) I N

theorem Submodule.ideal_span_singleton_smul {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] (r : R) (N : Submodule R M) : Ideal.span {r} • N = r • N

theorem Submodule.mem_of_span_eq_top_of_smul_pow_mem {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] (M' : Submodule R M) (s : Set R) (hs : Ideal.span s = ⊤) (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.

@[simp]

theorem Submodule.map_pointwise_smul {R : Type u} {M : Type v} {M' : Type u_1} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module R M'] (r : R) (N : Submodule R M) (f : M →ₗ[R] M') : map f (r • N) = r • map f N

@[simp]

theorem Ideal.add_eq_sup {R : Type u} [Semiring R] {I J : Ideal R} : I + J = I ⊔ J

@[simp]

theorem Ideal.zero_eq_bot {R : Type u} [Semiring R] : 0 = ⊥

@[simp]

theorem Ideal.sum_eq_sup {R : Type u} [Semiring R] {ι : Type u_1} (s : Finset ι) (f : ι → Ideal R) : s.sum f = s.sup f

@[simp]

theorem Ideal.one_eq_top {R : Type u} [Semiring R] : 1 = ⊤

theorem Ideal.add_eq_one_iff {R : Type u} [Semiring R] {I J : Ideal R} : I + J = 1 ↔ ∃ i ∈ I, ∃ j ∈ J, i + j = 1

theorem Ideal.mul_mem_mul {R : Type u} [Semiring R] {I J : Ideal R} {r s : R} (hr : r ∈ I) (hs : s ∈ J) : r * s ∈ I * J

theorem Ideal.bot_pow {R : Type u} [Semiring R] {n : ℕ} (hn : n ≠ 0) : ⊥ ^ n = ⊥

theorem Ideal.pow_mem_pow {R : Type u} [Semiring R] {I : Ideal R} {x : R} (hx : x ∈ I) (n : ℕ) : x ^ n ∈ I ^ n

theorem Ideal.mul_le {R : Type u} [Semiring R] {I J K : Ideal R} : I * J ≤ K ↔ ∀ r ∈ I, ∀ s ∈ J, r * s ∈ K

theorem Ideal.mul_le_left {R : Type u} [Semiring R] {I J : Ideal R} : I * J ≤ J

@[simp]

theorem Ideal.sup_mul_left_self {R : Type u} [Semiring R] {I J : Ideal R} : I ⊔ J * I = I

@[simp]

theorem Ideal.mul_left_self_sup {R : Type u} [Semiring R] {I J : Ideal R} : J * I ⊔ I = I

theorem Ideal.mul_le_right {R : Type u} [Semiring R] {I J : Ideal R} [I.IsTwoSided] : I * J ≤ I

@[simp]

theorem Ideal.sup_mul_right_self {R : Type u} [Semiring R] {I J : Ideal R} [I.IsTwoSided] : I ⊔ I * J = I

@[simp]

theorem Ideal.mul_right_self_sup {R : Type u} [Semiring R] {I J : Ideal R} [I.IsTwoSided] : I * J ⊔ I = I

theorem Ideal.mul_assoc {R : Type u} [Semiring R] {I J K : Ideal R} : I * J * K = I * (J * K)

theorem Ideal.mul_bot {R : Type u} [Semiring R] (I : Ideal R) : I * ⊥ = ⊥

theorem Ideal.bot_mul {R : Type u} [Semiring R] (I : Ideal R) : ⊥ * I = ⊥

@[simp]

theorem Ideal.top_mul {R : Type u} [Semiring R] (I : Ideal R) : ⊤ * I = I

theorem Ideal.mul_mono {R : Type u} [Semiring 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} [Semiring R] {I J K : Ideal R} (h : I ≤ J) : I * K ≤ J * K

theorem Ideal.mul_mono_right {R : Type u} [Semiring R] {I J K : Ideal R} (h : J ≤ K) : I * J ≤ I * K

theorem Ideal.mul_sup {R : Type u} [Semiring R] (I J K : Ideal R) : I * (J ⊔ K) = I * J ⊔ I * K

theorem Ideal.sup_mul {R : Type u} [Semiring R] (I J K : Ideal R) : (I ⊔ J) * K = I * K ⊔ J * K

theorem Ideal.mul_iSup {R : Type u} [Semiring R] (I : Ideal R) {ι : Sort u_1} (J : ι → Ideal R) : I * ⨆ (i : ι), J i = ⨆ (i : ι), I * J i

theorem Ideal.iSup_mul {R : Type u} [Semiring R] {ι : Sort u_1} (J : ι → Ideal R) (I : Ideal R) : (⨆ (i : ι), J i) * I = ⨆ (i : ι), J i * I

theorem Ideal.pow_le_pow_right {R : Type u} [Semiring R] {I : Ideal R} {m n : ℕ} (h : m ≤ n) : I ^ n ≤ I ^ m

theorem Ideal.pow_le_self {R : Type u} [Semiring R] {I : Ideal R} {n : ℕ} (hn : n ≠ 0) : I ^ n ≤ I

theorem Ideal.pow_right_mono {R : Type u} [Semiring R] {I J : Ideal R} (e : I ≤ J) (n : ℕ) : I ^ n ≤ J ^ n

@[instance 100]

instance Ideal.IsTwoSided.instHMul {R : Type u} [Semiring R] {I J : Ideal R} [J.IsTwoSided] : (I * J).IsTwoSided

@[instance 100]

instance Ideal.IsTwoSided.instHPowNat {R : Type u} [Semiring R] {I : Ideal R} [I.IsTwoSided] (n : ℕ) : (I ^ n).IsTwoSided

theorem Ideal.IsTwoSided.mul_one {R : Type u} [Semiring R] {I : Ideal R} [I.IsTwoSided] : I * 1 = I

theorem Ideal.IsTwoSided.pow_add {R : Type u} [Semiring R] {I : Ideal R} [I.IsTwoSided] (m n : ℕ) : I ^ (m + n) = I ^ m * I ^ n

theorem Ideal.IsTwoSided.pow_succ {R : Type u} [Semiring R] {I : Ideal R} [I.IsTwoSided] (n : ℕ) : I ^ (n + 1) = I * I ^ n

@[simp]

theorem Ideal.mul_eq_bot {R : Type u} [Semiring R] {I J : Ideal R} [NoZeroDivisors R] : I * J = ⊥ ↔ I = ⊥ ∨ J = ⊥

instance Ideal.instNoZeroDivisors {R : Type u} [Semiring R] [NoZeroDivisors R] : NoZeroDivisors (Ideal R)

instance Ideal.instIsTorsionFreeSubtypeMemSubmodule {R : Type u} [Semiring R] {S : Type u_1} {A : Type u_2} [Semiring S] [SMul R S] [AddCommMonoid A] [Module R A] [Module S A] [IsScalarTower R S A] [Module.IsTorsionFree R A] {I : Submodule S A} : Module.IsTorsionFree R ↥I

theorem Ideal.span_mul_span {R : Type u} [Semiring R] (S T : Set R) [(span S).IsTwoSided] : span S * span T = span (S * T)

theorem Ideal.span_mul_span' {R : Type u} [Semiring R] (S T : Set R) [(span S).IsTwoSided] : span S * span T = span (S * T)

theorem Ideal.span_singleton_mul_span_singleton {R : Type u} [Semiring R] (r s : R) [(span {r}).IsTwoSided] : span {r} * span {s} = span {r * s}

theorem Ideal.span_singleton_pow {R : Type u} [Semiring R] (s : R) [(span {s}).IsTwoSided] (n : ℕ) : span {s} ^ n = span {s ^ n}

theorem Ideal.mem_mul_span_singleton {R : Type u} [Semiring R] {x y : R} {I : Ideal R} [I.IsTwoSided] : x ∈ I * span {y} ↔ ∃ z ∈ I, z * y = x

theorem Ideal.span_singleton_mul_left_mono {R : Type u} [Semiring R] {I J : Ideal R} [IsDomain R] [I.IsTwoSided] [J.IsTwoSided] {x : R} (hx : x ≠ 0) : I * span {x} ≤ J * span {x} ↔ I ≤ J

theorem Ideal.span_singleton_mul_left_inj {R : Type u} [Semiring R] {I J : Ideal R} [IsDomain R] [I.IsTwoSided] [J.IsTwoSided] {x : R} (hx : x ≠ 0) : I * span {x} = J * span {x} ↔ I = J

theorem Ideal.mul_le_inf {R : Type u} [Semiring R] {I J : Ideal R} [I.IsTwoSided] : I * J ≤ I ⊓ J

theorem Ideal.sup_mul_eq_of_coprime_left {R : Type u} [Semiring R] {I J K : Ideal R} [I.IsTwoSided] (h : I ⊔ J = ⊤) : I ⊔ J * K = I ⊔ K

theorem Ideal.sup_mul_eq_of_coprime_right {R : Type u} [Semiring R] {I J K : Ideal R} [J.IsTwoSided] (h : I ⊔ K = ⊤) : I ⊔ J * K = I ⊔ J

theorem Ideal.mul_sup_eq_of_coprime_left {R : Type u} [Semiring R] {I J K : Ideal R} [J.IsTwoSided] (h : I ⊔ J = ⊤) : I * K ⊔ J = K ⊔ J

theorem Ideal.mul_sup_eq_of_coprime_right {R : Type u} [Semiring R] {I J K : Ideal R} [I.IsTwoSided] (h : K ⊔ J = ⊤) : I * K ⊔ J = I ⊔ J

theorem Ideal.sup_iInf_eq_top {R : Type u} [Semiring R] {I : Ideal R} {ι : Type u_1} {s : Finset ι} {J : ι → Ideal R} [∀ (i : ι), (J i).IsTwoSided] (h : ∀ i ∈ s, I ⊔ J i = ⊤) : I ⊔ ⨅ i ∈ s, J i = ⊤

theorem Ideal.iInf_sup_eq_top {R : Type u} [Semiring R] {I : Ideal R} {ι : Type u_1} {s : Finset ι} {J : ι → Ideal R} [∀ (i : ι), (J i).IsTwoSided] (h : ∀ i ∈ s, J i ⊔ I = ⊤) : (⨅ i ∈ s, J i) ⊔ I = ⊤

theorem Ideal.sup_pow_eq_top {R : Type u} [Semiring R] {I J : Ideal R} [I.IsTwoSided] {n : ℕ} (h : I ⊔ J = ⊤) : I ⊔ J ^ n = ⊤

theorem Ideal.sup_pow_eq_top' {R : Type u} [Semiring R] {I J : Ideal R} [J.IsTwoSided] {n : ℕ} (h : I ⊔ J = ⊤) : I ⊔ J ^ n = ⊤

theorem Ideal.pow_sup_eq_top {R : Type u} [Semiring R] {I J : Ideal R} [I.IsTwoSided] {n : ℕ} (h : I ⊔ J = ⊤) : I ^ n ⊔ J = ⊤

theorem Ideal.pow_sup_eq_top' {R : Type u} [Semiring R] {I J : Ideal R} [J.IsTwoSided] {n : ℕ} (h : I ⊔ J = ⊤) : I ^ n ⊔ J = ⊤

theorem Ideal.pow_sup_pow_eq_top {R : Type u} [Semiring R] {I J : Ideal R} [I.IsTwoSided] {m n : ℕ} (h : I ⊔ J = ⊤) : I ^ m ⊔ J ^ n = ⊤

theorem Ideal.pow_sup_pow_eq_top' {R : Type u} [Semiring R] {I J : Ideal R} [J.IsTwoSided] {m n : ℕ} (h : I ⊔ J = ⊤) : I ^ m ⊔ J ^ n = ⊤

@[simp]

theorem Ideal.mul_top {R : Type u} [Semiring R] (I : Ideal R) [I.IsTwoSided] : I * ⊤ = I

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

theorem Ideal.top_pow (R : Type u) [Semiring R] (n : ℕ) : ⊤ ^ n = ⊤

@[simp]

theorem Ideal.pow_eq_top_iff {R : Type u} [Semiring R] {I : Ideal R} {n : ℕ} : I ^ n = ⊤ ↔ I = ⊤ ∨ n = 0

theorem Ideal.natCast_eq_top {R : Type u} [Semiring R] {n : ℕ} (hn : n ≠ 0) : ↑n = ⊤

theorem Ideal.ofNat_eq_top {R : Type u} [Semiring R] {n : ℕ} [n.AtLeastTwo] : OfNat.ofNat n = ⊤

3 : Ideal R is not the ideal generated by 3 (which would be spelt Ideal.span {3}), it is simply 1 + 1 + 1 = ⊤.

theorem Ideal.pow_eq_zero_of_mem {R : Type u} [Semiring R] {I : Ideal R} {n m : ℕ} (hnI : I ^ n = 0) (hmn : n ≤ m) {x : R} (hx : x ∈ I) : x ^ m = 0

theorem Ideal.mul_mem_mul_rev {R : Type u} [CommSemiring R] {I J : Ideal R} {r s : R} (hr : r ∈ I) (hs : s ∈ J) : s * r ∈ I * J

theorem Ideal.prod_mem_prod {R : Type u} [CommSemiring R] {ι : Type u_2} {s : Finset ι} {I : ι → Ideal R} {x : ι → R} : (∀ i ∈ s, x i ∈ I i) → ∏ i ∈ s, x i ∈ ∏ i ∈ s, I i

theorem Ideal.sup_pow_add_le_pow_sup_pow {R : Type u} [CommSemiring R] {I J : Ideal R} {n m : ℕ} : (I ⊔ J) ^ (n + m) ≤ I ^ n ⊔ J ^ m

theorem Ideal.mul_comm {R : Type u} [CommSemiring R] (I J : Ideal R) : I * J = J * I

theorem Ideal.mem_span_singleton_mul {R : Type u} [CommSemiring R] {x y : R} {I : Ideal R} : x ∈ span {y} * I ↔ ∃ z ∈ I, y * z = x

@[simp]

theorem Ideal.range_mul {R : Type u} [CommSemiring R] (A : Type u_2) [CommSemiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] (a : A) : ((LinearMap.mul R A) a).range = Submodule.restrictScalars R (span {a})

theorem Ideal.range_mul' {R : Type u} [CommSemiring R] (a : R) : ((LinearMap.mul R R) a).range = span {a}

theorem Ideal.le_span_singleton_mul_iff {R : Type u} [CommSemiring R] {x : R} {I J : Ideal R} : I ≤ span {x} * J ↔ ∀ zI ∈ I, ∃ zJ ∈ J, x * zJ = zI

theorem Ideal.span_singleton_mul_le_iff {R : Type u} [CommSemiring R] {x : R} {I J : Ideal R} : span {x} * I ≤ J ↔ ∀ z ∈ I, x * z ∈ J

theorem Ideal.span_singleton_mul_le_span_singleton_mul {R : Type u} [CommSemiring R] {x y : R} {I J : Ideal R} : span {x} * I ≤ span {y} * J ↔ ∀ zI ∈ I, ∃ zJ ∈ J, x * zI = y * zJ

theorem Ideal.span_singleton_mul_right_mono {R : Type u} [CommSemiring R] {I J : Ideal R} [IsDomain R] {x : R} (hx : x ≠ 0) : span {x} * I ≤ span {x} * J ↔ I ≤ J

theorem Ideal.span_singleton_mul_right_inj {R : Type u} [CommSemiring R] {I J : Ideal R} [IsDomain R] {x : R} (hx : x ≠ 0) : span {x} * I = span {x} * J ↔ I = J

theorem Ideal.span_singleton_mul_right_injective {R : Type u} [CommSemiring R] [IsDomain R] {x : R} (hx : x ≠ 0) : Function.Injective fun (x_1 : Ideal R) => span {x} * x_1

theorem Ideal.span_singleton_mul_left_injective {R : Type u} [CommSemiring R] [IsDomain R] {x : R} (hx : x ≠ 0) : Function.Injective fun (I : Ideal R) => I * span {x}

theorem Ideal.eq_span_singleton_mul {R : Type u} [CommSemiring R] {x : R} (I J : Ideal R) : I = span {x} * J ↔ (∀ zI ∈ I, ∃ zJ ∈ J, x * zJ = zI) ∧ ∀ z ∈ J, x * z ∈ I

theorem Ideal.span_singleton_mul_eq_span_singleton_mul {R : Type u} [CommSemiring R] {x y : R} (I J : Ideal R) : span {x} * I = span {y} * J ↔ (∀ zI ∈ I, ∃ zJ ∈ J, x * zI = y * zJ) ∧ ∀ zJ ∈ J, ∃ zI ∈ I, x * zI = y * zJ

theorem Ideal.prod_span {R : Type u} [CommSemiring R] {ι : Type u_2} (s : Finset ι) (I : ι → Set R) : ∏ i ∈ s, span (I i) = span (∏ i ∈ s, I i)

theorem Ideal.prod_span_singleton {R : Type u} [CommSemiring R] {ι : Type u_2} (s : Finset ι) (I : ι → R) : ∏ i ∈ s, span {I i} = span {∏ i ∈ s, I i}

@[simp]

theorem Ideal.multiset_prod_span_singleton {R : Type u} [CommSemiring R] (m : Multiset R) : (Multiset.map (fun (x : R) => span {x}) m).prod = span {m.prod}

theorem Ideal.finset_inf_span_singleton {R : Type u} [CommSemiring R] {ι : Type u_2} (s : Finset ι) (I : ι → R) (hI : (↑s).Pairwise (Function.onFun IsCoprime I)) : (s.inf fun (i : ι) => span {I i}) = span {∏ i ∈ s, I i}

theorem Ideal.iInf_span_singleton {R : Type u} [CommSemiring R] {ι : Type u_2} [Fintype ι] {I : ι → R} (hI : ∀ (i j : ι), i ≠ j → IsCoprime (I i) (I j)) : ⨅ (i : ι), span {I i} = span {∏ i : ι, I i}

theorem Ideal.iInf_span_singleton_natCast {R : Type u_2} [CommRing R] {ι : Type u_3} [Fintype ι] {I : ι → ℕ} (hI : Pairwise fun (i j : ι) => (I i).Coprime (I j)) : ⨅ (i : ι), span {↑(I i)} = span {↑(∏ i : ι, I i)}

theorem Ideal.sup_eq_top_iff_isCoprime {R : Type u_2} [CommSemiring R] (x y : R) : span {x} ⊔ span {y} = ⊤ ↔ IsCoprime x y

theorem Ideal.multiset_prod_le_inf {R : Type u} [CommSemiring R] {s : Multiset (Ideal R)} : s.prod ≤ s.inf

theorem Ideal.prod_le_inf {R : Type u} {ι : Type u_1} [CommSemiring R] {s : Finset ι} {f : ι → Ideal R} : s.prod f ≤ s.inf f

theorem Ideal.mul_eq_inf_of_coprime {R : Type u} [CommSemiring R] {I J : Ideal R} (h : I ⊔ J = ⊤) : I * J = I ⊓ J

theorem Ideal.sup_prod_eq_top {R : Type u} {ι : Type u_1} [CommSemiring R] {I : Ideal R} {s : Finset ι} {J : ι → Ideal R} (h : ∀ i ∈ s, I ⊔ J i = ⊤) : I ⊔ ∏ i ∈ s, J i = ⊤

theorem Ideal.sup_multiset_prod_eq_top {R : Type u} [CommSemiring R] {I : Ideal R} {s : Multiset (Ideal R)} (h : ∀ p ∈ s, I ⊔ p = ⊤) : I ⊔ s.prod = ⊤

theorem Ideal.prod_sup_eq_top {R : Type u} {ι : Type u_1} [CommSemiring R] {I : Ideal R} {s : Finset ι} {J : ι → Ideal R} (h : ∀ i ∈ s, J i ⊔ I = ⊤) : (∏ i ∈ s, J i) ⊔ I = ⊤

@[simp]

theorem Ideal.multiset_prod_eq_bot {R : Type u_2} [CommSemiring R] [IsDomain R] {s : Multiset (Ideal R)} : s.prod = ⊥ ↔ ⊥ ∈ s

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

theorem Ideal.isCoprime_iff_codisjoint {R : Type u} [CommSemiring R] {I J : Ideal R} : IsCoprime I J ↔ Codisjoint I J

theorem Ideal.isCoprime_of_isMaximal {R : Type u} [CommSemiring R] {I J : Ideal R} [I.IsMaximal] [J.IsMaximal] (ne : I ≠ J) : IsCoprime I J

theorem Ideal.isCoprime_iff_add {R : Type u} [CommSemiring R] {I J : Ideal R} : IsCoprime I J ↔ I + J = 1

theorem Ideal.isCoprime_iff_exists {R : Type u} [CommSemiring R] {I J : Ideal R} : IsCoprime I J ↔ ∃ i ∈ I, ∃ j ∈ J, i + j = 1

theorem Ideal.isCoprime_iff_sup_eq {R : Type u} [CommSemiring R] {I J : Ideal R} : IsCoprime I J ↔ I ⊔ J = ⊤

theorem Ideal.coprime_of_no_prime_ge {R : Type u} [CommSemiring R] {I J : Ideal R} (h : ∀ (P : Ideal R), I ≤ P → J ≤ P → ¬P.IsPrime) : IsCoprime I J

theorem Ideal.isCoprime_tfae {R : Type u} [CommSemiring R] {I J : Ideal R} : [IsCoprime I J, Codisjoint I J, I + J = 1, ∃ i ∈ I, ∃ j ∈ J, i + j = 1, I ⊔ J = ⊤].TFAE

theorem IsCoprime.codisjoint {R : Type u} [CommSemiring R] {I J : Ideal R} (h : IsCoprime I J) : Codisjoint I J

theorem IsCoprime.add_eq {R : Type u} [CommSemiring R] {I J : Ideal R} (h : IsCoprime I J) : I + J = 1

theorem IsCoprime.exists {R : Type u} [CommSemiring R] {I J : Ideal R} (h : IsCoprime I J) : ∃ i ∈ I, ∃ j ∈ J, i + j = 1

theorem IsCoprime.sup_eq {R : Type u} [CommSemiring R] {I J : Ideal R} (h : IsCoprime I J) : I ⊔ J = ⊤

theorem Ideal.inf_eq_mul_of_isCoprime {R : Type u} [CommSemiring R] {I J : Ideal R} (coprime : IsCoprime I J) : I ⊓ J = I * J

theorem Ideal.isCoprime_span_singleton_iff {R : Type u} [CommSemiring R] (x y : R) : IsCoprime (span {x}) (span {y}) ↔ IsCoprime x y

theorem Ideal.isCoprime_biInf {R : Type u} {ι : Type u_1} [CommSemiring R] {I : Ideal R} {J : ι → Ideal R} {s : Finset ι} (hf : ∀ j ∈ s, IsCoprime I (J j)) : IsCoprime I (⨅ j ∈ s, J j)

def Ideal.radical {R : Type u} [CommSemiring R] (I : Ideal R) : Ideal R

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

theorem Ideal.mem_radical_iff {R : Type u} [CommSemiring R] {I : Ideal R} {r : R} : r ∈ I.radical ↔ ∃ (n : ℕ), r ^ n ∈ I

def Ideal.IsRadical {R : Type u} [CommSemiring R] (I : Ideal R) : Prop

An ideal is radical if it contains its radical.

theorem Ideal.le_radical {R : Type u} [CommSemiring R] {I : Ideal R} : I ≤ I.radical

theorem Ideal.radical_eq_iff {R : Type u} [CommSemiring R] {I : Ideal R} : I.radical = I ↔ I.IsRadical

An ideal is radical iff it is equal to its radical.

theorem Ideal.IsRadical.radical {R : Type u} [CommSemiring R] {I : Ideal R} : I.IsRadical → I.radical = I

Alias of the reverse direction of Ideal.radical_eq_iff.

---

An ideal is radical iff it is equal to its radical.

theorem Ideal.isRadical_iff_pow_one_lt {R : Type u} [CommSemiring R] {I : Ideal R} (k : ℕ) (hk : 1 < k) : I.IsRadical ↔ ∀ (r : R), r ^ k ∈ I → r ∈ I

theorem Ideal.radical_top (R : Type u) [CommSemiring R] : ⊤.radical = ⊤

theorem Ideal.radical_mono {R : Type u} [CommSemiring R] {I J : Ideal R} (H : I ≤ J) : I.radical ≤ J.radical

theorem Ideal.radical_isRadical {R : Type u} [CommSemiring R] (I : Ideal R) : I.radical.IsRadical

@[simp]

theorem Ideal.radical_idem {R : Type u} [CommSemiring R] (I : Ideal R) : I.radical.radical = I.radical

theorem Ideal.IsRadical.radical_le_iff {R : Type u} [CommSemiring R] {I J : Ideal R} (hJ : J.IsRadical) : I.radical ≤ J ↔ I ≤ J

theorem Ideal.radical_le_radical_iff {R : Type u} [CommSemiring R] {I J : Ideal R} : I.radical ≤ J.radical ↔ I ≤ J.radical

@[simp]

theorem Ideal.radical_eq_top {R : Type u} [CommSemiring R] {I : Ideal R} : I.radical = ⊤ ↔ I = ⊤

theorem Ideal.IsPrime.isRadical {R : Type u} [CommSemiring R] {I : Ideal R} (H : I.IsPrime) : I.IsRadical

theorem Ideal.IsPrime.radical {R : Type u} [CommSemiring R] {I : Ideal R} (H : I.IsPrime) : I.radical = I

theorem Ideal.mem_radical_of_pow_mem {R : Type u} [CommSemiring R] {I : Ideal R} {x : R} {m : ℕ} (hx : x ^ m ∈ I.radical) : x ∈ I.radical

theorem Ideal.disjoint_powers_iff_notMem {R : Type u} [CommSemiring R] {I : Ideal R} (y : R) (hI : I.IsRadical) : Disjoint ↑(Submonoid.powers y) ↑I ↔ y ∉ I.toAddSubmonoid

theorem Ideal.radical_sup {R : Type u} [CommSemiring R] (I J : Ideal R) : (I ⊔ J).radical = (I.radical ⊔ J.radical).radical

theorem Ideal.radical_inf {R : Type u} [CommSemiring R] (I J : Ideal R) : (I ⊓ J).radical = I.radical ⊓ J.radical

theorem Ideal.IsRadical.inf {R : Type u} [CommSemiring R] {I J : Ideal R} (hI : I.IsRadical) (hJ : J.IsRadical) : (I ⊓ J).IsRadical

theorem Ideal.isRadical_bot_iff {R : Type u} [CommSemiring R] : ⊥.IsRadical ↔ IsReduced R

theorem Ideal.isRadical_bot {R : Type u} [CommSemiring R] [IsReduced R] : ⊥.IsRadical

def Ideal.radicalInfTopHom {R : Type u} [CommSemiring R] : InfTopHom (Ideal R) (Ideal R)

Ideal.radical as an InfTopHom, bundling in that it distributes over inf.

@[simp]

theorem Ideal.radicalInfTopHom_apply {R : Type u} [CommSemiring R] (I : Ideal R) : radicalInfTopHom I = I.radical

theorem Ideal.radical_finset_inf {R : Type u} [CommSemiring R] {ι : Type u_2} {s : Finset ι} {f : ι → Ideal R} {i : ι} (hi : i ∈ s) (hs : ∀ ⦃y : ι⦄, y ∈ s → (f y).radical = (f i).radical) : (s.inf f).radical = (f i).radical

theorem Ideal.radical_iInf_le {R : Type u} [CommSemiring R] {ι : Sort u_2} (I : ι → Ideal R) : (⨅ (i : ι), I i).radical ≤ ⨅ (i : ι), (I i).radical

The reverse inclusion does not hold for e.g. I := fun n : ℕ ↦ Ideal.span {(2 ^ n : ℤ)}.

theorem Ideal.isRadical_iInf {R : Type u} [CommSemiring R] {ι : Sort u_2} (I : ι → Ideal R) (hI : ∀ (i : ι), (I i).IsRadical) : (⨅ (i : ι), I i).IsRadical

theorem Ideal.radical_mul {R : Type u} [CommSemiring R] (I J : Ideal R) : (I * J).radical = I.radical ⊓ J.radical

theorem Ideal.IsPrime.radical_le_iff {R : Type u} [CommSemiring R] {I J : Ideal R} (hJ : J.IsPrime) : I.radical ≤ J ↔ I ≤ J

theorem Ideal.radical_eq_sInf {R : Type u} [CommSemiring R] (I : Ideal R) : I.radical = sInf {J : Ideal R | I ≤ J ∧ J.IsPrime}

theorem Ideal.isRadical_bot_of_noZeroDivisors {R : Type u_2} [CommSemiring R] [NoZeroDivisors R] : ⊥.IsRadical

@[simp]

theorem Ideal.radical_bot_of_noZeroDivisors {R : Type u} [CommSemiring R] [NoZeroDivisors R] : ⊥.radical = ⊥

instance Ideal.instIdemCommSemiring {R : Type u} [CommSemiring R] : IdemCommSemiring (Ideal R)

theorem Ideal.radical_pow {R : Type u} [CommSemiring R] (I : Ideal R) {n : ℕ} : n ≠ 0 → (I ^ n).radical = I.radical

theorem Ideal.IsPrime.mul_le {R : Type u} [CommSemiring R] {I J P : Ideal R} (hp : P.IsPrime) : I * J ≤ P ↔ I ≤ P ∨ J ≤ P

theorem Ideal.IsPrime.inf_le {R : Type u} [CommSemiring R] {I J P : Ideal R} (hp : P.IsPrime) : I ⊓ J ≤ P ↔ I ≤ P ∨ J ≤ P

theorem Ideal.IsPrime.multiset_prod_le {R : Type u} [CommSemiring R] {s : Multiset (Ideal R)} {P : Ideal R} (hp : P.IsPrime) : s.prod ≤ P ↔ ∃ I ∈ s, I ≤ P

theorem Ideal.IsPrime.multiset_prod_map_le {R : Type u} {ι : Type u_1} [CommSemiring R] {s : Multiset ι} (f : ι → Ideal R) {P : Ideal R} (hp : P.IsPrime) : (Multiset.map f s).prod ≤ P ↔ ∃ i ∈ s, f i ≤ P

theorem Ideal.IsPrime.multiset_prod_mem_iff_exists_mem {R : Type u} [CommSemiring R] {I : Ideal R} (hI : I.IsPrime) (s : Multiset R) : s.prod ∈ I ↔ ∃ p ∈ s, p ∈ I

theorem Ideal.IsPrime.pow_le_iff {R : Type u} [CommSemiring R] {I P : Ideal R} [hP : P.IsPrime] {n : ℕ} (hn : n ≠ 0) : I ^ n ≤ P ↔ I ≤ P

theorem Ideal.IsPrime.le_of_pow_le {R : Type u} [CommSemiring R] {I P : Ideal R} [hP : P.IsPrime] {n : ℕ} (h : I ^ n ≤ P) : I ≤ P

theorem Ideal.IsPrime.prod_le {R : Type u} {ι : Type u_1} [CommSemiring R] {s : Finset ι} {f : ι → Ideal R} {P : Ideal R} (hp : P.IsPrime) : s.prod f ≤ P ↔ ∃ i ∈ s, f i ≤ P

theorem Ideal.IsPrime.prod_mem_iff {R : Type u} {ι : Type u_1} [CommSemiring R] {s : Finset ι} {x : ι → R} {p : Ideal R} [hp : p.IsPrime] : ∏ i ∈ s, x i ∈ p ↔ ∃ i ∈ s, x i ∈ p

The product of a finite number of elements in the commutative semiring R lies in the prime ideal p if and only if at least one of those elements is in p.

theorem Ideal.IsPrime.prod_mem_iff_exists_mem {R : Type u} [CommSemiring R] {I : Ideal R} (hI : I.IsPrime) (s : Finset R) : ∏ x ∈ s, x ∈ I ↔ ∃ p ∈ s, p ∈ I

theorem Ideal.IsPrime.inf_le' {R : Type u} {ι : Type u_1} [CommSemiring R] {s : Finset ι} {f : ι → Ideal R} {P : Ideal R} (hp : P.IsPrime) : s.inf f ≤ P ↔ ∃ i ∈ s, f i ≤ P

theorem Ideal.eq_inf_of_isPrime_inf {R : Type u} {ι : Type u_1} [CommSemiring R] {s : Finset ι} {f : ι → Ideal R} (hp : (s.inf f).IsPrime) : ∃ i ∈ s, f i = s.inf f

theorem Ideal.IsPrime.notMem_of_isCoprime_of_mem {R : Type u} [CommSemiring R] {I : Ideal R} [I.IsPrime] {x y : R} (h : IsCoprime x y) (hx : x ∈ I) : y ∉ I

theorem Ideal.subset_union {R : Type u} [Ring R] {I J K : Ideal R} : ↑I ⊆ ↑J ∪ ↑K ↔ I ≤ J ∨ I ≤ K

theorem Ideal.subset_union_prime' {ι : Type u_1} {R : Type u} [CommRing R] {s : Finset ι} {f : ι → Ideal R} {a b : ι} (hp : ∀ i ∈ s, (f i).IsPrime) {I : Ideal R} : ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ i ∈ ↑s, ↑(f i) ↔ I ≤ f a ∨ I ≤ f b ∨ ∃ i ∈ s, I ≤ f i

theorem Ideal.subset_union_prime {ι : Type u_1} {R : Type u} [CommRing R] {s : Finset ι} {f : ι → Ideal R} (a b : ι) (hp : ∀ i ∈ s, i ≠ a → i ≠ b → (f i).IsPrime) {I : Ideal R} : ↑I ⊆ ⋃ i ∈ ↑s, ↑(f i) ↔ ∃ i ∈ s, I ≤ f i

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

theorem Ideal.subset_union_prime_finite {R : Type u_2} {ι : Type u_3} [CommRing R] {s : Set ι} (hs : s.Finite) {f : ι → Ideal R} (a b : ι) (hp : ∀ i ∈ s, i ≠ a → i ≠ b → (f i).IsPrime) {I : Ideal R} : ↑I ⊆ ⋃ i ∈ s, ↑(f i) ↔ ∃ i ∈ s, I ≤ f i

Another version of prime avoidance using Set.Finite instead of Finset.

theorem Ideal.le_of_dvd {R : Type u} [CommSemiring R] {I J : Ideal R} : I ∣ J → J ≤ I

If I divides J, then I contains J.

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

@[simp]

theorem Ideal.dvd_bot {R : Type u} [CommSemiring R] {I : Ideal R} : I ∣ ⊥

@[simp]

theorem Ideal.isUnit_iff {R : Type u} [CommSemiring R] {I : Ideal R} : IsUnit I ↔ I = ⊤

See also isUnit_iff_eq_one.

instance Ideal.uniqueUnits {R : Type u} [CommSemiring R] : Unique (Ideal R)ˣ

noncomputable def Ideal.finsuppTotal (ι : Type u_1) (M : Type u_2) [AddCommGroup M] {R : Type u_3} [CommRing R] [Module R M] (I : Ideal R) (v : ι → M) : (ι →₀ ↥I) →ₗ[R] M

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

theorem Ideal.finsuppTotal_apply {ι : Type u_1} {M : Type u_2} [AddCommGroup M] {R : Type u_3} [CommRing R] [Module R M] (I : Ideal R) {v : ι → M} (f : ι →₀ ↥I) : (finsuppTotal ι M I v) f = f.sum fun (i : ι) (x : ↥I) => ↑x • v i

theorem Ideal.finsuppTotal_apply_eq_of_fintype {ι : Type u_1} {M : Type u_2} [AddCommGroup M] {R : Type u_3} [CommRing R] [Module R M] (I : Ideal R) {v : ι → M} [Fintype ι] (f : ι →₀ ↥I) : (finsuppTotal ι M I v) f = ∑ i : ι, ↑(f i) • v i

theorem Ideal.range_finsuppTotal {ι : Type u_1} {M : Type u_2} [AddCommGroup M] {R : Type u_3} [CommRing R] [Module R M] (I : Ideal R) {v : ι → M} : (finsuppTotal ι M I v).range = I • Submodule.span R (Set.range v)

theorem Finsupp.mem_ideal_span_range_iff_exists_finsupp {α : Type u_1} {R : Type u_2} [Semiring R] {x : R} {v : α → R} : x ∈ Ideal.span (Set.range v) ↔ ∃ (c : α →₀ R), (c.sum fun (i : α) (a : R) => a * v i) = x

theorem Ideal.mem_span_range_iff_exists_fun {α : Type u_1} {R : Type u_2} [Semiring R] [Fintype α] {x : R} {v : α → R} : x ∈ span (Set.range v) ↔ ∃ (c : α → R), ∑ i : α, c i * v i = x

An element x lies in the span of v iff it can be written as sum ∑ cᵢ • vᵢ = x.

theorem Associates.mk_ne_zero' {R : Type u_1} [CommSemiring R] {r : R} : Associates.mk (Ideal.span {r}) ≠ 0 ↔ r ≠ 0

theorem Ideal.span_singleton_nonZeroDivisors {R : Type u_1} [CommSemiring R] [NoZeroDivisors R] {r : R} : span {r} ∈ nonZeroDivisors (Ideal R) ↔ r ∈ nonZeroDivisors R

theorem Ideal.primeCompl_le_nonZeroDivisors {R : Type u_1} [CommSemiring R] [NoZeroDivisors R] (P : Ideal R) [P.IsPrime] : P.primeCompl ≤ nonZeroDivisors R

instance Submodule.moduleSubmodule {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] : Module (Ideal R) (Submodule R M)

theorem Submodule.span_smul_eq {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] (s : Set R) (N : Submodule R M) : Ideal.span s • N = s • N

@[simp]

theorem Submodule.set_smul_top_eq_span {R : Type u} [CommSemiring R] (s : Set R) : s • ⊤ = Ideal.span s

theorem Submodule.smul_le_span {R : Type u} [CommSemiring R] (s : Set R) (I : Ideal R) : s • I ≤ Ideal.span s

instance Submodule.algebraIdeal {R : Type u} [CommSemiring R] {A : Type u_1} [Semiring A] [Algebra R A] : Algebra (Ideal R) (Submodule R A)

def Submodule.mapAlgHom {R : Type u} [CommSemiring R] {A : Type u_1} {B : Type u_2} [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) : Submodule R A →ₐ[Ideal R] Submodule R B

Submonoid.map as an AlgHom, when applied to an AlgHom.

@[simp]

theorem Submodule.coe_mapAlgHom_apply {R : Type u} [CommSemiring R] {A : Type u_1} {B : Type u_2} [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) (p : Submodule R A) : ↑((mapAlgHom f) p) = ⇑f '' ↑p

def Submodule.mapAlgEquiv {R : Type u} [CommSemiring R] {A : Type u_1} {B : Type u_2} [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A ≃ₐ[R] B) : Submodule R A ≃ₐ[Ideal R] Submodule R B

Submonoid.map as an AlgEquiv, when applied to an AlgEquiv.

@[simp]

theorem Submodule.coe_mapAlgEquiv_symm_apply {R : Type u} [CommSemiring R] {A : Type u_1} {B : Type u_2} [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A ≃ₐ[R] B) (a : Submodule R B) : ↑((mapAlgEquiv f).symm a) = (fun (a : B) => f.symm a) '' ↑a

@[simp]

theorem Submodule.coe_mapAlgEquiv_apply {R : Type u} [CommSemiring R] {A : Type u_1} {B : Type u_2} [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A ≃ₐ[R] B) (a✝ : Submodule R A) : ↑((mapAlgEquiv f) a✝) = (fun (a : A) => f a) '' ↑a✝

instance instNonUnitalSubsemiringClassIdeal {R : Type u_1} [Semiring R] : NonUnitalSubsemiringClass (Ideal R) R

instance instNonUnitalSubringClassIdeal {R : Type u_1} [Ring R] : NonUnitalSubringClass (Ideal R) R

theorem Ideal.exists_subset_radical_span_sup_of_subset_radical_sup {R : Type u_1} [CommSemiring R] (s : Set R) (I J : Ideal R) (hs : s ⊆ ↑(I ⊔ J).radical) : ∃ (t : ↑s → R), Set.range t ⊆ ↑I ∧ s ⊆ ↑(span (Set.range t) ⊔ J).radical