PerfectModels.lean

1 import Mathlib.Algebra.Homology.DerivedCategory.KProjective
2 import Mathlib.Algebra.Category.ModuleCat.Projective
3 import Mathlib.Algebra.Category.ModuleCat.Abelian
4 import Mathlib.RingTheory.Finiteness.Basic
5 import Mathlib.RingTheory.TensorProduct.Finite
6 import PaperXII.ComplexBaseChange
7 
8 /-!
9 # Bounded finite projective models
10 
11 These models contain actual cochain complexes.  Their derived objects are formed
12 using Mathlib's localization at quasi-isomorphisms.  A derived isomorphism between
13 such models is lifted to a homotopy equivalence, rather than assumed to survive
14 an arbitrary extension of scalars.
15 -/
16 
17 noncomputable section
18 
19 open CategoryTheory
20 
21 namespace PaperXII.PerfectModels
22 
23 universe u
24 
25 attribute [local instance] HasDerivedCategory.standard
26 
27 /-- A bounded complex whose terms are finitely generated projective modules. -/
28 structure PerfectModel (R : Type u) [CommRing R] where
29   complex : CochainComplex (ModuleCat.{u} R) ℤ
30   lower : ℤ
31   upper : ℤ
32   boundedBelow : complex.IsStrictlyGE lower
33   boundedAbove : complex.IsStrictlyLE upper
34   finite (i : ℤ) : Module.Finite R (complex.X i)
35   projective (i : ℤ) : Module.Projective R (complex.X i)
36 
37 attribute [instance] PerfectModel.boundedBelow PerfectModel.boundedAbove
38   PerfectModel.finite PerfectModel.projective
39 
40 variable {R : Type u} [CommRing R]
41 
42 /-- The object of the actual derived category represented by this model. -/
43 abbrev PerfectModel.derivedObject (P : PerfectModel R) : DerivedCategory (ModuleCat.{u} R) :=
44   DerivedCategory.Q.obj P.complex
45 
46 instance PerfectModel.isKProjective (P : PerfectModel R) : P.complex.IsKProjective :=
47   CochainComplex.isKProjective_of_projective P.complex P.upper
48 
49 /-- Full faithfulness on K-projective sources lifts an actual derived isomorphism
50 between two bounded projective models to an isomorphism in the homotopy category. -/
51 def homotopyCategoryIsoOfDerivedIso (P Q : PerfectModel R)
52     (e : P.derivedObject ≅ Q.derivedObject) :
53     (HomotopyCategory.quotient _ _).obj P.complex ≅
54       (HomotopyCategory.quotient _ _).obj Q.complex := by
55   let e' := (DerivedCategory.quotientCompQhIso (ModuleCat.{u} R)).app P.complex ≪≫ e ≪≫
56     ((DerivedCategory.quotientCompQhIso (ModuleCat.{u} R)).app Q.complex).symm
57   let hfExists := (CochainComplex.IsKProjective.Qh_map_bijective P.complex
58     ((HomotopyCategory.quotient _ _).obj Q.complex)).surjective e'.hom
59   let hgExists := (CochainComplex.IsKProjective.Qh_map_bijective Q.complex
60     ((HomotopyCategory.quotient _ _).obj P.complex)).surjective e'.inv
61   let f := Classical.choose hfExists
62   let g := Classical.choose hgExists
63   have hf : DerivedCategory.Qh.map f = e'.hom := Classical.choose_spec hfExists
64   have hg : DerivedCategory.Qh.map g = e'.inv := Classical.choose_spec hgExists
65   refine ⟨f, g, ?_, ?_⟩
66   · apply (CochainComplex.IsKProjective.Qh_map_bijective P.complex
67       ((HomotopyCategory.quotient _ _).obj P.complex)).injective
68     simp only [Functor.map_comp, hf, hg, Iso.hom_inv_id]
69     exact (DerivedCategory.Qh.map_id _).symm
70   · apply (CochainComplex.IsKProjective.Qh_map_bijective Q.complex
71       ((HomotopyCategory.quotient _ _).obj Q.complex)).injective
72     simp only [Functor.map_comp, hf, hg, Iso.inv_hom_id]
73     exact (DerivedCategory.Qh.map_id _).symm
74 
75 /-- Derived-isomorphic bounded projective models are genuinely homotopy equivalent. -/
76 def homotopyEquivOfDerivedIso (P Q : PerfectModel R)
77     (e : P.derivedObject ≅ Q.derivedObject) : HomotopyEquiv P.complex Q.complex :=
78   HomotopyCategory.homotopyEquivOfIso (homotopyCategoryIsoOfDerivedIso P Q e)
79 
80 /-- A homotopy equivalence gives an isomorphism of actual derived objects. -/
81 def derivedIsoOfHomotopyEquiv {C D : CochainComplex (ModuleCat.{u} R) ℤ}
82     (e : HomotopyEquiv C D) : DerivedCategory.Q.obj C ≅ DerivedCategory.Q.obj D :=
83   ((DerivedCategory.quotientCompQhIso (ModuleCat.{u} R)).app C).symm ≪≫
84     DerivedCategory.Qh.mapIso (HomotopyCategory.isoOfHomotopyEquiv e) ≪≫
85     (DerivedCategory.quotientCompQhIso (ModuleCat.{u} R)).app D
86 
87 variable {S : Type u} [CommRing S]
88 
89 /-- Finite generation survives arbitrary scalar extension. -/
90 theorem finite_extendScalars (f : R →+* S) (M : ModuleCat.{u} R)
91     [Module.Finite R M] : Module.Finite S ((ModuleCat.extendScalars f).obj M) := by
92   let : Algebra R S := f.toAlgebra
93   change Module.Finite S (TensorProduct R S M)
94   infer_instance
95 
96 /-- Projectivity survives arbitrary scalar extension. -/
97 theorem projective_extendScalars (f : R →+* S) (M : ModuleCat.{u} R)
98     [Module.Projective R M] : Module.Projective S ((ModuleCat.extendScalars f).obj M) := by
99   let : Algebra R S := f.toAlgebra
100   change Module.Projective S (TensorProduct R S M)
101   infer_instance
102 
103 /-- Extension of scalars preserves the entire bounded finite-projective class. -/
104 def PerfectModel.baseChange (P : PerfectModel R) (f : R →+* S) : PerfectModel S where
105   complex := ComplexBaseChange.baseChange f P.complex
106   lower := P.lower
107   upper := P.upper
108   boundedBelow := by dsimp [ComplexBaseChange.baseChange, ComplexBaseChange.complexFunctor]; infer_instance
109   boundedAbove := by dsimp [ComplexBaseChange.baseChange, ComplexBaseChange.complexFunctor]; infer_instance
110   finite i := finite_extendScalars f (P.complex.X i)
111   projective i := projective_extendScalars f (P.complex.X i)
112 
113 /-- Independence of the projective model after arbitrary scalar extension.
114 The given isomorphism is in Mathlib's actual derived category; its homotopy lift
115 is preserved before taking the target derived category. No flatness is assumed. -/
116 def baseChange_derivedIso (f : R →+* S) (P Q : PerfectModel R)
117     (e : P.derivedObject ≅ Q.derivedObject) :
118     (P.baseChange f).derivedObject ≅ (Q.baseChange f).derivedObject :=
119   derivedIsoOfHomotopyEquiv
120     (ComplexBaseChange.baseChangeHomotopyEquiv f (homotopyEquivOfDerivedIso P Q e))
121 
122 end PaperXII.PerfectModels

Back to source controls