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 shall construct an isomorphism
(K.extend e).homology j' ≅ K.homology j (TODO).
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 .
Equations
- One or more equations did not get rendered due to their size.
Instances For
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 (HomologicalComplex.extend.leftHomologyData.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 .
Equations
- One or more equations did not get rendered due to their size.
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.{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
((HomologicalComplex.extend.leftHomologyData.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
((HomologicalComplex.extend.leftHomologyData.isLimitKernelFork K e hj' hk hk' cone hcone).lift
(CategoryTheory.Limits.KernelFork.ofι ((K.extend e).d i' j') ⋯))
Auxiliary definition for extend.leftHomologyData.
Equations
- HomologicalComplex.extend.leftHomologyData.cokernelCofork K e hj' hi hi' hk hk' cone hcone cocone = CategoryTheory.Limits.CokernelCofork.ofπ (CategoryTheory.Limits.Cofork.π cocone) ⋯
Instances For
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
(HomologicalComplex.extend.leftHomologyData.cokernelCofork K e hj' hi hi' hk hk' cone hcone cocone)
Auxiliary definition for extend.leftHomologyData.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[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)
:
(HomologicalComplex.extend.leftHomologyData K e hj' hi hi' hk hk' h).K = h.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)
:
(HomologicalComplex.extend.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)
:
(HomologicalComplex.extend.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)
:
(HomologicalComplex.extend.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.{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.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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 (HomologicalComplex.extend.rightHomologyData.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.
Equations
- One or more equations did not get rendered due to their size.
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.{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 φ
((HomologicalComplex.extend.rightHomologyData.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
((HomologicalComplex.extend.rightHomologyData.isColimitCokernelCofork K e hj' hi hi' cocone hcocone).desc
(CategoryTheory.Limits.CokernelCofork.ofπ ((K.extend e).d j' k') ⋯))
Auxiliary definition for extend.rightHomologyData.
Equations
- HomologicalComplex.extend.rightHomologyData.kernelFork K e hj' hi hi' hk hk' cocone hcocone cone = CategoryTheory.Limits.KernelFork.ofι (CategoryTheory.Limits.Fork.ι cone) ⋯
Instances For
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
(HomologicalComplex.extend.rightHomologyData.kernelFork K e hj' hi hi' hk hk' cocone hcocone cone)
Auxiliary definition for extend.rightHomologyData.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[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)
:
(HomologicalComplex.extend.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)
:
(HomologicalComplex.extend.rightHomologyData K e hj' hi hi' hk hk' h).H = h.H
@[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)
:
(HomologicalComplex.extend.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.{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)
:
(HomologicalComplex.extend.rightHomologyData K e hj' hi hi' hk hk' h).p = CategoryTheory.CategoryStruct.comp (K.extendXIso e hj').hom h.p
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.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[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)
:
(HomologicalComplex.extend.homologyData K e hj' hi hi' hk hk' h).right = HomologicalComplex.extend.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.{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)
:
(HomologicalComplex.extend.homologyData K e hj' hi hi' hk hk' h).left = HomologicalComplex.extend.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.{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)
:
(HomologicalComplex.extend.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.{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.
Equations
- HomologicalComplex.extend.homologyData' K e hj' hi hk h = HomologicalComplex.extend.homologyData K e hj' hi ⋯ hk ⋯ h
Instances For
@[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)
:
(HomologicalComplex.extend.homologyData' K e hj' hi hk h).right.H = h.right.H
@[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)
:
(HomologicalComplex.extend.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_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)
:
(HomologicalComplex.extend.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)
:
(HomologicalComplex.extend.homologyData' K e hj' hi hk h).right.Q = h.right.Q
@[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)
:
(HomologicalComplex.extend.homologyData' K e hj' hi hk h).right.ι = 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 : ι}
{j' : ι'}
(hj' : e.f j = j')
(hi : c.prev j = i)
(hk : c.next j = k)
(h : (K.sc' i j k).HomologyData)
:
(HomologicalComplex.extend.homologyData' K e hj' hi hk h).iso = h.iso
@[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)
:
(HomologicalComplex.extend.homologyData' K e hj' hi hk h).left.H = h.left.H
@[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)
:
(HomologicalComplex.extend.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)
:
(HomologicalComplex.extend.homologyData' K e hj' hi hk h).left.π = h.left.π
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'