Extension of degreewise splittings #
noncomputable def
ComplexShape.Embedding.splittingExtend
{ι₁ : Type u_1}
{ι₂ : Type u_2}
{c₁ : ComplexShape ι₁}
{c₂ : ComplexShape ι₂}
{C : Type u_3}
[CategoryTheory.Category.{v_1, u_3} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasZeroObject C]
(e : c₁.Embedding c₂)
{S : CategoryTheory.ShortComplex (HomologicalComplex C c₁)}
(σ : (i : ι₁) → (S.map (HomologicalComplex.eval C c₁ i)).Splitting)
(i₂ : ι₂)
:
((S.map (e.extendFunctor C)).map (HomologicalComplex.eval C c₂ i₂)).Splitting
If S is a short complex in HomologicalComplex C c₁ that is degreewise split,
then S.map (e.extendFunctor C) also is if e : Embedding c₁ c₂.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
ComplexShape.Embedding.splittingExtend_apply
{ι₁ : Type u_1}
{ι₂ : Type u_2}
{c₁ : ComplexShape ι₁}
{c₂ : ComplexShape ι₂}
{C : Type u_3}
[CategoryTheory.Category.{v_1, u_3} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasZeroObject C]
(e : c₁.Embedding c₂)
{S : CategoryTheory.ShortComplex (HomologicalComplex C c₁)}
(σ : (i : ι₁) → (S.map (HomologicalComplex.eval C c₁ i)).Splitting)
{i₁ : ι₁}
{i₂ : ι₂}
(h : e.f i₁ = i₂)
: