Degree-zero homology of a left resolution

The augmented initial segment identifies degree-zero homology of the mapped left-resolution chain complex with the resolved object. This is an objectwise identification; it does not totalize a resolution bicomplex or supply a K-flat replacement of an unbounded complex.

noncomputable def CategoryTheory.Abelian.LeftResolution.homologyZeroIso {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)).homology 0 ≅ X

Degree-zero homology of the mapped left resolution is the original object. The isomorphism descends the augmentation through the cokernel of the first differential, using exactness and the epi augmentation.

Equations

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

theorem CategoryTheory.Abelian.LeftResolution.homologyZeroIso_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 : A) {Y : A} (f : X ⟶ Y) : CategoryStruct.comp (HomologicalComplex.homologyMap ((ι.mapHomologicalComplex (ComplexShape.down ℕ)).map (Λ.chainComplexMap f)) 0) (homologyZeroIso ι Λ Y).hom = CategoryStruct.comp (homologyZeroIso ι Λ X).hom f

The degree-zero homology identification commutes with maps between resolved objects.

noncomputable def CategoryTheory.Abelian.LeftResolution.homologyZeroNatIso {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 ℕ)).comp (HomologicalComplex.homologyFunctor A (ComplexShape.down ℕ) 0)) ≅ Functor.id A

Functorially, degree-zero homology of the mapped left resolution is the identity.

Equations

• CategoryTheory.Abelian.LeftResolution.homologyZeroNatIso ι Λ = CategoryTheory.NatIso.ofComponents (fun (X : A) => CategoryTheory.Abelian.LeftResolution.homologyZeroIso ι Λ X) ⋯

theorem CategoryTheory.Abelian.LeftResolution.homologyZeroIso_eq_augmentationHomologyMap {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) : CategoryStruct.comp (HomologicalComplex.homologyMap (chainComplexAugmentation ι Λ X) 0) (HomologicalComplex.singleObjHomologySelfIso (ComplexShape.down ℕ) 0 X).hom = (homologyZeroIso ι Λ X).hom

Both maps descend the same degree-zero augmentation; cancellation against the epimorphic projection to homology identifies them.