ComplexBaseChange.lean

1 import Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
2 import Mathlib.Algebra.Category.ModuleCat.Abelian
3 import Mathlib.Algebra.Homology.Homotopy
4 
5 /-!
6 # Scalar extension of actual cochain complexes
7 
8 The functor below applies module scalar extension in every degree. Its
9 composition isomorphism is induced by the module tensor associator, including
10 its compatibility with the differentials. For a projective complex this is
11 the model used for derived scalar extension in `PerfectModels`.
12 -/
13 
14 noncomputable section
15 
16 open CategoryTheory
17 
18 universe u
19 
20 namespace PaperXII.ComplexBaseChange
21 
22 variable {R S T : Type u} [CommRing R] [CommRing S] [CommRing T]
23 
24 /-- Tensor extension is additive on module morphisms. -/
25 instance extendScalarsAdditive (f : R →+* S) :
26     (ModuleCat.extendScalars.{u, u, u} f).Additive := by
27   let := Limits.preservesBinaryBiproducts_of_preservesBinaryCoproducts
28     (ModuleCat.extendScalars.{u, u, u} f)
29   exact Functor.additive_of_preservesBinaryBiproducts (ModuleCat.extendScalars.{u, u, u} f)
30 
31 /-- Degreewise tensor extension, with the induced differentials. -/
32 abbrev complexFunctor (f : R →+* S) :
33     CochainComplex (ModuleCat.{u} R) ℤ ⥤ CochainComplex (ModuleCat.{u} S) ℤ :=
34   (ModuleCat.extendScalars f).mapHomologicalComplex (.up ℤ)
35 
36 /-- The actual specialized cochain complex. -/
37 abbrev baseChange (f : R →+* S) (K : CochainComplex (ModuleCat.{u} R) ℤ) :=
38   (complexFunctor f).obj K
39 
40 /-- The module in degree `n` is the scalar extension of that degree. -/
41 theorem baseChange_X (f : R →+* S) (K : CochainComplex (ModuleCat.{u} R) ℤ) (n : ℤ) :
42     (baseChange f K).X n = (ModuleCat.extendScalars f).obj (K.X n) := rfl
43 
44 /-- The specialized differential is obtained from the original differential. -/
45 theorem baseChange_d (f : R →+* S) (K : CochainComplex (ModuleCat.{u} R) ℤ) (i j : ℤ) :
46     (baseChange f K).d i j = (ModuleCat.extendScalars f).map (K.d i j) := rfl
47 
48 /-- Scalar extension by a composite agrees with successive scalar extensions. -/
49 def complexFunctorCompIso (f : R →+* S) (g : S →+* T) :
50     complexFunctor f ⋙ complexFunctor g ≅ complexFunctor (g.comp f) :=
51   Functor.mapHomologicalComplexCompIso (ModuleCat.extendScalarsComp f g).symm (.up ℤ)
52 
53 /-- The actual tensor association isomorphism, including all differentials. -/
54 def baseChangeCompIso (f : R →+* S) (g : S →+* T)
55     (K : CochainComplex (ModuleCat.{u} R) ℤ) :
56     baseChange g (baseChange f K) ≅ baseChange (g.comp f) K :=
57   (complexFunctorCompIso f g).app K
58 
59 /-- The tensor association isomorphism commutes with every cochain map. -/
60 theorem baseChangeCompIso_naturality (f : R →+* S) (g : S →+* T)
61     {K L : CochainComplex (ModuleCat.{u} R) ℤ} (φ : K ⟶ L) :
62     (complexFunctor g).map ((complexFunctor f).map φ) ≫
63       (baseChangeCompIso f g L).hom =
64     (baseChangeCompIso f g K).hom ≫ (complexFunctor (g.comp f)).map φ :=
65   (complexFunctorCompIso f g).hom.naturality φ
66 
67 /-- Scalar extension by the identity recovers the original complex. -/
68 def baseChangeIdIso (K : CochainComplex (ModuleCat.{u} R) ℤ) :
69     baseChange (RingHom.id R) K ≅ K :=
70   ((NatIso.mapHomologicalComplex (ModuleCat.extendScalarsId R) (.up ℤ)) ≪≫
71     Functor.mapHomologicalComplexIdIso (ModuleCat.{u} R) (.up ℤ)).app K
72 
73 /-- Every module scalar extension preserves a supplied cochain homotopy. -/
74 def baseChangeHomotopy (f : R →+* S)
75     {K L : CochainComplex (ModuleCat.{u} R) ℤ} {φ ψ : K ⟶ L}
76     (h : Homotopy φ ψ) :
77     Homotopy ((complexFunctor f).map φ) ((complexFunctor f).map ψ) :=
78   (ModuleCat.extendScalars f).mapHomotopy h
79 
80 /-- Arbitrary scalar extension preserves homotopy equivalence, without flatness. -/
81 def baseChangeHomotopyEquiv (f : R →+* S)
82     {K L : CochainComplex (ModuleCat.{u} R) ℤ} (h : HomotopyEquiv K L) :
83     HomotopyEquiv (baseChange f K) (baseChange f L) :=
84   (ModuleCat.extendScalars f).mapHomotopyEquiv h
85 
86 end PaperXII.ComplexBaseChange

Back to source controls