Augmentation of a left resolution

After applying ι, the functorial chain complex attached to a LeftResolution is exact in positive degrees. This file also records exactness of its first two terms after augmentation to the object being resolved. The augmentation is a natural chain map and an objectwise quasi-isomorphism. These statements do not assert a totalization theorem or K-flatness for a bicomplex built from such resolutions.

noncomputable def CategoryTheory.Abelian.LeftResolution.augmentedShortComplex {A : Type u_1} {C : Type u_2} [Category.{u_3, u_2} C] [Category.{u_4, u_1} A] (ι : Functor C A) [ι.Full] [ι.Faithful] [Limits.HasZeroMorphisms C] [Abelian A] (Λ : LeftResolution ι) (X : A) : ShortComplex A

The initial segment of Λ.chainComplex X, mapped to A and augmented by the epimorphism Λ.π.app X.

Equations

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

theorem CategoryTheory.Abelian.LeftResolution.augmentedShortComplex_exact {A : Type u_1} {C : Type u_2} [Category.{u_4, u_2} C] [Category.{u_3, u_1} A] (ι : Functor C A) [ι.Full] [ι.Faithful] [Limits.HasZeroMorphisms C] [Abelian A] (Λ : LeftResolution ι) (X : A) : (augmentedShortComplex ι Λ X).Exact

The first two terms of the mapped left resolution are exact after augmentation. This is only exactness at the middle term; the epimorphicity of the augmentation is recorded separately by augmentedShortComplex_epi_g.

theorem CategoryTheory.Abelian.LeftResolution.augmentedShortComplex_epi_g {A : Type u_1} {C : Type u_2} [Category.{u_4, u_2} C] [Category.{u_3, u_1} A] (ι : Functor C A) [ι.Full] [ι.Faithful] [Limits.HasZeroMorphisms C] [Abelian A] (Λ : LeftResolution ι) (X : A) : Epi (augmentedShortComplex ι Λ X).g

The augmentation is epi because it composes the degree-zero identification isomorphism with the epimorphism Λ.π.app X. Together with exactness at the middle term, this records the right end of the augmented resolution.

noncomputable def CategoryTheory.Abelian.LeftResolution.chainComplexAugmentation {A : Type u_1} {C : Type u_2} [Category.{u_3, u_2} C] [Category.{u_4, u_1} A] (ι : Functor C A) [ι.Full] [ι.Faithful] [Limits.HasZeroMorphisms C] [Abelian A] (Λ : LeftResolution ι) (X : A) : (ι.mapHomologicalComplex (ComplexShape.down ℕ)).obj (Λ.chainComplex X) ⟶ (ChainComplex.single₀ A).obj X

The canonical augmentation from the mapped chain complex of a left resolution to its degree-zero single complex. Its defining degree-zero map is the augmented short complex's epimorphism.

Equations

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

theorem CategoryTheory.Abelian.LeftResolution.chainComplexAugmentation_naturality {A : Type u_1} {C : Type u_2} [Category.{u_4, u_2} C] [Category.{u_3, u_1} A] (ι : Functor C A) [ι.Full] [ι.Faithful] [Limits.HasZeroMorphisms C] [Abelian A] (Λ : LeftResolution ι) {X Y : A} (f : X ⟶ Y) : CategoryStruct.comp ((ι.mapHomologicalComplex (ComplexShape.down ℕ)).map (Λ.chainComplexMap f)) (chainComplexAugmentation ι Λ Y) = CategoryStruct.comp (chainComplexAugmentation ι Λ X) ((ChainComplex.single₀ A).map f)

Maps to the degree-zero single complex are determined in degree zero, where this square follows from naturality of the resolution epimorphism.

theorem CategoryTheory.Abelian.LeftResolution.chainComplexAugmentation_naturality_assoc {A : Type u_1} {C : Type u_2} [Category.{u_4, u_2} C] [Category.{u_3, u_1} A] (ι : Functor C A) [ι.Full] [ι.Faithful] [Limits.HasZeroMorphisms C] [Abelian A] (Λ : LeftResolution ι) {X Y : A} (f : X ⟶ Y) {Z : HomologicalComplex A (ComplexShape.down ℕ)} (h : (ChainComplex.single₀ A).obj Y ⟶ Z) : CategoryStruct.comp ((ι.mapHomologicalComplex (ComplexShape.down ℕ)).map (Λ.chainComplexMap f)) (CategoryStruct.comp (chainComplexAugmentation ι Λ Y) h) = CategoryStruct.comp (chainComplexAugmentation ι Λ X) (CategoryStruct.comp ((ChainComplex.single₀ A).map f) h)

Maps to the degree-zero single complex are determined in degree zero, where this square follows from naturality of the resolution epimorphism.

noncomputable def CategoryTheory.Abelian.LeftResolution.chainComplexAugmentationNatTrans {A : Type u_1} {C : Type u_2} [Category.{u_3, u_2} C] [Category.{u_4, u_1} A] (ι : Functor C A) [ι.Full] [ι.Faithful] [Limits.HasZeroMorphisms C] [Abelian A] (Λ : LeftResolution ι) : Λ.chainComplexFunctor.comp (ι.mapHomologicalComplex (ComplexShape.down ℕ)) ⟶ ChainComplex.single₀ A

The components come from ChainComplex.toSingle₀Equiv applied to the augmented short complex.

Equations

• CategoryTheory.Abelian.LeftResolution.chainComplexAugmentationNatTrans ι Λ = { app := fun (X : A) => CategoryTheory.Abelian.LeftResolution.chainComplexAugmentation ι Λ X, naturality := ⋯ }

theorem CategoryTheory.Abelian.LeftResolution.chainComplexAugmentation_quasiIso {A : Type u_1} {C : Type u_2} [Category.{u_4, u_2} C] [Category.{u_3, u_1} A] (ι : Functor C A) [ι.Full] [ι.Faithful] [Limits.HasZeroMorphisms C] [Abelian A] (Λ : LeftResolution ι) (X : A) : QuasiIso (chainComplexAugmentation ι Λ X)

The canonical augmentation of an individual mapped left resolution is a quasi-isomorphism. This objectwise result does not compare the totalization of resolutions of an unbounded complex with that complex.