SupportTransport.lean

1 import PaperXII.QuotientSupport
2 import Mathlib.RingTheory.Spectrum.Prime.Topology
3 
4 /-! Paper XII, support portion of 7.1 and complete Corollary 7.2.
5 The Fitting-ideal assertion in 7.1 is not claimed by this module. -/
6 namespace PaperXII.SupportTransport
7 
8 open ModuleSupport
9 
10 variable {R S M : Type*} [CommRing R] [CommRing S] [Algebra R S]
11     [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower R S M]
12 
13 /-- Under a surjective scalar map, localization support agrees at corresponding primes.
14 No finite generation is needed for this change of scalars. -/
15 theorem mem_support_comap_iff (hf : Function.Surjective (algebraMap R S))
16     (q : PrimeSpectrum S) :
17     PrimeSpectrum.comap (algebraMap R S) q ∈ Module.support R M ↔
18       q ∈ Module.support S M := by
19   simp only [Module.mem_support_iff', PrimeSpectrum.comap_asIdeal, Ideal.mem_comap]
20   constructor
21   · rintro ⟨m, hm⟩
22     refine ⟨m, fun s hs ↦ ?_⟩
23     obtain ⟨r, rfl⟩ := hf s
24     simpa only [IsScalarTower.algebraMap_smul] using hm r hs
25   · rintro ⟨m, hm⟩
26     refine ⟨m, fun r hr ↦ ?_⟩
27     simpa only [IsScalarTower.algebraMap_smul] using hm (algebraMap R S r) hr
28 
29 /-- A ring isomorphism induces the actual homeomorphism of spectra. -/
30 theorem spectrum_isHomeomorph (hf : Function.Bijective (algebraMap R S)) :
31     IsHomeomorph (PrimeSpectrum.comap (algebraMap R S)) :=
32   PrimeSpectrum.isHomeomorph_comap_of_bijective hf
33 
34 /-- Support assertion in 7.1, using the actual spectral map. -/
35 theorem image_support (hf : Function.Bijective (algebraMap R S)) :
36     PrimeSpectrum.comap (algebraMap R S) '' Module.support S M = Module.support R M := by
37   ext p
38   constructor
39   · rintro ⟨q, hq, rfl⟩
40     exact (mem_support_comap_iff hf.surjective q).mpr hq
41   · intro hp
42     obtain ⟨q, rfl⟩ := (spectrum_isHomeomorph hf).surjective p
43     exact ⟨q, (mem_support_comap_iff hf.surjective q).mp hp, rfl⟩
44 
45 /-- Corollary 7.2: full support is invariant under the ring identification. -/
46 theorem fullSupport_iff (hf : Function.Bijective (algebraMap R S)) :
47     FullSupport R M ↔ FullSupport S M := by
48   constructor
49   · intro h
50     apply (fullSupport_iff_localizations S M).mpr
51     intro q
52     exact (mem_support_comap_iff hf.surjective q).mp
53       ((fullSupport_iff_localizations R M).mp h _)
54   · intro h
55     unfold FullSupport at h ⊢
56     rw [← image_support hf, h, Set.image_univ,
57       Set.range_eq_univ.mpr (spectrum_isHomeomorph hf).surjective]
58 
59 end PaperXII.SupportTransport

Back to source controls