HomotopyEquiv.toQuasiIso'
theorem HomotopyEquiv.toQuasiIso' :
∀ {ι : Type u_1} {c : ComplexShape ι} {W : Type u_2} [inst : CategoryTheory.Category.{u_3, u_2} W]
[inst_1 : CategoryTheory.Preadditive W] [inst_2 : CategoryTheory.Limits.HasCokernels W]
[inst_3 : CategoryTheory.Limits.HasImages W] [inst_4 : CategoryTheory.Limits.HasEqualizers W]
[inst_5 : CategoryTheory.Limits.HasImageMaps W] {C D : HomologicalComplex W c} (e : HomotopyEquiv C D),
QuasiIso' e.hom
This theorem states that for any type ι, any complex shape `c`, any type `W` that forms a category, and any two homological complexes `C` and `D` within the category `W`, if `W` is preadditive, has cokernels, images, equalizers, and image maps, then a homotopy equivalence `e` from `C` to `D` is also a quasi-isomorphism. In other words, a map that induces an isomorphism on the homology groups, known as a homotopy equivalence, also induces an isomorphism on a higher homotopy category, and is thus a quasi-isomorphism.
More concisely: If `W` is a preadditive category with cokernels, images, equalizers, and image maps, then a homotopy equivalence between two complexes in `W` is a quasi-isomorphism.
|
Mathlib.Algebra.Homology.QuasiIso._auxLemma.5
theorem Mathlib.Algebra.Homology.QuasiIso._auxLemma.5 :
∀ {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 from the Mathlib Algebra Homology library states that for any category `C`, which has zero morphisms, and any two short complexes `S₁` and `S₂` in `C`, if `S₁` and `S₂` both have homology and there is a morphism `φ` from `S₁` to `S₂`, then `φ` is a quasi-isomorphism in the short complex if and only if the `φ` map in homology is an isomorphism.
More concisely: For any short complexes $S\_1$ and $S\_2$ in a category $C$ with zero morphisms, if $S\_1$ and $S\_2$ have homology and there's a morphism $\varphi$ from $S\_1$ to $S\_2$, then $\varphi$ is a quasi-isomorphism in the short complex if and only if the homology map $\varphi_\ast$ is an isomorphism.
|
quasiIsoAt_iff
theorem quasiIsoAt_iff :
∀ {ι : Type u_2} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
[inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K L : HomologicalComplex C c}
(f : K ⟶ L) (i : ι) [inst_2 : K.HasHomology i] [inst_3 : L.HasHomology i],
QuasiIsoAt f i ↔ CategoryTheory.ShortComplex.QuasiIso ((HomologicalComplex.shortComplexFunctor C c i).map f)
In the setting of category theory, the theorem `quasiIsoAt_iff` establishes an equivalence between two properties concerning homological complexes. Given types `ι` and `C`, with `C` being a category that has zero morphisms, a complex shape `c`, and two homological complexes `K` and `L` over `C` with shape `c`, as well as a morphism `f` from `K` to `L` and an index `i` in `ι`, the theorem states that `f` is a quasi-isomorphism at the level `i` if and only if the map induced by `f` on the short complexes associated with `K` and `L` at level `i` is a quasi-isomorphism in the category of short complexes. This equivalence holds under the assumption that both `K` and `L` have homology at degree `i`.
More concisely: A morphism between homological complexes over a zero-morphism category is a quasi-isomorphism at a given degree if and only if the induced map on short complexes at that degree is a quasi-isomorphism. (Assumes homology exists at that degree.)
|
Mathlib.Algebra.Homology.QuasiIso._auxLemma.4
theorem Mathlib.Algebra.Homology.QuasiIso._auxLemma.4 :
∀ {ι : Type u_2} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
[inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K L : HomologicalComplex C c}
(f : K ⟶ L) (i : ι) [inst_2 : K.HasHomology i] [inst_3 : L.HasHomology i],
QuasiIsoAt f i = CategoryTheory.ShortComplex.QuasiIso ((HomologicalComplex.shortComplexFunctor C c i).map f)
This theorem states that for any type `ι`, any category `C` with zero morphisms, any `ComplexShape` `c`, any two `HomologicalComplex` `K` and `L` in the category `C` with shape `c`, a morphism `f` from `K` to `L`, and index `i`, if `K` has homology in degree `i` and `L` has homology in degree `i`, then the `QuasiIsoAt` of the morphism `f` at index `i` is equal to the quasi-isomorphism of the map of `f` under the action of the functor `shortComplexFunctor` at index `i`.
In other words, it asserts the equivalence between a quasi-isomorphism at a given index in a homological complex and the corresponding quasi-isomorphism in the associated short complex at that index.
More concisely: For any type `ι`, category `C` with zero morphisms, `ComplexShape` `c`, `HomologicalComplex` `K` and `L` in `C` with shape `c`, morphism `f` from `K` to `L`, and index `i`, if `K` and `L` have homology in degree `i`, then `QuasiIsoAt i f` equals the quasi-isomorphism of `f` under `shortComplexFunctor` at index `i`.
|
quasiIsoAt_iff_isIso_homologyMap
theorem quasiIsoAt_iff_isIso_homologyMap :
∀ {ι : Type u_2} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
[inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K L : HomologicalComplex C c}
(f : K ⟶ L) (i : ι) [inst_2 : K.HasHomology i] [inst_3 : L.HasHomology i],
QuasiIsoAt f i ↔ CategoryTheory.IsIso (HomologicalComplex.homologyMap f i)
This theorem, `quasiIsoAt_iff_isIso_homologyMap`, states that for any homological complexes `K` and `L` of objects in a category `C` (where `C` has zero morphisms and is indexed by some type `ι` in a complex shape `c`), and for any morphism `f` from `K` to `L` and index `i`, `f` is a quasi-isomorphism at index `i` if and only if the map arising from `f` on the homology at index `i` is an isomorphism. Here, the homology exists at index `i` for both `K` and `L`.
In other words, the theorem is about the relationship between a 'quasi-isomorphism at a specific index' and an 'isomorphism of the homology map at the same index'. They are equivalent concepts according to this theorem.
More concisely: For homological complexes K and L in a zero-morphism category C indexed by ι, and a morphism f from K to L, f is a quasi-isomorphism at index i if and only if the map on i-th homologies induced by f is an isomorphism.
|