Comparison maps and homotopy uniqueness for augmented exact complexes

A map from a degreewise projective chain complex to an object lifts through any exact, epimorphically augmented chain complex resolving that object. Only the target must be exact: this allows, for example, comparison of a Koszul complex with a resolution of its quotient without requiring the sequence defining the Koszul complex to be regular.

ChainComplex.liftToAugmented constructs the comparison from a degree-zero map annihilating the first differential. ChainComplex.liftToAugmented_comp expresses the compatibility as an equality of chain maps to the single complex. The construction adapts Mathlib's CategoryTheory.ProjectiveResolution.lift by Markus Himmel, Kim Morrison, Jakob von Raumer and Joël Riou, reusing its inductive chain-map constructor and exact lifting from projectives.

ChainComplex.homotopyOfCompAugmentationEq shows that maps agreeing after augmentation are homotopic, without requiring the augmentation to be epimorphic. The target terms need not be projective. In particular, this applies to the restriction of a projective resolution along an arbitrary group homomorphism, even when restriction fails to preserve projective objects. The homotopy construction follows Kim Morrison and Joël Riou's CategoryTheory.ProjectiveResolution.liftHomotopyZero in Mathlib, using only the exactness assumptions on its target. The induction is Mathlib's Homotopy.mkInductive.

References

• The Stacks Project, Lemma 10.71.4 (00LS), comparison with an exact complex.
• C. A. Weibel, An Introduction to Homological Algebra, Section 2.2, the comparison theorem for resolutions.

noncomputable def ChainComplex.liftToAugmented {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] (P : ChainComplex C ℕ) {Q : ChainComplex C ℕ} [∀ (n : ℕ), CategoryTheory.Projective (P.X n)] {Z : C} (ε : Q.X 0 ⟶ Z) (w : CategoryTheory.CategoryStruct.comp (Q.d 1 0) ε = 0) (h₀ : { X₁ := Q.X 1, X₂ := Q.X 0, X₃ := Z, f := Q.d 1 0, g := ε, zero := w }.Exact) (hQ : ∀ (n : ℕ), { X₁ := Q.X (n + 2), X₂ := Q.X (n + 1), X₃ := Q.X n, f := Q.d (n + 2) (n + 1), g := Q.d (n + 1) n, zero := ⋯ }.Exact) [CategoryTheory.Epi ε] (f : P.X 0 ⟶ Z) (hf : CategoryTheory.CategoryStruct.comp (P.d 1 0) f = 0) : P ⟶ Q

Lift a map annihilating the first differential of a degreewise projective complex through an exact epimorphic augmentation. The source need not be exact and the target terms need not be projective.

@[simp]

theorem ChainComplex.liftToAugmented_f_zero_comp {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] (P : ChainComplex C ℕ) {Q : ChainComplex C ℕ} [∀ (n : ℕ), CategoryTheory.Projective (P.X n)] {Z : C} (ε : Q.X 0 ⟶ Z) (w : CategoryTheory.CategoryStruct.comp (Q.d 1 0) ε = 0) (h₀ : { X₁ := Q.X 1, X₂ := Q.X 0, X₃ := Z, f := Q.d 1 0, g := ε, zero := w }.Exact) (hQ : ∀ (n : ℕ), { X₁ := Q.X (n + 2), X₂ := Q.X (n + 1), X₃ := Q.X n, f := Q.d (n + 2) (n + 1), g := Q.d (n + 1) n, zero := ⋯ }.Exact) [CategoryTheory.Epi ε] (f : P.X 0 ⟶ Z) (hf : CategoryTheory.CategoryStruct.comp (P.d 1 0) f = 0) : CategoryTheory.CategoryStruct.comp ((P.liftToAugmented ε w h₀ hQ f hf).f 0) ε = f

The comparison map lifts the prescribed degree-zero map through the augmentation.

@[simp]

