DerivedPatching.lean

1 import PaperXII.PerfectDerivedSupport
2 import Mathlib.RingTheory.Noetherian.Basic
3 
4 /-!
5 # Derived patching support and surviving cohomology
6 
7 The input is exactly an ideal quotient ring identification and an actual
8 isomorphism in the derived category. No pointwise fiber identification,
9 nonvanishing conclusion, or cohomology comparison is assumed.
10 -/
11 
12 noncomputable section
13 
14 open CategoryTheory CategoryTheory.Limits
15 
16 universe u
17 
18 attribute [local instance] HasDerivedCategory.standard
19 
20 namespace PaperXII.DerivedPatching
21 
22 open PerfectDerivedSupport
23 
24 variable {A R : Type u} [CommRing A] [CommRing R]
25 
26 /-- The actual coefficient specialization determined by the quotient identification. -/
27 def quotientScalar (I : Ideal A) (e : (A ⧸ I) ≃+* R) : A →+* R :=
28   e.toRingHom.comp (Ideal.Quotient.mk I)
29 
30 /-- The specialization is surjective. -/
31 theorem quotientScalar_surjective (I : Ideal A) (e : (A ⧸ I) ≃+* R) :
32     Function.Surjective (quotientScalar I e) :=
33   e.surjective.comp Ideal.Quotient.mk_surjective
34 
35 /-- Its kernel is the declared patching ideal, not an additional condition. -/
36 theorem quotientScalar_ker (I : Ideal A) (e : (A ⧸ I) ≃+* R) :
37     RingHom.ker (quotientScalar I e) = I := by
38   ext a
39   change e (Ideal.Quotient.mk I a) = 0 ↔ a ∈ I
40   rw [map_eq_zero_iff e e.injective, Ideal.Quotient.eq_zero_iff_mem]
41 
42 /-- Original Definition 6.17, with an arbitrary finite-level derived object. -/
43 structure Datum (A R : Type u) [CommRing A] [CommRing R] where
44   noetherian : IsNoetherianRing A
45   ideal : Ideal A
46   coefficient : (A ⧸ ideal) ≃+* R
47   patched : PerfectComplex A
48   finiteLevel : DerivedCategory (ModuleCat.{u} R)
49   comparison : finiteLevel ≅ (patched.baseChange (quotientScalar ideal coefficient)).object
50 
51 /-- The finite-level perfect model is constructed from the supplied derived identification. -/
52 def Datum.finitePerfect (D : Datum A R) : PerfectComplex R where
53   object := D.finiteLevel
54   model := D.patched.model.baseChange (quotientScalar D.ideal D.coefficient)
55   modelIso := D.comparison.symm
56 
57 /-- The constructed perfect object has the literal finite-level derived object. -/
58 theorem finitePerfect_object (D : Datum A R) : D.finitePerfect.object = D.finiteLevel := rfl
59 
60 /-- Full patched support descends using the actual derived comparison. -/
61 theorem fullSupport_descends (D : Datum A R) (h : FullSupport D.patched) :
62     FullSupport D.finitePerfect := by
63   unfold FullSupport
64   rw [support_eq_of_iso D.comparison]
65   exact fullSupport_baseChange D.patched (quotientScalar D.ideal D.coefficient) h
66 
67 /-- Every field-valued finite-level fiber is nonzero in the actual derived category. -/
68 theorem derived_fiber_nonzero {K : Type u} [Field K] (D : Datum A R)
69     (h : FullSupport D.patched) (x : R →+* K) :
70     ¬IsZero (D.finitePerfect.baseChange x).object :=
71   nonzero_fiber_of_fullSupport D.finitePerfect x (fullSupport_descends D h)
72 
73 /-- Original Theorem 6.18: full finite-level support and all nonzero field fibers. -/
74 theorem derived_support_descent (D : Datum A R) (h : FullSupport D.patched) :
75     FullSupport D.finitePerfect ∧
76       ∀ (K : Type u) [Field K] (x : R →+* K), ¬IsZero (D.finitePerfect.baseChange x).object := by
77   exact ⟨fullSupport_descends D h, fun _ _ x => derived_fiber_nonzero D h x⟩
78 
79 /-- Original Corollary 6.19, using Mathlib's actual derived cohomology functor. -/
80 theorem derived_degree_survives {K : Type u} [Field K] (D : Datum A R)
81     (h : FullSupport D.patched) (x : R →+* K) :
82     ∃ n : ℤ, ¬IsZero ((DerivedCategory.homologyFunctor (ModuleCat K) n).obj
83       (D.finitePerfect.baseChange x).object) :=
84   exists_nonzero_cohomology D.finitePerfect x (derived_fiber_nonzero D h x)
85 
86 /-- The surviving cohomology can also be read in the actual specialized projective model. -/
87 theorem model_degree_survives {K : Type u} [Field K] (D : Datum A R)
88     (h : FullSupport D.patched) (x : R →+* K) :
89     ∃ n : ℤ, ¬IsZero ((D.finitePerfect.baseChange x).model.complex.homology n) :=
90   exists_nonzero_model_cohomology D.finitePerfect x (derived_fiber_nonzero D h x)
91 
92 end PaperXII.DerivedPatching

Back to source controls