feat(Algebra/Homology): functoriality of extMk with respect to the injective resolution (leanprover-community#33360)

The dual statement for projective resolutions is also obtained.

Author: joelriou

Mathlib/Algebra/Homology/HomotopyCategory/HomComplexSingle.lean

@@ -114,6 +114,12 @@ lemma fromSingleMk_precomp
   apply (fromSingleEquiv h).injective
   simp [fromSingleEquiv, singleFunctor, singleFunctors, HomologicalComplex.single_map_f_self]
 
+lemma fromSingleMk_postcomp {p q : ℤ} (f : X ⟶ K.X q) {n : ℤ} (h : p + n = q)
+    {L : CochainComplex C ℤ} (g : K ⟶ L) :
+    fromSingleMk (f ≫ g.f q) h =
+      (fromSingleMk f h).comp (.ofHom g) (add_zero n) :=
+  (fromSingleEquiv h).injective (by simp [fromSingleEquiv, singleFunctor, singleFunctors])
+
 /-- Constructor for cochains to a single complex. -/
 @[nolint unusedArguments]
 noncomputable def toSingleMk {p q : ℤ} (f : K.X p ⟶ X) {n : ℤ} (_ : p + n = q) :
@@ -192,6 +198,13 @@ lemma toSingleMk_postcomp
   apply (toSingleEquiv h).injective
   simp [toSingleEquiv, singleFunctor, singleFunctors, HomologicalComplex.single_map_f_self]
 
+lemma toSingleMk_precomp
+    {p q : ℤ} (f : K.X p ⟶ X) {n : ℤ} (h : p + n = q)
+    {L : CochainComplex C ℤ} (g : L ⟶ K) :
+    toSingleMk (g.f p ≫ f) h =
+      (Cochain.ofHom g).comp (toSingleMk f h) (zero_add n) :=
+  (toSingleEquiv h).injective (by simp [toSingleEquiv, singleFunctor, singleFunctors])
+
 end Cochain
 
 namespace Cocycle
@@ -212,6 +225,14 @@ lemma fromSingleMk_precomp {X' : C} (g : X' ⟶ X) {p q : ℤ} (f : X ⟶ K.X q)
   ext : 1
   exact (Cochain.fromSingleEquiv h).injective (by simp [Cochain.fromSingleMk_precomp])
 
+lemma fromSingleMk_postcomp {p q : ℤ} (f : X ⟶ K.X q) {n : ℤ} (h : p + n = q)
+    (q' : ℤ) (hq' : q + 1 = q') (hf : f ≫ K.d q q' = 0) {L : CochainComplex C ℤ}
+    (g : K ⟶ L) :
+    fromSingleMk (f ≫ g.f q) h q' hq' (by simp [reassoc_of% hf]) =
+      (fromSingleMk f h q' hq' hf).postcomp g := by
+  ext : 1
+  exact (Cochain.fromSingleEquiv h).injective (by simp [Cochain.fromSingleMk_postcomp])
+
 lemma fromSingleMk_surjective {p n : ℤ} (α : Cocycle ((singleFunctor C p).obj X) K n)
     (q : ℤ) (h : p + n = q) (q' : ℤ) (hq' : q + 1 = q') :
     ∃ (f : X ⟶ K.X q) (hf : f ≫ K.d q q' = 0), fromSingleMk f h q' hq' hf = α := by
@@ -276,6 +297,15 @@ lemma toSingleMk_postcomp {p q : ℤ} (f : K.X p ⟶ X) {n : ℤ} (h : p + n = q
   ext : 1
   exact (Cochain.toSingleEquiv h).injective (by simp [Cochain.toSingleMk_postcomp])
 
+lemma toSingleMk_precomp
+    {p q : ℤ} (f : K.X p ⟶ X) {n : ℤ} (h : p + n = q)
+    (p' : ℤ) (hp' : p' + 1 = p) (hf : K.d p' p ≫ f = 0)
+    {L : CochainComplex C ℤ} (g : L ⟶ K) :
+    toSingleMk (g.f p ≫ f) h p' hp' (by simp [← g.comm_assoc, hf]) =
+      (toSingleMk f h p' hp' hf).precomp g := by
+  ext : 1
+  exact (Cochain.toSingleEquiv h).injective (by simp [Cochain.toSingleMk_precomp])
+
 lemma toSingleMk_surjective {q n : ℤ} (α : Cocycle K ((singleFunctor C q).obj X) n)
     (p : ℤ) (h : p + n = q) (p' : ℤ) (hp' : p' + 1 = p) :
     ∃ (f : K.X p ⟶ X) (hf : K.d p' p ≫ f = 0), toSingleMk f h p' hp' hf = α := by

Mathlib/CategoryTheory/Abelian/Injective/Ext.lean

@@ -19,13 +19,6 @@ Given an injective resolution `R` of an object `Y` in an abelian category `C`,
 we provide an API in order to construct elements in `Ext X Y n` in terms
 of the complex `R.cocomplex` and to make computations in the `Ext`-group.
 
-## TODO
-* Functoriality in `Y`: this would involve a morphism `Y ⟶ Y'`, injective
-resolutions `R` and `R'` of `Y` and `Y'`, a lift of `Y ⟶ Y'` as a morphism
-of cochain complexes `R.cocomplex ⟶ R'.cocomplex`; in this context,
-we should be able to compute the postcomposition of an element
-`R.extMk f m hm hf : Ext X Y n` by `Y ⟶ Y'`.
-
 -/
 
 @[expose] public section
@@ -182,6 +175,19 @@ lemma extMk_zero {n : ℕ} (m : ℕ) (hm : n + 1 = m) :
     R.extMk (0 : X ⟶ R.cocomplex.X n) m hm (by simp) = 0 := by
   simp [extMk]
 
+lemma extMk_hom
+    [HasDerivedCategory C] {n : ℕ} (f : X ⟶ R.cocomplex.X n) (m : ℕ) (hm : n + 1 = m)
+    (hf : f ≫ R.cocomplex.d n m = 0) :
+    (R.extMk f m hm hf).hom =
+    (ShiftedHom.mk₀ _ rfl ((DerivedCategory.singleFunctorIsoCompQ C 0).hom.app X)).comp
+      ((ShiftedHom.map (Cocycle.equivHomShift.symm
+        (Cocycle.fromSingleMk (f ≫ (R.cochainComplexXIso n n rfl).inv) (zero_add _) m
+          (by lia) (by simp [cochainComplex_d _ _ _ n m rfl rfl, reassoc_of% hf]))) _).comp
+            (.mk₀ _ rfl (inv (DerivedCategory.Q.map R.ι') ≫
+              (DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y))
+                (zero_add _)) (add_zero _) :=
+  extEquivCohomologyClass_symm_mk_hom _ _
+
 lemma extMk_eq_zero_iff (f : X ⟶ R.cocomplex.X n) (m : ℕ) (hm : n + 1 = m)
     (hf : f ≫ R.cocomplex.d n m = 0)
     (p : ℕ) (hp : p + 1 = n) :
@@ -222,4 +228,30 @@ lemma mk₀_comp_extMk {n : ℕ} (f : X ⟶ R.cocomplex.X n) (m : ℕ) (hm : n +
     ← ShiftedHom.comp_assoc _ _ _ (add_zero _) (add_zero (n : ℤ)) (by simp)]
   simp
 
+variable {R} in
+lemma extMk_comp_mk₀ {n : ℕ} (f : X ⟶ R.cocomplex.X n) (m : ℕ) (hm : n + 1 = m)
+    (hf : f ≫ R.cocomplex.d n m = 0)
+    {Y' : C} {R' : InjectiveResolution Y'} {g : Y ⟶ Y'} (φ : Hom R R' g) :
+    (R.extMk f m hm hf).comp (Ext.mk₀ g) (add_zero _) =
+      R'.extMk (f ≫ φ.hom.f n) m hm (by simp [reassoc_of% hf]) := by
+  have := HasDerivedCategory.standard C
+  ext
+  have : (f ≫ φ.hom.f n) ≫ (R'.cochainComplexXIso n n (by lia)).inv =
+      (f ≫ (R.cochainComplexXIso n n (by lia)).inv) ≫ φ.hom'.f n := by
+    simp [φ.hom'_f n n rfl]
+  simp only [Ext.comp_hom, extMk_hom, Ext.mk₀_hom, this]
+  rw [Cocycle.fromSingleMk_postcomp _ (zero_add _) _ (by lia)
+      (by simp [R.cochainComplex_d _ _ _ _ rfl rfl, reassoc_of% hf]),
+    Cocycle.equivHomShift_symm_postcomp,
+    ← ShiftedHom.comp_mk₀ _ 0 rfl, ShiftedHom.map_comp,
+    ShiftedHom.comp_assoc _ _ _ _ (zero_add _) (by simp),
+    ShiftedHom.comp_assoc _ _ _ _ (zero_add _) (by simp),
+    ShiftedHom.comp_assoc _ _ _ _ (zero_add _) (by simp),
+    ShiftedHom.map_mk₀, ShiftedHom.mk₀_comp_mk₀, ShiftedHom.mk₀_comp_mk₀]
+  congr 3
+  rw [Category.assoc, ← NatTrans.naturality, ← Category.assoc, ← Category.assoc]
+  congr 1
+  simpa only [IsIso.eq_comp_inv, Category.assoc, IsIso.inv_comp_eq,
+    Functor.map_comp] using DerivedCategory.Q.congr_map φ.ι'_comp_hom'.symm
+
 end CategoryTheory.InjectiveResolution

Mathlib/CategoryTheory/Abelian/Injective/Extend.lean

@@ -91,6 +91,35 @@ instance : R.cochainComplex.IsLE 0 := by
   simp only [← HomologicalComplex.isSupported_iff_of_quasiIso R.ι']
   infer_instance
 
+namespace Hom
+
+variable {R} {X' : C} {R' : InjectiveResolution X'} {f : X ⟶ X'}
+  (φ : Hom R R' f)
+
+/-- The morphism on cochain complexes indexed by `ℤ` that is induced by
+an (heterogeneous) morphism of injective resolutions. -/
+noncomputable def hom' : R.cochainComplex ⟶ R'.cochainComplex :=
+  HomologicalComplex.extendMap φ.hom _
+
+@[reassoc]
+lemma hom'_f (n : ℤ) (m : ℕ) (h : m = n) :
+    φ.hom'.f n =
+    (R.cochainComplexXIso n m h).hom ≫ φ.hom.f m ≫ (R'.cochainComplexXIso n m h).inv := by
+  simp [hom', HomologicalComplex.extendMap_f _
+    ComplexShape.embeddingUpNat (i := m) (i' := n) (by simpa),
+    cochainComplexXIso]
+
+@[reassoc (attr := simp)]
+lemma ι'_comp_hom' :
+    R.ι' ≫ φ.hom' = (CochainComplex.singleFunctor C 0).map f ≫ R'.ι' :=
+  HomologicalComplex.from_single_hom_ext (by
+    simp [hom'_f _ 0 0 rfl, ι'_f_zero, CochainComplex.singleFunctor,
+      CochainComplex.singleFunctors,
+      HomologicalComplex.single, HomologicalComplex.singleObjXSelf,
+      HomologicalComplex.singleObjXIsoOfEq])
+
+end Hom
+
 end InjectiveResolution
 
 end CategoryTheory

Mathlib/CategoryTheory/Abelian/Projective/Ext.lean

@@ -182,6 +182,19 @@ lemma extMk_zero {n : ℕ} (m : ℕ) (hm : n + 1 = m) :
     R.extMk (0 : R.complex.X n ⟶ Y) m hm (by simp) = 0 := by
   simp [extMk]
 
+lemma extMk_hom
+    [HasDerivedCategory C] {n : ℕ} (f : R.complex.X n ⟶ Y) (m : ℕ) (hm : n + 1 = m)
+    (hf : R.complex.d m n ≫ f = 0) :
+    (R.extMk f m hm hf).hom =
+    (ShiftedHom.mk₀ _ rfl ((DerivedCategory.singleFunctorIsoCompQ C 0).hom.app X ≫
+      inv (DerivedCategory.Q.map R.π'))).comp
+        ((ShiftedHom.map (Cocycle.equivHomShift.symm
+          (Cocycle.toSingleMk ((R.cochainComplexXIso (-n) n rfl).hom ≫ f) (by simp) (-m)
+            (by lia) (by simpa [cochainComplex_d _ _ _ _ _ rfl rfl]))) _).comp
+              (.mk₀ _ rfl ((DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y))
+                (zero_add _)) (add_zero _) :=
+  extEquivCohomologyClass_symm_mk_hom _ _
+
 lemma extMk_eq_zero_iff (f : R.complex.X n ⟶ Y) (m : ℕ) (hm : n + 1 = m)
     (hf : R.complex.d m n ≫ f = 0)
     (p : ℕ) (hp : p + 1 = n) :
@@ -227,4 +240,28 @@ lemma extMk_comp_mk₀ {n : ℕ} (f : R.complex.X n ⟶ Y) (m : ℕ) (hm : n + 1
     ShiftedHom.mk₀_comp_mk₀, ShiftedHom.mk₀_comp_mk₀, ← NatTrans.naturality]
   dsimp
 
+variable {R} in
+lemma mk₀_comp_extMk {n : ℕ} (f : R.complex.X n ⟶ Y) (m : ℕ) (hm : n + 1 = m)
+    (hf : R.complex.d m n ≫ f = 0)
+    {X' : C} {R' : ProjectiveResolution X'} {g : X' ⟶ X} (φ : Hom R' R g) :
+    (Ext.mk₀ g).comp (R.extMk f m hm hf) (zero_add _) =
+      R'.extMk (φ.hom.f n ≫ f) m hm (by simp [← φ.hom.comm_assoc, hf]) := by
+  have := HasDerivedCategory.standard C
+  ext
+  have : (R'.cochainComplexXIso (-n) n (by lia)).hom ≫ φ.hom.f n =
+      φ.hom'.f (-n) ≫ (R.cochainComplexXIso (-n) n (by lia)).hom := by
+    simp [φ.hom'_f _ _ rfl]
+  simp only [Ext.comp_hom, extMk_hom, Ext.mk₀_hom, reassoc_of% this]
+  rw [Cocycle.toSingleMk_precomp _ _ _ (by lia)
+    (by simpa [R.cochainComplex_d _ _ _ _ rfl rfl]),
+    Cocycle.equivHomShift_symm_precomp,
+    ← ShiftedHom.mk₀_comp 0 rfl, ShiftedHom.map_comp,
+    ← ShiftedHom.comp_assoc _ _ _ (zero_add _) _ (by simp),
+    ← ShiftedHom.comp_assoc _ _ _ (add_zero _) _ (by simp),
+    ← ShiftedHom.comp_assoc _ _ _ (add_zero _) _ (by simp),
+    ← ShiftedHom.comp_assoc _ _ _ (zero_add _) _ (by simp),
+    ShiftedHom.map_mk₀, ShiftedHom.mk₀_comp_mk₀, ShiftedHom.mk₀_comp_mk₀]
+  congr 3
+  simp [← Functor.map_comp_assoc, ← Functor.map_comp]
+
 end CategoryTheory.ProjectiveResolution

Mathlib/CategoryTheory/Abelian/Projective/Extend.lean

@@ -87,6 +87,35 @@ instance : R.cochainComplex.IsGE 0 := by
   simp only [HomologicalComplex.isSupported_iff_of_quasiIso R.π']
   infer_instance
 
+namespace Hom
+
+variable {R} {X' : C} {R' : ProjectiveResolution X'} {f : X ⟶ X'}
+  (φ : Hom R R' f)
+
+/-- The morphism on cochain complexes indexed by `ℤ` that is induced by
+a (heterogeneous) morphism of projective resolutions. -/
+noncomputable def hom' : R.cochainComplex ⟶ R'.cochainComplex :=
+  HomologicalComplex.extendMap φ.hom _
+
+@[reassoc]
+lemma hom'_f (n : ℤ) (m : ℕ) (h : -m = n) :
+    φ.hom'.f n =
+    (R.cochainComplexXIso n m h).hom ≫ φ.hom.f m ≫ (R'.cochainComplexXIso n m h).inv := by
+  simp [hom', HomologicalComplex.extendMap_f _
+    ComplexShape.embeddingDownNat (i := m) (i' := n) (by dsimp; lia),
+    cochainComplexXIso]
+
+@[reassoc (attr := simp)]
+lemma hom'_comp_π' :
+    φ.hom' ≫ R'.π' = R.π' ≫ (CochainComplex.singleFunctor C 0).map f :=
+  HomologicalComplex.to_single_hom_ext (by
+    simp [hom'_f _ 0 0 rfl, π'_f_zero, CochainComplex.singleFunctor,
+      CochainComplex.singleFunctors,
+      HomologicalComplex.single, HomologicalComplex.singleObjXSelf,
+      HomologicalComplex.singleObjXIsoOfEq])
+
+end Hom
+
 end ProjectiveResolution
 
 end CategoryTheory

Mathlib/CategoryTheory/Preadditive/Injective/Resolution.lean

@@ -138,6 +138,27 @@ def self [Injective Z] : InjectiveResolution Z where
       apply HomologicalComplex.isZero_single_obj_X
       simp
 
+variable {Z} {Z' : C} (I' : InjectiveResolution Z')
+
+/-- Given injective resolutions `I` and `I'` of two objects `Z` and `Z'`,
+and a morphism `f : Z ⟶ Z'`, this structure contains the data of a morphism
+`I.cocomplex ⟶ I'.cocomplex` which is compatible with `f` -/
+structure Hom (f : Z ⟶ Z') where
+  /-- A morphism between the cocomplexes -/
+  hom : I.cocomplex ⟶ I'.cocomplex
+  ι_f_zero_comp_hom_f_zero : I.ι.f 0 ≫ hom.f 0 = ((single₀ C).map f).f 0 ≫ I'.ι.f 0
+
+namespace Hom
+
+attribute [reassoc (attr := simp)] ι_f_zero_comp_hom_f_zero
+
+variable {I I'} in
+@[reassoc (attr := simp)]
+lemma ι_comp_hom {f : Z ⟶ Z'} (φ : Hom I I' f) :
+    I.ι ≫ φ.hom = (single₀ C).map f ≫ I'.ι := by cat_disch
+
+end Hom
+
 end InjectiveResolution
 
 end CategoryTheory

Mathlib/CategoryTheory/Preadditive/Projective/Resolution.lean

@@ -134,6 +134,27 @@ noncomputable def self [Projective Z] : ProjectiveResolution Z where
       apply HomologicalComplex.isZero_single_obj_X
       simp
 
+variable {Z} {Z' : C} (P' : ProjectiveResolution Z')
+
+/-- Given injective resolutions `P` and `P'` of two objects `Z` and `Z'`,
+and a morphism `f : Z ⟶ Z'`, this structure contains the data of a morphism
+`P.complex ⟶ P'.complex` which is compatible with `f` -/
+structure Hom (f : Z ⟶ Z') where
+  /-- A morphism between the cocomplexes -/
+  hom : P.complex ⟶ P'.complex
+  hom_f_zero_comp_π_f_zero : hom.f 0 ≫ P'.π.f 0 = P.π.f 0 ≫ ((single₀ C).map f).f 0
+
+namespace Hom
+
+attribute [reassoc (attr := simp)] hom_f_zero_comp_π_f_zero
+
+variable {I I'} in
+@[reassoc (attr := simp)]
+lemma hom_comp_π {f : Z ⟶ Z'} (φ : Hom P P' f) :
+    φ.hom ≫ P'.π = P.π ≫ (single₀ C).map f := by cat_disch
+
+end Hom
+
 end ProjectiveResolution
 
 namespace Functor