Projective resolutions #
A projective resolution P : ProjectiveResolution Z
of an object Z : C
consists of
an ℕ
-indexed chain complex P.complex
of projective objects,
along with a quasi-isomorphism P.π
from C
to the chain complex consisting just
of Z
in degree zero.
A ProjectiveResolution Z
consists of a bundled ℕ
-indexed chain complex of projective objects,
along with a quasi-isomorphism to the complex consisting of just Z
supported in degree 0
.
- complex : ChainComplex C ℕ
the chain complex involved in the resolution
- projective : ∀ (n : ℕ), CategoryTheory.Projective (self.complex.X n)
the chain complex must be degreewise projective
- hasHomology : ∀ (i : ℕ), HomologicalComplex.HasHomology self.complex i
the chain complex must have homology
- π : self.complex ⟶ (ChainComplex.single₀ C).obj Z
the morphism to the single chain complex with
Z
in degree0
- quasiIso : QuasiIso self.π
the morphism to the single chain complex with
Z
in degree0
is a quasi-isomorphism
Instances For
An object admits a projective resolution.
- out : Nonempty (CategoryTheory.ProjectiveResolution Z)
Instances
You will rarely use this typeclass directly: it is implied by the combination
[EnoughProjectives C]
and [Abelian C]
.
By itself it's enough to set up the basic theory of derived functors.
- out : ∀ (Z : C), CategoryTheory.HasProjectiveResolution Z
Instances
The (limit) cokernel cofork given by the composition
P.complex.X 1 ⟶ P.complex.X 0 ⟶ Z
when P : ProjectiveResolution Z
.
Equations
- P.cokernelCofork = CategoryTheory.Limits.CokernelCofork.ofπ (P.π.f 0) ⋯
Instances For
Z
is the cokernel of P.complex.X 1 ⟶ P.complex.X 0
when P : ProjectiveResolution Z
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A projective object admits a trivial projective resolution: itself in degree 0.