Colon ideals and quotient annihilators

For an R-algebra S, the ideal (N : x) of a submodule N of an S-module commutes with restricting scalars to R.

For an ideal I and an element f of a commutative ring, I ∩ (f) = f · (I : f). When f is regular this determines (I : f): generators of I ∩ (f), which an intersection computation supplies, divided by f generate (I : f).

Main results

• Submodule.le_annihilator_quotient_iff: an ideal annihilates a quotient exactly when its multiples of the ambient module lie in the submodule.
• Submodule.comap_colon_singleton: the ideal (N : x) of R is the preimage of the ideal (N : x) of S.
• Ideal.inf_span_singleton_eq_span_singleton_mul_colon: I ∩ (f) = f · (I : f).
• Ideal.colon_singleton_eq_of_inf_span_singleton_eq: for regular f, if I ∩ (f) = f · J then (I : f) = J.
• Ideal.exists_eq_span_pow_mul_colon_not_le: an ideal not contained in every power of (f) is (f ^ k) · (I : f ^ k) with (I : f ^ k) not contained in (f).

References

• D. Cox, J. Little, D. O'Shea, Ideals, Varieties, and Algorithms, Chapter 4, §4, computing ideal quotients from intersections.

theorem Submodule.le_annihilator_quotient_iff {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] {I : Ideal R} {N : Submodule R M} : I ≤ Module.annihilator R (M ⧸ N) ↔ I • ⊤ ≤ N

An ideal annihilates a quotient exactly when its multiples of the ambient module lie in the submodule being quotiented out.

theorem Submodule.comap_colon_singleton {R : Type u_1} {S : Type u_2} {M : Type u_3} [CommSemiring R] [CommSemiring S] [Algebra R S] [AddCommMonoid M] [Module R M] [Module S M] [IsScalarTower R S M] (N : Submodule S M) (x : M) : Ideal.comap (algebraMap R S) (N.colon {x}) = (restrictScalars R N).colon {x}

For a submodule N of an S-module M and x ∈ M, the ideal (N : x) of R is the preimage of the ideal (N : x) of S.

theorem Ideal.inf_span_singleton_eq_span_singleton_mul_colon {R : Type u_4} [CommSemiring R] (I : Ideal R) (f : R) : I ⊓ span {f} = span {f} * Submodule.colon I {f}

The intersection of an ideal I with the principal ideal (f) is f times the colon ideal (I : f).

theorem Ideal.colon_singleton_eq_of_inf_span_singleton_eq {R : Type u_4} [CommSemiring R] {I J : Ideal R} {f : R} (hf : IsLeftRegular f) (h : I ⊓ span {f} = span {f} * J) : Submodule.colon I {f} = J

Colon ideals from intersections. If f is regular and I ∩ (f) = f · J, then the colon ideal (I : f) is J.

theorem Ideal.exists_eq_span_pow_mul_colon_not_le {R : Type u_4} [CommSemiring R] {I : Ideal R} {f : R} (h : ∃ (n : ℕ), ¬I ≤ span {f ^ n}) : ∃ (k : ℕ), I = span {f ^ k} * Submodule.colon I {f ^ k} ∧ ¬Submodule.colon I {f ^ k} ≤ span {f}

Extracting a power of a principal ideal. If an ideal I does not lie in every power of (f), then I = (f ^ k) · (I : f ^ k) for some k, where the colon ideal (I : f ^ k) does not lie in (f).