Documentation

Mathlib.Algebra.Homology.ShortComplex.Pullback

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.

source
@[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] :
ShortComplex C

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
Instances For
    source
    @[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] :
    (S.pull f).X₃ = Y
    source
    @[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] :
    (S.pull f).X₁ = S.X₁
    source
    @[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] :
    (S.pull f).f = Limits.pullback.lift 0 S.f ⋯
    source
    @[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] :
    (S.pull f).X₂ = Limits.pullback f S.g
    source
    @[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] :
    (S.pull f).g = Limits.pullback.fst f S.g
    source
    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] :
    Epi (S.pull f).g
    source
    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] :
    Mono (S.pull f).f
    source
    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.