The comparison theorem for complete resolutions #
Complete resolutions, TauCeti.ExactStructure.CompleteResolution, are bi-infinite sequences of
conflations Zⁿ ↪ Xⁿ ↠ Zⁿ⁺¹ with projective-injective middle terms, spliced into a cochain
complex. This file proves that they are unique up to homotopy.
Let r and r' be complete resolutions and f : r.Z 0 ⟶ r'.Z 0. Then f lifts to a map of
complexes lift f. In negative degrees the lift is built downwards, lifting along the deflations
of r' out of the projective terms of r; in nonnegative degrees it is built upwards, extending
across the inflations of r into the injective terms of r'.
A map of complexes lifting f is null-homotopic exactly when f factors through a
projective-injective object. When E is Frobenius, the projective-injective objects are the
relative projectives, so this says that f vanishes in E.ProjectiveStableCategory. In
particular two lifts of the same morphism are homotopic, and two complete resolutions with
isomorphic objects of cycles in degree zero are homotopy equivalent. In a Frobenius exact
category every object has a complete resolution, so complete resolutions are unique up to
homotopy equivalence.
No Frobenius hypothesis is needed for the comparison theorem itself: the projectivity and injectivity of the terms of the two resolutions are all it uses.
Main definitions #
TauCeti.ExactStructure.CompleteResolution.lift: the map of complexes lifting a morphism of the objects of cycles in degree zero.TauCeti.ExactStructure.CompleteResolution.liftHomotopyZero: a map of complexes lifting a morphism that factors through a projective-injective object is null-homotopic.TauCeti.ExactStructure.CompleteResolution.liftHomotopy: two lifts of the same morphism are homotopic.TauCeti.ExactStructure.CompleteResolution.homotopyEquiv: complete resolutions with isomorphic objects of cycles in degree zero are homotopy equivalent.
Main results #
TauCeti.ExactStructure.CompleteResolution.ι_lift_f_zero: the lift inducesfon the objects of cycles in degree zero.TauCeti.ExactStructure.CompleteResolution.nonempty_homotopy_zero_iff: a map of complexes liftingfis null-homotopic if and only ifffactors through a projective-injective object.
References #
- Ragnar-Olaf Buchweitz, Maximal Cohen–Macaulay Modules and Tate Cohomology, Section 4, for complete resolutions and their uniqueness up to homotopy.
- Theo Bühler, Exact categories, Expositiones Mathematicae 28 (2010), 1--69, Section 12, for the comparison theorem for projective resolutions in an exact category.
Mathlib/CategoryTheory/Abelian/Projective/Resolution.lean, whoselift,liftHomotopyZero,liftHomotopy,liftIdHomotopy,liftCompHomotopyandhomotopyEquivAPI for projective resolutions in abelian categories is followed here, including the derivation ofliftHomotopyfromliftHomotopyZerothroughHomotopy.equivSubZero, and the construction of the lift and of the null-homotopy from a base case and a repeated step.Mathlib/CategoryTheory/Abelian/Injective/Resolution.lean, the dual comparison theory for injective resolutions, which the upward half of the construction follows.TauCeti/CategoryTheory/Exact/Resolution/Comparison.lean, the comparison theorem for finite projective resolutions in an exact category (TauCeti.ExactStructure.FiniteResolution.lift,liftHomotopy,homotopyEquiv), of which this is the bi-infinite analogue.
The lift #
The lift is assembled from the comparison maps of presentations. Each conflation
Zⁿ ↪ Xⁿ ↠ Zⁿ⁺¹ is an injective presentation of Zⁿ and a projective presentation of Zⁿ⁺¹.
Upwards, a map Zⁿ ⟶ Z'ⁿ extends to the injective middle terms and induces a map Zⁿ⁺¹ ⟶ Z'ⁿ⁺¹
on cokernels (InjectivePresentation.middleMap and cokernelMap). Downwards, a map
Zⁿ⁺¹ ⟶ Z'ⁿ⁺¹ lifts to the projective middle terms and induces a map Zⁿ ⟶ Z'ⁿ on kernels
(ProjectivePresentation.middleMap and kernelMap).
The equations of these recursions at the constructors of ℤ, and at their successors. The
index Int.negSucc (k + 1) + 1 reduces to Int.negSucc k, and Int.ofNat k + 1 to
Int.ofNat (k + 1); these lemmas record the resulting unfoldings once, so that the proofs below
rewrite with them instead of relying on the reductions.
The comparison map. The map of complexes lifting f : r.Z 0 ⟶ r'.Z 0 between the
complexes of two complete resolutions.
Instances For
The lift induces f on the objects of cycles in degree zero.
The lift induces f on the objects of cycles in degree zero.
The morphism of the objects of cycles induced by the lift of f is f.
The null-homotopy #
Let φ lift f = ι₀ ≫ c ≫ π₋₁. The null-homotopy has component c : X⁰ ⟶ X'⁻¹, and its other
components come from two steps, each stated for an arbitrary degree n.
Upwards, a correction χ : Xⁿ⁺¹ ⟶ X'ⁿ⁺¹ vanishing on Zⁿ⁺¹, and agreeing with φⁿ⁺¹ after the
differential, induces Zⁿ⁺² ⟶ X'ⁿ⁺¹. Its extension across Zⁿ⁺² ↪ Xⁿ⁺², into the injective
X'ⁿ⁺¹, is a component h' with d ≫ h' = χ. The next correction is φⁿ⁺² - h' ≫ d.
This is the step TauCeti.ExactStructure.AcyclicData.homotopyStep, shared with maps from
acyclic complexes to complexes of injectives, applied to r.acyclicData.
Downwards, a correction ω : Xⁿ⁺¹ ⟶ X'ⁿ⁺¹ vanishing after X'ⁿ⁺¹ ↠ Z'ⁿ⁺², and agreeing with φⁿ⁺¹
before the differential, corestricts to Xⁿ⁺¹ ⟶ Z'ⁿ⁺¹; its lift along X'ⁿ ↠ Z'ⁿ⁺¹, out of the
projective Xⁿ⁺¹, is a component h' with h' ≫ d = ω. The next correction is φⁿ - d ≫ h'.
The corrections in degree zero and -1 are φ⁰ - c ≫ d and φ⁻¹ - d ≫ c.
The two starting corrections, stated in degrees 0 and -1. They are the hypotheses of the
first upward step in degree n = -1 and of the first downward step in degree n = -2, whose
indices Int.negSucc 0 + 1 and Int.negSucc 1 + 1 reduce to 0 and Int.negSucc 0.
The equations of these recursions at the constructors of ℤ and at their successors, by
rfl, as for the lift.
The homotopy identities, one for each kind of degree: each is the equation d ≫ h' = χ or
h' ≫ d = ω returned by the step that produced the component. After the equations above, the
goal and that equation differ only in the indices Int.ofNat k + 1 against ↑k + 1 and
Int.negSucc (k + 1) + 1 against Int.negSucc k, which exact identifies by reduction.
The homotopy criterion. A map of complexes lifting a morphism that factors through a projective-injective object is null-homotopic.
Instances For
Conversely, if a map of complexes lifting f is null-homotopic, then f factors through
the projective-injective term X⁰.
A map of complexes lifting f is null-homotopic if and only if f factors through a
projective-injective object. When E is Frobenius, this says that f vanishes in the stable
category, by TauCeti.ExactStructure.IsFrobenius.projectiveInjective_eq_isProjective and
TauCeti.ExactStructure.projectiveStableFunctor_map_eq_zero_iff.
Two lifts of the same morphism are homotopic.
Instances For
The lift of the identity is homotopic to the identity.
Instances For
The lift of a composite is homotopic to the composite of the lifts.
Instances For
Uniqueness of complete resolutions up to homotopy. Complete resolutions whose objects of cycles in degree zero are isomorphic have homotopy equivalent complexes.
Instances For
The homotopy equivalence induces e.hom on the objects of cycles in degree zero.
The homotopy equivalence induces e.hom on the objects of cycles in degree zero.
The homotopy equivalence induces e.inv on the objects of cycles in degree zero.
The homotopy equivalence induces e.inv on the objects of cycles in degree zero.
The morphism of cycles induced by the homotopy equivalence is e.hom.
The morphism of cycles induced by the inverse homotopy equivalence is e.inv.
Two maps of complete resolutions agree in the homotopy category exactly when the difference of the morphisms they induce on the cycles in degree zero factors through a projective-injective object.