More operations on modules and ideals

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

Equations

• Submodule.hasSMul' = { smul := Submodule.map₂ (LinearMap.lsmul R M) }

theorem Ideal.smul_eq_mul {R : Type u} [CommSemiring R] (I : Ideal R) (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.

def Module.annihilator (R : Type u) (M : Type v) [CommSemiring R] [AddCommMonoid M] [Module R M] : Ideal R

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

Equations

• Module.annihilator R M = LinearMap.ker (LinearMap.lsmul R M)

theorem Module.mem_annihilator {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] {r : R} : r ∈ Module.annihilator R M ↔ ∀ (m : M), r • m = 0

theorem LinearMap.annihilator_le_of_injective {R : Type u} {M : Type v} {M' : Type u_1} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module R M'] (f : M →ₗ[R] M') (hf : Function.Injective ⇑f) : Module.annihilator R M' ≤ Module.annihilator R M

theorem LinearMap.annihilator_le_of_surjective {R : Type u} {M : Type v} {M' : Type u_1} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module R M'] (f : M →ₗ[R] M') (hf : Function.Surjective ⇑f) : Module.annihilator R M ≤ Module.annihilator R M'

theorem LinearEquiv.annihilator_eq {R : Type u} {M : Type v} {M' : Type u_1} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module R M'] (e : M ≃ₗ[R] M') : Module.annihilator R M = Module.annihilator R M'

@[inline, reducible]

abbrev Submodule.annihilator {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] (N : Submodule R M) : Ideal R

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

Equations

• Submodule.annihilator N = Module.annihilator R ↥N

theorem Submodule.annihilator_top {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] : Submodule.annihilator ⊤ = Module.annihilator R M

theorem Submodule.mem_annihilator {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] {N : Submodule R M} {r : R} : r ∈ Submodule.annihilator N ↔ ∀ n ∈ N, r • n = 0

theorem Submodule.mem_annihilator' {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] {N : Submodule R M} {r : R} : r ∈ Submodule.annihilator N ↔ N ≤ Submodule.comap (r • LinearMap.id) ⊥

theorem Submodule.mem_annihilator_span {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] (s : Set M) (r : R) : r ∈ Submodule.annihilator (Submodule.span R s) ↔ ∀ (n : ↑s), r • ↑n = 0

theorem Submodule.mem_annihilator_span_singleton {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] (g : M) (r : R) : r ∈ Submodule.annihilator (Submodule.span R {g}) ↔ r • g = 0

theorem Submodule.annihilator_bot {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] : Submodule.annihilator ⊥ = ⊤

theorem Submodule.annihilator_eq_top_iff {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] {N : Submodule R M} : Submodule.annihilator N = ⊤ ↔ N = ⊥

theorem Submodule.annihilator_mono {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] {N : Submodule R M} {P : Submodule R M} (h : N ≤ P) : Submodule.annihilator P ≤ Submodule.annihilator N

theorem Submodule.annihilator_iSup {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] (ι : Sort w) (f : ι → Submodule R M) : Submodule.annihilator (⨆ (i : ι), f i) = ⨅ (i : ι), Submodule.annihilator (f i)

theorem Submodule.smul_mem_smul {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] {I : Ideal R} {N : Submodule R 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} [CommSemiring R] [AddCommMonoid M] [Module R M] {I : Ideal R} {N : Submodule R M} {P : Submodule R M} : I • N ≤ P ↔ ∀ r ∈ I, ∀ n ∈ N, r • n ∈ P

@[simp]

theorem Submodule.coe_set_smul {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] {I : Ideal R} {N : Submodule R M} : ↑I • N = I • N

theorem Submodule.smul_induction_on {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] {I : Ideal R} {N : Submodule R M} {p : M → Prop} {x : M} (H : x ∈ I • N) (smul : ∀ r ∈ I, ∀ n ∈ N, p (r • n)) (add : ∀ (x y : M), p x → p y → p (x + y)) : p x

theorem Submodule.smul_induction_on' {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] {I : Ideal R} {N : Submodule R M} {x : M} (hx : x ∈ I • N) {p : (x : M) → x ∈ I • N → Prop} (smul : ∀ (r : R) (hr : r ∈ I) (n : M) (hn : n ∈ N), p (r • n) ⋯) (add : ∀ (x : M) (hx : x ∈ I • N) (y : M) (hy : y ∈ I • N), p x hx → p y hy → p (x + y) ⋯) : p x hx

Dependent version of Submodule.smul_induction_on.

theorem Submodule.mem_smul_span_singleton {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] {I : Ideal R} {m : M} {x : M} : x ∈ I • Submodule.span R {m} ↔ ∃ y ∈ I, y • m = x

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

theorem Submodule.smul_mono {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] {I : Ideal R} {J : Ideal R} {N : Submodule R M} {P : Submodule R M} (hij : I ≤ J) (hnp : N ≤ P) : I • N ≤ J • P

theorem Submodule.smul_mono_left {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] {I : Ideal R} {J : Ideal R} {N : Submodule R M} (h : I ≤ J) : I • N ≤ J • N

instance Submodule.instCovariantClassIdealToSemiringSubmoduleHSMulLeToLEToPreorderToPartialOrderInstOmegaCompletePartialOrderCompleteLattice {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] : CovariantClass (Ideal R) (Submodule R M) HSMul.hSMul LE.le

Equations

• ⋯ = ⋯

@[deprecated smul_mono_right]

theorem Submodule.smul_mono_right {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] {I : Ideal R} {N : Submodule R M} {P : Submodule R M} (h : N ≤ P) : I • N ≤ I • P

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

@[simp]

theorem Submodule.annihilator_smul {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] (N : Submodule R M) : Submodule.annihilator N • N = ⊥

@[simp]

theorem Submodule.annihilator_mul {R : Type u} [CommSemiring R] (I : Ideal R) : Submodule.annihilator I * I = ⊥

@[simp]

theorem Submodule.mul_annihilator {R : Type u} [CommSemiring R] (I : Ideal R) : I * Submodule.annihilator I = ⊥

@[simp]

theorem Submodule.smul_bot {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] (I : Ideal R) : I • ⊥ = ⊥

@[simp]

theorem Submodule.bot_smul {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] (N : Submodule R M) : ⊥ • N = ⊥

@[simp]

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

theorem Submodule.smul_sup {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] (I : Ideal R) (N : Submodule R M) (P : Submodule R M) : I • (N ⊔ P) = I • N ⊔ I • P

theorem Submodule.sup_smul {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] (I : Ideal R) (J : Ideal R) (N : Submodule R M) : (I ⊔ J) • N = I • N ⊔ J • N

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

@[deprecated smul_inf_le]

theorem Submodule.smul_inf_le {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] (I : Ideal R) (M₁ : Submodule R M) (M₂ : Submodule R M) : I • (M₁ ⊓ M₂) ≤ I • M₁ ⊓ I • M₂

theorem Submodule.smul_iSup {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] {ι : Sort u_4} {I : Ideal R} {t : ι → Submodule R M} : I • iSup t = ⨆ (i : ι), I • t i

@[deprecated smul_iInf_le]

theorem Submodule.smul_iInf_le {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] {ι : Sort u_4} {I : Ideal R} {t : ι → Submodule R M} : I • iInf t ≤ ⨅ (i : ι), I • t i

theorem Submodule.span_smul_span {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] (S : Set R) (T : Set M) : Ideal.span S • Submodule.span R T = Submodule.span R (⋃ s ∈ S, ⋃ t ∈ T, {s • t})

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_top_of_smul_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), ↑r • x ∈ M') : x ∈ M'

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.

theorem Submodule.map_smul'' {R : Type u} {M : Type v} [CommSemiring 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') : Submodule.map f (I • N) = I • Submodule.map f N

theorem Submodule.mem_smul_span {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] {I : Ideal R} {s : Set M} {x : M} : x ∈ I • Submodule.span R s ↔ x ∈ Submodule.span R (⋃ a ∈ I, ⋃ b ∈ s, {a • b})

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

theorem Submodule.mem_smul_top_iff {R : Type u} {M : Type v} [CommSemiring 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} [CommSemiring 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 • Submodule.comap f S ≤ Submodule.comap f (I • S)

@[simp]

theorem Ideal.add_eq_sup {R : Type u} [Semiring R] {I : Ideal R} {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) : Finset.sum s f = Finset.sup s f

instance Ideal.instMulIdealToSemiring {R : Type u} [CommSemiring R] : Mul (Ideal R)

Equations

• Ideal.instMulIdealToSemiring = { mul := fun (x x_1 : Ideal R) => x • x_1 }

@[simp]

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

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

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

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

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

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) → (Finset.prod s fun (i : ι) => x i) ∈ Finset.prod s fun (i : ι) => I i

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

theorem Ideal.span_mul_span {R : Type u} [CommSemiring R] (S : Set R) (T : Set R) : Ideal.span S * Ideal.span T = Ideal.span (⋃ s ∈ S, ⋃ t ∈ T, {s * t})

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

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

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

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

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

theorem Ideal.le_span_singleton_mul_iff {R : Type u} [CommSemiring R] {x : R} {I : Ideal R} {J : Ideal R} : I ≤ Ideal.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 : Ideal R} {J : Ideal R} : Ideal.span {x} * I ≤ J ↔ ∀ z ∈ I, x * z ∈ J

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

theorem Ideal.span_singleton_mul_right_mono {R : Type u} [CommSemiring R] {I : Ideal R} {J : Ideal R} [IsDomain R] {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} [CommSemiring R] {I : Ideal R} {J : Ideal R} [IsDomain R] {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} [CommSemiring R] {I : Ideal R} {J : Ideal R} [IsDomain R] {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} [CommSemiring R] {I : Ideal R} {J : Ideal R} [IsDomain R] {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} [CommSemiring R] [IsDomain R] {x : R} (hx : x ≠ 0) : Function.Injective fun (x_1 : Ideal R) => Ideal.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 * Ideal.span {x}

theorem Ideal.eq_span_singleton_mul {R : Type u} [CommSemiring R] {x : R} (I : Ideal R) (J : Ideal R) : I = Ideal.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 : R} {y : R} (I : Ideal R) (J : Ideal R) : Ideal.span {x} * I = Ideal.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) : (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} [CommSemiring R] {ι : Type u_2} (s : Finset ι) (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} [CommSemiring R] (m : Multiset R) : Multiset.prod (Multiset.map (fun (x : R) => Ideal.span {x}) m) = Ideal.span {Multiset.prod m}

theorem Ideal.finset_inf_span_singleton {R : Type u} [CommSemiring R] {ι : Type u_2} (s : Finset ι) (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} [CommSemiring R] {ι : Type u_2} [Fintype ι] {I : ι → R} (hI : ∀ (i j : ι), i ≠ j → IsCoprime (I i) (I j)) : ⨅ (i : ι), Ideal.span {I i} = Ideal.span {Finset.prod Finset.univ fun (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 : ι) => Nat.Coprime (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} [CommSemiring R] (x : R) (y : R) : Ideal.span {x} ⊔ Ideal.span {y} = ⊤ ↔ IsCoprime x y

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

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

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

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

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

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

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

theorem Ideal.mul_sup_eq_of_coprime_right {R : Type u} [CommSemiring R] {I : Ideal R} {J : Ideal R} {K : Ideal R} (h : K ⊔ J = ⊤) : I * K ⊔ 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 ⊔ Finset.prod s fun (i : ι) => J i) = ⊤

theorem Ideal.sup_iInf_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.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 = ⊤) : (Finset.prod s fun (i : ι) => J i) ⊔ I = ⊤

