BaseChangeSupport.lean

1 import PaperXII.FieldFibers
2 import Mathlib.RingTheory.TensorProduct.Finite
3 import Mathlib.RingTheory.Spectrum.Prime.RingHom
4 
5 /-! Supporting theorems: arbitrary scalar extension of a finite module.
6 These strengthen the support tools, but do not claim the paper's Fitting identities. -/
7 namespace PaperXII.BaseChangeSupport
8 
9 open scoped TensorProduct
10 open FieldFibers ModuleSupport
11 
12 variable {R S M : Type*} [CommRing R] [CommRing S] [Algebra R S]
13     [AddCommGroup M] [Module R M] [Module.Finite R M]
14 
15 /-- Pointwise support under arbitrary scalar extension of a finite module. -/
16 theorem mem_support_baseChange_iff (q : PrimeSpectrum S) :
17     q ∈ Module.support S (S ⊗[R] M) ↔
18       PrimeSpectrum.comap (algebraMap R S) q ∈ Module.support R M := by
19   let K := q.asIdeal.ResidueField
20   let e := TensorProduct.AlgebraTensorModule.cancelBaseChange R S K K M
21   rw [Module.mem_support_iff_nontrivial_residueField_tensorProduct q, e.nontrivial_congr]
22   have hp : pointPrime (algebraMap R K) = PrimeSpectrum.comap (algebraMap R S) q := by
23     ext r
24     change algebraMap R K r = 0 ↔ algebraMap R S r ∈ q.asIdeal
25     rw [IsScalarTower.algebraMap_apply R S K, Ideal.algebraMap_residueField_eq_zero]
26   rw [← hp]
27   exact nontrivial_tensor_iff_support
28 
29 /-- Support of scalar extension is the inverse image of the original support. -/
30 theorem support_baseChange :
31     Module.support S (S ⊗[R] M) =
32       PrimeSpectrum.comap (algebraMap R S) ⁻¹' Module.support R M := by
33   ext q
34   exact mem_support_baseChange_iff q
35 
36 /-- Full support survives any commutative scalar extension. -/
37 theorem fullSupport_baseChange (h : FullSupport R M) : FullSupport S (S ⊗[R] M) := by
38   unfold FullSupport at h ⊢
39   rw [support_baseChange, h, Set.preimage_univ]
40 
41 /-- Near faithfulness survives scalar extension when both rings are Noetherian. -/
42 theorem nearlyFaithful_baseChange [IsNoetherianRing R] [IsNoetherianRing S]
43     (h : NearlyFaithful R M) : NearlyFaithful S (S ⊗[R] M) :=
44   (nearlyFaithful_iff_fullSupport S _).mpr
45     (fullSupport_baseChange ((nearlyFaithful_iff_fullSupport R M).mp h))
46 
47 end PaperXII.BaseChangeSupport

Back to source controls