The comparison theorem for finite projective resolutions

Let r be a finite resolution of X in an exact category whose resolving terms are relatively projective, and let r' be any finite resolution of Y. Every morphism f : X ⟶ Y lifts to a chain map between the complexes of the two resolutions compatible with the augmentations, and any two such lifts are chain homotopic. The lift is built one conflation at a time: a projective term Qₙ lifts along the deflation Q'ₙ ↠ K'ₙ, and the induced map on the kernels Kₙ₊₁ ⟶ K'ₙ₊₁ is the input to the next step. The homotopy is built the same way, after subtracting the part of the chain map already accounted for.

Consequently any two finite projective resolutions of the same object are homotopy equivalent, and the resolution is unique up to chain homotopy. This is the relative version of Mathlib's CategoryTheory.ProjectiveResolution.lift, liftHomotopyZero and homotopyEquiv for abelian categories: the ambient category need not have kernels or cokernels, and exactness is the exact-structure datum rather than Mathlib's ShortComplex.Exact.

The uniqueness also makes the comparison map functorial: the image of a lift under a conflation-exact functor is again a lift, so it is homotopic to the lift between the image resolutions. Applied to the grading shift of a graded exact category, this is the graded comparison theorem.

Main definitions

• TauCeti.ExactStructure.FiniteResolution.lift: the chain map lifting f : X ⟶ Y from a finite projective resolution of X to a finite resolution of Y.
• TauCeti.ExactStructure.FiniteResolution.liftHomotopyZero: a chain map from a finite projective resolution to a finite resolution which vanishes against the augmentation is null-homotopic.
• TauCeti.ExactStructure.FiniteResolution.liftHomotopy: two lifts of the same morphism are homotopic.
• TauCeti.ExactStructure.FiniteResolution.liftIdHomotopy and TauCeti.ExactStructure.FiniteResolution.liftCompHomotopy: the lift of an identity is homotopic to the identity, and the lift of a composite to the composite of the lifts.
• TauCeti.ExactStructure.FiniteResolution.homotopyEquiv: two finite projective resolutions of the same object are homotopy equivalent.
• TauCeti.ExactStructure.FiniteResolution.liftMapHomotopy: the comparison map is functorial up to homotopy along conflation-exact functors preserving the projective terms.

Main results

• TauCeti.ExactStructure.FiniteResolution.lift_f_zero_comp_aug: the lift is compatible with the augmentations, (lift f).f 0 ≫ aug' = aug ≫ f.

References

• Theo Bühler, Exact categories, Expositiones Mathematicae 28 (2010), 1--69, Section 12, for the comparison theorem for projective resolutions in a Quillen exact category.
• Charles A. Weibel, An Introduction to Homological Algebra, Cambridge University Press (1994), Theorem 2.2.6, the comparison theorem, and Section 2.2 for its proof by induction along the resolution.
• Mathlib/CategoryTheory/Abelian/Projective/Resolution.lean, whose lift, liftHomotopyZero, liftHomotopy, liftIdHomotopy, liftCompHomotopy and homotopyEquiv API for projective resolutions in abelian categories is followed here.
• Mathlib/CategoryTheory/Preadditive/Projective/Resolution.lean, whose CategoryTheory.Functor.mapProjectiveResolution is the abelian counterpart of the image of a resolution under a functor used in liftMapHomotopy.

noncomputable def TauCeti.ExactStructure.FiniteResolution.lift {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P P' : CategoryTheory.ObjectProperty C} (hP : P ≤ E.isProjective) {X Y : C} (f : X ⟶ Y) (r : E.FiniteResolution P X) (r' : E.FiniteResolution P' Y) : r.toChainComplex ⟶ r'.toChainComplex

The comparison map. The chain map lifting f : X ⟶ Y from a finite resolution r of X by relative projectives to any finite resolution r' of Y, compatible with the two augmentations.

Equations

• TauCeti.ExactStructure.FiniteResolution.lift hP f r r' = ChainComplex.ofHom ↑(TauCeti.ExactStructure.FiniteResolution.liftAux✝ hP r r' f) ⋯

