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.

Moreover, if C is an abelian category, we introduce the cokernel sequence K.shortComplexTruncLE e of the monomorphism K.ιTruncLE e.

theorem HomologicalComplex.truncLE'.quasiIsoAt_truncLE'ToRestriction {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, 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] : QuasiIso (K.ιTruncLE e) ↔ K.IsSupported e

theorem HomologicalComplex.acyclic_truncLE_iff_isSupportedOutside {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{v_1, 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] : (K.truncLE e).Acyclic ↔ K.IsSupportedOutside e

theorem HomologicalComplex.Acyclic.truncLE {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{v_1, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K : HomologicalComplex C c'} [∀ (i' : ι'), K.HasHomology i'] [CategoryTheory.Limits.HasZeroObject C] (hK : K.Acyclic) (e : c.Embedding c') [e.IsTruncLE] : (K.truncLE e).Acyclic

theorem HomologicalComplex.quasiIso_truncLEMap_iff {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{v_1, 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] : QuasiIso (truncLEMap φ e) ↔ ∀ (i : ι) (i' : ι'), e.f i = i' → QuasiIsoAt φ i'

noncomputable def HomologicalComplex.shortComplexTruncLE {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{v_1, u_3} C] [CategoryTheory.Abelian C] (K : HomologicalComplex C c') (e : c.Embedding c') [e.IsTruncLE] : CategoryTheory.ShortComplex (HomologicalComplex C c')

The cokernel sequence of the monomorphism K.ιTruncLE e.

Equations

• K.shortComplexTruncLE e = { X₁ := K.truncLE e, X₂ := K, X₃ := CategoryTheory.Limits.cokernel (K.ιTruncLE e), f := K.ιTruncLE e, g := CategoryTheory.Limits.cokernel.π (K.ιTruncLE e), zero := ⋯ }

@[simp]

theorem HomologicalComplex.shortComplexTruncLE_f {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{v_1, u_3} C] [CategoryTheory.Abelian C] (K : HomologicalComplex C c') (e : c.Embedding c') [e.IsTruncLE] : (K.shortComplexTruncLE e).f = K.ιTruncLE e

@[simp]

theorem HomologicalComplex.shortComplexTruncLE_X₁ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{v_1, u_3} C] [CategoryTheory.Abelian C] (K : HomologicalComplex C c') (e : c.Embedding c') [e.IsTruncLE] : (K.shortComplexTruncLE e).X₁ = K.truncLE e

@[simp]

theorem HomologicalComplex.shortComplexTruncLE_X₂ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{v_1, u_3} C] [CategoryTheory.Abelian C] (K : HomologicalComplex C c') (e : c.Embedding c') [e.IsTruncLE] : (K.shortComplexTruncLE e).X₂ = K

instance HomologicalComplex.instMonoFShortComplexTruncLE {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{v_1, u_3} C] [CategoryTheory.Abelian C] (K : HomologicalComplex C c') (e : c.Embedding c') [e.IsTruncLE] : CategoryTheory.Mono (K.shortComplexTruncLE e).f

instance HomologicalComplex.instEpiGShortComplexTruncLE {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{v_1, u_3} C] [CategoryTheory.Abelian C] (K : HomologicalComplex C c') (e : c.Embedding c') [e.IsTruncLE] : CategoryTheory.Epi (K.shortComplexTruncLE e).g

theorem HomologicalComplex.shortComplexTruncLE_shortExact {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{v_1, u_3} C] [CategoryTheory.Abelian C] (K : HomologicalComplex C c') (e : c.Embedding c') [e.IsTruncLE] : (K.shortComplexTruncLE e).ShortExact

theorem HomologicalComplex.mono_homologyMap_shortComplexTruncLE_g {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{v_1, u_3} C] [CategoryTheory.Abelian C] (K : HomologicalComplex C c') (e : c.Embedding c') [e.IsTruncLE] (i' : ι') (hi' : ∀ (i : ι), e.f i ≠ i') : CategoryTheory.Mono (homologyMap (K.shortComplexTruncLE e).g i')

@[simp]

theorem HomologicalComplex.shortComplexTruncLE_shortExact_δ_eq_zero {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{v_1, u_3} C] [CategoryTheory.Abelian C] (K : HomologicalComplex C c') (e : c.Embedding c') [e.IsTruncLE] (i' j' : ι') (hij' : c'.Rel i' j') : ⋯.δ i' j' hij' = 0

instance HomologicalComplex.epi_homologyMap_shortComplexTruncLE_g {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{v_1, u_3} C] [CategoryTheory.Abelian C] (K : HomologicalComplex C c') (e : c.Embedding c') [e.IsTruncLE] (i' : ι') : CategoryTheory.Epi (homologyMap (K.shortComplexTruncLE e).g i')

theorem HomologicalComplex.isIso_homologyMap_shortComplexTruncLE_g {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{v_1, u_3} C] [CategoryTheory.Abelian C] (K : HomologicalComplex C c') (e : c.Embedding c') [e.IsTruncLE] (i' : ι') (hi' : ∀ (i : ι), e.f i ≠ i') : CategoryTheory.IsIso (homologyMap (K.shortComplexTruncLE e).g i')

theorem HomologicalComplex.quasiIsoAt_shortComplexTruncLE_g {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{v_1, u_3} C] [CategoryTheory.Abelian C] (K : HomologicalComplex C c') (e : c.Embedding c') [e.IsTruncLE] (i' : ι') (hi' : ∀ (i : ι), e.f i ≠ i') : QuasiIsoAt (K.shortComplexTruncLE e).g i'

theorem HomologicalComplex.shortComplexTruncLE_X₃_isSupportedOutside {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{v_1, u_3} C] [CategoryTheory.Abelian C] (K : HomologicalComplex C c') (e : c.Embedding c') [e.IsTruncLE] : (K.shortComplexTruncLE e).X₃.IsSupportedOutside e