theorem Ideal.iInf_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 = ⊤

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

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

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

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

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

@[simp]

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

@[simp]

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

theorem Ideal.mul_mono {R : Type u} [CommSemiring R] {I : Ideal R} {J : Ideal R} {K : Ideal R} {L : Ideal R} (hik : I ≤ K) (hjl : J ≤ L) : I * J ≤ K * L

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

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

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

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

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

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

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

@[simp]

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

instance Ideal.instNoZeroDivisorsIdealToSemiringInstMulIdealToSemiringPointwiseZeroToAddCommMonoidToNonUnitalNonAssocSemiringToNonAssocSemiringToModule {R : Type u_2} [CommSemiring R] [NoZeroDivisors R] : NoZeroDivisors (Ideal R)

Equations

• ⋯ = ⋯

instance Ideal.instNoZeroSMulDivisorsSubtypeMemIdealToSemiringToCommSemiringInstMembershipSetLikeToAddCommMonoidToNonUnitalNonAssocSemiringToNonAssocSemiringToModuleToZeroToCommMonoidWithZeroZeroSmulToSMulRight {R : Type u_2} [CommSemiring R] {S : Type u_3} [CommRing S] [Algebra R S] [NoZeroSMulDivisors R S] {I : Ideal S} : NoZeroSMulDivisors R ↥I

