The horseshoe of finite projective resolutions #
For a conflation X ↪ Y ↠ Z and finite resolutions of X and Z by relative projectives,
construct a finite projective resolution of Y and compatible chain maps. In each degree the
resulting short complex splits, so the middle term is the biproduct of the two prescribed outer
terms. Its length is at most the maximum of the two outer lengths.
The construction iterates the one-step horseshoe lemma for conflations, retaining the maps between successive syzygies. No ambient kernels, cokernels, or enough-projectives hypothesis is needed. In a graded exact category the same construction applies to graded objects and morphisms; the shift and every conflation-exact functor preserving projectives transport the resulting horseshoe.
References #
- Theo Bühler, Exact categories, Section 12, for the horseshoe lemma in exact categories.
- Charles A. Weibel, An Introduction to Homological Algebra, Lemma 2.2.8.
A horseshoe over a conflation, with prescribed finite projective resolutions of its outer terms: a middle resolution, augmentation-compatible chain maps, and degreewise split exactness. The middle resolution is no longer than the longer of the prescribed resolutions.
- resolution : E.FiniteResolution E.isProjective S.X₂
The finite projective resolution of the middle object.
The chain map lifting the inflation of the conflation.
The chain map lifting the deflation of the conflation.
The two chain maps have zero composite.
- ι_aug : CategoryTheory.CategoryStruct.comp (self.ι.f 0) self.resolution.aug = CategoryTheory.CategoryStruct.comp r₁.aug S.f
The left chain map commutes with the augmentations.
- π_aug : CategoryTheory.CategoryStruct.comp (self.π.f 0) r₃.aug = CategoryTheory.CategoryStruct.comp self.resolution.aug S.g
The right chain map commutes with the augmentations.
- split (n : ℕ) : Nonempty { X₁ := r₁.toChainComplex.X n, X₂ := self.resolution.toChainComplex.X n, X₃ := r₃.toChainComplex.X n, f := self.ι.f n, g := self.π.f n, zero := ⋯ }.Splitting
The induced short complex in each degree splits.
The bound on the length of the middle resolution.
Instances For
The two chain maps have zero composite.
The left chain map commutes with the augmentations.
The right chain map commutes with the augmentations.
The finite projective horseshoe lemma. A conflation and finite projective resolutions of its outer terms admit an augmentation-compatible, degreewise split horseshoe whose middle resolution has length at most the maximum of the outer lengths.
Equations
Instances For
Each middle term of a horseshoe is isomorphic to the biproduct of the prescribed outer terms. The isomorphism is compatible with the injection and projection, through the standard splitting API.
Equations
- h.termIsoBiprod n = ⋯.some.isoBinaryBiproduct
Instances For
The termwise biproduct isomorphism sends the horseshoe injection to the left inclusion.
The termwise biproduct isomorphism sends the horseshoe injection to the left inclusion.
The right projection after the termwise biproduct isomorphism is the horseshoe projection.
The right projection after the termwise biproduct isomorphism is the horseshoe projection.
A conflation-exact additive functor preserving relative projectives transports a horseshoe. In particular this applies to the grading shift and its inverse in a graded exact category.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The middle resolution of the transported horseshoe is the transported middle resolution.
Each component of the transported injection is the functor's image of the original component, conjugated by the term isomorphisms and identified with the transported middle term.
Each component of the transported projection is the functor's image of the original component, conjugated by the term isomorphisms after identifying the transported middle term.