The homology of a restriction

Under extremely favourable circumstrnaces, we may relate the homology of K : HomologicalComplex C c' in degree j' and that of K.restriction e id a degree j when e : Embedding c c' is an embedding of complex shapes. See restriction.sc'Iso and restriction.hasHomology.

def HomologicalComplex.restriction.sc'Iso {ι : 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.IsRelIff] (i j k : ι) {i' j' k' : ι'} (hi' : e.f i = i') (hj' : e.f j = j') (hk' : e.f k = k') (hi'' : c'.prev j' = i') (hk'' : c'.next j' = k') : (K.restriction e).sc' i j k ≅ K.sc' i' j' k'

The isomorphism (K.restriction e).sc' i j k ≅ K.sc' i' j' k' when e is an embedding of complex shapes, i', j, k' are the respective images of i, j, k by e.f, j is the previous index of i, etc.

Equations

• HomologicalComplex.restriction.sc'Iso K e i j k hi' hj' hk' hi'' hk'' = CategoryTheory.ShortComplex.isoMk (K.restrictionXIso e hi') (K.restrictionXIso e hj') (K.restrictionXIso e hk') ⋯ ⋯

@[simp]

theorem HomologicalComplex.restriction.sc'Iso_inv_τ₃ {ι : 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.IsRelIff] (i j k : ι) {i' j' k' : ι'} (hi' : e.f i = i') (hj' : e.f j = j') (hk' : e.f k = k') (hi'' : c'.prev j' = i') (hk'' : c'.next j' = k') : (sc'Iso K e i j k hi' hj' hk' hi'' hk'').inv.τ₃ = (K.restrictionXIso e hk').inv

@[simp]

theorem HomologicalComplex.restriction.sc'Iso_hom_τ₃ {ι : 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.IsRelIff] (i j k : ι) {i' j' k' : ι'} (hi' : e.f i = i') (hj' : e.f j = j') (hk' : e.f k = k') (hi'' : c'.prev j' = i') (hk'' : c'.next j' = k') : (sc'Iso K e i j k hi' hj' hk' hi'' hk'').hom.τ₃ = (K.restrictionXIso e hk').hom

@[simp]

theorem HomologicalComplex.restriction.sc'Iso_hom_τ₂ {ι : 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.IsRelIff] (i j k : ι) {i' j' k' : ι'} (hi' : e.f i = i') (hj' : e.f j = j') (hk' : e.f k = k') (hi'' : c'.prev j' = i') (hk'' : c'.next j' = k') : (sc'Iso K e i j k hi' hj' hk' hi'' hk'').hom.τ₂ = (K.restrictionXIso e hj').hom

@[simp]

theorem HomologicalComplex.restriction.sc'Iso_inv_τ₂ {ι : 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.IsRelIff] (i j k : ι) {i' j' k' : ι'} (hi' : e.f i = i') (hj' : e.f j = j') (hk' : e.f k = k') (hi'' : c'.prev j' = i') (hk'' : c'.next j' = k') : (sc'Iso K e i j k hi' hj' hk' hi'' hk'').inv.τ₂ = (K.restrictionXIso e hj').inv

@[simp]

theorem HomologicalComplex.restriction.sc'Iso_hom_τ₁ {ι : 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.IsRelIff] (i j k : ι) {i' j' k' : ι'} (hi' : e.f i = i') (hj' : e.f j = j') (hk' : e.f k = k') (hi'' : c'.prev j' = i') (hk'' : c'.next j' = k') : (sc'Iso K e i j k hi' hj' hk' hi'' hk'').hom.τ₁ = (K.restrictionXIso e hi').hom

@[simp]

theorem HomologicalComplex.restriction.sc'Iso_inv_τ₁ {ι : 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.IsRelIff] (i j k : ι) {i' j' k' : ι'} (hi' : e.f i = i') (hj' : e.f j = j') (hk' : e.f k = k') (hi'' : c'.prev j' = i') (hk'' : c'.next j' = k') : (sc'Iso K e i j k hi' hj' hk' hi'' hk'').inv.τ₁ = (K.restrictionXIso e hi').inv

theorem HomologicalComplex.restriction.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.IsRelIff] (i j k : ι) (hi : c.prev j = i) (hk : c.next j = k) {i' j' k' : ι'} (hi' : e.f i = i') (hj' : e.f j = j') (hk' : e.f k = k') (hi'' : c'.prev j' = i') (hk'' : c'.next j' = k') [K.HasHomology j'] : (K.restriction e).HasHomology j