Equations

• ⋯ = ⋯

@[simp]

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

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

@[deprecated Ideal.multiset_prod_eq_bot]

theorem Ideal.prod_eq_bot {R : Type u_2} [CommRing R] [IsDomain R] {s : Multiset (Ideal R)} : Multiset.prod s = ⊥ ↔ ∃ 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} [CommSemiring R] (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}

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

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

theorem Ideal.isCoprime_iff_exists {R : Type u} [CommSemiring R] {I : Ideal R} {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 : Ideal R} {J : Ideal R} : IsCoprime I J ↔ I ⊔ J = ⊤

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

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

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

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

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

theorem Ideal.isCoprime_span_singleton_iff {R : Type u} [CommSemiring R] (x : R) (y : R) : IsCoprime (Ideal.span {x}) (Ideal.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.

Equations

• Ideal.radical I = { toAddSubmonoid := { toAddSubsemigroup := { carrier := {r : R | ∃ (n : ℕ), r ^ n ∈ I}, add_mem' := ⋯ }, zero_mem' := ⋯ }, smul_mem' := ⋯ }

theorem Ideal.mem_radical_iff {R : Type u} [CommSemiring R] {I : Ideal R} {r : R} : r ∈ Ideal.radical I ↔ ∃ (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.

Equations

• Ideal.IsRadical I = (Ideal.radical I ≤ I)

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

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

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

theorem Ideal.IsRadical.radical {R : Type u} [CommSemiring R] {I : Ideal R} : Ideal.IsRadical I → Ideal.radical I = 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) : Ideal.IsRadical I ↔ ∀ (r : R), r ^ k ∈ I → r ∈ I

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

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

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

@[simp]

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

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

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

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

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

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

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

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

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

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

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 : ι), Ideal.IsRadical (I i)) : Ideal.IsRadical (⨅ (i : ι), I i)

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

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

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

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

@[simp]

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

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

Equations

• Ideal.instIdemCommSemiringIdealToSemiring = inferInstance

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

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

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

theorem Ideal.IsPrime.inf_le {R : Type u} [CommSemiring R] {I : Ideal R} {J : Ideal R} {P : Ideal R} (hp : Ideal.IsPrime P) : 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 : Ideal.IsPrime P) : Multiset.prod s ≤ 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 : Ideal.IsPrime P) : Multiset.prod (Multiset.map f s) ≤ P ↔ ∃ i ∈ s, f i ≤ P

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

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

theorem Ideal.IsPrime.prod_mem_iff_exists_mem {R : Type u} [CommSemiring R] {I : Ideal R} (hI : Ideal.IsPrime I) (s : Finset R) : (Finset.prod s fun (x : R) => 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 : Ideal.IsPrime P) : Finset.inf s f ≤ P ↔ ∃ i ∈ s, f i ≤ P

