ModuleSupport.lean

1 import Mathlib.RingTheory.Support
2 import Mathlib.RingTheory.Noetherian.Nilpotent
3 
4 /-! Paper XII, claims 6.2, 6.7 and 6.8.
5 Support is Mathlib's actual localized-module support. -/
6 namespace PaperXII.ModuleSupport
7 
8 variable (R M : Type*) [CommRing R] [AddCommGroup M] [Module R M]
9 
10 /-- Every localization at a prime is nontrivial. -/
11 def FullSupport : Prop := Module.support R M = Set.univ
12 
13 /-- The annihilator ideal has a zero power. -/
14 def NearlyFaithful : Prop := IsNilpotent (Module.annihilator R M)
15 
16 /-- Manuscript 6.2. Finite generation suffices; no Noetherian assumption. -/
17 theorem support_eq_zeroLocus_annihilator [Module.Finite R M] :
18     Module.support R M = PrimeSpectrum.zeroLocus (Module.annihilator R M) :=
19   Module.support_eq_zeroLocus
20 
21 /-- The localization meaning of full support, without a finiteness assumption. -/
22 theorem fullSupport_iff_localizations :
23     FullSupport R M ↔ ∀ p : PrimeSpectrum R,
24       Nontrivial (LocalizedModule p.asIdeal.primeCompl M) := by
25   simp only [FullSupport, Set.eq_univ_iff_forall, Module.mem_support_iff]
26 
27 /-- Manuscript 6.7, conditions (2) and (3). -/
28 theorem fullSupport_iff_annihilator_le_nilradical [Module.Finite R M] :
29     FullSupport R M ↔ Module.annihilator R M ≤ nilradical R := by
30   rw [FullSupport, Module.support_eq_zeroLocus, PrimeSpectrum.zeroLocus_eq_univ_iff]
31   rfl
32 
33 /-- Manuscript 6.7, conditions (1) and (3). -/
34 theorem nearlyFaithful_iff_annihilator_le_nilradical [IsNoetherianRing R] :
35     NearlyFaithful R M ↔ Module.annihilator R M ≤ nilradical R :=
36   Ideal.FG.isNilpotent_iff_le_nilradical (IsNoetherian.noetherian _)
37 
38 /-- Manuscript 6.7, conditions (1) and (2). -/
39 theorem nearlyFaithful_iff_fullSupport [IsNoetherianRing R] [Module.Finite R M] :
40     NearlyFaithful R M ↔ FullSupport R M :=
41   (nearlyFaithful_iff_annihilator_le_nilradical R M).trans
42     (fullSupport_iff_annihilator_le_nilradical R M).symm
43 
44 /-- Manuscript 6.8, strengthened to every prime, hence every component generic point. -/
45 theorem nontrivial_localization_of_nearlyFaithful [IsNoetherianRing R]
46     [Module.Finite R M] (h : NearlyFaithful R M) (p : PrimeSpectrum R) :
47     Nontrivial (LocalizedModule p.asIdeal.primeCompl M) :=
48   (fullSupport_iff_localizations R M).mp
49     ((nearlyFaithful_iff_fullSupport R M).mp h) p
50 
51 /-- Manuscript 6.7, reduced-ring refinement. -/
52 theorem nearlyFaithful_iff_faithful_of_reduced [IsNoetherianRing R] [IsReduced R] :
53     NearlyFaithful R M ↔ FaithfulSMul R M := by
54   rw [nearlyFaithful_iff_annihilator_le_nilradical, nilradical_eq_zero,
55     Ideal.zero_eq_bot, le_bot_iff, Module.annihilator_eq_bot]
56 
57 /-- Full support detects faithfulness over a reduced ring for finite modules. -/
58 theorem fullSupport_iff_faithful_of_reduced [Module.Finite R M] [IsReduced R] :
59     FullSupport R M ↔ FaithfulSMul R M := by
60   rw [fullSupport_iff_annihilator_le_nilradical, nilradical_eq_zero,
61     Ideal.zero_eq_bot, le_bot_iff, Module.annihilator_eq_bot]
62 
63 end PaperXII.ModuleSupport

Back to source controls