The homology of a canonical truncation #
Given an embedding of complex shapes e : Embedding c c', we shall
relate the homology of K : HomologicalComplex C c' and of
K.truncGE e : HomologicalComplex C c' (TODO).
So far, we only compute the homology of K.truncGE' e : HomologicalComplex C c.
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'_f
{ι : 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
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)
:
CategoryTheory.Limits.IsLimit
(CategoryTheory.Limits.KernelFork.ofι
(CategoryTheory.CategoryStruct.comp (K.homologyι j') (K.truncGE'XIsoOpcycles e hj' hj).inv) ⋯)
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)
:
(homologyData K e i j k hk hj' hj).right.g' = (K.truncGE' e).d j k
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