Homology of the extension of a homological complex #
Given an embedding e : c.Embedding c' and K : HomologicalComplex C c, we shall
compute the homology of K.extend e. In degrees that are not in the image of e.f,
the homology is obviously zero. When e.f j = j, we construct an isomorphism
(K.extend e).homology j' ≅ K.homology j.
theorem
HomologicalComplex.extend.comp_d_eq_zero_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]
[CategoryTheory.Limits.HasZeroObject C]
(K : HomologicalComplex C c)
(e : c.Embedding c')
{j k : ι}
{j' k' : ι'}
(hj' : e.f j = j')
(hk : c.next j = k)
(hk' : c'.next j' = k')
⦃W : C⦄
(φ : W ⟶ K.X j)
:
CategoryTheory.CategoryStruct.comp φ (K.d j k) = 0 ↔ CategoryTheory.CategoryStruct.comp φ
(CategoryTheory.CategoryStruct.comp (K.extendXIso e hj').inv ((K.extend e).d j' k')) = 0
theorem
HomologicalComplex.extend.d_comp_eq_zero_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]
[CategoryTheory.Limits.HasZeroObject C]
(K : HomologicalComplex C c)
(e : c.Embedding c')
{i j : ι}
{i' j' : ι'}
(hj' : e.f j = j')
(hi : c.prev j = i)
(hi' : c'.prev j' = i')
⦃W : C⦄
(φ : K.X j ⟶ W)
:
CategoryTheory.CategoryStruct.comp (K.d i j) φ = 0 ↔ CategoryTheory.CategoryStruct.comp ((K.extend e).d i' j')
(CategoryTheory.CategoryStruct.comp (K.extendXIso e hj').hom φ) = 0
noncomputable def
HomologicalComplex.extend.leftHomologyData.kernelFork
{ι : 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]
[CategoryTheory.Limits.HasZeroObject C]
(K : HomologicalComplex C c)
(e : c.Embedding c')
{j k : ι}
{j' k' : ι'}
(hj' : e.f j = j')
(hk : c.next j = k)
(hk' : c'.next j' = k')
(cone : CategoryTheory.Limits.KernelFork (K.d j k))
:
CategoryTheory.Limits.KernelFork ((K.extend e).d j' k')
The kernel fork of (K.extend e).d j' k' that is deduced from a kernel
fork of K.d j k .
Instances For
noncomputable def
HomologicalComplex.extend.leftHomologyData.isLimitKernelFork
{ι : 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]
[CategoryTheory.Limits.HasZeroObject C]
(K : HomologicalComplex C c)
(e : c.Embedding c')
{j k : ι}
{j' k' : ι'}
(hj' : e.f j = j')
(hk : c.next j = k)
(hk' : c'.next j' = k')
(cone : CategoryTheory.Limits.KernelFork (K.d j k))
(hcone : CategoryTheory.Limits.IsLimit cone)
:
CategoryTheory.Limits.IsLimit (kernelFork K e hj' hk hk' cone)
The limit kernel fork of (K.extend e).d j' k' that is deduced from a limit
kernel fork of K.d j k .
Instances For
theorem
HomologicalComplex.extend.leftHomologyData.lift_d_comp_eq_zero_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]
[CategoryTheory.Limits.HasZeroObject C]
(K : HomologicalComplex C c)
(e : c.Embedding c')
{i j k : ι}
{i' j' : ι'}
(hj' : e.f j = j')
(hi : c.prev j = i)
(hi' : c'.prev j' = i')
(cone : CategoryTheory.Limits.KernelFork (K.d j k))
(hcone : CategoryTheory.Limits.IsLimit cone)
⦃W : C⦄
(f' : K.X i ⟶ cone.pt)
(hf' : CategoryTheory.CategoryStruct.comp f' (CategoryTheory.Limits.Fork.ι cone) = K.d i j)
(f'' : (K.extend e).X i' ⟶ cone.pt)
(hf'' :
CategoryTheory.CategoryStruct.comp f''
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι cone) (K.extendXIso e hj').inv) = (K.extend e).d i' j')
(φ : cone.pt ⟶ W)
:
CategoryTheory.CategoryStruct.comp f' φ = 0 ↔ CategoryTheory.CategoryStruct.comp f'' φ = 0
Auxiliary lemma for lift_d_comp_eq_zero_iff.
theorem
HomologicalComplex.extend.leftHomologyData.lift_d_comp_eq_zero_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]
[CategoryTheory.Limits.HasZeroObject C]
(K : HomologicalComplex C c)
(e : c.Embedding c')
{i j k : ι}
{i' j' k' : ι'}
(hj' : e.f j = j')
(hi : c.prev j = i)
(hi' : c'.prev j' = i')
(hk : c.next j = k)
(hk' : c'.next j' = k')
(cone : CategoryTheory.Limits.KernelFork (K.d j k))
(hcone : CategoryTheory.Limits.IsLimit cone)
⦃W : C⦄
(φ : cone.pt ⟶ W)
:
CategoryTheory.CategoryStruct.comp (hcone.lift (CategoryTheory.Limits.KernelFork.ofι (K.d i j) ⋯)) φ = 0 ↔ CategoryTheory.CategoryStruct.comp
((isLimitKernelFork K e hj' hk hk' cone hcone).lift
(CategoryTheory.Limits.KernelFork.ofι ((K.extend e).d i' j') ⋯))
φ = 0
noncomputable def
HomologicalComplex.extend.leftHomologyData.cokernelCofork
{ι : 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]
[CategoryTheory.Limits.HasZeroObject C]
(K : HomologicalComplex C c)
(e : c.Embedding c')
{i j k : ι}
{i' j' k' : ι'}
(hj' : e.f j = j')
(hi : c.prev j = i)
(hi' : c'.prev j' = i')
(hk : c.next j = k)
(hk' : c'.next j' = k')
(cone : CategoryTheory.Limits.KernelFork (K.d j k))
(hcone : CategoryTheory.Limits.IsLimit cone)
(cocone : CategoryTheory.Limits.CokernelCofork (hcone.lift (CategoryTheory.Limits.KernelFork.ofι (K.d i j) ⋯)))
:
CategoryTheory.Limits.CokernelCofork
((isLimitKernelFork K e hj' hk hk' cone hcone).lift (CategoryTheory.Limits.KernelFork.ofι ((K.extend e).d i' j') ⋯))
Auxiliary definition for extend.leftHomologyData.
Instances For
noncomputable def
HomologicalComplex.extend.leftHomologyData.isColimitCokernelCofork
{ι : 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]
[CategoryTheory.Limits.HasZeroObject C]
(K : HomologicalComplex C c)
(e : c.Embedding c')
{i j k : ι}
{i' j' k' : ι'}
(hj' : e.f j = j')
(hi : c.prev j = i)
(hi' : c'.prev j' = i')
(hk : c.next j = k)
(hk' : c'.next j' = k')
(cone : CategoryTheory.Limits.KernelFork (K.d j k))
(hcone : CategoryTheory.Limits.IsLimit cone)
(cocone : CategoryTheory.Limits.CokernelCofork (hcone.lift (CategoryTheory.Limits.KernelFork.ofι (K.d i j) ⋯)))
(hcocone : CategoryTheory.Limits.IsColimit cocone)
:
CategoryTheory.Limits.IsColimit (cokernelCofork K e hj' hi hi' hk hk' cone hcone cocone)
Auxiliary definition for extend.leftHomologyData.
Instances For
noncomputable def
HomologicalComplex.extend.leftHomologyData
{ι : 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]
[CategoryTheory.Limits.HasZeroObject C]
(K : HomologicalComplex C c)
(e : c.Embedding c')
{i j k : ι}
{i' j' k' : ι'}
(hj' : e.f j = j')
(hi : c.prev j = i)
(hi' : c'.prev j' = i')
(hk : c.next j = k)
(hk' : c'.next j' = k')
(h : (K.sc' i j k).LeftHomologyData)
:
((K.extend e).sc' i' j' k').LeftHomologyData
The left homology data of (K.extend e).sc' i' j' k' that is deduced
from a left homology data of K.sc' i j k.
Instances For
@[simp]
theorem
HomologicalComplex.extend.leftHomologyData_H
{ι : 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]
[CategoryTheory.Limits.HasZeroObject C]
(K : HomologicalComplex C c)
(e : c.Embedding c')
{i j k : ι}
{i' j' k' : ι'}
(hj' : e.f j = j')
(hi : c.prev j = i)
(hi' : c'.prev j' = i')
(hk : c.next j = k)
(hk' : c'.next j' = k')
(h : (K.sc' i j k).LeftHomologyData)
:
(leftHomologyData K e hj' hi hi' hk hk' h).H = h.H
@[simp]
theorem
HomologicalComplex.extend.leftHomologyData_K
{ι : 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]
[CategoryTheory.Limits.HasZeroObject C]
(K : HomologicalComplex C c)
(e : c.Embedding c')
{i j k : ι}
{i' j' k' : ι'}
(hj' : e.f j = j')
(hi : c.prev j = i)
(hi' : c'.prev j' = i')
(hk : c.next j = k)
(hk' : c'.next j' = k')
(h : (K.sc' i j k).LeftHomologyData)
:
(leftHomologyData K e hj' hi hi' hk hk' h).K = h.K
@[simp]
theorem
HomologicalComplex.extend.leftHomologyData_π
{ι : 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]
[CategoryTheory.Limits.HasZeroObject C]
(K : HomologicalComplex C c)
(e : c.Embedding c')
{i j k : ι}
{i' j' k' : ι'}
(hj' : e.f j = j')
(hi : c.prev j = i)
(hi' : c'.prev j' = i')
(hk : c.next j = k)
(hk' : c'.next j' = k')
(h : (K.sc' i j k).LeftHomologyData)
:
(leftHomologyData K e hj' hi hi' hk hk' h).π = h.π
@[simp]
theorem
HomologicalComplex.extend.leftHomologyData_i
{ι : 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]
[CategoryTheory.Limits.HasZeroObject C]
(K : HomologicalComplex C c)
(e : c.Embedding c')
{i j k : ι}
{i' j' k' : ι'}
(hj' : e.f j = j')
(hi : c.prev j = i)
(hi' : c'.prev j' = i')
(hk : c.next j = k)
(hk' : c'.next j' = k')
(h : (K.sc' i j k).LeftHomologyData)
:
(leftHomologyData K e hj' hi hi' hk hk' h).i = CategoryTheory.CategoryStruct.comp h.i (K.extendXIso e hj').inv
noncomputable def
HomologicalComplex.extend.rightHomologyData.cokernelCofork
{ι : 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]
[CategoryTheory.Limits.HasZeroObject C]
(K : HomologicalComplex C c)
(e : c.Embedding c')
{i j : ι}
{i' j' : ι'}
(hj' : e.f j = j')
(hi : c.prev j = i)
(hi' : c'.prev j' = i')
(cocone : CategoryTheory.Limits.CokernelCofork (K.d i j))
:
CategoryTheory.Limits.CokernelCofork ((K.extend e).d i' j')
The cokernel cofork of (K.extend e).d i' j' that is deduced from a cokernel
cofork of K.d i j.
Instances For
noncomputable def
HomologicalComplex.extend.rightHomologyData.isColimitCokernelCofork
{ι : 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]
[CategoryTheory.Limits.HasZeroObject C]
(K : HomologicalComplex C c)
(e : c.Embedding c')
{i j : ι}
{i' j' : ι'}
(hj' : e.f j = j')
(hi : c.prev j = i)
(hi' : c'.prev j' = i')
(cocone : CategoryTheory.Limits.CokernelCofork (K.d i j))
(hcocone : CategoryTheory.Limits.IsColimit cocone)
:
CategoryTheory.Limits.IsColimit (cokernelCofork K e hj' hi hi' cocone)
The colimit cokernel cofork of (K.extend e).d i' j' that is deduced from a
colimit cokernel cofork of K.d i j.
Instances For
theorem
HomologicalComplex.extend.rightHomologyData.d_comp_desc_eq_zero_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]
[CategoryTheory.Limits.HasZeroObject C]
(K : HomologicalComplex C c)
(e : c.Embedding c')
{i j k : ι}
{j' k' : ι'}
(hj' : e.f j = j')
(hk : c.next j = k)
(hk' : c'.next j' = k')
(cocone : CategoryTheory.Limits.CokernelCofork (K.d i j))
(hcocone : CategoryTheory.Limits.IsColimit cocone)
⦃W : C⦄
(f' : cocone.pt ⟶ K.X k)
(hf' : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofork.π cocone) f' = K.d j k)
(f'' : cocone.pt ⟶ (K.extend e).X k')
(hf'' :
CategoryTheory.CategoryStruct.comp (K.extendXIso e hj').hom
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofork.π cocone) f'') = (K.extend e).d j' k')
(φ : W ⟶ cocone.pt)
:
CategoryTheory.CategoryStruct.comp φ f' = 0 ↔ CategoryTheory.CategoryStruct.comp φ f'' = 0
theorem
HomologicalComplex.extend.rightHomologyData.d_comp_desc_eq_zero_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]
[CategoryTheory.Limits.HasZeroObject C]
(K : HomologicalComplex C c)
(e : c.Embedding c')
{i j k : ι}
{i' j' k' : ι'}
(hj' : e.f j = j')
(hi : c.prev j = i)
(hi' : c'.prev j' = i')
(hk : c.next j = k)
(hk' : c'.next j' = k')
(cocone : CategoryTheory.Limits.CokernelCofork (K.d i j))
(hcocone : CategoryTheory.Limits.IsColimit cocone)
⦃W : C⦄
(φ : W ⟶ cocone.pt)
:
CategoryTheory.CategoryStruct.comp φ (hcocone.desc (CategoryTheory.Limits.CokernelCofork.ofπ (K.d j k) ⋯)) = 0 ↔ CategoryTheory.CategoryStruct.comp φ
((isColimitCokernelCofork K e hj' hi hi' cocone hcocone).desc
(CategoryTheory.Limits.CokernelCofork.ofπ ((K.extend e).d j' k') ⋯)) = 0
noncomputable def
HomologicalComplex.extend.rightHomologyData.kernelFork
{ι : 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]
[CategoryTheory.Limits.HasZeroObject C]
(K : HomologicalComplex C c)
(e : c.Embedding c')
{i j k : ι}
{i' j' k' : ι'}
(hj' : e.f j = j')
(hi : c.prev j = i)
(hi' : c'.prev j' = i')
(hk : c.next j = k)
(hk' : c'.next j' = k')
(cocone : CategoryTheory.Limits.CokernelCofork (K.d i j))
(hcocone : CategoryTheory.Limits.IsColimit cocone)
(cone : CategoryTheory.Limits.KernelFork (hcocone.desc (CategoryTheory.Limits.CokernelCofork.ofπ (K.d j k) ⋯)))
:
CategoryTheory.Limits.KernelFork
((isColimitCokernelCofork K e hj' hi hi' cocone hcocone).desc
(CategoryTheory.Limits.CokernelCofork.ofπ ((K.extend e).d j' k') ⋯))
Auxiliary definition for extend.rightHomologyData.
Instances For
noncomputable def
HomologicalComplex.extend.rightHomologyData.isLimitKernelFork
{ι : 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]
[CategoryTheory.Limits.HasZeroObject C]
(K : HomologicalComplex C c)
(e : c.Embedding c')
{i j k : ι}
{i' j' k' : ι'}
(hj' : e.f j = j')
(hi : c.prev j = i)
(hi' : c'.prev j' = i')
(hk : c.next j = k)
(hk' : c'.next j' = k')
(cocone : CategoryTheory.Limits.CokernelCofork (K.d i j))
(hcocone : CategoryTheory.Limits.IsColimit cocone)
(cone : CategoryTheory.Limits.KernelFork (hcocone.desc (CategoryTheory.Limits.CokernelCofork.ofπ (K.d j k) ⋯)))
(hcone : CategoryTheory.Limits.IsLimit cone)
:
CategoryTheory.Limits.IsLimit (kernelFork K e hj' hi hi' hk hk' cocone hcocone cone)
Auxiliary definition for extend.rightHomologyData.
Instances For
noncomputable def
HomologicalComplex.extend.rightHomologyData
{ι : 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]
[CategoryTheory.Limits.HasZeroObject C]
(K : HomologicalComplex C c)
(e : c.Embedding c')
{i j k : ι}
{i' j' k' : ι'}
(hj' : e.f j = j')
(hi : c.prev j = i)
(hi' : c'.prev j' = i')
(hk : c.next j = k)
(hk' : c'.next j' = k')
(h : (K.sc' i j k).RightHomologyData)
:
((K.extend e).sc' i' j' k').RightHomologyData
The right homology data of (K.extend e).sc' i' j' k' that is deduced
from a right homology data of K.sc' i j k.
Instances For
@[simp]
theorem
HomologicalComplex.extend.rightHomologyData_Q
{ι : 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]
[CategoryTheory.Limits.HasZeroObject C]
(K : HomologicalComplex C c)
(e : c.Embedding c')
{i j k : ι}
{i' j' k' : ι'}
(hj' : e.f j = j')
(hi : c.prev j = i)
(hi' : c'.prev j' = i')
(hk : c.next j = k)
(hk' : c'.next j' = k')
(h : (K.sc' i j k).RightHomologyData)
:
(rightHomologyData K e hj' hi hi' hk hk' h).Q = h.Q
@[simp]
theorem
HomologicalComplex.extend.rightHomologyData_ι
{ι : 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]
[CategoryTheory.Limits.HasZeroObject C]
(K : HomologicalComplex C c)
(e : c.Embedding c')
{i j k : ι}
{i' j' k' : ι'}
(hj' : e.f j = j')
(hi : c.prev j = i)
(hi' : c'.prev j' = i')
(hk : c.next j = k)
(hk' : c'.next j' = k')
(h : (K.sc' i j k).RightHomologyData)
:
(rightHomologyData K e hj' hi hi' hk hk' h).ι = h.ι
@[simp]
theorem
HomologicalComplex.extend.rightHomologyData_p
{ι : 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]
[CategoryTheory.Limits.HasZeroObject C]
(K : HomologicalComplex C c)
(e : c.Embedding c')
{i j k : ι}
{i' j' k' : ι'}
(hj' : e.f j = j')
(hi : c.prev j = i)
(hi' : c'.prev j' = i')
(hk : c.next j = k)
(hk' : c'.next j' = k')
(h : (K.sc' i j k).RightHomologyData)
:
(rightHomologyData K e hj' hi hi' hk hk' h).p = CategoryTheory.CategoryStruct.comp (K.extendXIso e hj').hom h.p
@[simp]
theorem
HomologicalComplex.extend.rightHomologyData_H
{ι : 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]
[CategoryTheory.Limits.HasZeroObject C]
(K : HomologicalComplex C c)
(e : c.Embedding c')
{i j k : ι}
{i' j' k' : ι'}
(hj' : e.f j = j')
(hi : c.prev j = i)
(hi' : c'.prev j' = i')
(hk : c.next j = k)
(hk' : c'.next j' = k')
(h : (K.sc' i j k).RightHomologyData)
:
(rightHomologyData K e hj' hi hi' hk hk' h).H = h.H
theorem
HomologicalComplex.extend.rightHomologyData_g'
{ι : 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]
[CategoryTheory.Limits.HasZeroObject C]
(K : HomologicalComplex C c)
(e : c.Embedding c')
{i j k : ι}
{i' j' k' : ι'}
(hj' : e.f j = j')
(hi : c.prev j = i)
(hi' : c'.prev j' = i')
(hk : c.next j = k)
(hk' : c'.next j' = k')
(h : (K.sc' i j k).RightHomologyData)
(hk'' : e.f k = k')
:
(rightHomologyData K e hj' hi hi' hk hk' h).g' = CategoryTheory.CategoryStruct.comp h.g' (K.extendXIso e hk'').inv
Computation of the g' field of extend.rightHomologyData.
noncomputable def
HomologicalComplex.extend.homologyData
{ι : 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]
[CategoryTheory.Limits.HasZeroObject C]
(K : HomologicalComplex C c)
(e : c.Embedding c')
{i j k : ι}
{i' j' k' : ι'}
(hj' : e.f j = j')
(hi : c.prev j = i)
(hi' : c'.prev j' = i')
(hk : c.next j = k)
(hk' : c'.next j' = k')
(h : (K.sc' i j k).HomologyData)
:
((K.extend e).sc' i' j' k').HomologyData
The homology data of (K.extend e).sc' i' j' k' that is deduced
from a homology data of K.sc' i j k.
Instances For
@[simp]
theorem
HomologicalComplex.extend.homologyData_right
{ι : 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]
[CategoryTheory.Limits.HasZeroObject C]
(K : HomologicalComplex C c)
(e : c.Embedding c')
{i j k : ι}
{i' j' k' : ι'}
(hj' : e.f j = j')
(hi : c.prev j = i)
(hi' : c'.prev j' = i')
(hk : c.next j = k)
(hk' : c'.next j' = k')
(h : (K.sc' i j k).HomologyData)
:
(homologyData K e hj' hi hi' hk hk' h).right = rightHomologyData K e hj' hi hi' hk hk' h.right
@[simp]
theorem
HomologicalComplex.extend.homologyData_left
{ι : 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]
[CategoryTheory.Limits.HasZeroObject C]
(K : HomologicalComplex C c)
(e : c.Embedding c')
{i j k : ι}
{i' j' k' : ι'}
(hj' : e.f j = j')
(hi : c.prev j = i)
(hi' : c'.prev j' = i')
(hk : c.next j = k)
(hk' : c'.next j' = k')
(h : (K.sc' i j k).HomologyData)
:
(homologyData K e hj' hi hi' hk hk' h).left = leftHomologyData K e hj' hi hi' hk hk' h.left
@[simp]
theorem
HomologicalComplex.extend.homologyData_iso
{ι : 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]
[CategoryTheory.Limits.HasZeroObject C]
(K : HomologicalComplex C c)
(e : c.Embedding c')
{i j k : ι}
{i' j' k' : ι'}
(hj' : e.f j = j')
(hi : c.prev j = i)
(hi' : c'.prev j' = i')
(hk : c.next j = k)
(hk' : c'.next j' = k')
(h : (K.sc' i j k).HomologyData)
:
(homologyData K e hj' hi hi' hk hk' h).iso = h.iso
noncomputable def
HomologicalComplex.extend.homologyData'
{ι : 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]
[CategoryTheory.Limits.HasZeroObject C]
(K : HomologicalComplex C c)
(e : c.Embedding c')
{i j k : ι}
{j' : ι'}
(hj' : e.f j = j')
(hi : c.prev j = i)
(hk : c.next j = k)
(h : (K.sc' i j k).HomologyData)
:
((K.extend e).sc j').HomologyData
The homology data of (K.extend e).sc j' that is deduced
from a homology data of K.sc' i j k.
Instances For
@[simp]
theorem
HomologicalComplex.extend.homologyData'_left_π
{ι : 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]
[CategoryTheory.Limits.HasZeroObject C]
(K : HomologicalComplex C c)
(e : c.Embedding c')
{i j k : ι}
{j' : ι'}
(hj' : e.f j = j')
(hi : c.prev j = i)
(hk : c.next j = k)
(h : (K.sc' i j k).HomologyData)
:
(homologyData' K e hj' hi hk h).left.π = h.left.π
@[simp]
theorem
HomologicalComplex.extend.homologyData'_right_H
{ι : 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]
[CategoryTheory.Limits.HasZeroObject C]
(K : HomologicalComplex C c)
(e : c.Embedding c')
{i j k : ι}
{j' : ι'}
(hj' : e.f j = j')
(hi : c.prev j = i)
(hk : c.next j = k)
(h : (K.sc' i j k).HomologyData)
:
(homologyData' K e hj' hi hk h).right.H = h.right.H
@[simp]
theorem
HomologicalComplex.extend.homologyData'_left_K
{ι : 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]
[CategoryTheory.Limits.HasZeroObject C]
(K : HomologicalComplex C c)
(e : c.Embedding c')
{i j k : ι}
{j' : ι'}
(hj' : e.f j = j')
(hi : c.prev j = i)
(hk : c.next j = k)
(h : (K.sc' i j k).HomologyData)
:
(homologyData' K e hj' hi hk h).left.K = h.left.K
@[simp]
theorem
HomologicalComplex.extend.homologyData'_left_H
{ι : 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]
[CategoryTheory.Limits.HasZeroObject C]
(K : HomologicalComplex C c)
(e : c.Embedding c')
{i j k : ι}
{j' : ι'}
(hj' : e.f j = j')
(hi : c.prev j = i)
(hk : c.next j = k)
(h : (K.sc' i j k).HomologyData)
:
(homologyData' K e hj' hi hk h).left.H = h.left.H
@[simp]
theorem
HomologicalComplex.extend.homologyData'_right_Q
{ι : 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]
[CategoryTheory.Limits.HasZeroObject C]
(K : HomologicalComplex C c)
(e : c.Embedding c')
{i j k : ι}
{j' : ι'}
(hj' : e.f j = j')
(hi : c.prev j = i)
(hk : c.next j = k)
(h : (K.sc' i j k).HomologyData)
:
(homologyData' K e hj' hi hk h).right.Q = h.right.Q
@[simp]
theorem
HomologicalComplex.extend.homologyData'_right_p
{ι : 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]
[CategoryTheory.Limits.HasZeroObject C]
(K : HomologicalComplex C c)
(e : c.Embedding c')
{i j k : ι}
{j' : ι'}
(hj' : e.f j = j')
(hi : c.prev j = i)
(hk : c.next j = k)
(h : (K.sc' i j k).HomologyData)
:
(homologyData' K e hj' hi hk h).right.p = CategoryTheory.CategoryStruct.comp (K.extendXIso e hj').hom h.right.p
@[simp]
theorem
HomologicalComplex.extend.homologyData'_left_i
{ι : 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]
[CategoryTheory.Limits.HasZeroObject C]
(K : HomologicalComplex C c)
(e : c.Embedding c')
{i j k : ι}
{j' : ι'}
(hj' : e.f j = j')
(hi : c.prev j = i)
(hk : c.next j = k)
(h : (K.sc' i j k).HomologyData)
:
(homologyData' K e hj' hi hk h).left.i = CategoryTheory.CategoryStruct.comp h.left.i (K.extendXIso e hj').inv
@[simp]
theorem
HomologicalComplex.extend.homologyData'_iso
{ι : 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]
[CategoryTheory.Limits.HasZeroObject C]
(K : HomologicalComplex C c)
(e : c.Embedding c')
{i j k : ι}
{j' : ι'}
(hj' : e.f j = j')
(hi : c.prev j = i)
(hk : c.next j = k)
(h : (K.sc' i j k).HomologyData)
:
(homologyData' K e hj' hi hk h).iso = h.iso
@[simp]
theorem
HomologicalComplex.extend.homologyData'_right_ι
{ι : 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]
[CategoryTheory.Limits.HasZeroObject C]
(K : HomologicalComplex C c)
(e : c.Embedding c')
{i j k : ι}
{j' : ι'}
(hj' : e.f j = j')
(hi : c.prev j = i)
(hk : c.next j = k)
(h : (K.sc' i j k).HomologyData)
:
(homologyData' K e hj' hi hk h).right.ι = h.right.ι
theorem
HomologicalComplex.extend.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]
[CategoryTheory.Limits.HasZeroObject C]
(K : HomologicalComplex C c)
(e : c.Embedding c')
{j : ι}
{j' : ι'}
(hj' : e.f j = j')
[K.HasHomology j]
:
(K.extend e).HasHomology j'
instance
HomologicalComplex.extend.instHasHomologyF
{ι : 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]
[CategoryTheory.Limits.HasZeroObject C]
(K : HomologicalComplex C c)
(e : c.Embedding c')
(j : ι)
[K.HasHomology j]
:
(K.extend e).HasHomology (e.f j)
instance
HomologicalComplex.extend.instHasHomology
{ι : 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]
[CategoryTheory.Limits.HasZeroObject C]
(K : HomologicalComplex C c)
(e : c.Embedding c')
[∀ (j : ι), K.HasHomology j]
(j' : ι')
:
(K.extend e).HasHomology j'
theorem
HomologicalComplex.extend_exactAt
{ι : 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]
[CategoryTheory.Limits.HasZeroObject C]
(K : HomologicalComplex C c)
(e : c.Embedding c')
(j' : ι')
(hj' : ∀ (j : ι), e.f j ≠ j')
:
noncomputable def
HomologicalComplex.extendCyclesIso
{ι : 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]
[CategoryTheory.Limits.HasZeroObject C]
(K : HomologicalComplex C c)
(e : c.Embedding c')
{j : ι}
{j' : ι'}
(hj' : e.f j = j')
[K.HasHomology j]
[(K.extend e).HasHomology j']
:
The isomorphism (K.extend e).cycles j' ≅ K.cycles j when e.f j = j'.
Instances For
noncomputable def
HomologicalComplex.extendOpcyclesIso
{ι : 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]
[CategoryTheory.Limits.HasZeroObject C]
(K : HomologicalComplex C c)
(e : c.Embedding c')
{j : ι}
{j' : ι'}
(hj' : e.f j = j')
[K.HasHomology j]
[(K.extend e).HasHomology j']
:
The isomorphism (K.extend e).opcycles j' ≅ K.opcycles j when e.f j = j'.
Instances For
noncomputable def
HomologicalComplex.extendHomologyIso
{ι : 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]
[CategoryTheory.Limits.HasZeroObject C]
(K : HomologicalComplex C c)
(e : c.Embedding c')
{j : ι}
{j' : ι'}
(hj' : e.f j = j')
[K.HasHomology j]
[(K.extend e).HasHomology j']
:
The isomorphism (K.extend e).homology j' ≅ K.homology j when e.f j = j'.
Instances For
theorem
HomologicalComplex.extend_exactAt_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]
[CategoryTheory.Limits.HasZeroObject C]
(K : HomologicalComplex C c)
(e : c.Embedding c')
{j : ι}
{j' : ι'}
(hj' : e.f j = j')
[K.HasHomology j]
[(K.extend e).HasHomology j']
:
@[simp]
theorem
HomologicalComplex.extendCyclesIso_hom_iCycles
{ι : 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]
[CategoryTheory.Limits.HasZeroObject C]
(K : HomologicalComplex C c)
(e : c.Embedding c')
{j : ι}
{j' : ι'}
(hj' : e.f j = j')
[K.HasHomology j]
[(K.extend e).HasHomology j']
:
CategoryTheory.CategoryStruct.comp (K.extendCyclesIso e hj').hom (K.iCycles j) = CategoryTheory.CategoryStruct.comp ((K.extend e).iCycles j') (K.extendXIso e hj').hom
@[simp]
theorem
HomologicalComplex.extendCyclesIso_hom_iCycles_assoc
{ι : 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]
[CategoryTheory.Limits.HasZeroObject C]
(K : HomologicalComplex C c)
(e : c.Embedding c')
{j : ι}
{j' : ι'}
(hj' : e.f j = j')
[K.HasHomology j]
[(K.extend e).HasHomology j']
{Z : C}
(h : K.X j ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (K.extendCyclesIso e hj').hom (CategoryTheory.CategoryStruct.comp (K.iCycles j) h) = CategoryTheory.CategoryStruct.comp ((K.extend e).iCycles j')
(CategoryTheory.CategoryStruct.comp (K.extendXIso e hj').hom h)
@[simp]
theorem
HomologicalComplex.extendCyclesIso_inv_iCycles
{ι : 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]
[CategoryTheory.Limits.HasZeroObject C]
(K : HomologicalComplex C c)
(e : c.Embedding c')
{j : ι}
{j' : ι'}
(hj' : e.f j = j')
[K.HasHomology j]
[(K.extend e).HasHomology j']
:
CategoryTheory.CategoryStruct.comp (K.extendCyclesIso e hj').inv ((K.extend e).iCycles j') = CategoryTheory.CategoryStruct.comp (K.iCycles j) (K.extendXIso e hj').inv
@[simp]
theorem
HomologicalComplex.extendCyclesIso_inv_iCycles_assoc
{ι : 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]
[CategoryTheory.Limits.HasZeroObject C]
(K : HomologicalComplex C c)
(e : c.Embedding c')
{j : ι}
{j' : ι'}
(hj' : e.f j = j')
[K.HasHomology j]
[(K.extend e).HasHomology j']
{Z : C}
(h : (K.extend e).X j' ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (K.extendCyclesIso e hj').inv
(CategoryTheory.CategoryStruct.comp ((K.extend e).iCycles j') h) = CategoryTheory.CategoryStruct.comp (K.iCycles j) (CategoryTheory.CategoryStruct.comp (K.extendXIso e hj').inv h)
@[simp]
theorem
HomologicalComplex.homologyπ_extendHomologyIso_hom
{ι : 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]
[CategoryTheory.Limits.HasZeroObject C]
(K : HomologicalComplex C c)
(e : c.Embedding c')
{j : ι}
{j' : ι'}
(hj' : e.f j = j')
[K.HasHomology j]
[(K.extend e).HasHomology j']
:
CategoryTheory.CategoryStruct.comp ((K.extend e).homologyπ j') (K.extendHomologyIso e hj').hom = CategoryTheory.CategoryStruct.comp (K.extendCyclesIso e hj').hom (K.homologyπ j)
@[simp]
theorem
HomologicalComplex.homologyπ_extendHomologyIso_hom_assoc
{ι : 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]
[CategoryTheory.Limits.HasZeroObject C]
(K : HomologicalComplex C c)
(e : c.Embedding c')
{j : ι}
{j' : ι'}
(hj' : e.f j = j')
[K.HasHomology j]
[(K.extend e).HasHomology j']
{Z : C}
(h : K.homology j ⟶ Z)
:
CategoryTheory.CategoryStruct.comp ((K.extend e).homologyπ j')
(CategoryTheory.CategoryStruct.comp (K.extendHomologyIso e hj').hom h) = CategoryTheory.CategoryStruct.comp (K.extendCyclesIso e hj').hom
(CategoryTheory.CategoryStruct.comp (K.homologyπ j) h)
@[simp]
theorem
HomologicalComplex.homologyπ_extendHomologyIso_inv
{ι : 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]
[CategoryTheory.Limits.HasZeroObject C]
(K : HomologicalComplex C c)
(e : c.Embedding c')
{j : ι}
{j' : ι'}
(hj' : e.f j = j')
[K.HasHomology j]
[(K.extend e).HasHomology j']
:
CategoryTheory.CategoryStruct.comp (K.homologyπ j) (K.extendHomologyIso e hj').inv = CategoryTheory.CategoryStruct.comp (K.extendCyclesIso e hj').inv ((K.extend e).homologyπ j')
@[simp]
theorem
HomologicalComplex.homologyπ_extendHomologyIso_inv_assoc
{ι : 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]
[CategoryTheory.Limits.HasZeroObject C]
(K : HomologicalComplex C c)
(e : c.Embedding c')
{j : ι}
{j' : ι'}
(hj' : e.f j = j')
[K.HasHomology j]
[(K.extend e).HasHomology j']
{Z : C}
(h : (K.extend e).homology j' ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (K.homologyπ j)
(CategoryTheory.CategoryStruct.comp (K.extendHomologyIso e hj').inv h) = CategoryTheory.CategoryStruct.comp (K.extendCyclesIso e hj').inv
(CategoryTheory.CategoryStruct.comp ((K.extend e).homologyπ j') h)
@[simp]
theorem
HomologicalComplex.pOpcycles_extendOpcyclesIso_inv
{ι : 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]
[CategoryTheory.Limits.HasZeroObject C]
(K : HomologicalComplex C c)
(e : c.Embedding c')
{j : ι}
{j' : ι'}
(hj' : e.f j = j')
[K.HasHomology j]
[(K.extend e).HasHomology j']
:
CategoryTheory.CategoryStruct.comp (K.pOpcycles j) (K.extendOpcyclesIso e hj').inv = CategoryTheory.CategoryStruct.comp (K.extendXIso e hj').inv ((K.extend e).pOpcycles j')
@[simp]
theorem
HomologicalComplex.pOpcycles_extendOpcyclesIso_inv_assoc
{ι : 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]
[CategoryTheory.Limits.HasZeroObject C]
(K : HomologicalComplex C c)
(e : c.Embedding c')
{j : ι}
{j' : ι'}
(hj' : e.f j = j')
[K.HasHomology j]
[(K.extend e).HasHomology j']
{Z : C}
(h : (K.extend e).opcycles j' ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (K.pOpcycles j)
(CategoryTheory.CategoryStruct.comp (K.extendOpcyclesIso e hj').inv h) = CategoryTheory.CategoryStruct.comp (K.extendXIso e hj').inv
(CategoryTheory.CategoryStruct.comp ((K.extend e).pOpcycles j') h)
@[simp]
theorem
HomologicalComplex.pOpcycles_extendOpcyclesIso_hom
{ι : 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]
[CategoryTheory.Limits.HasZeroObject C]
(K : HomologicalComplex C c)
(e : c.Embedding c')
{j : ι}
{j' : ι'}
(hj' : e.f j = j')
[K.HasHomology j]
[(K.extend e).HasHomology j']
:
CategoryTheory.CategoryStruct.comp ((K.extend e).pOpcycles j') (K.extendOpcyclesIso e hj').hom = CategoryTheory.CategoryStruct.comp (K.extendXIso e hj').hom (K.pOpcycles j)
@[simp]
theorem
HomologicalComplex.pOpcycles_extendOpcyclesIso_hom_assoc
{ι : 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]
[CategoryTheory.Limits.HasZeroObject C]
(K : HomologicalComplex C c)
(e : c.Embedding c')
{j : ι}
{j' : ι'}
(hj' : e.f j = j')
[K.HasHomology j]
[(K.extend e).HasHomology j']
{Z : C}
(h : K.opcycles j ⟶ Z)
:
CategoryTheory.CategoryStruct.comp ((K.extend e).pOpcycles j')
(CategoryTheory.CategoryStruct.comp (K.extendOpcyclesIso e hj').hom h) = CategoryTheory.CategoryStruct.comp (K.extendXIso e hj').hom (CategoryTheory.CategoryStruct.comp (K.pOpcycles j) h)
@[simp]
theorem
HomologicalComplex.extendHomologyIso_hom_homologyι
{ι : 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]
[CategoryTheory.Limits.HasZeroObject C]
(K : HomologicalComplex C c)
(e : c.Embedding c')
{j : ι}
{j' : ι'}
(hj' : e.f j = j')
[K.HasHomology j]
[(K.extend e).HasHomology j']
:
CategoryTheory.CategoryStruct.comp (K.extendHomologyIso e hj').hom (K.homologyι j) = CategoryTheory.CategoryStruct.comp ((K.extend e).homologyι j') (K.extendOpcyclesIso e hj').hom
@[simp]
theorem
HomologicalComplex.extendHomologyIso_hom_homologyι_assoc
{ι : 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]
[CategoryTheory.Limits.HasZeroObject C]
(K : HomologicalComplex C c)
(e : c.Embedding c')
{j : ι}
{j' : ι'}
(hj' : e.f j = j')
[K.HasHomology j]
[(K.extend e).HasHomology j']
{Z : C}
(h : K.opcycles j ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (K.extendHomologyIso e hj').hom
(CategoryTheory.CategoryStruct.comp (K.homologyι j) h) = CategoryTheory.CategoryStruct.comp ((K.extend e).homologyι j')
(CategoryTheory.CategoryStruct.comp (K.extendOpcyclesIso e hj').hom h)
@[simp]
theorem
HomologicalComplex.extendHomologyIso_inv_homologyι
{ι : 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]
[CategoryTheory.Limits.HasZeroObject C]
(K : HomologicalComplex C c)
(e : c.Embedding c')
{j : ι}
{j' : ι'}
(hj' : e.f j = j')
[K.HasHomology j]
[(K.extend e).HasHomology j']
:
CategoryTheory.CategoryStruct.comp (K.extendHomologyIso e hj').inv ((K.extend e).homologyι j') = CategoryTheory.CategoryStruct.comp (K.homologyι j) (K.extendOpcyclesIso e hj').inv
@[simp]
theorem
HomologicalComplex.extendHomologyIso_inv_homologyι_assoc
{ι : 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]
[CategoryTheory.Limits.HasZeroObject C]
(K : HomologicalComplex C c)
(e : c.Embedding c')
{j : ι}
{j' : ι'}
(hj' : e.f j = j')
[K.HasHomology j]
[(K.extend e).HasHomology j']
{Z : C}
(h : (K.extend e).opcycles j' ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (K.extendHomologyIso e hj').inv
(CategoryTheory.CategoryStruct.comp ((K.extend e).homologyι j') h) = CategoryTheory.CategoryStruct.comp (K.homologyι j)
(CategoryTheory.CategoryStruct.comp (K.extendOpcyclesIso e hj').inv h)
@[simp]
theorem
HomologicalComplex.extendCyclesIso_hom_naturality
{ι : 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]
[CategoryTheory.Limits.HasZeroObject C]
{K L : HomologicalComplex C c}
(φ : K ⟶ L)
(e : c.Embedding c')
{j : ι}
{j' : ι'}
(hj' : e.f j = j')
[K.HasHomology j]
[L.HasHomology j]
[(K.extend e).HasHomology j']
[(L.extend e).HasHomology j']
:
CategoryTheory.CategoryStruct.comp (cyclesMap (extendMap φ e) j') (L.extendCyclesIso e hj').hom = CategoryTheory.CategoryStruct.comp (K.extendCyclesIso e hj').hom (cyclesMap φ j)
@[simp]
theorem
HomologicalComplex.extendCyclesIso_hom_naturality_assoc
{ι : 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]
[CategoryTheory.Limits.HasZeroObject C]
{K L : HomologicalComplex C c}
(φ : K ⟶ L)
(e : c.Embedding c')
{j : ι}
{j' : ι'}
(hj' : e.f j = j')
[K.HasHomology j]
[L.HasHomology j]
[(K.extend e).HasHomology j']
[(L.extend e).HasHomology j']
{Z : C}
(h : L.cycles j ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (cyclesMap (extendMap φ e) j')
(CategoryTheory.CategoryStruct.comp (L.extendCyclesIso e hj').hom h) = CategoryTheory.CategoryStruct.comp (K.extendCyclesIso e hj').hom
(CategoryTheory.CategoryStruct.comp (cyclesMap φ j) h)
@[simp]
theorem
HomologicalComplex.extendHomologyIso_hom_naturality
{ι : 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]
[CategoryTheory.Limits.HasZeroObject C]
{K L : HomologicalComplex C c}
(φ : K ⟶ L)
(e : c.Embedding c')
{j : ι}
{j' : ι'}
(hj' : e.f j = j')
[K.HasHomology j]
[L.HasHomology j]
[(K.extend e).HasHomology j']
[(L.extend e).HasHomology j']
:
CategoryTheory.CategoryStruct.comp (homologyMap (extendMap φ e) j') (L.extendHomologyIso e hj').hom = CategoryTheory.CategoryStruct.comp (K.extendHomologyIso e hj').hom (homologyMap φ j)
@[simp]
theorem
HomologicalComplex.extendHomologyIso_hom_naturality_assoc
{ι : 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]
[CategoryTheory.Limits.HasZeroObject C]
{K L : HomologicalComplex C c}
(φ : K ⟶ L)
(e : c.Embedding c')
{j : ι}
{j' : ι'}
(hj' : e.f j = j')
[K.HasHomology j]
[L.HasHomology j]
[(K.extend e).HasHomology j']
[(L.extend e).HasHomology j']
{Z : C}
(h : L.homology j ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (homologyMap (extendMap φ e) j')
(CategoryTheory.CategoryStruct.comp (L.extendHomologyIso e hj').hom h) = CategoryTheory.CategoryStruct.comp (K.extendHomologyIso e hj').hom
(CategoryTheory.CategoryStruct.comp (homologyMap φ j) h)
theorem
HomologicalComplex.quasiIsoAt_extendMap_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]
[CategoryTheory.Limits.HasZeroObject C]
{K L : HomologicalComplex C c}
(φ : K ⟶ L)
(e : c.Embedding c')
{j : ι}
{j' : ι'}
(hj' : e.f j = j')
[K.HasHomology j]
[L.HasHomology j]
[(K.extend e).HasHomology j']
[(L.extend e).HasHomology j']
:
QuasiIsoAt (extendMap φ e) j' ↔ QuasiIsoAt φ j
theorem
HomologicalComplex.quasiIso_extendMap_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]
[CategoryTheory.Limits.HasZeroObject C]
(K L : HomologicalComplex C c)
(φ : K ⟶ L)
(e : c.Embedding c')
[∀ (j : ι), K.HasHomology j]
[∀ (j : ι), L.HasHomology j]
:
instance
HomologicalComplex.instQuasiIsoExtendMap
{ι : 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]
[CategoryTheory.Limits.HasZeroObject C]
(K L : HomologicalComplex C c)
(φ : K ⟶ L)
(e : c.Embedding c')
[∀ (j : ι), K.HasHomology j]
[∀ (j : ι), L.HasHomology j]
[QuasiIso φ]
: