Quotients by consecutive powers of an ideal

For an ideal P of a commutative ring B and an element a ∈ P ^ n, multiplication by a descends to a B-linear map B ⧸ P → B ⧸ P ^ (n + 1). This file studies the sequence

0 → B ⧸ P --· a--> B ⧸ P ^ (n + 1) → B ⧸ P ^ n → 0

for a ∈ P ^ n with a ∉ P ^ (n + 1). The first map is injective as soon as P is maximal, and the sequence is exact in the middle when P is a nonzero prime of a Dedekind domain, where P ^ n / P ^ (n + 1) is a one-dimensional B ⧸ P-vector space spanned by the class of a.

Main results

• Ideal.le_comap_mulLeft_pow_succ: multiplication by a ∈ I ^ n carries I into I ^ (n + 1).
• Ideal.mapQ_mulLeft_pow_succ_injective: for P maximal, multiplication by a is injective on B ⧸ P → B ⧸ P ^ (n + 1).
• Ideal.exact_mapQ_mulLeft_pow_succ: for P a nonzero prime of a Dedekind domain, the sequence B ⧸ P → B ⧸ P ^ (n + 1) → B ⧸ P ^ n is exact.

theorem Ideal.le_comap_mulLeft_pow_succ {B : Type u_1} [CommSemiring B] {I : Ideal B} {a : B} {n : ℕ} (ha : a ∈ I ^ n) : I ≤ Submodule.comap (LinearMap.mulLeft B a) (I ^ (n + 1))

Multiplication by an element a ∈ I ^ n carries I into I ^ (n + 1). This is the compatibility condition under which LinearMap.mulLeft B a descends, via Submodule.mapQ, to a B-linear map B ⧸ I → B ⧸ I ^ (n + 1).

theorem Ideal.mapQ_mulLeft_pow_succ_injective {B : Type u_1} [CommRing B] {P : Ideal B} {a : B} {n : ℕ} [P.IsMaximal] (ha : a ∈ P ^ n) (ha' : a ∉ P ^ (n + 1)) : Function.Injective ⇑(Submodule.mapQ P (P ^ (n + 1)) (LinearMap.mulLeft B a) ⋯)

For a maximal ideal P and a ∈ P ^ n with a ∉ P ^ (n + 1), multiplication by a induces an injective B-linear map B ⧸ P → B ⧸ P ^ (n + 1).

theorem Ideal.exact_mapQ_mulLeft_pow_succ {B : Type u_1} [CommRing B] {P : Ideal B} {a : B} {n : ℕ} [IsDedekindDomain B] [P.IsPrime] (hP : P ≠ ⊥) (ha : a ∈ P ^ n) (ha' : a ∉ P ^ (n + 1)) : Function.Exact ⇑(Submodule.mapQ P (P ^ (n + 1)) (LinearMap.mulLeft B a) ⋯) ⇑(Submodule.factor ⋯)

For a nonzero prime P of a Dedekind domain and a ∈ P ^ n with a ∉ P ^ (n + 1), the sequence B ⧸ P → B ⧸ P ^ (n + 1) → B ⧸ P ^ n, whose first map is multiplication by a and whose second map is the quotient map, is exact.