theorem ChainComplex.liftToAugmented_f_zero_comp_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] (P : ChainComplex C ℕ) {Q : ChainComplex C ℕ} [∀ (n : ℕ), CategoryTheory.Projective (P.X n)] {Z : C} (ε : Q.X 0 ⟶ Z) (w : CategoryTheory.CategoryStruct.comp (Q.d 1 0) ε = 0) (h₀ : { X₁ := Q.X 1, X₂ := Q.X 0, X₃ := Z, f := Q.d 1 0, g := ε, zero := w }.Exact) (hQ : ∀ (n : ℕ), { X₁ := Q.X (n + 2), X₂ := Q.X (n + 1), X₃ := Q.X n, f := Q.d (n + 2) (n + 1), g := Q.d (n + 1) n, zero := ⋯ }.Exact) [CategoryTheory.Epi ε] (f : P.X 0 ⟶ Z) (hf : CategoryTheory.CategoryStruct.comp (P.d 1 0) f = 0) {Z✝ : C} (h : Z ⟶ Z✝) : CategoryTheory.CategoryStruct.comp ((P.liftToAugmented ε w h₀ hQ f hf).f 0) (CategoryTheory.CategoryStruct.comp ε h) = CategoryTheory.CategoryStruct.comp f h

The comparison map lifts the prescribed degree-zero map through the augmentation.

@[simp]

theorem ChainComplex.liftToAugmented_comp {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] (P : ChainComplex C ℕ) {Q : ChainComplex C ℕ} [∀ (n : ℕ), CategoryTheory.Projective (P.X n)] {Z : C} (ε : Q.X 0 ⟶ Z) (w : CategoryTheory.CategoryStruct.comp (Q.d 1 0) ε = 0) (h₀ : { X₁ := Q.X 1, X₂ := Q.X 0, X₃ := Z, f := Q.d 1 0, g := ε, zero := w }.Exact) (hQ : ∀ (n : ℕ), { X₁ := Q.X (n + 2), X₂ := Q.X (n + 1), X₃ := Q.X n, f := Q.d (n + 2) (n + 1), g := Q.d (n + 1) n, zero := ⋯ }.Exact) [CategoryTheory.Epi ε] (f : P.X 0 ⟶ Z) (hf : CategoryTheory.CategoryStruct.comp (P.d 1 0) f = 0) : CategoryTheory.CategoryStruct.comp (P.liftToAugmented ε w h₀ hQ f hf) ((Q.toSingle₀Equiv Z).symm ⟨ε, w⟩) = (P.toSingle₀Equiv Z).symm ⟨f, hf⟩

The comparison map preserves the augmentation, as an equality of chain maps.

@[simp]

