Theorems · Definition · category theory

CategoryTheory.Limits.kernel

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} → (f : X ⟶ Y) → [CategoryTheory.Limits.HasKernel f] → C

The kernel of a morphism, expressed as the equalizer with the 0 morphism.

Defined in: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Cited by: 272 results in Mathlib
Foundations: Depth 21 from the axioms, rests on 97 definitions · uses propext, Classical.choice
Assumes: CategoryTheory.Category CategoryTheory.Limits.HasZeroMorphisms CategoryTheory.Limits.HasKernel

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites5

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

CategoryTheory.Categorystatement and proof · cited by 32,673
Quiver.Homstatement and proof · cited by 32,603
CategoryTheory.Limits.HasZeroMorphismsstatement and proof · cited by 3,275
CategoryTheory.Limits.HasKernelstatement and proof · cited by 169
CategoryTheory.Limits.equalizerproof · cited by 60

Cited by369

Results whose statement or proof uses this declaration.

CategoryTheory.Limits.kernel.ιstatement · cited by 214
CategoryTheory.Abelian.SpectralObject.cyclesproof · cited by 103
CategoryTheory.Limits.kernel.liftstatement · cited by 64
CategoryTheory.Abelian.imageproof · cited by 57
CategoryTheory.Limits.kernel.lift_ιstatement · cited by 55
CategoryTheory.Limits.kernel.conditionstatement · cited by 52
CategoryTheory.Abelian.coimagestatement · cited by 44
CategoryTheory.Limits.kernel.mapstatement · cited by 32
CategoryTheory.Limits.kernelIsKernelstatement · cited by 24
CategoryTheory.Limits.kernelSubobjectIsostatement · cited by 20
CategoryTheory.Abelian.coimage.πstatement · cited by 19
CategoryTheory.Abelian.coimageImageComparisonstatement · cited by 18

Showing the 200 most cited of 369.