CategoryTheory.ShortComplex.quasiIso_iff
theorem CategoryTheory.ShortComplex.quasiIso_iff :
∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{S₁ S₂ : CategoryTheory.ShortComplex C} [inst_2 : S₁.HasHomology] [inst_3 : S₂.HasHomology] (φ : S₁ ⟶ S₂),
CategoryTheory.ShortComplex.QuasiIso φ ↔ CategoryTheory.IsIso (CategoryTheory.ShortComplex.homologyMap φ)
This theorem states that for any two short complexes `S₁` and `S₂` in a category `C`, which possesses zero morphisms, and for any morphism `φ` from `S₁` to `S₂`, the short complex `φ` is a quasi-isomorphism if and only if the homology map of `φ` is an isomorphism. Essentially, this theorem is revealing a connection between the concepts of quasi-isomorphism in the domain of short complexes and isomorphism in the domain of homology maps.
More concisely: A morphism between short complexes in a category with zero morphisms is a quasi-isomorphism if and only if its induced homology map is an isomorphism.
|
CategoryTheory.ShortComplex.LeftHomologyMapData.quasiIso_iff
theorem CategoryTheory.ShortComplex.LeftHomologyMapData.quasiIso_iff :
∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{S₁ S₂ : CategoryTheory.ShortComplex C} [inst_2 : S₁.HasHomology] [inst_3 : S₂.HasHomology] {φ : S₁ ⟶ S₂}
{h₁ : S₁.LeftHomologyData} {h₂ : S₂.LeftHomologyData}
(γ : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂),
CategoryTheory.ShortComplex.QuasiIso φ ↔ CategoryTheory.IsIso γ.φH
This theorem states that in the context of a category `C` equipped with zero morphisms, given two short complexes `S₁` and `S₂` that have homologies, a morphism `φ` from `S₁` to `S₂`, and left homology data `h₁` for `S₁` and `h₂` for `S₂`, then a left homology map data `γ` for `φ`, `h₁`, and `h₂` exists if and only if `φ` is a quasi-isomorphism in the short complex category if and only if the associated `φH` in the left homology map data `γ` is an isomorphism in the category `C`.
More concisely: A morphism `φ` between two short complexes `S₁` and `S₂` in a category `C` equipped with zero morphisms with homologies and given left homology data `h₁` for `S₁` and `h₂` for `S₂`, has an isomorphism `γ(φ)` in the category of left homology data if and only if `φ` is a quasi-isomorphism and `γ(φ)` is an isomorphism in the category `C`.
|
CategoryTheory.ShortComplex.RightHomologyMapData.quasiIso_iff
theorem CategoryTheory.ShortComplex.RightHomologyMapData.quasiIso_iff :
∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{S₁ S₂ : CategoryTheory.ShortComplex C} [inst_2 : S₁.HasHomology] [inst_3 : S₂.HasHomology] {φ : S₁ ⟶ S₂}
{h₁ : S₁.RightHomologyData} {h₂ : S₂.RightHomologyData}
(γ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂),
CategoryTheory.ShortComplex.QuasiIso φ ↔ CategoryTheory.IsIso γ.φH
This theorem states that for any two short complexes `S₁` and `S₂` in a category `C`, which has zero morphisms, and given certain homological data `h₁` and `h₂` for these complexes, a specific morphism `φ` from `S₁` to `S₂` is a quasi-isomorphism if and only if a certain morphism `γ.φH` associated with the mapping data `γ` (which is based on `φ`, `h₁`, and `h₂`) is an isomorphism. This theorem thus establishes a connection between the concepts of quasi-isomorphisms of short complexes and isomorphisms of their associated homological mapping data.
More concisely: A morphism between two short complexes in a zero-morphism category is a quasi-isomorphism if and only if the associated homological morphism induced by mapping data is an isomorphism.
|
CategoryTheory.ShortComplex.QuasiIso.isIso'
theorem CategoryTheory.ShortComplex.QuasiIso.isIso' :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{S₁ S₂ : CategoryTheory.ShortComplex C} [inst_2 : S₁.HasHomology] [inst_3 : S₂.HasHomology] {φ : S₁ ⟶ S₂}
[self : CategoryTheory.ShortComplex.QuasiIso φ],
CategoryTheory.IsIso (CategoryTheory.ShortComplex.homologyMap φ)
This theorem states that in the context of a category `C` which has zero morphisms, given two short complexes `S₁` and `S₂` which both have homology, and a morphism `φ` from `S₁` to `S₂` that is a quasi-isomorphism, the homology map of `φ` is an isomorphism. This is an important result in abstract algebra and category theory, specifically in the study of homological algebra where we look at algebraic structures from the point of view of their homologies.
More concisely: In a category with zero morphisms, if two short complexes have homology and a quasi-isomorphism between them induces isomorphisms on homologies, then the homology map of the quasi-isomorphism is an isomorphism.
|