Documentation

Mathlib.Algebra.Homology.ShortComplex.Pushout

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.

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

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