@[simp]

theorem TauCeti.ExactStructure.FiniteResolution.lift_f_zero_comp_aug {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P P' : CategoryTheory.ObjectProperty C} (hP : P ≤ E.isProjective) {X Y : C} (f : X ⟶ Y) (r : E.FiniteResolution P X) (r' : E.FiniteResolution P' Y) : CategoryTheory.CategoryStruct.comp ((lift hP f r r').f 0) r'.aug = CategoryTheory.CategoryStruct.comp r.aug f

The lift is compatible with the augmentations.

@[simp]

theorem TauCeti.ExactStructure.FiniteResolution.lift_f_zero_comp_aug_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P P' : CategoryTheory.ObjectProperty C} (hP : P ≤ E.isProjective) {X Y : C} (f : X ⟶ Y) (r : E.FiniteResolution P X) (r' : E.FiniteResolution P' Y) {Z : C} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp ((lift hP f r r').f 0) (CategoryTheory.CategoryStruct.comp r'.aug h) = CategoryTheory.CategoryStruct.comp r.aug (CategoryTheory.CategoryStruct.comp f h)

The lift is compatible with the augmentations.

noncomputable def TauCeti.ExactStructure.FiniteResolution.liftHomotopyZero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P P' : CategoryTheory.ObjectProperty C} (hP : P ≤ E.isProjective) {X Y : C} {r : E.FiniteResolution P X} {r' : E.FiniteResolution P' Y} (φ : r.toChainComplex ⟶ r'.toChainComplex) (hφ : CategoryTheory.CategoryStruct.comp (φ.f 0) r'.aug = 0) : Homotopy φ 0

A chain map from the complex of a finite projective resolution to the complex of a finite resolution which vanishes against the augmentation is null-homotopic.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def TauCeti.ExactStructure.FiniteResolution.liftHomotopy {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P P' : CategoryTheory.ObjectProperty C} (hP : P ≤ E.isProjective) {X Y : C} (f : X ⟶ Y) {r : E.FiniteResolution P X} {r' : E.FiniteResolution P' Y} (φ ψ : r.toChainComplex ⟶ r'.toChainComplex) (hφ : CategoryTheory.CategoryStruct.comp (φ.f 0) r'.aug = CategoryTheory.CategoryStruct.comp r.aug f) (hψ : CategoryTheory.CategoryStruct.comp (ψ.f 0) r'.aug = CategoryTheory.CategoryStruct.comp r.aug f) : Homotopy φ ψ

Two lifts of the same morphism are homotopic.

Equations

• TauCeti.ExactStructure.FiniteResolution.liftHomotopy hP f φ ψ hφ hψ = Homotopy.equivSubZero.symm (TauCeti.ExactStructure.FiniteResolution.liftHomotopyZero hP (φ - ψ) ⋯)

noncomputable def TauCeti.ExactStructure.FiniteResolution.liftIdHomotopy {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P : CategoryTheory.ObjectProperty C} (hP : P ≤ E.isProjective) {X : C} (r : E.FiniteResolution P X) : Homotopy (lift hP (CategoryTheory.CategoryStruct.id X) r r) (CategoryTheory.CategoryStruct.id r.toChainComplex)

The lift of the identity is homotopic to the identity chain map.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def TauCeti.ExactStructure.FiniteResolution.liftCompHomotopy {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P P' P'' : CategoryTheory.ObjectProperty C} (hP : P ≤ E.isProjective) (hP' : P' ≤ E.isProjective) {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (r : E.FiniteResolution P X) (r' : E.FiniteResolution P' Y) (r'' : E.FiniteResolution P'' Z) : Homotopy (lift hP (CategoryTheory.CategoryStruct.comp f g) r r'') (CategoryTheory.CategoryStruct.comp (lift hP f r r') (lift hP' g r' r''))

