Homology of the extension of an 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.{u_4, 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.{u_4, 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.{u_4, 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 .

noncomputable def HomologicalComplex.extend.leftHomologyData.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] [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 .

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.{u_4, 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.{u_4, 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.{u_4, 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.

noncomputable def HomologicalComplex.extend.leftHomologyData.isColimitCokernelCofork {ι : 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] [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.

noncomputable def HomologicalComplex.extend.leftHomologyData {ι : 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] [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.

@[simp]

theorem HomologicalComplex.extend.leftHomologyData_H {ι : 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] [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_π {ι : 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] [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.{u_4, 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

@[simp]

theorem HomologicalComplex.extend.leftHomologyData_K {ι : 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] [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

noncomputable def HomologicalComplex.extend.rightHomologyData.cokernelCofork {ι : 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] [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.

noncomputable def HomologicalComplex.extend.rightHomologyData.isColimitCokernelCofork {ι : 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] [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.

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.{u_4, 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.{u_4, 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.{u_4, 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.

noncomputable def HomologicalComplex.extend.rightHomologyData.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] [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.

noncomputable def HomologicalComplex.extend.rightHomologyData {ι : 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] [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.

@[simp]

theorem HomologicalComplex.extend.rightHomologyData_ι {ι : 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] [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_Q {ι : 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] [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_H {ι : 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] [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

@[simp]

theorem HomologicalComplex.extend.rightHomologyData_p {ι : 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] [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

theorem HomologicalComplex.extend.rightHomologyData_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] [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.{u_4, 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.

@[simp]

theorem HomologicalComplex.extend.homologyData_right {ι : 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] [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_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] [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

@[simp]

theorem HomologicalComplex.extend.homologyData_left {ι : 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] [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

noncomputable def HomologicalComplex.extend.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] [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.

@[simp]

theorem HomologicalComplex.extend.homologyData'_right_ι {ι : 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] [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.ι

@[simp]

theorem HomologicalComplex.extend.homologyData'_right_p {ι : 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] [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_π {ι : 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] [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'_left_i {ι : 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] [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'_left_H {ι : 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] [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'_left_K {ι : 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] [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'_right_Q {ι : 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] [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_H {ι : 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] [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'_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] [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

theorem HomologicalComplex.extend.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] [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.{u_4, 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.{u_4, 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.{u_4, 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') : (K.extend e).ExactAt j'

noncomputable def HomologicalComplex.extendCyclesIso {ι : 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] [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'] : (K.extend e).cycles j' ≅ K.cycles j

The isomorphism (K.extend e).cycles j' ≅ K.cycles j when e.f j = j'.

noncomputable def HomologicalComplex.extendOpcyclesIso {ι : 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] [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'] : (K.extend e).opcycles j' ≅ K.opcycles j

The isomorphism (K.extend e).opcycles j' ≅ K.opcycles j when e.f j = j'.

noncomputable def HomologicalComplex.extendHomologyIso {ι : 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] [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'] : (K.extend e).homology j' ≅ K.homology j

The isomorphism (K.extend e).homology j' ≅ K.homology j when e.f j = j'.

theorem HomologicalComplex.extend_exactAt_iff {ι : 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] [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'] : (K.extend e).ExactAt j' ↔ K.ExactAt j

@[simp]

theorem HomologicalComplex.extendCyclesIso_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] [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.{u_4, 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.{u_4, 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.{u_4, 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.{u_4, 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.{u_4, 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.{u_4, 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.{u_4, 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.{u_4, 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.{u_4, 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.{u_4, 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.{u_4, 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.{u_4, 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.{u_4, 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.{u_4, 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.{u_4, 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.{u_4, 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.{u_4, 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.{u_4, 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.{u_4, 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.{u_4, 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.{u_4, 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 (extendMap φ e) ↔ QuasiIso φ