Research proof index

Associated primes of the kernel of the localization map. This identifies the associated primes of ker (LocalizedModule.mkLinearMap S M) : Submodule R M with the associated primes of M that do meet the multiplicative set S. Equivalently, these are the associated primes of M after removing those disjoint from S. This lemma is used as the “kernel...

One-sided inclusion for associated primes of the kernel of the localization map. If p ∈ associatedPrimes R (ker (mkLinearMap S M)), then p is an associated prime of M and p is not disjoint from the multiplicative set S. This is one direction of associatedPrimes_ker_mkLinearMap_eq.

Associated primes of a localized module are disjoint from the multiplicative set. More precisely, if p ∈ associatedPrimes R (LocalizedModule S M), then p.carrier ∩ S = ∅. This is a standard fact in commutative algebra: an element of S becomes a unit after localization, so no associated prime of the localized module can contain an element of S.

Associated primes of the localization quotient are disjoint from the multiplicative set. More precisely, any p ∈ associatedPrimes R (M ⧸ ker(mkLinearMap S M)) satisfies p.carrier ∩ S = ∅. In this file this is used as a “black box” input in the Bourbaki-style splitting of associated primes under localization.

Associated primes under localization, characterized by the kernel of the localization map. This packages a classical statement (Bourbaki, Algèbre commutative, Ch. IV, §1, no. 2, Prop. 6) describing how associated primes split between a submodule and its quotient when localizing at a multiplicative set S.

Associated primes disjoint from S survive in the localization quotient. If p is an associated prime of M and p.carrier ∩ S = ∅, then p is an associated prime of the quotient M ⧸ ker(mkLinearMap S M). This is the “disjoint part” inclusion used in the splitting of associated primes under localization.