ComplexFieldFibers.lean

1 import PaperXII.ComplexBaseChange
2 import Mathlib.Algebra.Homology.DerivedCategory.HomologySequence
3 import Mathlib.Algebra.Homology.ShortComplex.ModuleCat
4 import Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
5 import Mathlib.LinearAlgebra.Basis.VectorSpace
6 
7 /-!
8 # Field extension detects cohomology and derived nonvanishing
9 
10 These statements use actual cochain complexes and the localization functor to
11 Mathlib's derived category. Reflection is proved through faithful flatness of
12 a field extension; no homology comparison or nonvanishing axiom is assumed.
13 -/
14 
15 noncomputable section
16 
17 open CategoryTheory CategoryTheory.Limits
18 open PaperXII.ComplexBaseChange
19 
20 universe u
21 
22 attribute [local instance] HasDerivedCategory.standard
23 
24 namespace PaperXII.ComplexFieldFibers
25 
26 variable {R : Type u} [CommRing R]
27 
28 /-- A derived object vanishes exactly when all its actual cohomology objects vanish. -/
29 theorem derived_isZero_iff_homology (D : DerivedCategory (ModuleCat.{u} R)) :
30     IsZero D ↔ ∀ n : ℤ, IsZero ((DerivedCategory.homologyFunctor (ModuleCat R) n).obj D) := by
31   constructor
32   · intro h n
33     exact (DerivedCategory.homologyFunctor (ModuleCat R) n).map_isZero h
34   · intro h
35     have hz : IsIso (0 : D ⟶ D) := by
36       rw [DerivedCategory.isIso_iff]
37       intro n
38       rw [Functor.map_zero]
39       exact (isIsoZero_iff_source_target_isZero _ _).mpr ⟨h n, h n⟩
40     exact ((isIsoZero_iff_source_target_isZero _ _).mp hz).1
41 
42 /-- Localization kills precisely the acyclic cochain complexes. -/
43 theorem isZero_Q_iff_acyclic (C : CochainComplex (ModuleCat.{u} R) ℤ) :
44     IsZero (DerivedCategory.Q.obj C) ↔ C.Acyclic := by
45   rw [derived_isZero_iff_homology, HomologicalComplex.acyclic_iff]
46   apply forall_congr'
47   intro n
48   rw [HomologicalComplex.exactAt_iff_isZero_homology]
49   exact ((DerivedCategory.homologyFunctorFactors (ModuleCat R) n).app C).isZero_iff
50 
51 /-- Nonzero derived complexes have a nonzero cohomology object in some degree. -/
52 theorem exists_nonzero_homology_of_not_isZero
53     (C : CochainComplex (ModuleCat.{u} R) ℤ) (h : ¬ IsZero (DerivedCategory.Q.obj C)) :
54     ∃ n : ℤ, ¬ IsZero (C.homology n) := by
55   contrapose! h
56   rw [isZero_Q_iff_acyclic, HomologicalComplex.acyclic_iff]
57   intro n
58   exact (HomologicalComplex.exactAt_iff_isZero_homology C n).mpr (h n)
59 
60 /-- A nonzero cohomology object witnesses nonvanishing in the derived category. -/
61 theorem not_isZero_Q_iff_exists_nonzero_homology
62     (C : CochainComplex (ModuleCat.{u} R) ℤ) :
63     ¬ IsZero (DerivedCategory.Q.obj C) ↔ ∃ n : ℤ, ¬ IsZero (C.homology n) := by
64   constructor
65   · exact exists_nonzero_homology_of_not_isZero C
66   · rintro ⟨n, hn⟩ h
67     exact hn (((isZero_Q_iff_acyclic C).mp h n).isZero_homology)
68 
69 variable {k K : Type u} [Field k] [Field K]
70 
71 /-- Extending the coefficient field preserves and reflects exactness in every degree. -/
72 theorem exactAt_baseChange_iff (f : k →+* K)
73     (C : CochainComplex (ModuleCat.{u} k) ℤ) (n : ℤ) :
74     (baseChange f C).ExactAt n ↔ C.ExactAt n := by
75   let : Algebra k K := f.toAlgebra
76   rw [HomologicalComplex.exactAt_iff, HomologicalComplex.exactAt_iff,
77     ShortComplex.ShortExact.moduleCat_exact_iff_function_exact,
78     ShortComplex.ShortExact.moduleCat_exact_iff_function_exact]
79   change Function.Exact ((C.sc n).f.hom.lTensor K) ((C.sc n).g.hom.lTensor K) ↔
80     Function.Exact (C.sc n).f.hom (C.sc n).g.hom
81   exact Module.FaithfullyFlat.lTensor_exact_iff_exact k K _ _
82 
83 /-- A field extension preserves and reflects acyclicity of arbitrary cochain complexes. -/
84 theorem acyclic_baseChange_iff (f : k →+* K)
85     (C : CochainComplex (ModuleCat.{u} k) ℤ) :
86     (baseChange f C).Acyclic ↔ C.Acyclic := by
87   simp only [HomologicalComplex.acyclic_iff, exactAt_baseChange_iff]
88 
89 /-- A field extension preserves and reflects zero objects after actual derived localization. -/
90 theorem isZero_baseChange_iff (f : k →+* K)
91     (C : CochainComplex (ModuleCat.{u} k) ℤ) :
92     IsZero (DerivedCategory.Q.obj (baseChange f C)) ↔ IsZero (DerivedCategory.Q.obj C) := by
93   rw [isZero_Q_iff_acyclic, isZero_Q_iff_acyclic, acyclic_baseChange_iff]
94 
95 /-- Derived nonvanishing survives every extension of the coefficient field. -/
96 theorem not_isZero_baseChange_iff (f : k →+* K)
97     (C : CochainComplex (ModuleCat.{u} k) ℤ) :
98     ¬ IsZero (DerivedCategory.Q.obj (baseChange f C)) ↔ ¬ IsZero (DerivedCategory.Q.obj C) :=
99   not_congr (isZero_baseChange_iff f C)
100 
101 /-- Each individual cohomology degree vanishes after field extension exactly when it did before. -/
102 theorem homology_isZero_baseChange_iff (f : k →+* K)
103     (C : CochainComplex (ModuleCat.{u} k) ℤ) (n : ℤ) :
104     IsZero ((baseChange f C).homology n) ↔ IsZero (C.homology n) := by
105   rw [← HomologicalComplex.exactAt_iff_isZero_homology,
106     ← HomologicalComplex.exactAt_iff_isZero_homology, exactAt_baseChange_iff]
107 
108 end PaperXII.ComplexFieldFibers

Back to source controls