Pulling back a short complex #
Given a short complex S and a morphism f : Y ⟶ S.X₃, we construct the short complex
S.pull f, which is S.X₁ ⟶ pullback f S.g ⟶ Y, and show that it is short exact when S is,
if the ambient category is abelian.
This is dual to ShortComplex.push, see Mathlib/Algebra/Homology/ShortComplex/Pushout.lean.
@[implicit_reducible]
noncomputable def
CategoryTheory.ShortComplex.pull
{C : Type u_1}
[Category.{v_1, u_1} C]
[Limits.HasZeroMorphisms C]
(S : ShortComplex C)
{Y : C}
(f : Y ⟶ S.X₃)
[Limits.HasPullback f S.g]
:
The pullback of a short complex S along a morphism f : Y ⟶ S.X₃: the short complex
S.X₁ ⟶ pullback f S.g ⟶ Y, whose first map is induced by 0 and S.f and whose second map
is pullback.fst.
Equations
- S.pull f = { X₁ := S.X₁, X₂ := CategoryTheory.Limits.pullback f S.g, X₃ := Y, f := CategoryTheory.Limits.pullback.lift 0 S.f ⋯, g := CategoryTheory.Limits.pullback.fst f S.g, zero := ⋯ }
Instances For
@[simp]
theorem
CategoryTheory.ShortComplex.pull_X₃
{C : Type u_1}
[Category.{v_1, u_1} C]
[Limits.HasZeroMorphisms C]
(S : ShortComplex C)
{Y : C}
(f : Y ⟶ S.X₃)
[Limits.HasPullback f S.g]
:
@[simp]
theorem
CategoryTheory.ShortComplex.pull_X₁
{C : Type u_1}
[Category.{v_1, u_1} C]
[Limits.HasZeroMorphisms C]
(S : ShortComplex C)
{Y : C}
(f : Y ⟶ S.X₃)
[Limits.HasPullback f S.g]
:
@[simp]
theorem
CategoryTheory.ShortComplex.pull_f
{C : Type u_1}
[Category.{v_1, u_1} C]
[Limits.HasZeroMorphisms C]
(S : ShortComplex C)
{Y : C}
(f : Y ⟶ S.X₃)
[Limits.HasPullback f S.g]
:
@[simp]
theorem
CategoryTheory.ShortComplex.pull_X₂
{C : Type u_1}
[Category.{v_1, u_1} C]
[Limits.HasZeroMorphisms C]
(S : ShortComplex C)
{Y : C}
(f : Y ⟶ S.X₃)
[Limits.HasPullback f S.g]
:
@[simp]
theorem
CategoryTheory.ShortComplex.pull_g
{C : Type u_1}
[Category.{v_1, u_1} C]
[Limits.HasZeroMorphisms C]
(S : ShortComplex C)
{Y : C}
(f : Y ⟶ S.X₃)
[Limits.HasPullback f S.g]
:
instance
CategoryTheory.instEpiGPull
{C : Type u_1}
[Category.{v_1, u_1} C]
[Abelian C]
(S : ShortComplex C)
{Y : C}
(f : Y ⟶ S.X₃)
[Epi S.g]
:
instance
CategoryTheory.instMonoFPull
{C : Type u_1}
[Category.{v_1, u_1} C]
[Limits.HasZeroMorphisms C]
(S : ShortComplex C)
{Y : C}
(f : Y ⟶ S.X₃)
[Limits.HasPullback f S.g]
[Mono S.f]
:
theorem
CategoryTheory.ShortComplex.ShortExact.pull
{C : Type u_1}
[Category.{v_1, u_1} C]
[Abelian C]
{S : ShortComplex C}
(hS : S.ShortExact)
{Y : C}
(f : Y ⟶ S.X₃)
:
(S.pull f).ShortExact
The pullback of a short exact short complex along any morphism f : Y ⟶ S.X₃ is
short exact.