QuotientSupport.lean

1 import PaperXII.ModuleSupport
2 import Mathlib.Algebra.Module.Torsion.Basic
3 import Mathlib.RingTheory.Spectrum.Prime.RingHom
4 
5 /-! Paper XII, claim 6.9. Quotient rings and quotient modules are actual quotients. -/
6 namespace PaperXII.QuotientSupport
7 
8 variable {R S M : Type*} [CommRing R] [CommRing S]
9     [AddCommGroup M] [Module R M]
10 
11 /-- Support under a surjective change of scalars. -/
12 theorem mem_support_restrictScalars_iff [Algebra R S] [Module S M]
13     [IsScalarTower R S M] [Module.Finite R M]
14     (hf : Function.Surjective (algebraMap R S)) (q : PrimeSpectrum S) :
15     PrimeSpectrum.comap (algebraMap R S) q ∈ Module.support R M ↔
16       q ∈ Module.support S M := by
17   let : Module.Finite S M := Module.Finite.of_restrictScalars_finite R S M
18   rw [Module.mem_support_iff_of_finite, Module.mem_support_iff_of_finite,
19     ← Module.comap_annihilator (R := S) (R₀ := R)]
20   exact Ideal.comap_le_comap_iff_of_surjective (algebraMap R S) hf _ _
21 
22 /-- The ambient-spectrum quotient identity, from actual localization and Nakayama. -/
23 theorem support_quotient_over_base [Module.Finite R M] (I : Ideal R) :
24     Module.support R (M ⧸ (I • ⊤ : Submodule R M)) =
25       Module.support R M ∩ PrimeSpectrum.zeroLocus I :=
26   Module.support_quotient I
27 
28 /-- Manuscript 6.9, with its two spectra explicitly distinguished. -/
29 theorem support_quotient_iff [Module.Finite R M] (I : Ideal R)
30     (q : PrimeSpectrum (R ⧸ I)) :
31     q ∈ Module.support (R ⧸ I) (M ⧸ (I • ⊤ : Submodule R M)) ↔
32       PrimeSpectrum.comap (Ideal.Quotient.mk I) q ∈ Module.support R M := by
33   rw [← mem_support_restrictScalars_iff (R := R)
34     (S := R ⧸ I) (Ideal.Quotient.mk_surjective) q,
35     support_quotient_over_base]
36   have hI : PrimeSpectrum.comap (Ideal.Quotient.mk I) q ∈
37       PrimeSpectrum.zeroLocus I := by
38     intro x hx
39     change Ideal.Quotient.mk I x ∈ q.asIdeal
40     rw [Ideal.Quotient.eq_zero_iff_mem.mpr hx]
41     exact q.asIdeal.zero_mem
42   exact and_iff_left hI
43 
44 /-- Set form of 6.9: inverse image along Spec(R/I) → Spec R. -/
45 theorem support_quotient_eq_preimage [Module.Finite R M] (I : Ideal R) :
46     Module.support (R ⧸ I) (M ⧸ (I • ⊤ : Submodule R M)) =
47       PrimeSpectrum.comap (Ideal.Quotient.mk I) ⁻¹' Module.support R M := by
48   ext q
49   exact support_quotient_iff I q
50 
51 /-- Manuscript 6.9, literal image form under the canonical spectrum identification. -/
52 theorem image_support_quotient [Module.Finite R M] (I : Ideal R) :
53     PrimeSpectrum.comap (Ideal.Quotient.mk I) ''
54       Module.support (R ⧸ I) (M ⧸ (I • ⊤ : Submodule R M)) =
55       Module.support R M ∩ PrimeSpectrum.zeroLocus I := by
56   rw [support_quotient_eq_preimage, Set.image_preimage_eq_inter_range,
57     range_comap_of_surjective (R ⧸ I) (Ideal.Quotient.mk I)
58       Ideal.Quotient.mk_surjective, Ideal.mk_ker]
59 
60 end PaperXII.QuotientSupport

Back to source controls