theorem Ideal.subset_union {R : Type u} [Ring R] {I : Ideal R} {J : Ideal R} {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, Ideal.IsPrime (f i)) {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 → Ideal.IsPrime (f i)) {I : Ideal R} : ↑I ⊆ ⋃ i ∈ ↑s, ↑(f 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} [CommSemiring R] {I : Ideal R} {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.isUnit_iff {R : Type u} [CommSemiring R] {I : Ideal R} : IsUnit I ↔ I = ⊤

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

Equations

• Ideal.uniqueUnits = { toInhabited := { default := 1 }, uniq := ⋯ }

def Ideal.map {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] (f : F) (I : Ideal R) : Ideal S

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

Equations

• Ideal.map f I = Ideal.span (⇑f '' ↑I)

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

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

Equations

• Ideal.comap f I = { toAddSubmonoid := { toAddSubsemigroup := { carrier := ⇑f ⁻¹' ↑I, add_mem' := ⋯ }, zero_mem' := ⋯ }, smul_mem' := ⋯ }

theorem Ideal.coe_comap {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] [rc : RingHomClass F R S] (f : F) (I : Ideal S) : ↑(Ideal.comap f I) = ⇑f ⁻¹' ↑I

theorem Ideal.map_mono {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] {f : F} {I : Ideal R} {J : Ideal R} (h : I ≤ J) : Ideal.map f I ≤ Ideal.map f J

theorem Ideal.mem_map_of_mem {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] (f : F) {I : Ideal R} {x : R} (h : x ∈ I) : f x ∈ Ideal.map f I

theorem Ideal.apply_coe_mem_map {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] (f : F) (I : Ideal R) (x : ↥I) : f ↑x ∈ Ideal.map f I

theorem Ideal.map_le_iff_le_comap {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] [rc : RingHomClass F R S] {f : F} {I : Ideal R} {K : Ideal S} : Ideal.map f I ≤ K ↔ I ≤ Ideal.comap f K

@[simp]

theorem Ideal.mem_comap {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] [rc : RingHomClass F R S] {f : F} {K : Ideal S} {x : R} : x ∈ Ideal.comap f K ↔ f x ∈ K

theorem Ideal.comap_mono {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] [rc : RingHomClass F R S] {f : F} {K : Ideal S} {L : Ideal S} (h : K ≤ L) : Ideal.comap f K ≤ Ideal.comap f L

theorem Ideal.comap_ne_top {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] [rc : RingHomClass F R S] (f : F) {K : Ideal S} (hK : K ≠ ⊤) : Ideal.comap f K ≠ ⊤

theorem Ideal.map_le_comap_of_inv_on {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] (f : F) {G : Type u_2} [FunLike G S R] [rcg : RingHomClass G S R] (g : G) (I : Ideal R) (hf : Set.LeftInvOn ⇑g ⇑f ↑I) : Ideal.map f I ≤ Ideal.comap g I

theorem Ideal.comap_le_map_of_inv_on {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] [rc : RingHomClass F R S] (f : F) {G : Type u_2} [FunLike G S R] (g : G) (I : Ideal S) (hf : Set.LeftInvOn (⇑g) (⇑f) (⇑f ⁻¹' ↑I)) : Ideal.comap f I ≤ Ideal.map g I

theorem Ideal.map_le_comap_of_inverse {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] (f : F) {G : Type u_2} [FunLike G S R] [rcg : RingHomClass G S R] (g : G) (I : Ideal R) (h : Function.LeftInverse ⇑g ⇑f) : Ideal.map f I ≤ Ideal.comap g I

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} [Semiring R] [Semiring S] [FunLike F R S] [rc : RingHomClass F R S] (f : F) {G : Type u_2} [FunLike G S R] (g : G) (I : Ideal S) (h : Function.LeftInverse ⇑g ⇑f) : Ideal.comap f I ≤ Ideal.map g I

The Ideal version of Set.preimage_subset_image_of_inverse.

instance Ideal.IsPrime.comap {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] [rc : RingHomClass F R S] (f : F) {K : Ideal S} [hK : Ideal.IsPrime K] : Ideal.IsPrime (Ideal.comap f K)

Equations

• ⋯ = ⋯

theorem Ideal.map_top {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] [rc : RingHomClass F R S] (f : F) : Ideal.map f ⊤ = ⊤

theorem Ideal.gc_map_comap {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] [rc : RingHomClass F R S] (f : F) : GaloisConnection (Ideal.map f) (Ideal.comap f)

@[simp]

theorem Ideal.comap_id {R : Type u} [Semiring R] (I : Ideal R) : Ideal.comap (RingHom.id R) I = I

@[simp]

theorem Ideal.map_id {R : Type u} [Semiring R] (I : Ideal R) : Ideal.map (RingHom.id R) I = I

theorem Ideal.comap_comap {R : Type u} {S : Type v} [Semiring R] [Semiring S] {T : Type u_3} [Semiring T] {I : Ideal T} (f : R →+* S) (g : S →+* T) : Ideal.comap f (Ideal.comap g I) = Ideal.comap (RingHom.comp g f) I

theorem Ideal.map_map {R : Type u} {S : Type v} [Semiring R] [Semiring S] {T : Type u_3} [Semiring T] {I : Ideal R} (f : R →+* S) (g : S →+* T) : Ideal.map g (Ideal.map f I) = Ideal.map (RingHom.comp g f) I

theorem Ideal.map_span {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] [rc : RingHomClass F R S] (f : F) (s : Set R) : Ideal.map f (Ideal.span s) = Ideal.span (⇑f '' s)

theorem Ideal.map_le_of_le_comap {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] [rc : RingHomClass F R S] {f : F} {I : Ideal R} {K : Ideal S} : I ≤ Ideal.comap f K → Ideal.map f I ≤ K

theorem Ideal.le_comap_of_map_le {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] [rc : RingHomClass F R S] {f : F} {I : Ideal R} {K : Ideal S} : Ideal.map f I ≤ K → I ≤ Ideal.comap f K

theorem Ideal.le_comap_map {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] [rc : RingHomClass F R S] {f : F} {I : Ideal R} : I ≤ Ideal.comap f (Ideal.map f I)

theorem Ideal.map_comap_le {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] [rc : RingHomClass F R S] {f : F} {K : Ideal S} : Ideal.map f (Ideal.comap f K) ≤ K

@[simp]

theorem Ideal.comap_top {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] [rc : RingHomClass F R S] {f : F} : Ideal.comap f ⊤ = ⊤

@[simp]

theorem Ideal.comap_eq_top_iff {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] [rc : RingHomClass F R S] {f : F} {I : Ideal S} : Ideal.comap f I = ⊤ ↔ I = ⊤

@[simp]

theorem Ideal.map_bot {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] [rc : RingHomClass F R S] {f : F} : Ideal.map f ⊥ = ⊥

@[simp]

theorem Ideal.map_comap_map {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] [rc : RingHomClass F R S] (f : F) (I : Ideal R) : Ideal.map f (Ideal.comap f (Ideal.map f I)) = Ideal.map f I

@[simp]

theorem Ideal.comap_map_comap {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] [rc : RingHomClass F R S] (f : F) (K : Ideal S) : Ideal.comap f (Ideal.map f (Ideal.comap f K)) = Ideal.comap f K

theorem Ideal.map_sup {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] [rc : RingHomClass F R S] (f : F) (I : Ideal R) (J : Ideal R) : Ideal.map f (I ⊔ J) = Ideal.map f I ⊔ Ideal.map f J

theorem Ideal.comap_inf {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] [rc : RingHomClass F R S] (f : F) (K : Ideal S) (L : Ideal S) : Ideal.comap f (K ⊓ L) = Ideal.comap f K ⊓ Ideal.comap f L

theorem Ideal.map_iSup {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] [rc : RingHomClass F R S] (f : F) {ι : Sort u_3} (K : ι → Ideal R) : 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} [Semiring R] [Semiring S] [FunLike F R S] [rc : RingHomClass F R S] (f : F) {ι : Sort u_3} (K : ι → Ideal S) : 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} [Semiring R] [Semiring S] [FunLike F R S] [rc : RingHomClass F R S] (f : F) (s : Set (Ideal R)) : Ideal.map f (sSup s) = ⨆ I ∈ s, Ideal.map f I

theorem Ideal.comap_sInf {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] [rc : RingHomClass F R S] (f : F) (s : Set (Ideal S)) : Ideal.comap f (sInf s) = ⨅ I ∈ s, Ideal.comap f I

theorem Ideal.comap_sInf' {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] [rc : RingHomClass F R S] (f : F) (s : Set (Ideal S)) : Ideal.comap f (sInf s) = ⨅ I ∈ Ideal.comap f '' s, I

theorem Ideal.comap_isPrime {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] [rc : RingHomClass F R S] (f : F) (K : Ideal S) [H : Ideal.IsPrime K] : Ideal.IsPrime (Ideal.comap f K)

theorem Ideal.map_inf_le {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] [rc : RingHomClass F R S] (f : F) {I : Ideal R} {J : Ideal R} : Ideal.map f (I ⊓ J) ≤ Ideal.map f I ⊓ Ideal.map f J

theorem Ideal.le_comap_sup {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] [rc : RingHomClass F R S] (f : F) {K : Ideal S} {L : Ideal S} : Ideal.comap f K ⊔ Ideal.comap f L ≤ Ideal.comap f (K ⊔ L)

@[simp]

theorem Ideal.smul_top_eq_map {R : Type u_4} {S : Type u_5} [CommSemiring R] [CommSemiring S] [Algebra R S] (I : Ideal R) : I • ⊤ = Submodule.restrictScalars R (Ideal.map (algebraMap R S) I)

@[simp]

theorem Ideal.coe_restrictScalars {R : Type u_4} {S : Type u_5} [CommSemiring R] [Semiring S] [Algebra R S] (I : Ideal S) : ↑(Submodule.restrictScalars R I) = ↑I

@[simp]

theorem Ideal.restrictScalars_mul {R : Type u_4} {S : Type u_5} [CommSemiring R] [CommSemiring S] [Algebra R S] (I : Ideal S) (J : Ideal S) : Submodule.restrictScalars R (I * J) = Submodule.restrictScalars R I * Submodule.restrictScalars R 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} [Semiring R] [Semiring S] [FunLike F R S] [rc : RingHomClass F R S] (f : F) (hf : Function.Surjective ⇑f) (I : Ideal S) : Ideal.map f (Ideal.comap f I) = I

