Pushing out a short complex #
Given a short complex S and a morphism f : S.X₁ ⟶ Y, we construct the short complex
S.push f, which is Y ⟶ pushout S.f f ⟶ S.X₃, and show that it is short exact when S is,
if the ambient category is abelian.
This is dual to ShortComplex.pull, see Mathlib/Algebra/Homology/ShortComplex/Pullback.lean.
@[implicit_reducible]
noncomputable def
CategoryTheory.ShortComplex.push
{C : Type u_1}
[Category.{v_1, u_1} C]
[Limits.HasZeroMorphisms C]
(S : ShortComplex C)
{Y : C}
(f : S.X₁ ⟶ Y)
[Limits.HasPushout S.f f]
:
The pushout of a short complex S along a morphism f : S.X₁ ⟶ Y: the short complex
Y ⟶ pushout S.f f ⟶ S.X₃, whose first map is pushout.inr and whose second map is induced
by S.g and 0.
Equations
- S.push f = { X₁ := Y, X₂ := CategoryTheory.Limits.pushout S.f f, X₃ := S.X₃, f := CategoryTheory.Limits.pushout.inr S.f f, g := CategoryTheory.Limits.pushout.desc S.g 0 ⋯, zero := ⋯ }
Instances For
@[simp]
theorem
CategoryTheory.ShortComplex.push_X₃
{C : Type u_1}
[Category.{v_1, u_1} C]
[Limits.HasZeroMorphisms C]
(S : ShortComplex C)
{Y : C}
(f : S.X₁ ⟶ Y)
[Limits.HasPushout S.f f]
:
@[simp]
theorem
CategoryTheory.ShortComplex.push_f
{C : Type u_1}
[Category.{v_1, u_1} C]
[Limits.HasZeroMorphisms C]
(S : ShortComplex C)
{Y : C}
(f : S.X₁ ⟶ Y)
[Limits.HasPushout S.f f]
:
@[simp]
theorem
CategoryTheory.ShortComplex.push_X₂
{C : Type u_1}
[Category.{v_1, u_1} C]
[Limits.HasZeroMorphisms C]
(S : ShortComplex C)
{Y : C}
(f : S.X₁ ⟶ Y)
[Limits.HasPushout S.f f]
:
@[simp]
theorem
CategoryTheory.ShortComplex.push_X₁
{C : Type u_1}
[Category.{v_1, u_1} C]
[Limits.HasZeroMorphisms C]
(S : ShortComplex C)
{Y : C}
(f : S.X₁ ⟶ Y)
[Limits.HasPushout S.f f]
:
@[simp]
theorem
CategoryTheory.ShortComplex.push_g
{C : Type u_1}
[Category.{v_1, u_1} C]
[Limits.HasZeroMorphisms C]
(S : ShortComplex C)
{Y : C}
(f : S.X₁ ⟶ Y)
[Limits.HasPushout S.f f]
:
instance
CategoryTheory.instMonoFPush
{C : Type u_1}
[Category.{v_1, u_1} C]
[Abelian C]
(S : ShortComplex C)
{Y : C}
(f : S.X₁ ⟶ Y)
[Mono S.f]
:
instance
CategoryTheory.instEpiGPush
{C : Type u_1}
[Category.{v_1, u_1} C]
[Limits.HasZeroMorphisms C]
(S : ShortComplex C)
{Y : C}
(f : S.X₁ ⟶ Y)
[Limits.HasPushout S.f f]
[Epi S.g]
:
theorem
CategoryTheory.ShortComplex.ShortExact.push
{C : Type u_1}
[Category.{v_1, u_1} C]
[Abelian C]
{S : ShortComplex C}
(hS : S.ShortExact)
{Y : C}
(f : S.X₁ ⟶ Y)
:
(S.push f).ShortExact
The pushout of a short exact short complex along any morphism f : S.X₁ ⟶ Y is
short exact.