FittingStrata.lean

1 import PaperXII.FittingBoundaryChecks
2 import Mathlib.RingTheory.LocalRing.Module
3 
4 /-! Intrinsic Fitting support and all higher residue-fiber strata. -/
5 noncomputable section
6 namespace PaperXII
7 open TensorProduct
8 
9 /-- Over a field, all intrinsic Fitting ideals are determined by actual vector-space dimension. -/
10 theorem fittingIdeal_field {K V : Type*} [Field K] [AddCommGroup V] [Module K V]
11     [Module.FinitePresentation K V] (j : ℕ) :
12     fittingIdeal K V j = if Module.finrank K V ≤ j then ⊤ else ⊥ := by
13   calc
14     fittingIdeal K V j = fittingIdeal K (Fin (Module.finrank K V) → K) j :=
15       fittingIdeal_linearEquiv (Module.finBasis K V).equivFun j
16     _ = _ := fittingIdeal_free _ _
17 
18 variable {R M : Type*} [CommRing R] [AddCommGroup M] [Module R M]
19 
20 /-- Ideal containment at a prime is exactly the strict residue-fiber dimension condition. -/
21 theorem fittingIdeal_le_prime_iff [Module.FinitePresentation R M]
22     (p : PrimeSpectrum R) (j : ℕ) :
23     fittingIdeal R M j ≤ p.asIdeal ↔
24       j < Module.finrank p.asIdeal.ResidueField (p.asIdeal.ResidueField ⊗[R] M) := by
25   have hmap : Ideal.map (algebraMap R p.asIdeal.ResidueField) (fittingIdeal R M j) = ⊥ ↔
26       fittingIdeal R M j ≤ p.asIdeal := by
27     rw [Ideal.map_eq_bot_iff_le_ker,Ideal.ker_algebraMap_residueField]
28   rw [← hmap, ← fittingIdeal_baseChange, fittingIdeal_field]
29   by_cases h : Module.finrank p.asIdeal.ResidueField (p.asIdeal.ResidueField ⊗[R] M) ≤ j
30   · simp [h,not_lt_of_ge h]
31   · simp [h,Nat.lt_of_not_ge h]
32 
33 /-- Paper XII, Claim 6.3: intrinsic zeroth Fitting ideals cut out actual module support. -/
34 theorem support_eq_zeroLocus_fittingIdeal [Module.FinitePresentation R M] :
35     Module.support R M = PrimeSpectrum.zeroLocus (fittingIdeal R M 0 : Set R) := by
36   ext p
37   change p ∈ Module.support R M ↔ fittingIdeal R M 0 ≤ p.asIdeal
38   rw [fittingIdeal_le_prime_iff,
39     Module.mem_support_iff_nontrivial_residueField_tensorProduct,
40     Module.finrank_pos_iff]
41 
42 /-- Paper XII, Claim 6.4: all higher Fitting strata, including r above every generator bound. -/
43 theorem higherFittingStrata [Module.FinitePresentation R M] (r : ℕ) (hr : 1 ≤ r) :
44     {p : PrimeSpectrum R |
45       r ≤ Module.finrank p.asIdeal.ResidueField (p.asIdeal.ResidueField ⊗[R] M)} =
46       PrimeSpectrum.zeroLocus (fittingIdeal R M (r-1) : Set R) := by
47   ext p
48   change r ≤ Module.finrank p.asIdeal.ResidueField (p.asIdeal.ResidueField ⊗[R] M) ↔
49     fittingIdeal R M (r-1) ≤ p.asIdeal
50   rw [fittingIdeal_le_prime_iff]
51   omega
52 
53 /-- Claims 6.3 and 6.4 under exactly the manuscript's finite-Noetherian hypotheses. -/
54 theorem fitting_support_and_strata_noetherian [IsNoetherianRing R] [Module.Finite R M] :
55     let _ : Module.FinitePresentation R M := Module.finitePresentation_of_finite R M
56     Module.support R M = PrimeSpectrum.zeroLocus (fittingIdeal R M 0 : Set R) ∧
57     ∀ r : ℕ, 1 ≤ r →
58       {p : PrimeSpectrum R |
59         r ≤ Module.finrank p.asIdeal.ResidueField (p.asIdeal.ResidueField ⊗[R] M)} =
60         PrimeSpectrum.zeroLocus (fittingIdeal R M (r-1) : Set R) := by
61   let : Module.FinitePresentation R M := Module.finitePresentation_of_finite R M
62   exact ⟨support_eq_zeroLocus_fittingIdeal, higherFittingStrata⟩
63 
64 end PaperXII

Back to source controls