def Ideal.giMapComap {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] [rc : RingHomClass F R S] (f : F) (hf : Function.Surjective ⇑f) : GaloisInsertion (Ideal.map f) (Ideal.comap f)

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

Equations

• Ideal.giMapComap f hf = GaloisInsertion.monotoneIntro ⋯ ⋯ ⋯ ⋯

theorem Ideal.map_surjective_of_surjective {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] [rc : RingHomClass F R S] (f : F) (hf : Function.Surjective ⇑f) : Function.Surjective (Ideal.map f)

theorem Ideal.comap_injective_of_surjective {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] [rc : RingHomClass F R S] (f : F) (hf : Function.Surjective ⇑f) : Function.Injective (Ideal.comap f)

theorem Ideal.map_sup_comap_of_surjective {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] [rc : RingHomClass F R S] (f : F) (hf : Function.Surjective ⇑f) (I : Ideal S) (J : Ideal S) : Ideal.map f (Ideal.comap f I ⊔ Ideal.comap f J) = I ⊔ J

theorem Ideal.map_iSup_comap_of_surjective {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] [rc : RingHomClass F R S] (f : F) {ι : Sort u_3} (hf : Function.Surjective ⇑f) (K : ι → Ideal S) : 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} [Semiring R] [Semiring S] [FunLike F R S] [rc : RingHomClass F R S] (f : F) (hf : Function.Surjective ⇑f) (I : Ideal S) (J : Ideal S) : Ideal.map f (Ideal.comap f I ⊓ Ideal.comap f J) = I ⊓ J

theorem Ideal.map_iInf_comap_of_surjective {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] [rc : RingHomClass F R S] (f : F) {ι : Sort u_3} (hf : Function.Surjective ⇑f) (K : ι → Ideal S) : 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} [Semiring R] [Semiring S] [FunLike F R S] [rc : RingHomClass F R S] (f : F) (hf : Function.Surjective ⇑f) {I : Ideal R} {y : S} (H : y ∈ Ideal.map f I) : y ∈ ⇑f '' ↑I

theorem Ideal.mem_map_iff_of_surjective {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] [rc : RingHomClass F R S] (f : F) (hf : Function.Surjective ⇑f) {I : Ideal R} {y : S} : y ∈ Ideal.map f I ↔ ∃ x ∈ I, f x = y

theorem Ideal.le_map_of_comap_le_of_surjective {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] [rc : RingHomClass F R S] (f : F) {I : Ideal R} {K : Ideal S} (hf : Function.Surjective ⇑f) : Ideal.comap f K ≤ I → K ≤ Ideal.map f I

theorem Ideal.map_eq_submodule_map {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) [h : RingHomSurjective f] (I : Ideal R) : Ideal.map f I = Submodule.map (RingHom.toSemilinearMap f) I

