CategoryTheory.ProjectiveResolution.quasiIso
theorem CategoryTheory.ProjectiveResolution.quasiIso :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
[inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {Z : C} (self : CategoryTheory.ProjectiveResolution Z),
QuasiIso self.π
This theorem states that for any category `C` with a zero object and zero morphisms, and any object `Z` in `C`, the morphism from a projective resolution of `Z` to a single chain complex with `Z` in degree `0` is a quasi-isomorphism. A quasi-isomorphism is a type of morphism in category theory that induces a bijection on homology groups.
More concisely: For any category with a zero object and zero morphisms, the morphism from a projective resolution of an object to the single chain complex with that object in degree 0 is a quasi-isomorphism.
|
CategoryTheory.ProjectiveResolution.projective
theorem CategoryTheory.ProjectiveResolution.projective :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
[inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {Z : C} (self : CategoryTheory.ProjectiveResolution Z)
(n : ℕ), CategoryTheory.Projective (self.complex.X n)
This theorem states that in the setting of a category `C`, which has a zero object and zero morphisms, the objects of the chain complex at each degree `n` in a projective resolution of an object `Z` are projective. In other words, for any object `Z` in the category `C`, and a projective resolution `self` of `Z`, the chain complex `self.complex` is degreewise projective. This is an important property in homological algebra, ensuring that a projective resolution can be used to compute derived functors.
More concisely: In a category with a zero object and zero morphisms, the objects of a projective resolution of an object form a degreewise projective chain complex.
|
CategoryTheory.ProjectiveResolution.hasHomology
theorem CategoryTheory.ProjectiveResolution.hasHomology :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
[inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {Z : C} (self : CategoryTheory.ProjectiveResolution Z)
(i : ℕ), HomologicalComplex.HasHomology self.complex i
The theorem `CategoryTheory.ProjectiveResolution.hasHomology` states that for any category `C` with zero objects and zero morphisms, any object `Z` in `C`, and any projective resolution `self` of `Z`, the homological complex associated with the projective resolution has homology at any natural number `i`. In other words, the chain complex designated by the projective resolution must have homology at every degree.
More concisely: For any category with zero objects and morphisms, any projective resolution of an object implies the associated homological complex has non-empty homology at every degree.
|
CategoryTheory.ProjectiveResolution.complex_d_comp_π_f_zero
theorem CategoryTheory.ProjectiveResolution.complex_d_comp_π_f_zero :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
[inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {Z : C} (P : CategoryTheory.ProjectiveResolution Z),
CategoryTheory.CategoryStruct.comp (P.complex.d 1 0) (P.π.f 0) = 0
The theorem `CategoryTheory.ProjectiveResolution.complex_d_comp_π_f_zero` states that for any category `C`, given that `C` has a zero object and zero morphisms, and for any object `Z` in `C` with a projective resolution `P`, the composition of the morphism `P.complex.d 1 0` and `P.π.f 0` is equal to the zero morphism. In simpler terms, the theorem specifies a property of projective resolutions in a category, whereby a certain composition of morphisms results in the zero morphism.
More concisely: For any category with a zero object and zero morphisms, the composition of the differential `d` at degree 1 and the augmentation morphism `π` for a projective resolution is the zero morphism.
|
CategoryTheory.ProjectiveResolution.exact_succ
theorem CategoryTheory.ProjectiveResolution.exact_succ :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
[inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {Z : C} (P : CategoryTheory.ProjectiveResolution Z) (n : ℕ),
(CategoryTheory.ShortComplex.mk (P.complex.d (n + 2) (n + 1)) (P.complex.d (n + 1) n) ⋯).Exact
This theorem states that for any category `C` (with `C` being a type), given that `C` has zero objects and zero morphisms, and for any object `Z` in `C` and a projective resolution `P` of `Z`, the short complex made from the differential maps `d` at positions `n+2` to `n+1` and `n+1` to `n` in the complex `P` is an exact sequence. In category theory, an exact sequence is a sequence of objects and morphisms between them such that the image of one morphism is equal to the kernel of the next.
More concisely: Given a category `C` with zero objects and morphisms, for any projective resolution `P` of an object `Z` in `C`, the sequence obtained by considering the differential maps from positions `n+2` to `n+1` and `n+1` to `n` forms an exact sequence in `C`.
|