Documentation

Mathlib.Algebra.Homology.Square

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

This file is the bundled counterpart of Mathlib/Algebra/Homology/CommSq.lean. The same results are obtained here for squares sq : Square C where C is an additive category.

source
🔸 coverage
@[reducible, inline]
noncomputable abbrev CategoryTheory.Square.cokernelCofork {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] (sq : Square C) [Limits.HasBinaryBiproduct sq.X₂ sq.X₃] :
Limits.CokernelCofork (Limits.biprod.lift sq.f₁₂ (-sq.f₁₃))

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

Equations
    Instances For
      source
      🔸 coverage
      noncomputable def CategoryTheory.Square.isPushoutEquivIsColimitCokernelCofork {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] (sq : Square C) [Limits.HasBinaryBiproduct sq.X₂ sq.X₃] :
      sq.IsPushout ≃ 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
          🔸 coverage
          noncomputable def CategoryTheory.Square.IsPushout.isColimitCokernelCofork {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] {sq : Square C} [Limits.HasBinaryBiproduct sq.X₂ sq.X₃] (h : sq.IsPushout) :
          Limits.IsColimit sq.cokernelCofork

          The colimit cokernel cofork attached to a pushout square.

          Equations
            Instances For
              source
              🔸 coverage
              @[reducible, inline]
              noncomputable abbrev CategoryTheory.Square.kernelFork {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] (sq : Square C) [Limits.HasBinaryBiproduct sq.X₂ sq.X₃] :
              Limits.KernelFork (Limits.biprod.desc sq.f₂₄ (-sq.f₃₄))

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

              Equations
                Instances For
                  source
                  🔸 coverage
                  noncomputable def CategoryTheory.Square.isPullbackEquivIsLimitKernelFork {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] (sq : Square C) [Limits.HasBinaryBiproduct sq.X₂ sq.X₃] :
                  sq.IsPullback ≃ 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
                      🔸 coverage
                      noncomputable def CategoryTheory.Square.IsPullback.isLimitKernelFork {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] {sq : Square C} [Limits.HasBinaryBiproduct sq.X₂ sq.X₃] (h : sq.IsPullback) :
                      Limits.IsLimit sq.kernelFork

                      The limit kernel fork attached to a pullback square.

                      Equations
                        Instances For