theorem Ideal.comap_bot_le_of_injective {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] [rc : RingHomClass F R S] (f : F) {I : Ideal R} (hf : Function.Injective ⇑f) : Ideal.comap f ⊥ ≤ I

theorem Ideal.comap_bot_of_injective {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] [rc : RingHomClass F R S] (f : F) (hf : Function.Injective ⇑f) : Ideal.comap f ⊥ = ⊥

@[simp]

theorem Ideal.map_of_equiv {R : Type u} {S : Type v} [Semiring R] [Semiring S] (I : Ideal R) (f : R ≃+* S) : Ideal.map (↑(RingEquiv.symm f)) (Ideal.map (↑f) I) = I

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

@[simp]

theorem Ideal.comap_of_equiv {R : Type u} {S : Type v} [Semiring R] [Semiring S] (I : Ideal R) (f : R ≃+* S) : Ideal.comap (↑f) (Ideal.comap (↑(RingEquiv.symm f)) I) = I

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

theorem Ideal.map_comap_of_equiv {R : Type u} {S : Type v} [Semiring R] [Semiring S] (I : Ideal R) (f : R ≃+* S) : Ideal.map (↑f) I = Ideal.comap (RingEquiv.symm f) I

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

@[simp]

theorem Ideal.comap_symm {R : Type u} {S : Type v} [Semiring R] [Semiring S] (I : Ideal R) (f : R ≃+* S) : Ideal.comap (RingEquiv.symm f) I = Ideal.map f I

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

@[simp]

theorem Ideal.map_symm {R : Type u} {S : Type v} [Semiring R] [Semiring S] (I : Ideal S) (f : R ≃+* S) : Ideal.map (RingEquiv.symm f) I = Ideal.comap f I

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

theorem Ideal.comap_map_of_surjective {R : Type u} {S : Type v} {F : Type u_1} [Ring R] [Ring S] [FunLike F R S] [RingHomClass F R S] (f : F) (hf : Function.Surjective ⇑f) (I : Ideal R) : Ideal.comap f (Ideal.map f I) = I ⊔ Ideal.comap f ⊥

