Projective resolutions of ideal quotients

Ideal.quotientProjectiveResolution I resolves A ⧸ I by prepending the regular module A to the chosen projective resolution of I. Its complex and augmentation are described by Ideal.quotientProjectiveResolution_complex and Ideal.quotientProjectiveResolution_π_f_zero.

noncomputable def Ideal.quotientProjectiveResolution {A : Type u} [Ring A] (I : Ideal A) : CategoryTheory.ProjectiveResolution ↧(A ⧸ I)

The projective resolution of A ⧸ I obtained by prepending A to the chosen projective resolution of I. The final differential is the resolution map followed by the ideal inclusion, and the augmentation is the quotient map.

theorem Ideal.quotientProjectiveResolution_complex {A : Type u} [Ring A] (I : Ideal A) : I.quotientProjectiveResolution.complex = (CategoryTheory.projectiveResolution ↧↥I).complex.augment (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp ((CategoryTheory.projectiveResolution ↧↥I).π.f 0) (HomologicalComplex.singleObjXSelf (ComplexShape.down ℕ) 0 ↧↥I).hom) (ModuleCat.ofHom (Submodule.subtype I))) ⋯

The ideal-quotient resolution is the resolution of I augmented by its inclusion into A.

theorem Ideal.quotientProjectiveResolution_π_f_zero {A : Type u} [Ring A] (I : Ideal A) : CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (I.quotientProjectiveResolution.π.f 0) = ModuleCat.ofHom (Submodule.mkQ I)

The augmentation in degree zero is the quotient map, after identifying the degree-zero object with the regular module through quotientProjectiveResolution_complex.