The horseshoe lemma for complete resolutions

Let X₁ ↪ X₂ ↠ X₃ be a conflation and let r₁ and r₃ be complete resolutions of X₁ and X₃. Then X₂ has a complete resolution r₂ with maps of spliced complexes r₁ ⟶ r₂ ⟶ r₃ which split in every degree and restrict to the given conflation on the cycles in degree zero.

The construction proceeds one degree at a time in both directions. In nonnegative degrees it applies the injective horseshoe lemma TauCeti.ExactStructure.exists_conflation_of_conflation_of_injective, in negative degrees the projective one TauCeti.ExactStructure.exists_conflation_biprod_of_conflation_of_projective. Each step produces a conflation of cycles Z₁ⁿ ↪ Z₂ⁿ ↠ Z₃ⁿ in the next degree and the conflation Z₂ⁿ ↪ X₂ⁿ ↠ Z₂ⁿ⁺¹ linking two consecutive degrees, whose middle term splits as an extension of X₃ⁿ by X₁ⁿ.

Main definitions

• TauCeti.ExactStructure.CompleteResolution.Horseshoe: a horseshoe of complete resolutions over a conflation.
• TauCeti.ExactStructure.CompleteResolution.horseshoe: its existence.

References

• Ragnar-Olaf Buchweitz, Maximal Cohen–Macaulay Modules and Tate Cohomology, Section 4.
• Charles A. Weibel, An Introduction to Homological Algebra, Lemma 2.2.8.

structure TauCeti.ExactStructure.CompleteResolution.Horseshoe {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {r₁ r₃ : E.CompleteResolution} {X₂ : C} (f : r₁.Z 0 ⟶ X₂) (g : X₂ ⟶ r₃.Z 0) : Type (max u v)

A horseshoe of complete resolutions over a conflation r₁.Z 0 ↪ X₂ ↠ r₃.Z 0: a complete resolution of X₂ with maps of spliced complexes from the first and to the third resolution, which split in every degree and restrict to the given conflation on the cycles in degree zero.

• resolution : E.CompleteResolution

  The complete resolution of the middle term.

• iso : self.resolution.Z 0 ≅ X₂

  The identification of its cycles in degree zero with the middle term.

• ι : r₁.complex ⟶ self.resolution.complex

  The map from the first complete resolution.

• π : self.resolution.complex ⟶ r₃.complex

  The map to the third complete resolution.

• ι_π : CategoryTheory.CategoryStruct.comp self.ι self.π = 0
• cyclesMap_ι : cyclesMap self.ι = CategoryTheory.CategoryStruct.comp f self.iso.inv
• cyclesMap_π : cyclesMap self.π = CategoryTheory.CategoryStruct.comp self.iso.hom g
• split (n : ℤ) : Nonempty ({ X₁ := r₁.complex, X₂ := self.resolution.complex, X₃ := r₃.complex, f := self.ι, g := self.π, zero := ⋯ }.map (HomologicalComplex.eval C (ComplexShape.up ℤ) n)).Splitting

  In every degree, the maps form a split short complex.

@[simp]

theorem TauCeti.ExactStructure.CompleteResolution.Horseshoe.ι_π_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {r₁ r₃ : E.CompleteResolution} {X₂ : C} {f : r₁.Z 0 ⟶ X₂} {g : X₂ ⟶ r₃.Z 0} (self : Horseshoe f g) {Z : CochainComplex C ℤ} (h : r₃.complex ⟶ Z) : CategoryTheory.CategoryStruct.comp self.ι (CategoryTheory.CategoryStruct.comp self.π h) = CategoryTheory.CategoryStruct.comp 0 h

noncomputable def TauCeti.ExactStructure.CompleteResolution.horseshoe {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} (r₁ r₃ : E.CompleteResolution) {X₂ : C} (f : r₁.Z 0 ⟶ X₂) (g : X₂ ⟶ r₃.Z 0) (hfg : CategoryTheory.CategoryStruct.comp f g = 0) (hS : E.Conflation { X₁ := r₁.Z 0, X₂ := X₂, X₃ := r₃.Z 0, f := f, g := g, zero := hfg }) : Horseshoe f g

The horseshoe lemma for complete resolutions. A conflation whose outer terms are the cycles in degree zero of two complete resolutions has a horseshoe of complete resolutions.

theorem TauCeti.ExactStructure.CompleteResolution.Horseshoe.g_comp_connecting {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {r₁ r₃ : E.CompleteResolution} {X₂ : C} {f : r₁.Z 0 ⟶ X₂} {g : X₂ ⟶ r₃.Z 0} (h : Horseshoe f g) (σ : (n : ℤ) → ({ X₁ := r₁.complex, X₂ := h.resolution.complex, X₃ := r₃.complex, f := h.ι, g := h.π, zero := ⋯ }.map (HomologicalComplex.eval C (ComplexShape.up ℤ) n)).Splitting) : CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.comp (r₃.ι 0) (CategoryTheory.CategoryStruct.comp (σ 0).s (CategoryTheory.CategoryStruct.comp (h.resolution.d 0) (σ (0 + 1)).r))) = -CategoryTheory.CategoryStruct.comp h.iso.inv (CategoryTheory.CategoryStruct.comp (h.resolution.ι 0) (CategoryTheory.CategoryStruct.comp (σ 0).r (r₁.d 0)))

The connecting cocycle of a horseshoe in degree zero, restricted to the cycles of the third resolution and precomposed with g, is minus the map obtained by extending the inflation of the first resolution along f through the retraction σ 0. This compares the triangle of the degreewise split sequence with the connecting map of the conflation.