CategoryTheory.InjectiveResolution.ι_f_succ
theorem CategoryTheory.InjectiveResolution.ι_f_succ :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
[inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {Z : C} (I : CategoryTheory.InjectiveResolution Z) (n : ℕ),
I.ι.f (n + 1) = 0
This theorem states that for any category `C` that has a zero object and zero morphisms, and for any object `Z` in `C` for which we have an injective resolution `I`, the `n+1`-th morphism in the injective resolution is a zero morphism. Here, `n` is any natural number. In terms of category theory, it's saying that in the sequence of morphisms that make up the injective resolution, each morphism after the first one is a zero morphism.
More concisely: For any category with a zero object and zero morphisms, the morphisms in an injective resolution of an object are zero morphisms from the second onwards.
|
CategoryTheory.InjectiveResolution.injective
theorem CategoryTheory.InjectiveResolution.injective :
∀ {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.InjectiveResolution Z) (n : ℕ),
CategoryTheory.Injective (self.cocomplex.X n)
This theorem states that for any category 'C' with a zero object and zero morphisms, and any object 'Z' in 'C', the cochain complex of an injective resolution of 'Z' is injective for every natural number 'n'. Essentially, it asserts the injectivity of each degree in the cochain complex associated with an injective resolution in a given category.
More concisely: In any category with a zero object and zero morphisms, the cochain complex of an injective resolution of an object is injective in every degree.
|
CategoryTheory.InjectiveResolution.hasHomology
theorem CategoryTheory.InjectiveResolution.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.InjectiveResolution Z) (i : ℕ),
HomologicalComplex.HasHomology self.cocomplex i
The theorem `CategoryTheory.InjectiveResolution.hasHomology` states that for any category `C` with zero object and zero morphisms, any object `Z` in `C`, and any injective resolution `self` of `Z`, the cochain complex `self.cocomplex` has homology at any non-negative integer degree `i`. In other words, for every integer `i`, the associated short complex of the `i`-th component of the cochain complex in the injective resolution has homology.
More concisely: For any category with zero object and zero morphisms, every injective resolution of an object has non-negative degree homology.
|
CategoryTheory.InjectiveResolution.ι_f_zero_comp_complex_d
theorem CategoryTheory.InjectiveResolution.ι_f_zero_comp_complex_d :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
[inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {Z : C} (I : CategoryTheory.InjectiveResolution Z),
CategoryTheory.CategoryStruct.comp (I.ι.f 0) (I.cocomplex.d 0 1) = 0
This theorem, `CategoryTheory.InjectiveResolution.ι_f_zero_comp_complex_d`, states that for all categories `C` of type `u` that have zero objects and zero morphisms, and for any object `Z` in `C` with an injective resolution `I`, the composition of the morphism `I.ι.f 0` and the differential `I.cocomplex.d 0 1` in the chain complex equals the zero morphism. In other words, the differential of a zero morphism in a chain complex is zero when composed with another morphism.
More concisely: For any injective resolution I of an object Z in a zero category C, the composition of I.ι.f 0 and I.cocomplex.d 0 1 is the zero morphism.
|
CategoryTheory.InjectiveResolution.quasiIso
theorem CategoryTheory.InjectiveResolution.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.InjectiveResolution Z),
QuasiIso self.ι
The theorem states that, for any type `C` that is a category with zero objects and zero morphisms, and for any object `Z` in the category `C`, the morphism from the single cochain complex with `Z` in degree `0` is a quasi-isomorphism. This property is proven for any injective resolution of `Z`. Here, an injective resolution is a specific kind of object in homological algebra, and a quasi-isomorphism is a morphism that induces a bijection on homology.
More concisely: For any category `C` with zero objects and morphisms, and any object `Z` in `C`, the single cochain complex of `Z` is quasi-isomorphic to any injective resolution of `Z`.
|
CategoryTheory.HasInjectiveResolution.out
theorem CategoryTheory.HasInjectiveResolution.out :
∀ {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.HasInjectiveResolution Z],
Nonempty (CategoryTheory.InjectiveResolution Z)
The theorem `CategoryTheory.HasInjectiveResolution.out` states that for any given object `Z` in a category `C`, there exists an injective resolution if `C` is a category with a zero object and zero morphisms. An injective resolution is a specific kind of resolution in category theory, which in this context, is a non-empty sequence of morphisms from one object to another.
More concisely: In a category with a zero object and zero morphisms, every object has an injective resolution.
|
CategoryTheory.InjectiveResolution.exact_succ
theorem CategoryTheory.InjectiveResolution.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} (I : CategoryTheory.InjectiveResolution Z) (n : ℕ),
(CategoryTheory.ShortComplex.mk (I.cocomplex.d n (n + 1)) (I.cocomplex.d (n + 1) (n + 2)) ⋯).Exact
This theorem states that for any category `C` (of a certain type `u`), given that `C` has a zero object and zero morphisms, any object `Z` in `C` and its corresponding injective resolution `I`, for any natural number `n`, the short complex created by the differentials of `I` at indices `n` and `n+1`, and `n+1` and `n+2`, is exact. In category theory, a short exact sequence (or more specifically here, a short complex) is a certain sequence of morphisms between objects such that certain conditions hold, which captures some important properties of the objects and their relationships.
More concisely: For any category `C` of type `u` with a zero object and zero morphisms, the short complex formed by the differentials of an injective resolution of an object `Z` in `C` is exact at degrees `n` and `n+1`.
|