Theorems · Theorem · category theory

CategoryTheory.Limits.KernelFork.map_condition

∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  {X Y : C} {f : X ⟶ Y} (c : CategoryTheory.Limits.KernelFork f) (G : CategoryTheory.Functor C D)
  [G.PreservesZeroMorphisms], CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.Fork.ι c)) (G.map f) = 0

Defined in

Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasZeroMorphismsCategoryTheory.CategoryCategoryTheory.Limits.HasZeroMorphismsCategoryTheory.Functor.PreservesZeroMorphisms