Theorems · Theorem · category theory

CategoryTheory.Limits.kernel.lift_map

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {X Y Z X' Y' Z' : C} (f : X ⟶ Y) (g : Y ⟶ Z) [inst_2 : CategoryTheory.Limits.HasKernel g]
  (w : CategoryTheory.CategoryStruct.comp f g = 0) (f' : X' ⟶ Y') (g' : Y' ⟶ Z')
  [inst_3 : CategoryTheory.Limits.HasKernel g'] (w' : CategoryTheory.CategoryStruct.comp f' g' = 0) (p : X ⟶ X')
  (q : Y ⟶ Y') (r : Z ⟶ Z'),
  CategoryTheory.CategoryStruct.comp f q = CategoryTheory.CategoryStruct.comp p f' →
    ∀ (h₂ : CategoryTheory.CategoryStruct.comp g r = CategoryTheory.CategoryStruct.comp q g'),
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.lift g f w)
          (CategoryTheory.Limits.kernel.map g g' q r h₂) =
        CategoryTheory.CategoryStruct.comp p (CategoryTheory.Limits.kernel.lift g' f' w')

Given a commutative diagram `` X --f--> Y --g--> Z | | | | | | v v v X' -f'-> Y' -g'-> Z' ` with horizontal arrows composing to zero, then we obtain a commutative square ` X > kernel g | | | | kernel.map | | v v X' --> kernel g' ``

Defined in

Mathlib.CategoryTheory.Limits.Shapes.Kernels

Cited by

1 results in Mathlib

Foundations

Depth 35 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasZeroMorphismsCategoryTheory.Limits.HasKernelCategoryTheory.Limits.HasKernel