Transport of minimal-prime support avoidance through localization

For a finite module, localization commutes with its annihilator. The reverse inclusion uses a finite generating set to clear all denominators at once. Minimal-prime avoidance then follows from the ordinary minimal-prime correspondence for a localization.

theorem AlgebraicAnalysis.LocalizedMinimalSupportAvoidance.annihilator_localizedModule {C : Type u_1} {E : Type u_2} [CommRing C] [AddCommGroup E] [Module C E] [Module.Finite C E] (S : Submonoid C) : Module.annihilator (Localization S) (LocalizedModule S E) = Ideal.map (algebraMap C (Localization S)) (Module.annihilator C E)

The annihilator of a finite module commutes with localization.

theorem AlgebraicAnalysis.LocalizedMinimalSupportAvoidance.localized_minimalPrime_avoids {C : Type u_1} {E : Type u_2} [CommRing C] [AddCommGroup E] [Module C E] [Module.Finite C E] (S : Submonoid C) (x : C) (havoid : ∀ p ∈ (Module.annihilator C E).minimalPrimes, x ∉ p) (Q : Ideal (Localization S)) : Q ∈ (Module.annihilator (Localization S) (LocalizedModule S E)).minimalPrimes → (algebraMap C (Localization S)) x ∉ Q

Minimal-prime avoidance survives localization.