The lift of a composite is homotopic to the composite of the lifts.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def TauCeti.ExactStructure.FiniteResolution.homotopyEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P P' : CategoryTheory.ObjectProperty C} (hP : P ≤ E.isProjective) (hP' : P' ≤ E.isProjective) {X : C} (r : E.FiniteResolution P X) (r' : E.FiniteResolution P' X) : HomotopyEquiv r.toChainComplex r'.toChainComplex

Uniqueness of finite projective resolutions up to homotopy. Two finite resolutions of the same object by relative projectives have homotopy equivalent complexes.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.ExactStructure.FiniteResolution.homotopyEquiv_hom_f_zero_comp_aug {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P P' : CategoryTheory.ObjectProperty C} (hP : P ≤ E.isProjective) (hP' : P' ≤ E.isProjective) {X : C} (r : E.FiniteResolution P X) (r' : E.FiniteResolution P' X) : CategoryTheory.CategoryStruct.comp ((homotopyEquiv hP hP' r r').hom.f 0) r'.aug = r.aug

@[simp]

theorem TauCeti.ExactStructure.FiniteResolution.homotopyEquiv_hom_f_zero_comp_aug_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P P' : CategoryTheory.ObjectProperty C} (hP : P ≤ E.isProjective) (hP' : P' ≤ E.isProjective) {X : C} (r : E.FiniteResolution P X) (r' : E.FiniteResolution P' X) {Z : C} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp ((homotopyEquiv hP hP' r r').hom.f 0) (CategoryTheory.CategoryStruct.comp r'.aug h) = CategoryTheory.CategoryStruct.comp r.aug h

@[simp]

theorem TauCeti.ExactStructure.FiniteResolution.homotopyEquiv_inv_f_zero_comp_aug {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P P' : CategoryTheory.ObjectProperty C} (hP : P ≤ E.isProjective) (hP' : P' ≤ E.isProjective) {X : C} (r : E.FiniteResolution P X) (r' : E.FiniteResolution P' X) : CategoryTheory.CategoryStruct.comp ((homotopyEquiv hP hP' r r').inv.f 0) r.aug = r'.aug

@[simp]

theorem TauCeti.ExactStructure.FiniteResolution.homotopyEquiv_inv_f_zero_comp_aug_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P P' : CategoryTheory.ObjectProperty C} (hP : P ≤ E.isProjective) (hP' : P' ≤ E.isProjective) {X : C} (r : E.FiniteResolution P X) (r' : E.FiniteResolution P' X) {Z : C} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp ((homotopyEquiv hP hP' r r').inv.f 0) (CategoryTheory.CategoryStruct.comp r.aug h) = CategoryTheory.CategoryStruct.comp r'.aug h

noncomputable def TauCeti.ExactStructure.FiniteResolution.liftMapHomotopy {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P P' : CategoryTheory.ObjectProperty C} {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] {E' : ExactStructure D} {Q Q' : CategoryTheory.ObjectProperty D} {F : CategoryTheory.Functor C D} [F.Additive] (hP : P ≤ E.isProjective) (hQ : Q ≤ E'.isProjective) (hF : E.IsConflationExact E' F) (hPQ : P ≤ Q.inverseImage F) (hP'Q' : P' ≤ Q'.inverseImage F) {X Y : C} (f : X ⟶ Y) (r : E.FiniteResolution P X) (r' : E.FiniteResolution P' Y) : Homotopy (lift hQ (F.map f) (map hF hPQ r) (map hF hP'Q' r')) (CategoryTheory.CategoryStruct.comp (toChainComplexMapIso hF hPQ r).hom (CategoryTheory.CategoryStruct.comp ((F.mapHomologicalComplex (ComplexShape.down ℕ)).map (lift hP f r r')) (toChainComplexMapIso hF hP'Q' r').inv))

Functoriality of the comparison map. Let F be a conflation-exact functor carrying the relative projectives of P into relative projectives of Q. The lift of F f between the images of two resolutions is homotopic to the image of the lift of f, transported along the identifications TauCeti.ExactStructure.FiniteResolution.toChainComplexMapIso of the complexes of the image resolutions with the images of the complexes.

Equations

• One or more equations did not get rendered due to their size.