theorem ChainComplex.liftToAugmented_comp_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] (P : ChainComplex C ℕ) {Q : ChainComplex C ℕ} [∀ (n : ℕ), CategoryTheory.Projective (P.X n)] {Z : C} (ε : Q.X 0 ⟶ Z) (w : CategoryTheory.CategoryStruct.comp (Q.d 1 0) ε = 0) (h₀ : { X₁ := Q.X 1, X₂ := Q.X 0, X₃ := Z, f := Q.d 1 0, g := ε, zero := w }.Exact) (hQ : ∀ (n : ℕ), { X₁ := Q.X (n + 2), X₂ := Q.X (n + 1), X₃ := Q.X n, f := Q.d (n + 2) (n + 1), g := Q.d (n + 1) n, zero := ⋯ }.Exact) [CategoryTheory.Epi ε] (f : P.X 0 ⟶ Z) (hf : CategoryTheory.CategoryStruct.comp (P.d 1 0) f = 0) {Z✝ : ChainComplex C ℕ} (h : (single₀ C).obj Z ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (P.liftToAugmented ε w h₀ hQ f hf) (CategoryTheory.CategoryStruct.comp ((Q.toSingle₀Equiv Z).symm ⟨ε, w⟩) h) = CategoryTheory.CategoryStruct.comp ((P.toSingle₀Equiv Z).symm ⟨f, hf⟩) h

The comparison map preserves the augmentation, as an equality of chain maps.

noncomputable def ChainComplex.nullHomotopyOfCompAugmentationEqZero {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {P Q : ChainComplex C ℕ} [∀ (n : ℕ), CategoryTheory.Projective (P.X n)] {Z : C} (ε : Q.X 0 ⟶ Z) (w : CategoryTheory.CategoryStruct.comp (Q.d 1 0) ε = 0) (h₀ : { X₁ := Q.X 1, X₂ := Q.X 0, X₃ := Z, f := Q.d 1 0, g := ε, zero := w }.Exact) (hQ : ∀ (n : ℕ), { X₁ := Q.X (n + 2), X₂ := Q.X (n + 1), X₃ := Q.X n, f := Q.d (n + 2) (n + 1), g := Q.d (n + 1) n, zero := ⋯ }.Exact) (f : P ⟶ Q) (hf : CategoryTheory.CategoryStruct.comp (f.f 0) ε = 0) : Homotopy f 0

A map from a degreewise projective chain complex to an augmented exact complex that vanishes after augmentation is null-homotopic. No projectivity of the target, exactness of the source, or surjectivity of the augmentation is required.

noncomputable def ChainComplex.homotopyOfCompAugmentationEq {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {P Q : ChainComplex C ℕ} [∀ (n : ℕ), CategoryTheory.Projective (P.X n)] {Z : C} (ε : Q.X 0 ⟶ Z) (w : CategoryTheory.CategoryStruct.comp (Q.d 1 0) ε = 0) (h₀ : { X₁ := Q.X 1, X₂ := Q.X 0, X₃ := Z, f := Q.d 1 0, g := ε, zero := w }.Exact) (hQ : ∀ (n : ℕ), { X₁ := Q.X (n + 2), X₂ := Q.X (n + 1), X₃ := Q.X n, f := Q.d (n + 2) (n + 1), g := Q.d (n + 1) n, zero := ⋯ }.Exact) (f g : P ⟶ Q) (hfg : CategoryTheory.CategoryStruct.comp (f.f 0) ε = CategoryTheory.CategoryStruct.comp (g.f 0) ε) : Homotopy f g

Two maps from a degreewise projective complex into an augmented exact complex are homotopic if they agree after augmentation. The target need not be degreewise projective.

noncomputable def CategoryTheory.ProjectiveResolution.liftFromComplex {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] {Z : C} (Q : ProjectiveResolution Z) (P : ChainComplex C ℕ) [∀ (n : ℕ), Projective (P.X n)] (f : P ⟶ (ChainComplex.single₀ C).obj Z) : P ⟶ Q.complex

An augmented degreewise projective complex admits an augmentation-preserving map into any projective resolution. No exactness assumption is made on the source complex.

@[simp]

theorem CategoryTheory.ProjectiveResolution.liftFromComplex_f_zero_comp {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] {Z : C} (Q : ProjectiveResolution Z) (P : ChainComplex C ℕ) [∀ (n : ℕ), Projective (P.X n)] (f : P ⟶ (ChainComplex.single₀ C).obj Z) : CategoryStruct.comp ((Q.liftFromComplex P f).f 0) (Q.π.f 0) = f.f 0

The degree-zero comparison lifts the prescribed augmentation through the resolution.

@[simp]

theorem CategoryTheory.ProjectiveResolution.liftFromComplex_f_zero_comp_assoc {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] {Z : C} (Q : ProjectiveResolution Z) (P : ChainComplex C ℕ) [∀ (n : ℕ), Projective (P.X n)] (f : P ⟶ (ChainComplex.single₀ C).obj Z) {Z✝ : C} (h : ((ChainComplex.single₀ C).obj Z).X 0 ⟶ Z✝) : CategoryStruct.comp ((Q.liftFromComplex P f).f 0) (CategoryStruct.comp (Q.π.f 0) h) = CategoryStruct.comp (f.f 0) h

The degree-zero comparison lifts the prescribed augmentation through the resolution.

@[simp]

theorem CategoryTheory.ProjectiveResolution.liftFromComplex_comp {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] {Z : C} (Q : ProjectiveResolution Z) (P : ChainComplex C ℕ) [∀ (n : ℕ), Projective (P.X n)] (f : P ⟶ (ChainComplex.single₀ C).obj Z) : CategoryStruct.comp (Q.liftFromComplex P f) Q.π = f

The comparison from an augmented projective complex lies over its given augmentation.

@[simp]

theorem CategoryTheory.ProjectiveResolution.liftFromComplex_comp_assoc {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] {Z : C} (Q : ProjectiveResolution Z) (P : ChainComplex C ℕ) [∀ (n : ℕ), Projective (P.X n)] (f : P ⟶ (ChainComplex.single₀ C).obj Z) {Z✝ : ChainComplex C ℕ} (h : (ChainComplex.single₀ C).obj Z ⟶ Z✝) : CategoryStruct.comp (Q.liftFromComplex P f) (CategoryStruct.comp Q.π h) = CategoryStruct.comp f h

The comparison from an augmented projective complex lies over its given augmentation.