HomologicalComplex.opcycles_right_exact
theorem HomologicalComplex.opcycles_right_exact :
∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{u_3, u_1} C] [inst_1 : CategoryTheory.Abelian C]
{c : ComplexShape ι} (S : CategoryTheory.ShortComplex (HomologicalComplex C c)),
S.Exact →
∀ [inst_2 : CategoryTheory.Epi S.g] (i : ι) [inst_3 : S.X₁.HasHomology i] [inst_4 : S.X₂.HasHomology i]
[inst_5 : S.X₃.HasHomology i],
(CategoryTheory.ShortComplex.mk (HomologicalComplex.opcyclesMap S.f i) (HomologicalComplex.opcyclesMap S.g i)
⋯).Exact
This theorem states that if there exists an exact sequence of homological complexes `X₁ ⟶ X₂ ⟶ X₃ ⟶ 0`, then there exists another exact sequence `X₁.opcycles i ⟶ X₂.opcycles i ⟶ X₃.opcycles i ⟶ 0`. More specifically, it verifies the exactness at `X₂.opcycles i`, while the fact that `X₂.opcycles i ⟶ X₃.opcycles i` is an epimorphism is an instance. This statement is valid for any category `C` (with `C` being Abelian), any complex shape `c`, and any short complex `S` composed of the aforementioned homological complexes.
More concisely: Given an exact sequence of homological complexes `X₁ ⟶ X₂ ⟶ X₃ ⟶ 0` in an Abelian category, the sequence `X₁.opcycles ⟶ X₂.opcycles ⟶ X₃.opcycles ⟶ 0` is exact at `X₂.opcycles`.
|
HomologicalComplex.HomologySequence.composableArrows₃_exact
theorem HomologicalComplex.HomologySequence.composableArrows₃_exact :
∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{u_3, u_1} C]
[inst_1 : CategoryTheory.Preadditive C] {c : ComplexShape ι} (K : HomologicalComplex C c) (i j : ι),
c.Rel i j →
∀ [inst_2 : CategoryTheory.CategoryWithHomology C],
(HomologicalComplex.HomologySequence.composableArrows₃ K i j).Exact
This theorem states that for any given complex shape `c`, homological complex `K`, and indices `i` and `j` in the complex shape, if a relation `c.Rel` exists between `i` and `j`, then the sequence of mappings `K.homology i ⟶ K.opcycles i ⟶ K.cycles j ⟶ K.homology j` is exact in the context of a category with homology. Here, "exact" refers to the property of a sequence in category theory where the image of one morphism equals the kernel of the next.
More concisely: For any complex shape `c` and homological complex `K`, if `i` and `j` are indices with a relation `c.Rel` between them, then the sequence of homomorphisms from `K.homology i` to `K.opcycles i` to `K.cycles j` to `K.homology j` forms an exact sequence in the category of homology groups.
|
CategoryTheory.ShortComplex.ShortExact.homology_exact₁
theorem CategoryTheory.ShortComplex.ShortExact.homology_exact₁ :
∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{u_3, u_1} C] [inst_1 : CategoryTheory.Abelian C]
{c : ComplexShape ι} {S : CategoryTheory.ShortComplex (HomologicalComplex C c)} (hS : S.ShortExact) (i j : ι)
(hij : c.Rel i j),
(CategoryTheory.ShortComplex.mk (hS.δ i j hij) (HomologicalComplex.homologyMap S.f j) ⋯).Exact
The theorem `CategoryTheory.ShortComplex.ShortExact.homology_exact₁` states that for any category `C` of type `u_1` and any `ι` of type `u_2`, assuming `C` is an Abelian category, given a complex shape `c`, and a short complex `S` of a homological complex `C c`, if `S` is short exact (i.e., it satisfies the properties of a short exact sequence), then for any indices `i` and `j` such that `i` is related to `j` in complex shape `c`, the sequence formed by `S.X₃.homology i ⟶ S.X₁.homology j ⟶ S.X₂.homology j` is exact. In the context of homological algebra, an exact sequence is a sequence of morphisms between objects such that the image of one morphism is equal to the kernel of the next.
More concisely: Given an Abelian category `C` and a short exact complex `S` in `C`, the sequence obtained from the homology of `S` along any two homologically connected indices `i` and `j` is exact.
|
HomologicalComplex.cycles_left_exact
theorem HomologicalComplex.cycles_left_exact :
∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{u_3, u_1} C] [inst_1 : CategoryTheory.Abelian C]
{c : ComplexShape ι} (S : CategoryTheory.ShortComplex (HomologicalComplex C c)),
S.Exact →
∀ [inst_2 : CategoryTheory.Mono S.f] (i : ι) [inst_3 : S.X₁.HasHomology i] [inst_4 : S.X₂.HasHomology i]
[inst_5 : S.X₃.HasHomology i],
(CategoryTheory.ShortComplex.mk (HomologicalComplex.cyclesMap S.f i) (HomologicalComplex.cyclesMap S.g i)
⋯).Exact
This theorem states that if there is an exact sequence of homological complex `0 ⟶ X₁ ⟶ X₂ ⟶ X₃`, then the sequence `0 ⟶ X₁.cycles i ⟶ X₂.cycles i ⟶ X₃.cycles i` is also exact, specifically at `X₂.cycles i`. This follows from the exactness of the original sequence and the fact that `X₁.cycles i ⟶ X₂.cycles i` is a monomorphism. The theorem applies to any abelian category and any complex shape, and it deals with the homology at an arbitrary point `i`.
More concisely: If `0 ⟶ X₁ ⟶ X₂ ⟶ X₃` is an exact sequence of homological complexes in an abelian category, then so is `0 ⟶ X₁.cycles i ⟶ X₂.cycles i ⟶ X₃.cycles i` at `X₂.cycles i`, where `i` is an arbitrary point.
|
CategoryTheory.ShortComplex.ShortExact.homology_exact₃
theorem CategoryTheory.ShortComplex.ShortExact.homology_exact₃ :
∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{u_3, u_1} C] [inst_1 : CategoryTheory.Abelian C]
{c : ComplexShape ι} {S : CategoryTheory.ShortComplex (HomologicalComplex C c)} (hS : S.ShortExact) (i j : ι)
(hij : c.Rel i j),
(CategoryTheory.ShortComplex.mk (HomologicalComplex.homologyMap S.g i) (hS.δ i j hij) ⋯).Exact
The theorem `CategoryTheory.ShortComplex.ShortExact.homology_exact₃` states that for any given type `C` which forms a category and is Abelian, any complex shape `c`, and any short complex `S` on the homological complex of `C` with shape `c` that is short exact, for any index `i` and `j` such that `i` is related to `j` in the complex shape `c`, the sequence `S.X₂.homology i ⟶ S.X₃.homology i ⟶ S.X₁.homology j` is exact. Here, `S.X₂.homology i`, `S.X₃.homology i`, and `S.X₁.homology j` are the homologies of the second, third, and first objects in the short complex `S` at positions `i` and `j`.
More concisely: For any Abelian category C and short exact complex S on C with shape c, the sequence of homologies S.X₂.homology i ← S.X₃.homology i → S.X₁.homology j is exact for all i and j related in c.
|
CategoryTheory.ShortComplex.ShortExact.homology_exact₂
theorem CategoryTheory.ShortComplex.ShortExact.homology_exact₂ :
∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{u_3, u_1} C] [inst_1 : CategoryTheory.Abelian C]
{c : ComplexShape ι} {S : CategoryTheory.ShortComplex (HomologicalComplex C c)},
S.ShortExact →
∀ (i : ι),
(CategoryTheory.ShortComplex.mk (HomologicalComplex.homologyMap S.f i) (HomologicalComplex.homologyMap S.g i)
⋯).Exact
This theorem states that given a category `C` which is Abelian, and a short complex `S` of homological complexes in `C`, if `S` is short exact, then for any object `i` in the indexing category `ι`, the sequence formed by the homology maps of `S.X1`, `S.X2`, and `S.X3` at `i` is exact. In other words, the image of the first homology map is equal to the kernel of the second. This is a key property in the theory of homological algebra.
More concisely: Given an Abelian category `C` and a short exact complex `S` in `C`, the sequence of homology groups formed by `S.X1`, `S.X2`, and `S.X3` at any object `i` in the indexing category is an exact sequence.
|