def Ideal.relIsoOfSurjective {R : Type u} {S : Type v} {F : Type u_1} [Ring R] [Ring S] [FunLike F R S] [RingHomClass F R S] (f : F) (hf : Function.Surjective ⇑f) : Ideal S ≃o { p : Ideal R // Ideal.comap f ⊥ ≤ p }

Correspondence theorem

Equations

• One or more equations did not get rendered due to their size.

def Ideal.orderEmbeddingOfSurjective {R : Type u} {S : Type v} {F : Type u_1} [Ring R] [Ring S] [FunLike F R S] [RingHomClass F R S] (f : F) (hf : Function.Surjective ⇑f) : Ideal S ↪o Ideal R

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

Equations

• One or more equations did not get rendered due to their size.

theorem Ideal.map_eq_top_or_isMaximal_of_surjective {R : Type u} {S : Type v} {F : Type u_1} [Ring R] [Ring S] [FunLike F R S] [RingHomClass F R S] (f : F) (hf : Function.Surjective ⇑f) {I : Ideal R} (H : Ideal.IsMaximal I) : Ideal.map f I = ⊤ ∨ Ideal.IsMaximal (Ideal.map f I)

theorem Ideal.comap_isMaximal_of_surjective {R : Type u} {S : Type v} {F : Type u_1} [Ring R] [Ring S] [FunLike F R S] [RingHomClass F R S] (f : F) (hf : Function.Surjective ⇑f) {K : Ideal S} [H : Ideal.IsMaximal K] : Ideal.IsMaximal (Ideal.comap f K)

theorem Ideal.comap_le_comap_iff_of_surjective {R : Type u} {S : Type v} {F : Type u_1} [Ring R] [Ring S] [FunLike F R S] [RingHomClass F R S] (f : F) (hf : Function.Surjective ⇑f) (I : Ideal S) (J : Ideal S) : Ideal.comap f I ≤ Ideal.comap f J ↔ I ≤ J

def Ideal.relIsoOfBijective {R : Type u} {S : Type v} {F : Type u_1} [Ring R] [Ring S] [FunLike F R S] [RingHomClass F R S] (f : F) (hf : Function.Bijective ⇑f) : Ideal S ≃o Ideal R

Special case of the correspondence theorem for isomorphic rings

Equations

• Ideal.relIsoOfBijective f hf = { toEquiv := { toFun := Ideal.comap f, invFun := Ideal.map f, left_inv := ⋯, right_inv := ⋯ }, map_rel_iff' := ⋯ }

theorem Ideal.comap_le_iff_le_map {R : Type u} {S : Type v} {F : Type u_1} [Ring R] [Ring S] [FunLike F R S] [RingHomClass F R S] (f : F) (hf : Function.Bijective ⇑f) {I : Ideal R} {K : Ideal S} : Ideal.comap f K ≤ I ↔ K ≤ Ideal.map f I

theorem Ideal.map.isMaximal {R : Type u} {S : Type v} {F : Type u_1} [Ring R] [Ring S] [FunLike F R S] [RingHomClass F R S] (f : F) (hf : Function.Bijective ⇑f) {I : Ideal R} (H : Ideal.IsMaximal I) : Ideal.IsMaximal (Ideal.map f I)

theorem Ideal.RingEquiv.bot_maximal_iff {R : Type u} {S : Type v} [Ring R] [Ring S] (e : R ≃+* S) : Ideal.IsMaximal ⊥ ↔ Ideal.IsMaximal ⊥

theorem Ideal.map_mul {R : Type u} {S : Type v} {F : Type u_1} [CommRing R] [CommRing S] [FunLike F R S] [rc : RingHomClass F R S] (f : F) (I : Ideal R) (J : Ideal R) : Ideal.map f (I * J) = Ideal.map f I * Ideal.map f J

@[simp]

theorem Ideal.mapHom_apply {R : Type u} {S : Type v} {F : Type u_1} [CommRing R] [CommRing S] [FunLike F R S] [rc : RingHomClass F R S] (f : F) (I : Ideal R) : (Ideal.mapHom f) I = Ideal.map f I

def Ideal.mapHom {R : Type u} {S : Type v} {F : Type u_1} [CommRing R] [CommRing S] [FunLike F R S] [rc : RingHomClass F R S] (f : F) : Ideal R →*₀ Ideal S

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

Equations

• Ideal.mapHom f = { toZeroHom := { toFun := Ideal.map f, map_zero' := ⋯ }, map_one' := ⋯, map_mul' := ⋯ }

theorem Ideal.map_pow {R : Type u} {S : Type v} {F : Type u_1} [CommRing R] [CommRing S] [FunLike F R S] [rc : RingHomClass F R S] (f : F) (I : Ideal R) (n : ℕ) : Ideal.map f (I ^ n) = Ideal.map f I ^ n

theorem Ideal.comap_radical {R : Type u} {S : Type v} {F : Type u_1} [CommRing R] [CommRing S] [FunLike F R S] [rc : RingHomClass F R S] (f : F) (K : Ideal S) : Ideal.comap f (Ideal.radical K) = Ideal.radical (Ideal.comap f K)

theorem Ideal.IsRadical.comap {R : Type u} {S : Type v} {F : Type u_1} [CommRing R] [CommRing S] [FunLike F R S] [rc : RingHomClass F R S] (f : F) {K : Ideal S} (hK : Ideal.IsRadical K) : Ideal.IsRadical (Ideal.comap f K)

theorem Ideal.map_radical_le {R : Type u} {S : Type v} {F : Type u_1} [CommRing R] [CommRing S] [FunLike F R S] [rc : RingHomClass F R S] (f : F) {I : Ideal R} : Ideal.map f (Ideal.radical I) ≤ Ideal.radical (Ideal.map f I)

theorem Ideal.le_comap_mul {R : Type u} {S : Type v} {F : Type u_1} [CommRing R] [CommRing S] [FunLike F R S] [rc : RingHomClass F R S] (f : F) {K : Ideal S} {L : Ideal S} : Ideal.comap f K * Ideal.comap f L ≤ Ideal.comap f (K * L)

theorem Ideal.le_comap_pow {R : Type u} {S : Type v} {F : Type u_1} [CommRing R] [CommRing S] [FunLike F R S] [rc : RingHomClass F R S] (f : F) {K : Ideal S} (n : ℕ) : Ideal.comap f K ^ n ≤ Ideal.comap f (K ^ n)

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.total that takes in vectors valued in I.

Equations

• Ideal.finsuppTotal ι M I v = Finsupp.total ι M R v ∘ₗ Finsupp.mapRange.linearMap (Submodule.subtype 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) : (Ideal.finsuppTotal ι M I v) f = Finsupp.sum f 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) : (Ideal.finsuppTotal ι M I v) f = Finset.sum Finset.univ fun (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} : LinearMap.range (Ideal.finsuppTotal ι M I v) = 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), (Finsupp.sum c fun (i : α) (a : R) => a * v i) = x

theorem mem_ideal_span_range_iff_exists_fun {α : Type u_1} {R : Type u_2} [Semiring R] [Fintype α] {x : R} {v : α → R} : x ∈ Ideal.span (Set.range v) ↔ ∃ (c : α → R), (Finset.sum Finset.univ fun (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

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

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

Equations

• RingHom.ker f = Ideal.comap f ⊥

theorem RingHom.mem_ker {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] [rcf : RingHomClass F R S] (f : F) {r : R} : r ∈ RingHom.ker f ↔ 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} [Semiring R] [Semiring S] [FunLike F R S] [rcf : RingHomClass F R S] (f : F) : ↑(RingHom.ker f) = ⇑f ⁻¹' {0}

theorem RingHom.ker_eq_comap_bot {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] [rcf : RingHomClass F R S] (f : F) : RingHom.ker f = Ideal.comap f ⊥

theorem RingHom.comap_ker {R : Type u} {S : Type v} {T : Type w} [Semiring R] [Semiring S] [Semiring T] (f : S →+* R) (g : T →+* S) : Ideal.comap g (RingHom.ker f) = RingHom.ker (RingHom.comp f g)

theorem RingHom.not_one_mem_ker {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] [rcf : RingHomClass F R S] [Nontrivial S] (f : F) : 1 ∉ RingHom.ker 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} [Semiring R] [Semiring S] [FunLike F R S] [rcf : RingHomClass F R S] [Nontrivial S] (f : F) : RingHom.ker f ≠ ⊤

theorem Pi.ker_ringHom {S : Type v} [Semiring S] {ι : Type u_3} {R : ι → Type u_4} [(i : ι) → Semiring (R i)] (φ : (i : ι) → S →+* R i) : RingHom.ker (Pi.ringHom φ) = ⨅ (i : ι), RingHom.ker (φ i)

@[simp]

theorem RingHom.ker_rangeSRestrict {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) : RingHom.ker (RingHom.rangeSRestrict f) = RingHom.ker f

theorem RingHom.injective_iff_ker_eq_bot {R : Type u} {S : Type v} {F : Type u_1} [Ring R] [Semiring S] [FunLike F R S] [rc : RingHomClass F R S] (f : F) : Function.Injective ⇑f ↔ RingHom.ker f = ⊥

theorem RingHom.ker_eq_bot_iff_eq_zero {R : Type u} {S : Type v} {F : Type u_1} [Ring R] [Semiring S] [FunLike F R S] [rc : RingHomClass F R S] (f : F) : RingHom.ker f = ⊥ ↔ ∀ (x : R), f x = 0 → x = 0

@[simp]

theorem RingHom.ker_coe_equiv {R : Type u} {S : Type v} [Ring R] [Semiring S] (f : R ≃+* S) : RingHom.ker ↑f = ⊥

@[simp]

theorem RingHom.ker_equiv {R : Type u} {S : Type v} [Ring R] [Semiring S] {F' : Type u_2} [EquivLike F' R S] [RingEquivClass F' R S] (f : F') : RingHom.ker f = ⊥

theorem RingHom.sub_mem_ker_iff {R : Type u} {S : Type v} {F : Type u_1} [Ring R] [Ring S] [FunLike F R S] [rc : RingHomClass F R S] (f : F) {x : R} {y : R} : x - y ∈ RingHom.ker f ↔ f x = f y

@[simp]

theorem RingHom.ker_rangeRestrict {R : Type u} {S : Type v} [Ring R] [Ring S] (f : R →+* S) : RingHom.ker (RingHom.rangeRestrict f) = RingHom.ker f

theorem RingHom.ker_isPrime {R : Type u} {S : Type v} {F : Type u_1} [Ring R] [Ring S] [IsDomain S] [FunLike F R S] [RingHomClass F R S] (f : F) : Ideal.IsPrime (RingHom.ker 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] [Field K] [FunLike F R K] [RingHomClass F R K] (f : F) (hf : Function.Surjective ⇑f) : Ideal.IsMaximal (RingHom.ker 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} {F : Type u_3} [Semiring R] [Semiring S] [FunLike F R S] [rc : RingHomClass F R S] {I : Ideal R} (f : F) : Ideal.map f I = ⊥ ↔ I ≤ RingHom.ker f

theorem Ideal.ker_le_comap {R : Type u_1} {S : Type u_2} {F : Type u_3} [Semiring R] [Semiring S] [FunLike F R S] [rc : RingHomClass F R S] {K : Ideal S} (f : F) : RingHom.ker f ≤ Ideal.comap f K

theorem Ideal.map_isPrime_of_equiv {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] {F' : Type u_4} [EquivLike F' R S] [RingEquivClass F' R S] (f : F') {I : Ideal R} [Ideal.IsPrime I] : Ideal.IsPrime (Ideal.map f I)

theorem Ideal.map_sInf {R : Type u_1} {S : Type u_2} {F : Type u_3} [Ring R] [Ring S] [FunLike F R S] [rc : RingHomClass F R S] {A : Set (Ideal R)} {f : F} (hf : Function.Surjective ⇑f) : (∀ J ∈ A, RingHom.ker f ≤ J) → Ideal.map f (sInf A) = sInf (Ideal.map f '' A)

theorem Ideal.map_isPrime_of_surjective {R : Type u_1} {S : Type u_2} {F : Type u_3} [Ring R] [Ring S] [FunLike F R S] [rc : RingHomClass F R S] {f : F} (hf : Function.Surjective ⇑f) {I : Ideal R} [H : Ideal.IsPrime I] (hk : RingHom.ker f ≤ I) : Ideal.IsPrime (Ideal.map f 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] [FunLike F R S] [rc : RingHomClass F R S] {I : Ideal R} {f : F} (hf : Function.Injective ⇑f) : Ideal.map f I = ⊥ ↔ I = ⊥

theorem Ideal.map_eq_iff_sup_ker_eq_of_surjective {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] {I : Ideal R} {J : Ideal R} (f : R →+* S) (hf : Function.Surjective ⇑f) : Ideal.map f I = Ideal.map f J ↔ I ⊔ RingHom.ker f = J ⊔ RingHom.ker f

theorem Ideal.map_radical_of_surjective {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] {f : R →+* S} (hf : Function.Surjective ⇑f) {I : Ideal R} (h : RingHom.ker f ≤ I) : Ideal.map f (Ideal.radical I) = Ideal.radical (Ideal.map f I)

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

Equations

• Submodule.moduleSubmodule = Module.mk ⋯ ⋯

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

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 : B → A) (hf : Function.RightInverse f_inv ⇑f) (g : A →+* C) (hg : RingHom.ker f ≤ RingHom.ker g) : B →+* C

Auxiliary definition used to define liftOfRightInverse

Equations

• One or more equations did not get rendered due to their size.

@[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 : B → A) (hf : Function.RightInverse f_inv ⇑f) (g : A →+* C) (hg : RingHom.ker f ≤ RingHom.ker g) (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 : B → A) (hf : Function.RightInverse f_inv ⇑f) : { g : A →+* C // RingHom.ker f ≤ RingHom.ker 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
      ∃!φ

Equations

• One or more equations did not get rendered due to their size.

@[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 : Function.Surjective ⇑f) : { g : A →+* C // RingHom.ker f ≤ RingHom.ker g } ≃ (B →+* C)

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

Equations

• RingHom.liftOfSurjective f hf = RingHom.liftOfRightInverse f (Function.surjInv hf) ⋯

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 : B → A) (hf : Function.RightInverse f_inv ⇑f) (g : { g : A →+* C // RingHom.ker f ≤ RingHom.ker 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 : B → A) (hf : Function.RightInverse f_inv ⇑f) (g : { g : A →+* C // RingHom.ker f ≤ RingHom.ker 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 : B → A) (hf : Function.RightInverse f_inv ⇑f) (g : A →+* C) (hg : RingHom.ker f ≤ RingHom.ker g) (h : B →+* C) (hh : RingHom.comp h f = g) : h = (RingHom.liftOfRightInverse f f_inv hf) { val := g, property := hg }

theorem AlgHom.coe_ker {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) : RingHom.ker f = RingHom.ker ↑f

theorem AlgHom.coe_ideal_map {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) (I : Ideal A) : Ideal.map f I = Ideal.map (↑f) I