Research proof index

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.

If p is an associated prime of M and p meets the multiplicative set S, then p is an associated prime of the kernel of the localization map mkLinearMap S M : M →ₗ[R] LocalizedModule S M. This is the “meets S” direction used to identify associated primes of ker (mkLinearMap S M) with the associated primes of M that are not disjoint from...

If p is an associated prime of the quotient M ⧸ ker(mkLinearMap S M) and p is disjoint from the multiplicative set S, then p is already an associated prime of M. This lemma is used to identify the “disjoint part” of the associated primes of M with the associated primes of the localization quotient.