The homology of a canonical truncation #
Given an embedding of complex shapes e : Embedding c c',
we relate the homology of K : HomologicalComplex C c' and of
K.truncLE e : HomologicalComplex C c'.
The main result is that K.ιTruncLE e : K.truncLE e ⟶ K induces a
quasi-isomorphism in degree e.f i for all i. (Note that the complex
K.truncLE e is exact in degrees that are not in the image of e.f.)
All the results are obtained by dualising the results in the file Embedding.TruncGEHomology.
theorem
HomologicalComplex.truncLE'.quasiIsoAt_truncLE'ToRestriction
{ι : Type u_1}
{ι' : Type u_2}
{c : ComplexShape ι}
{c' : ComplexShape ι'}
{C : Type u_3}
[CategoryTheory.Category.{u_4, u_3} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
(K : HomologicalComplex C c')
(e : c.Embedding c')
[e.IsTruncLE]
[∀ (i' : ι'), K.HasHomology i']
(j : ι)
(hj : ¬e.BoundaryLE j)
[(K.restriction e).HasHomology j]
[(K.truncLE' e).HasHomology j]
:
QuasiIsoAt (K.truncLE'ToRestriction e) j
K.truncLE'ToRestriction e is a quasi-isomorphism in degrees that are not at the boundary.
instance
HomologicalComplex.truncLE'.truncLE'_hasHomology
{ι : Type u_1}
{ι' : Type u_2}
{c : ComplexShape ι}
{c' : ComplexShape ι'}
{C : Type u_3}
[CategoryTheory.Category.{u_4, u_3} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
(K : HomologicalComplex C c')
(e : c.Embedding c')
[e.IsTruncLE]
[∀ (i' : ι'), K.HasHomology i']
(i : ι)
:
(K.truncLE' e).HasHomology i
instance
HomologicalComplex.instHasHomologyTruncLE
{ι : Type u_1}
{ι' : Type u_2}
{c : ComplexShape ι}
{c' : ComplexShape ι'}
{C : Type u_3}
[CategoryTheory.Category.{u_4, u_3} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
(K : HomologicalComplex C c')
(e : c.Embedding c')
[e.IsTruncLE]
[∀ (i' : ι'), K.HasHomology i']
[CategoryTheory.Limits.HasZeroObject C]
(i' : ι')
:
(K.truncLE e).HasHomology i'
theorem
HomologicalComplex.quasiIsoAt_ιTruncLE
{ι : Type u_1}
{ι' : Type u_2}
{c : ComplexShape ι}
{c' : ComplexShape ι'}
{C : Type u_3}
[CategoryTheory.Category.{u_4, u_3} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
(K : HomologicalComplex C c')
(e : c.Embedding c')
[e.IsTruncLE]
[∀ (i' : ι'), K.HasHomology i']
[CategoryTheory.Limits.HasZeroObject C]
{j : ι}
{j' : ι'}
(hj' : e.f j = j')
:
QuasiIsoAt (K.ιTruncLE e) j'
instance
HomologicalComplex.instQuasiIsoAtιTruncLEF
{ι : Type u_1}
{ι' : Type u_2}
{c : ComplexShape ι}
{c' : ComplexShape ι'}
{C : Type u_3}
[CategoryTheory.Category.{u_4, u_3} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
(K : HomologicalComplex C c')
(e : c.Embedding c')
[e.IsTruncLE]
[∀ (i' : ι'), K.HasHomology i']
[CategoryTheory.Limits.HasZeroObject C]
(i : ι)
:
QuasiIsoAt (K.ιTruncLE e) (e.f i)
theorem
HomologicalComplex.quasiIso_ιTruncLE_iff_isSupported
{ι : Type u_1}
{ι' : Type u_2}
{c : ComplexShape ι}
{c' : ComplexShape ι'}
{C : Type u_3}
[CategoryTheory.Category.{u_4, u_3} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
(K : HomologicalComplex C c')
(e : c.Embedding c')
[e.IsTruncLE]
[∀ (i' : ι'), K.HasHomology i']
[CategoryTheory.Limits.HasZeroObject C]
:
theorem
HomologicalComplex.acyclic_truncLE_iff_isSupportedOutside
{ι : Type u_1}
{ι' : Type u_2}
{c : ComplexShape ι}
{c' : ComplexShape ι'}
{C : Type u_3}
[CategoryTheory.Category.{u_4, u_3} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
(K : HomologicalComplex C c')
(e : c.Embedding c')
[e.IsTruncLE]
[∀ (i' : ι'), K.HasHomology i']
[CategoryTheory.Limits.HasZeroObject C]
:
theorem
HomologicalComplex.quasiIso_truncLEMap_iff
{ι : Type u_1}
{ι' : Type u_2}
{c : ComplexShape ι}
{c' : ComplexShape ι'}
{C : Type u_3}
[CategoryTheory.Category.{u_4, u_3} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{K L : HomologicalComplex C c'}
(φ : K ⟶ L)
(e : c.Embedding c')
[e.IsTruncLE]
[∀ (i' : ι'), K.HasHomology i']
[∀ (i' : ι'), L.HasHomology i']
[CategoryTheory.Limits.HasZeroObject C]
: