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} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {X₁ : C} {X₂ : C} {X₃ : C} {X₄ : C} [CategoryTheory.Limits.HasBinaryBiproduct X₂ X₃] {f : X₁ ⟶ X₂} {g : X₁ ⟶ X₃} {inl : X₂ ⟶ X₄} {inr : X₃ ⟶ X₄} (sq : CategoryTheory.CommSq f g inl inr) :
CategoryTheory.Limits.CokernelCofork (CategoryTheory.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.isColimitEquivIsColimitCokernelCofork {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {X₁ : C} {X₂ : C} {X₃ : C} {X₄ : C} [CategoryTheory.Limits.HasBinaryBiproduct X₂ X₃] {f : X₁ ⟶ X₂} {g : X₁ ⟶ X₃} {inl : X₂ ⟶ X₄} {inr : X₃ ⟶ X₄} (sq : CategoryTheory.CommSq f g inl inr) :
    CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.PushoutCocone.mk inl inr ⋯) ≃ CategoryTheory.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
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      noncomputable def CategoryTheory.IsPushout.isColimitCokernelCofork {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {X₁ : C} {X₂ : C} {X₃ : C} {X₄ : C} [CategoryTheory.Limits.HasBinaryBiproduct X₂ X₃] {f : X₁ ⟶ X₂} {g : X₁ ⟶ X₃} {inl : X₂ ⟶ X₄} {inr : X₃ ⟶ X₄} (h : CategoryTheory.IsPushout f g inl inr) :
      CategoryTheory.Limits.IsColimit ⋯.cokernelCofork

      The colimit cokernel cofork attached to a pushout square.

      Equations
      • h.isColimitCokernelCofork = ⋯.isColimitEquivIsColimitCokernelCofork h.isColimit
      Instances For
        source
        @[reducible, inline]
        noncomputable abbrev CategoryTheory.CommSq.kernelFork {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {X₁ : C} {X₂ : C} {X₃ : C} {X₄ : C} [CategoryTheory.Limits.HasBinaryBiproduct X₂ X₃] {fst : X₁ ⟶ X₂} {snd : X₁ ⟶ X₃} {f : X₂ ⟶ X₄} {g : X₃ ⟶ X₄} (sq : CategoryTheory.CommSq fst snd f g) :
        CategoryTheory.Limits.KernelFork (CategoryTheory.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.isLimitEquivIsLimitKernelFork {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {X₁ : C} {X₂ : C} {X₃ : C} {X₄ : C} [CategoryTheory.Limits.HasBinaryBiproduct X₂ X₃] {fst : X₁ ⟶ X₂} {snd : X₁ ⟶ X₃} {f : X₂ ⟶ X₄} {g : X₃ ⟶ X₄} (sq : CategoryTheory.CommSq fst snd f g) :
          CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.PullbackCone.mk fst snd ⋯) ≃ CategoryTheory.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
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            noncomputable def CategoryTheory.IsPullback.isLimitKernelFork {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {X₁ : C} {X₂ : C} {X₃ : C} {X₄ : C} [CategoryTheory.Limits.HasBinaryBiproduct X₂ X₃] {fst : X₁ ⟶ X₂} {snd : X₁ ⟶ X₃} {f : X₂ ⟶ X₄} {g : X₃ ⟶ X₄} (h : CategoryTheory.IsPullback fst snd f g) :
            CategoryTheory.Limits.IsLimit ⋯.kernelFork

            The limit kernel fork attached to a pullback square.

            Equations
            • h.isLimitKernelFork = ⋯.isLimitEquivIsLimitKernelFork h.isLimit
            Instances For