The homology of a restriction #
Under favourable circumstances, we may relate the
homology of K : HomologicalComplex C c' in degree j' and
that of K.restriction e in 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')
:
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') ⋯ ⋯
Instances For
@[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')
:
@[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')
:
@[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')
:
@[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')
:
@[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')
:
@[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')
:
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
noncomputable def
HomologicalComplex.restrictionCyclesIso
{ι : 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]
(j k : ι)
(hk : c.next j = k)
{j' k' : ι'}
(hj' : e.f j = j')
(hk' : e.f k = k')
(hk'' : c'.next j' = k')
[K.HasHomology j']
[(K.restriction e).HasHomology j]
:
The isomorphism (K.restriction e).cycles j ≅ K.cycles j' when e.f j = j'
and the successors k and k' of j and j' satisfy e.f k = k'.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
HomologicalComplex.restrictionCyclesIso_hom_iCycles
{ι : 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]
(j k : ι)
(hk : c.next j = k)
{j' k' : ι'}
(hj' : e.f j = j')
(hk' : e.f k = k')
(hk'' : c'.next j' = k')
[K.HasHomology j']
[(K.restriction e).HasHomology j]
:
CategoryTheory.CategoryStruct.comp (K.restrictionCyclesIso e j k hk hj' hk' hk'').hom (K.iCycles j') = CategoryTheory.CategoryStruct.comp ((K.restriction e).iCycles j) (K.restrictionXIso e hj').hom
@[simp]
theorem
HomologicalComplex.restrictionCyclesIso_hom_iCycles_assoc
{ι : 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]
(j k : ι)
(hk : c.next j = k)
{j' k' : ι'}
(hj' : e.f j = j')
(hk' : e.f k = k')
(hk'' : c'.next j' = k')
[K.HasHomology j']
[(K.restriction e).HasHomology j]
{Z : C}
(h : K.X j' ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (K.restrictionCyclesIso e j k hk hj' hk' hk'').hom
(CategoryTheory.CategoryStruct.comp (K.iCycles j') h) = CategoryTheory.CategoryStruct.comp ((K.restriction e).iCycles j)
(CategoryTheory.CategoryStruct.comp (K.restrictionXIso e hj').hom h)
@[simp]
theorem
HomologicalComplex.restrictionCyclesIso_inv_iCycles
{ι : 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]
(j k : ι)
(hk : c.next j = k)
{j' k' : ι'}
(hj' : e.f j = j')
(hk' : e.f k = k')
(hk'' : c'.next j' = k')
[K.HasHomology j']
[(K.restriction e).HasHomology j]
:
CategoryTheory.CategoryStruct.comp (K.restrictionCyclesIso e j k hk hj' hk' hk'').inv ((K.restriction e).iCycles j) = CategoryTheory.CategoryStruct.comp (K.iCycles j') (K.restrictionXIso e hj').inv
@[simp]
theorem
HomologicalComplex.restrictionCyclesIso_inv_iCycles_assoc
{ι : 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]
(j k : ι)
(hk : c.next j = k)
{j' k' : ι'}
(hj' : e.f j = j')
(hk' : e.f k = k')
(hk'' : c'.next j' = k')
[K.HasHomology j']
[(K.restriction e).HasHomology j]
{Z : C}
(h : (K.restriction e).X j ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (K.restrictionCyclesIso e j k hk hj' hk' hk'').inv
(CategoryTheory.CategoryStruct.comp ((K.restriction e).iCycles j) h) = CategoryTheory.CategoryStruct.comp (K.iCycles j') (CategoryTheory.CategoryStruct.comp (K.restrictionXIso e hj').inv h)
noncomputable def
HomologicalComplex.restrictionOpcyclesIso
{ι : 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 : ι)
(hi : c.prev j = i)
{i' j' : ι'}
(hi' : e.f i = i')
(hj' : e.f j = j')
(hi'' : c'.prev j' = i')
[K.HasHomology j']
[(K.restriction e).HasHomology j]
:
The isomorphism (K.restriction e).opcycles j ≅ K.opcycles j' when e.f j = j'
and the predecessors i and i' of j and j' satisfy e.f i = i'.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
HomologicalComplex.pOpcycles_restrictionOpcyclesIso_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 : ι)
(hi : c.prev j = i)
{i' j' : ι'}
(hi' : e.f i = i')
(hj' : e.f j = j')
(hi'' : c'.prev j' = i')
[K.HasHomology j']
[(K.restriction e).HasHomology j]
:
CategoryTheory.CategoryStruct.comp ((K.restriction e).pOpcycles j)
(K.restrictionOpcyclesIso e i j hi hi' hj' hi'').hom = CategoryTheory.CategoryStruct.comp (K.restrictionXIso e hj').hom (K.pOpcycles j')
@[simp]
theorem
HomologicalComplex.pOpcycles_restrictionOpcyclesIso_hom_assoc
{ι : 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 : ι)
(hi : c.prev j = i)
{i' j' : ι'}
(hi' : e.f i = i')
(hj' : e.f j = j')
(hi'' : c'.prev j' = i')
[K.HasHomology j']
[(K.restriction e).HasHomology j]
{Z : C}
(h : K.opcycles j' ⟶ Z)
:
CategoryTheory.CategoryStruct.comp ((K.restriction e).pOpcycles j)
(CategoryTheory.CategoryStruct.comp (K.restrictionOpcyclesIso e i j hi hi' hj' hi'').hom h) = CategoryTheory.CategoryStruct.comp (K.restrictionXIso e hj').hom
(CategoryTheory.CategoryStruct.comp (K.pOpcycles j') h)
@[simp]
theorem
HomologicalComplex.pOpcycles_restrictionOpcyclesIso_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 : ι)
(hi : c.prev j = i)
{i' j' : ι'}
(hi' : e.f i = i')
(hj' : e.f j = j')
(hi'' : c'.prev j' = i')
[K.HasHomology j']
[(K.restriction e).HasHomology j]
:
CategoryTheory.CategoryStruct.comp (K.pOpcycles j') (K.restrictionOpcyclesIso e i j hi hi' hj' hi'').inv = CategoryTheory.CategoryStruct.comp (K.restrictionXIso e hj').inv ((K.restriction e).pOpcycles j)
@[simp]
theorem
HomologicalComplex.pOpcycles_restrictionOpcyclesIso_inv_assoc
{ι : 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 : ι)
(hi : c.prev j = i)
{i' j' : ι'}
(hi' : e.f i = i')
(hj' : e.f j = j')
(hi'' : c'.prev j' = i')
[K.HasHomology j']
[(K.restriction e).HasHomology j]
{Z : C}
(h : (K.restriction e).opcycles j ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (K.pOpcycles j')
(CategoryTheory.CategoryStruct.comp (K.restrictionOpcyclesIso e i j hi hi' hj' hi'').inv h) = CategoryTheory.CategoryStruct.comp (K.restrictionXIso e hj').inv
(CategoryTheory.CategoryStruct.comp ((K.restriction e).pOpcycles j) h)
noncomputable def
HomologicalComplex.restrictionHomologyIso
{ι : 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]
:
The isomorphism (K.restriction e).homology j ≅ K.homology j' when e.f j = j',
the predecessors i and i' of j and j' satisfy e.f i = i',
and the successors k and k' of j and j' satisfy e.f k = k'
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
HomologicalComplex.homologyπ_restrictionHomologyIso_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 : ι)
(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]
:
CategoryTheory.CategoryStruct.comp ((K.restriction e).homologyπ j)
(K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk'').hom = CategoryTheory.CategoryStruct.comp (K.restrictionCyclesIso e j k hk hj' hk' hk'').hom (K.homologyπ j')
@[simp]
theorem
HomologicalComplex.homologyπ_restrictionHomologyIso_hom_assoc
{ι : 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]
{Z : C}
(h : K.homology j' ⟶ Z)
:
CategoryTheory.CategoryStruct.comp ((K.restriction e).homologyπ j)
(CategoryTheory.CategoryStruct.comp (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk'').hom h) = CategoryTheory.CategoryStruct.comp (K.restrictionCyclesIso e j k hk hj' hk' hk'').hom
(CategoryTheory.CategoryStruct.comp (K.homologyπ j') h)
theorem
HomologicalComplex.homologyπ_restrictionHomologyIso_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 : ι)
(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]
:
CategoryTheory.CategoryStruct.comp (K.homologyπ j') (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk'').inv = CategoryTheory.CategoryStruct.comp (K.restrictionCyclesIso e j k hk hj' hk' hk'').inv ((K.restriction e).homologyπ j)
theorem
HomologicalComplex.homologyπ_restrictionHomologyIso_inv_assoc
{ι : 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]
{Z : C}
(h : (K.restriction e).homology j ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (K.homologyπ j')
(CategoryTheory.CategoryStruct.comp (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk'').inv h) = CategoryTheory.CategoryStruct.comp (K.restrictionCyclesIso e j k hk hj' hk' hk'').inv
(CategoryTheory.CategoryStruct.comp ((K.restriction e).homologyπ j) h)
@[simp]
theorem
HomologicalComplex.restrictionHomologyIso_inv_homologyι
{ι : 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]
:
CategoryTheory.CategoryStruct.comp (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk'').inv
((K.restriction e).homologyι j) = CategoryTheory.CategoryStruct.comp (K.homologyι j') (K.restrictionOpcyclesIso e i j hi hi' hj' hi'').inv
@[simp]
theorem
HomologicalComplex.restrictionHomologyIso_inv_homologyι_assoc
{ι : 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]
{Z : C}
(h : (K.restriction e).opcycles j ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk'').inv
(CategoryTheory.CategoryStruct.comp ((K.restriction e).homologyι j) h) = CategoryTheory.CategoryStruct.comp (K.homologyι j')
(CategoryTheory.CategoryStruct.comp (K.restrictionOpcyclesIso e i j hi hi' hj' hi'').inv h)
@[simp]
theorem
HomologicalComplex.restrictionHomologyIso_hom_homologyι
{ι : 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]
:
CategoryTheory.CategoryStruct.comp (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk'').hom (K.homologyι j') = CategoryTheory.CategoryStruct.comp ((K.restriction e).homologyι j)
(K.restrictionOpcyclesIso e i j hi hi' hj' hi'').hom
@[simp]
theorem
HomologicalComplex.restrictionHomologyIso_hom_homologyι_assoc
{ι : 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]
{Z : C}
(h : K.opcycles j' ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk'').hom
(CategoryTheory.CategoryStruct.comp (K.homologyι j') h) = CategoryTheory.CategoryStruct.comp ((K.restriction e).homologyι j)
(CategoryTheory.CategoryStruct.comp (K.restrictionOpcyclesIso e i j hi hi' hj' hi'').hom h)