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.truncGE e : HomologicalComplex C c'.
The main result is that K.πTruncGE e : K ⟶ K.truncGE e induces a
quasi-isomorphism in degree e.f i for all i. (Note that the complex
K.truncGE e is exact in degrees that are not in the image of e.f.)
theorem
HomologicalComplex.truncGE'.hasHomology_sc'_of_not_mem_boundary
{ι : 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.IsTruncGE]
[∀ (i' : ι'), K.HasHomology i']
(i j k : ι)
(hi : c.prev j = i)
(hk : c.next j = k)
(hj : ¬e.BoundaryGE j)
:
((K.truncGE' e).sc' i j k).HasHomology
theorem
HomologicalComplex.truncGE'.hasHomology_of_not_mem_boundary
{ι : 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.IsTruncGE]
[∀ (i' : ι'), K.HasHomology i']
(j : ι)
(hj : ¬e.BoundaryGE j)
:
(K.truncGE' e).HasHomology j
theorem
HomologicalComplex.truncGE'.quasiIsoAt_restrictionToTruncGE'
{ι : 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.IsTruncGE]
[∀ (i' : ι'), K.HasHomology i']
(j : ι)
(hj : ¬e.BoundaryGE j)
[(K.restriction e).HasHomology j]
[(K.truncGE' e).HasHomology j]
:
QuasiIsoAt (K.restrictionToTruncGE' e) j
K.restrictionToTruncGE' e is a quasi-isomorphism in degrees that are not at the boundary.
theorem
HomologicalComplex.truncGE'.homologyι_truncGE'XIsoOpcycles_inv_d
{ι : 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.IsTruncGE]
[∀ (i' : ι'), K.HasHomology i']
(j k : ι)
{j' : ι'}
(hj' : e.f j = j')
(hj : e.BoundaryGE j)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.CategoryStruct.comp (K.homologyι j') (K.truncGE'XIsoOpcycles e hj' hj).inv) ((K.truncGE' e).d j k) = 0
noncomputable def
HomologicalComplex.truncGE'.isLimitKernelFork
{ι : 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.IsTruncGE]
[∀ (i' : ι'), K.HasHomology i']
(j k : ι)
(hk : c.next j = k)
{j' : ι'}
(hj' : e.f j = j')
(hj : e.BoundaryGE j)
:
Auxiliary definition for truncGE'.homologyData.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
HomologicalComplex.truncGE'.homologyData
{ι : 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.IsTruncGE]
[∀ (i' : ι'), K.HasHomology i']
(i j k : ι)
(hk : c.next j = k)
{j' : ι'}
(hj' : e.f j = j')
(hj : e.BoundaryGE j)
:
((K.truncGE' e).sc' i j k).HomologyData
When j is at the boundary of the embedding e of complex shapes,
this is a homology data for K.truncGE' e in degree j: the homology is
given by K.homology j' where e.f j = j'.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
HomologicalComplex.truncGE'.homologyData_right_g'
{ι : 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.IsTruncGE]
[∀ (i' : ι'), K.HasHomology i']
(i j k : ι)
(hk : c.next j = k)
{j' : ι'}
(hj' : e.f j = j')
(hj : e.BoundaryGE j)
:
Computation of the right.g' field of truncGE'.homologyData K e i j k hk hj' hj.
instance
HomologicalComplex.truncGE'.truncGE'_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.IsTruncGE]
[∀ (i' : ι'), K.HasHomology i']
(i : ι)
:
(K.truncGE' e).HasHomology i
instance
HomologicalComplex.truncGE.instHasHomology
{ι : 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.IsTruncGE]
[∀ (i' : ι'), K.HasHomology i']
[CategoryTheory.Limits.HasZeroObject C]
(i' : ι')
:
(K.truncGE e).HasHomology i'
noncomputable def
HomologicalComplex.truncGE.rightHomologyMapData
{ι : 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.IsTruncGE]
[∀ (i' : ι'), K.HasHomology i']
[CategoryTheory.Limits.HasZeroObject C]
{i j k : ι}
{j' : ι'}
(hj' : e.f j = j')
(hi : c.prev j = i)
(hk : c.next j = k)
(hj : e.BoundaryGE j)
:
CategoryTheory.ShortComplex.RightHomologyMapData ((shortComplexFunctor C c' j').map (K.πTruncGE e))
(CategoryTheory.ShortComplex.RightHomologyData.canonical (K.sc j'))
(extend.rightHomologyData (K.truncGE' e) e hj' hi ⋯ hk ⋯ (truncGE'.homologyData K e i j k hk hj' hj).right)
The right homology data which allows to show that K.πTruncGE e
induces an isomorphism in homology in degrees j' such that e.f j = j' for some j.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
HomologicalComplex.truncGE.rightHomologyMapData_φH
{ι : 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.IsTruncGE]
[∀ (i' : ι'), K.HasHomology i']
[CategoryTheory.Limits.HasZeroObject C]
{i j k : ι}
{j' : ι'}
(hj' : e.f j = j')
(hi : c.prev j = i)
(hk : c.next j = k)
(hj : e.BoundaryGE j)
:
(rightHomologyMapData K e hj' hi hk hj).φH = CategoryTheory.CategoryStruct.id (CategoryTheory.ShortComplex.RightHomologyData.canonical (K.sc j')).H
@[simp]
theorem
HomologicalComplex.truncGE.rightHomologyMapData_φQ
{ι : 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.IsTruncGE]
[∀ (i' : ι'), K.HasHomology i']
[CategoryTheory.Limits.HasZeroObject C]
{i j k : ι}
{j' : ι'}
(hj' : e.f j = j')
(hi : c.prev j = i)
(hk : c.next j = k)
(hj : e.BoundaryGE j)
:
theorem
HomologicalComplex.quasiIsoAt_πTruncGE
{ι : 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.IsTruncGE]
[∀ (i' : ι'), K.HasHomology i']
[CategoryTheory.Limits.HasZeroObject C]
{j : ι}
{j' : ι'}
(hj' : e.f j = j')
:
QuasiIsoAt (K.πTruncGE e) j'
instance
HomologicalComplex.instQuasiIsoAtπTruncGEF
{ι : 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.IsTruncGE]
[∀ (i' : ι'), K.HasHomology i']
[CategoryTheory.Limits.HasZeroObject C]
(i : ι)
:
QuasiIsoAt (K.πTruncGE e) (e.f i)
theorem
HomologicalComplex.quasiIso_πTruncGE_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.IsTruncGE]
[∀ (i' : ι'), K.HasHomology i']
[CategoryTheory.Limits.HasZeroObject C]
:
theorem
HomologicalComplex.acyclic_truncGE_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.IsTruncGE]
[∀ (i' : ι'), K.HasHomology i']
[CategoryTheory.Limits.HasZeroObject C]
:
theorem
HomologicalComplex.quasiIso_truncGEMap_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.IsTruncGE]
[∀ (i' : ι'), K.HasHomology i']
[∀ (i' : ι'), L.HasHomology i']
[CategoryTheory.Limits.HasZeroObject C]
: