The multiplier ring of a submodule of an algebra

Let B be a commutative R-algebra and M an R-submodule of B. The multiplier ring B₀ = {b ∈ B | b M ⊆ M} of the underlying additive subgroup of M (AddSubgroup.multiplierRing) is a subring of B containing the image of R. This file compares the R-submodule I • M of B coming from an ideal I of R with the extension of I to B₀. The submodule I • M lies in B₀ only under a hypothesis such as I • (M * M) ≤ M (see Submodule.smul_subset_multiplierRing). These comparisons are how a lattice in a finite algebra over a Huber ring yields a pair of definition.

Main results

• Submodule.toMultiplierRing: the structure map R → B₀.
• Submodule.smul_subset_multiplierRing: if I carries M * M into M, then I • M ⊆ B₀.
• Submodule.coe_map_pow_subset: if 1 ∈ M, the powers of the extension J = I B₀ satisfy Jⁿ ⊆ Iⁿ • M.
• Submodule.smul_subset_coe_map_pow: if Iʲ • M ⊆ B₀, then I^(n + j) • M ⊆ Jⁿ.
• Submodule.isIntegral_of_mem_multiplierRing: if M is finitely generated and contains 1, every element of B₀ is integral over R.

theorem Submodule.algebraMap_mem_multiplierRing {R : Type u_1} [CommRing R] {B : Type u_2} [CommRing B] [Algebra R B] (M : Submodule R B) (a : R) : (algebraMap R B) a ∈ M.toAddSubgroup.multiplierRing

The image of R lies in the multiplier ring of an R-submodule.

theorem Submodule.smul_subset_multiplierRing {R : Type u_1} [CommRing R] {B : Type u_2} [CommRing B] [Algebra R B] {M : Submodule R B} {I : Ideal R} (h : I • (M * M) ≤ M) : ↑(I • M) ⊆ ↑M.toAddSubgroup.multiplierRing

If an ideal I carries M * M into M, then I • M lies in the multiplier ring of M.

noncomputable def Submodule.toMultiplierRing {R : Type u_1} [CommRing R] {B : Type u_2} [CommRing B] [Algebra R B] (M : Submodule R B) : R →+* ↥M.toAddSubgroup.multiplierRing

The structure map R → B₀ into the multiplier ring of an R-submodule.

@[simp]

theorem Submodule.coe_toMultiplierRing {R : Type u_1} [CommRing R] {B : Type u_2} [CommRing B] [Algebra R B] (M : Submodule R B) (a : R) : ↑(M.toMultiplierRing a) = a • 1

The structure map R → B₀ sends a to a • 1.

theorem Submodule.coe_map_pow_subset {R : Type u_1} [CommRing R] {B : Type u_2} [CommRing B] [Algebra R B] {M : Submodule R B} (h1 : 1 ∈ M) (I : Ideal R) (n : ℕ) : Subtype.val '' ↑(Ideal.map M.toMultiplierRing I ^ n) ⊆ ↑(I ^ n • M)

The powers of the extension J = I B₀ of an ideal I of R to the multiplier ring lie in Iⁿ • M when 1 ∈ M.

theorem Submodule.smul_subset_coe_map_pow {R : Type u_1} [CommRing R] {B : Type u_2} [CommRing B] [Algebra R B] {M : Submodule R B} {I : Ideal R} {j : ℕ} (hj : ↑(I ^ j • M) ⊆ ↑M.toAddSubgroup.multiplierRing) (n : ℕ) : ↑(I ^ (n + j) • M) ⊆ Subtype.val '' ↑(Ideal.map M.toMultiplierRing I ^ n)

If Iʲ • M lies in the multiplier ring, then I^(n + j) • M lies in the n-th power of the extension J = I B₀ of I to the multiplier ring.

theorem Submodule.isIntegral_of_mem_multiplierRing {R : Type u_1} [CommRing R] {B : Type u_2} [CommRing B] [Algebra R B] {M : Submodule R B} (hM : M.FG) (h1 : 1 ∈ M) {b : B} (hb : b ∈ M.toAddSubgroup.multiplierRing) : IsIntegral R b

The multiplier ring of a finitely generated submodule containing 1 is integral. If M is a finitely generated R-submodule of B with 1 ∈ M, every b ∈ B with b M ⊆ M is integral over R: by Cayley–Hamilton, multiplication by b on M satisfies a monic polynomial, and evaluating at 1 shows that b satisfies it too.