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
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_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
@[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_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