ComplexSupport.lean

1 import PaperXII.ComplexFieldFibers
2 import PaperXII.FieldFibers
3 import Mathlib.RingTheory.Spectrum.Prime.RingHom
4 
5 /-!
6 # Residue-field support of scalar-extended cochain models
7 
8 The fibers are objects in Mathlib's actual derived category. For bounded
9 projective models the construction is derived scalar extension, with model
10 independence established separately in `PerfectDerivedSupport`.
11 -/
12 
13 noncomputable section
14 
15 open CategoryTheory CategoryTheory.Limits
16 
17 universe u
18 
19 attribute [local instance] HasDerivedCategory.standard
20 
21 namespace PaperXII.ComplexSupport
22 
23 open ComplexBaseChange ComplexFieldFibers FieldFibers
24 
25 variable {R S T : Type u} [CommRing R] [CommRing S] [CommRing T]
26 
27 /-- The actual derived-category object of the specialized cochain model. -/
28 def fiber (f : R →+* S) (C : CochainComplex (ModuleCat.{u} R) ℤ) :
29     DerivedCategory (ModuleCat.{u} S) := DerivedCategory.Q.obj (baseChange f C)
30 
31 /-- Fiber composition is induced by the actual cochain tensor associator. -/
32 def fiberCompIso (f : R →+* S) (g : S →+* T)
33     (C : CochainComplex (ModuleCat.{u} R) ℤ) :
34     fiber g (baseChange f C) ≅ fiber (g.comp f) C :=
35   DerivedCategory.Q.mapIso (baseChangeCompIso f g C)
36 
37 /-- Nonvanishing of the actual residue-field specialization. -/
38 def support (C : CochainComplex (ModuleCat.{u} R) ℤ) : Set (PrimeSpectrum R) :=
39   {p | ¬IsZero (fiber (algebraMap R p.asIdeal.ResidueField) C)}
40 
41 /-- The support fills the spectrum of the coefficient ring. -/
42 def FullSupport (C : CochainComplex (ModuleCat.{u} R) ℤ) : Prop := support C = Set.univ
43 
44 /-- Every field-valued point detects precisely the residue-field support at its kernel. -/
45 theorem nonzero_fiber_iff_support {K : Type u} [Field K] (x : R →+* K)
46     (C : CochainComplex (ModuleCat.{u} R) ℤ) :
47     ¬IsZero (fiber x C) ↔ pointPrime x ∈ support C := by
48   let p := pointPrime x
49   let h := residueFieldLift x
50   have e := fiberCompIso (algebraMap R p.asIdeal.ResidueField) h C
51   have hx : h.comp (algebraMap R p.asIdeal.ResidueField) = x := residueFieldLift_comp x
52   rw [hx] at e
53   change ¬IsZero (fiber x C) ↔ ¬IsZero (fiber (algebraMap R p.asIdeal.ResidueField) C)
54   exact not_congr (e.isZero_iff.symm.trans
55     (isZero_baseChange_iff h (baseChange (algebraMap R p.asIdeal.ResidueField) C)))
56 
57 /-- The kernel of the residue-field point after a scalar map is the actual inverse-image prime. -/
58 theorem pointPrime_residue_comp (f : R →+* S) (q : PrimeSpectrum S) :
59     pointPrime ((algebraMap S q.asIdeal.ResidueField).comp f) = PrimeSpectrum.comap f q := by
60   ext r
61   change algebraMap S q.asIdeal.ResidueField (f r) = 0 ↔ f r ∈ q.asIdeal
62   exact Ideal.algebraMap_residueField_eq_zero
63 
64 /-- Support under arbitrary scalar extension, on actual corresponding primes. -/
65 theorem mem_support_baseChange_iff (f : R →+* S)
66     (C : CochainComplex (ModuleCat.{u} R) ℤ) (q : PrimeSpectrum S) :
67     q ∈ support (baseChange f C) ↔ PrimeSpectrum.comap f q ∈ support C := by
68   change ¬IsZero (fiber (algebraMap S q.asIdeal.ResidueField) (baseChange f C)) ↔ _
69   rw [(fiberCompIso f (algebraMap S q.asIdeal.ResidueField) C).isZero_iff]
70   rw [nonzero_fiber_iff_support, pointPrime_residue_comp]
71 
72 /-- Set form of the scalar-extension support identity. -/
73 theorem support_baseChange (f : R →+* S)
74     (C : CochainComplex (ModuleCat.{u} R) ℤ) :
75     support (baseChange f C) = PrimeSpectrum.comap f ⁻¹' support C := by
76   ext q
77   exact mem_support_baseChange_iff f C q
78 
79 /-- The ambient-spectrum equality for the actual ideal quotient. -/
80 theorem image_support_quotient (I : Ideal R)
81     (C : CochainComplex (ModuleCat.{u} R) ℤ) :
82     PrimeSpectrum.comap (Ideal.Quotient.mk I) '' support (baseChange (Ideal.Quotient.mk I) C) =
83       support C ∩ PrimeSpectrum.zeroLocus I := by
84   rw [support_baseChange, Set.image_preimage_eq_inter_range,
85     range_comap_of_surjective (R ⧸ I) (Ideal.Quotient.mk I)
86       Ideal.Quotient.mk_surjective, Ideal.mk_ker]
87 
88 /-- Full support survives arbitrary scalar extension. -/
89 theorem fullSupport_baseChange (f : R →+* S)
90     (C : CochainComplex (ModuleCat.{u} R) ℤ) (h : FullSupport C) :
91     FullSupport (baseChange f C) := by
92   unfold FullSupport at h ⊢
93   rw [support_baseChange, h, Set.preimage_univ]
94 
95 /-- Every field specialization of a full-support model is nonzero in the derived category. -/
96 theorem nonzero_fiber_of_fullSupport {K : Type u} [Field K] (x : R →+* K)
97     (C : CochainComplex (ModuleCat.{u} R) ℤ) (h : FullSupport C) :
98     ¬IsZero (fiber x C) := by
99   apply (nonzero_fiber_iff_support x C).mpr
100   rw [show support C = Set.univ from h]
101   trivial
102 
103 end PaperXII.ComplexSupport

Back to source controls