FittingTransport.lean

1 import PaperXII.FittingBaseChange
2 import PaperXII.SupportTransport
3 
4 noncomputable section
5 namespace PaperXII
6 open TensorProduct
7 variable {R S M : Type*} [CommRing R] [CommRing S] [Algebra R S]
8   [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower R S M]
9 
10 /-- Extension of scalars cancels for an existing S-module when R → S is surjective. -/
11 def scalarTensorEquiv (hf : Function.Surjective (algebraMap R S)) : S ⊗[R] M ≃ₗ[S] M :=
12   { ((LinearMap.id : M →ₗ[S] M).restrictScalars R).liftBaseChange S with
13     invFun := fun m => (1 : S) ⊗ₜ[R] m
14     left_inv := by
15       intro z
16       change (1 : S) ⊗ₜ[R] ((((LinearMap.id : M →ₗ[S] M).restrictScalars R).liftBaseChange S) z) = z
17       induction z with
18       | zero => simp
19       | tmul s m =>
20         obtain ⟨r,rfl⟩ := hf s
21         simp only [LinearMap.liftBaseChange_tmul,LinearMap.restrictScalars_apply,
22           LinearMap.id_apply,IsScalarTower.algebraMap_smul]
23         rw [← TensorProduct.smul_tmul]
24         simp [Algebra.smul_def]
25       | add x y hx hy => simp only [map_add,TensorProduct.tmul_add,hx,hy]
26     right_inv := by intro m; simp }
27 
28 /-- Intrinsic Fitting transport, in fact valid for any surjective scalar map. -/
29 theorem fittingIdeal_transport [Module.FinitePresentation R M] [Module.FinitePresentation S M]
30     (hf : Function.Surjective (algebraMap R S)) (j : ℕ) :
31     Ideal.map (algebraMap R S) (fittingIdeal R M j) = fittingIdeal S M j := by
32   rw [← fittingIdeal_baseChange]
33   exact fittingIdeal_linearEquiv (scalarTensorEquiv hf) j
34 
35 /-- Complete support and Fitting transport in Claim 7.1, under a ring identification. -/
36 theorem support_and_fitting_transport [Module.FinitePresentation R M] [Module.FinitePresentation S M]
37     (hf : Function.Bijective (algebraMap R S)) :
38     IsHomeomorph (PrimeSpectrum.comap (algebraMap R S)) ∧
39     PrimeSpectrum.comap (algebraMap R S) '' Module.support S M = Module.support R M ∧
40     ∀ j : ℕ, Ideal.map (algebraMap R S) (fittingIdeal R M j) = fittingIdeal S M j := by
41   exact ⟨SupportTransport.spectrum_isHomeomorph hf, SupportTransport.image_support hf,
42     fun j => fittingIdeal_transport hf.surjective j⟩
43 
44 /-- Claim 7.1 at the manuscript hypotheses. All finite-presentation inputs are derived. -/
45 theorem support_and_fitting_transport_noetherian [IsNoetherianRing R] [IsNoetherianRing S]
46     [Module.Finite S M] (hf : Function.Bijective (algebraMap R S)) :
47     let _ : Module.Finite R S := Module.Finite.of_surjective (Algebra.linearMap R S) hf.surjective
48     let _ : Module.Finite R M := Module.Finite.trans S M
49     let _ : Module.FinitePresentation R M := Module.finitePresentation_of_finite R M
50     let _ : Module.FinitePresentation S M := Module.finitePresentation_of_finite S M
51     IsHomeomorph (PrimeSpectrum.comap (algebraMap R S)) ∧
52     PrimeSpectrum.comap (algebraMap R S) '' Module.support S M = Module.support R M ∧
53     ∀ j : ℕ, Ideal.map (algebraMap R S) (fittingIdeal R M j) = fittingIdeal S M j := by
54   let : Module.Finite R S := Module.Finite.of_surjective (Algebra.linearMap R S) hf.surjective
55   let : Module.Finite R M := Module.Finite.trans S M
56   let : Module.FinitePresentation R M := Module.finitePresentation_of_finite R M
57   let : Module.FinitePresentation S M := Module.finitePresentation_of_finite S M
58   exact support_and_fitting_transport hf
59 
60 end PaperXII

Back to source controls