Complements on ideal multiplication and the ideal action

This file collects general facts about the multiplication of ideals and about the action I • N of an ideal on a module, complementing Mathlib/RingTheory/Ideal/Operations.lean.

Main results

• Ideal.eq_one_of_mul_eq_one: a two-sided left factor of the unit ideal is the unit ideal. Over a commutative semiring, this implies that the divisor antidiagonal of the unit ideal is a singleton.
• Ideal.toAddSubgroup_mul_eq_closure_mul: additive generators of a product of ideals.
• Ideal.smul_top_eq_top_of_pi: an ideal that expands the whole of a product of modules expands the whole of every factor.
• LinearMap.apply_mem_of_mem_smul_top: a linear functional carries I • M into I.
• Ideal.span_insert_eq_top_of_subset: a generating set S may be replaced by a set S', both taken together with a common element a, as soon as every element of S is a itself or belongs to S'.
• Ideal.span_singleton_pow_sup_span_singleton_pow: the left ideals generated by a ^ j and a ^ m have as supremum the left ideal generated by a ^ min j m.
• Ideal.sup_pow_le_sup_pow_right: modulo a two-sided ideal I, powers of I ⊔ J are controlled by the corresponding power of the left ideal J.
• Ideal.isTwoSided_span_of_subset_center: a left ideal spanned by central elements is two-sided.
• Submodule.mem_span_algebraMap_smul_top_iff: over an algebra A, the action on V of the left ideal spanned by a scalar x produces exactly the multiples x • w.
• Subalgebra.toSubmodule_sup_pow_restrictScalars_eq_top: if a subalgebra and a principal left ideal additively span the ambient algebra, and the subalgebra contains a generator of the ideal, then the same holds with the ideal replaced by any power.

theorem Ideal.toAddSubgroup_mul_eq_closure_mul {R : Type u_1} [Ring R] {I J : Ideal R} {S T : Set R} (hI : Submodule.toAddSubgroup I = AddSubgroup.closure S) (hJ : Submodule.toAddSubgroup J = AddSubgroup.closure T) : Submodule.toAddSubgroup (I * J) = AddSubgroup.closure (S * T)

If S and T additively generate the ideals I and J, then their pairwise products additively generate I * J.

theorem Ideal.eq_one_of_mul_eq_one {R : Type u_2} [Semiring R] {I J : Ideal R} [I.IsTwoSided] (h : I * J = 1) : I = 1

If a two-sided ideal times a left ideal is the unit ideal, then the first ideal is the unit ideal.

theorem Ideal.smul_top_eq_top_of_pi {R : Type u_2} [Semiring R] {ι : Type u_3} {M : ι → Type u_4} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] (I : Ideal R) (h : I • ⊤ = ⊤) (i : ι) : I • ⊤ = ⊤

Expanding a product expands every factor: if I • ⊤ = ⊤ in ∀ i, M i then I • ⊤ = ⊤ in each M i. Thus properness of I • ⊤ in one factor implies properness in the product.

theorem Ideal.span_insert_eq_top_of_subset {R : Type u_1} [Semiring R] {a : R} {S S' : Set R} (hsub : S ⊆ insert a S') (hspan : span (insert a S) = ⊤) : span (insert a S') = ⊤

Replacing one generating set by another: if every element of S is either a itself or an element of S', then S' together with a generates the unit ideal as soon as S together with a does. Note that S' need not be contained in S, and may be larger: the hypothesis constrains only where the elements of S are found. Both spans contain a, so only the rest of S has to be accounted for.

theorem Ideal.span_singleton_pow_sup_span_singleton_pow {R : Type u_1} [Semiring R] (a : R) (j m : ℕ) : span {a ^ j} ⊔ span {a ^ m} = span {a ^ min j m}

The left ideals generated by two powers of the same element have as supremum the left ideal generated by the smaller power.

theorem Ideal.isTwoSided_span_of_subset_center {A : Type u_2} [Semiring A] {s : Set A} (hs : s ⊆ Set.center A) : (span s).IsTwoSided

A left ideal spanned by central elements is two-sided.

theorem LinearMap.apply_mem_of_mem_smul_top {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] (f : M →ₗ[R] R) {I : Ideal R} [I.IsTwoSided] {x : M} (hx : x ∈ I • ⊤) : f x ∈ I

A linear functional f : M → R carries I • M into the ideal I: the ideal action on R itself is multiplication, and f is linear over it.

@[instance 100]

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

A supremum of two two-sided ideals is two-sided.

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

The n-th power of the supremum of a two-sided ideal and a left ideal is contained in the first ideal plus the n-th power of the second.

theorem Subalgebra.toSubmodule_sup_pow_restrictScalars_eq_top {R : Type u_1} {S : Type u_2} [CommSemiring R] [Semiring S] [Algebra R S] {T : Subalgebra R S} {I : Ideal S} {π : S} (hπ : Ideal.span {π} = I) (hπT : π ∈ T) (h : toSubmodule T ⊔ Submodule.restrictScalars R I = ⊤) (n : ℕ) : toSubmodule T ⊔ Submodule.restrictScalars R (I ^ n) = ⊤

If every element of S is a sum of an element of a subalgebra T and an element of a principal left ideal I, and T contains a generator of I, then the same holds with I replaced by any power.

theorem Submodule.mem_span_algebraMap_smul_top_iff {R : Type u_1} {A : Type u_2} {V : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid V] [Module R V] [Module A V] [IsScalarTower R A V] (x : R) {v : V} : v ∈ Ideal.span {(algebraMap R A) x} • ⊤ ↔ ∃ (w : V), x • w = v

The action of a principal ideal with a scalar generator. For an R-algebra A, possibly noncommutative, and x : R, the submodule (x) • V generated by the left ideal of A spanned by x consists of the multiples x • w. Over a commutative ring this is Submodule.ideal_span_singleton_smul.