Documentation

Mathlib.Algebra.Homology.CommSq

Relation between pullback/pushout squares and kernel/cokernel sequences #

Consider a commutative square in a preadditive category:

X₁ ⟶ X₂
|    |
v    v
X₃ ⟶ X₄

In this file, we show that this is a pushout square iff the object X₄ identifies to the cokernel of the difference map X₁ ⟶ X₂ ⊞ X₃ via the obvious map X₂ ⊞ X₃ ⟶ X₄.

Similarly, it is a pullback square iff the object X₁ identifies to the kernel of the difference map X₂ ⊞ X₃ ⟶ X₄ via the obvious map X₁ ⟶ X₂ ⊞ X₃.

source
@[reducible, inline]
noncomputable abbrev CategoryTheory.CommSq.cokernelCofork {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {X₁ X₂ X₃ X₄ : C} [Limits.HasBinaryBiproduct X₂ X₃] {f : X₁ ⟶ X₂} {g : X₁ ⟶ X₃} {inl : X₂ ⟶ X₄} {inr : X₃ ⟶ X₄} (sq : CommSq f g inl inr) :
Limits.CokernelCofork (Limits.biprod.lift f (-g))

The cokernel cofork attached to a commutative square in a preadditive category.

Equations
    Instances For
      source
      noncomputable def CategoryTheory.CommSq.shortComplex {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {X₁ X₂ X₃ X₄ : C} [Limits.HasBinaryBiproduct X₂ X₃] {f : X₁ ⟶ X₂} {g : X₁ ⟶ X₃} {inl : X₂ ⟶ X₄} {inr : X₃ ⟶ X₄} (sq : CommSq f g inl inr) :
      ShortComplex C

      The short complex attached to the cokernel cofork of a commutative square.

      Equations
        Instances For
          source
          @[simp]
          theorem CategoryTheory.CommSq.shortComplex_X₃ {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {X₁ X₂ X₃ X₄ : C} [Limits.HasBinaryBiproduct X₂ X₃] {f : X₁ ⟶ X₂} {g : X₁ ⟶ X₃} {inl : X₂ ⟶ X₄} {inr : X₃ ⟶ X₄} (sq : CommSq f g inl inr) :
          sq.shortComplex.X₃ = X₄
          source
          @[simp]
          theorem CategoryTheory.CommSq.shortComplex_g {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {X₁ X₂ X₃ X₄ : C} [Limits.HasBinaryBiproduct X₂ X₃] {f : X₁ ⟶ X₂} {g : X₁ ⟶ X₃} {inl : X₂ ⟶ X₄} {inr : X₃ ⟶ X₄} (sq : CommSq f g inl inr) :
          sq.shortComplex.g = Limits.biprod.desc inl inr
          source
          @[simp]
          theorem CategoryTheory.CommSq.shortComplex_X₂ {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {X₁ X₂ X₃ X₄ : C} [Limits.HasBinaryBiproduct X₂ X₃] {f : X₁ ⟶ X₂} {g : X₁ ⟶ X₃} {inl : X₂ ⟶ X₄} {inr : X₃ ⟶ X₄} (sq : CommSq f g inl inr) :
          sq.shortComplex.X₂ = (X₂ ⊞ X₃)
          source
          @[simp]
          theorem CategoryTheory.CommSq.shortComplex_X₁ {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {X₁ X₂ X₃ X₄ : C} [Limits.HasBinaryBiproduct X₂ X₃] {f : X₁ ⟶ X₂} {g : X₁ ⟶ X₃} {inl : X₂ ⟶ X₄} {inr : X₃ ⟶ X₄} (sq : CommSq f g inl inr) :
          sq.shortComplex.X₁ = X₁
          source
          @[simp]
          theorem CategoryTheory.CommSq.shortComplex_f {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {X₁ X₂ X₃ X₄ : C} [Limits.HasBinaryBiproduct X₂ X₃] {f : X₁ ⟶ X₂} {g : X₁ ⟶ X₃} {inl : X₂ ⟶ X₄} {inr : X₃ ⟶ X₄} (sq : CommSq f g inl inr) :
          sq.shortComplex.f = Limits.biprod.lift f (-g)
          source
          noncomputable def CategoryTheory.CommSq.isColimitEquivIsColimitCokernelCofork {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {X₁ X₂ X₃ X₄ : C} [Limits.HasBinaryBiproduct X₂ X₃] {f : X₁ ⟶ X₂} {g : X₁ ⟶ X₃} {inl : X₂ ⟶ X₄} {inr : X₃ ⟶ X₄} (sq : CommSq f g inl inr) :
          Limits.IsColimit (Limits.PushoutCocone.mk inl inr ⋯) ≃ Limits.IsColimit sq.cokernelCofork

          A commutative square in a preadditive category is a pushout square iff the corresponding diagram X₁ ⟶ X₂ ⊞ X₃ ⟶ X₄ ⟶ 0 makes X₄ a cokernel.

          Equations
            Instances For
              source
              noncomputable def CategoryTheory.IsPushout.isColimitCokernelCofork {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {X₁ X₂ X₃ X₄ : C} [Limits.HasBinaryBiproduct X₂ X₃] {f : X₁ ⟶ X₂} {g : X₁ ⟶ X₃} {inl : X₂ ⟶ X₄} {inr : X₃ ⟶ X₄} (h : IsPushout f g inl inr) :
              Limits.IsColimit ⋯.cokernelCofork

              The colimit cokernel cofork attached to a pushout square.

              Equations
                Instances For
                  source
                  theorem CategoryTheory.IsPushout.epi_shortComplex_g {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {X₁ X₂ X₃ X₄ : C} [Limits.HasBinaryBiproduct X₂ X₃] {f : X₁ ⟶ X₂} {g : X₁ ⟶ X₃} {inl : X₂ ⟶ X₄} {inr : X₃ ⟶ X₄} (h : IsPushout f g inl inr) :
                  Epi ⋯.shortComplex.g
                  source
                  @[reducible, inline]
                  noncomputable abbrev CategoryTheory.CommSq.kernelFork {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {X₁ X₂ X₃ X₄ : C} [Limits.HasBinaryBiproduct X₂ X₃] {fst : X₁ ⟶ X₂} {snd : X₁ ⟶ X₃} {f : X₂ ⟶ X₄} {g : X₃ ⟶ X₄} (sq : CommSq fst snd f g) :
                  Limits.KernelFork (Limits.biprod.desc f (-g))

                  The kernel fork attached to a commutative square in a preadditive category.

                  Equations
                    Instances For
                      source
                      noncomputable def CategoryTheory.CommSq.shortComplex' {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {X₁ X₂ X₃ X₄ : C} [Limits.HasBinaryBiproduct X₂ X₃] {fst : X₁ ⟶ X₂} {snd : X₁ ⟶ X₃} {f : X₂ ⟶ X₄} {g : X₃ ⟶ X₄} (sq : CommSq fst snd f g) :
                      ShortComplex C

                      The short complex attached to the kernel fork of a commutative square. (This is similar to CommSq.shortComplex, but with different signs.)

                      Equations
                        Instances For
                          source
                          @[simp]
                          theorem CategoryTheory.CommSq.shortComplex'_X₃ {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {X₁ X₂ X₃ X₄ : C} [Limits.HasBinaryBiproduct X₂ X₃] {fst : X₁ ⟶ X₂} {snd : X₁ ⟶ X₃} {f : X₂ ⟶ X₄} {g : X₃ ⟶ X₄} (sq : CommSq fst snd f g) :
                          sq.shortComplex'.X₃ = X₄
                          source
                          @[simp]
                          theorem CategoryTheory.CommSq.shortComplex'_f {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {X₁ X₂ X₃ X₄ : C} [Limits.HasBinaryBiproduct X₂ X₃] {fst : X₁ ⟶ X₂} {snd : X₁ ⟶ X₃} {f : X₂ ⟶ X₄} {g : X₃ ⟶ X₄} (sq : CommSq fst snd f g) :
                          sq.shortComplex'.f = Limits.biprod.lift fst snd
                          source
                          @[simp]
                          theorem CategoryTheory.CommSq.shortComplex'_X₁ {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {X₁ X₂ X₃ X₄ : C} [Limits.HasBinaryBiproduct X₂ X₃] {fst : X₁ ⟶ X₂} {snd : X₁ ⟶ X₃} {f : X₂ ⟶ X₄} {g : X₃ ⟶ X₄} (sq : CommSq fst snd f g) :
                          sq.shortComplex'.X₁ = X₁
                          source
                          @[simp]
                          theorem CategoryTheory.CommSq.shortComplex'_g {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {X₁ X₂ X₃ X₄ : C} [Limits.HasBinaryBiproduct X₂ X₃] {fst : X₁ ⟶ X₂} {snd : X₁ ⟶ X₃} {f : X₂ ⟶ X₄} {g : X₃ ⟶ X₄} (sq : CommSq fst snd f g) :
                          sq.shortComplex'.g = Limits.biprod.desc f (-g)
                          source
                          @[simp]
                          theorem CategoryTheory.CommSq.shortComplex'_X₂ {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {X₁ X₂ X₃ X₄ : C} [Limits.HasBinaryBiproduct X₂ X₃] {fst : X₁ ⟶ X₂} {snd : X₁ ⟶ X₃} {f : X₂ ⟶ X₄} {g : X₃ ⟶ X₄} (sq : CommSq fst snd f g) :
                          sq.shortComplex'.X₂ = (X₂ ⊞ X₃)
                          source
                          noncomputable def CategoryTheory.CommSq.isLimitEquivIsLimitKernelFork {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {X₁ X₂ X₃ X₄ : C} [Limits.HasBinaryBiproduct X₂ X₃] {fst : X₁ ⟶ X₂} {snd : X₁ ⟶ X₃} {f : X₂ ⟶ X₄} {g : X₃ ⟶ X₄} (sq : CommSq fst snd f g) :
                          Limits.IsLimit (Limits.PullbackCone.mk fst snd ⋯) ≃ Limits.IsLimit sq.kernelFork

                          A commutative square in a preadditive category is a pullback square iff the corresponding diagram 0 ⟶ X₁ ⟶ X₂ ⊞ X₃ ⟶ X₄ ⟶ 0 makes X₁ a kernel.

                          Equations
                            Instances For
                              source
                              noncomputable def CategoryTheory.IsPullback.isLimitKernelFork {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {X₁ X₂ X₃ X₄ : C} [Limits.HasBinaryBiproduct X₂ X₃] {fst : X₁ ⟶ X₂} {snd : X₁ ⟶ X₃} {f : X₂ ⟶ X₄} {g : X₃ ⟶ X₄} (h : IsPullback fst snd f g) :
                              Limits.IsLimit ⋯.kernelFork

                              The limit kernel fork attached to a pullback square.

                              Equations
                                Instances For
                                  source
                                  theorem CategoryTheory.IsPullback.mono_shortComplex'_f {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {X₁ X₂ X₃ X₄ : C} [Limits.HasBinaryBiproduct X₂ X₃] {fst : X₁ ⟶ X₂} {snd : X₁ ⟶ X₃} {f : X₂ ⟶ X₄} {g : X₃ ⟶ X₄} (h : IsPullback fst snd f g) :
                                  Mono ⋯.shortComplex'.f