Theorems · Definition · category theory
CategoryTheory.Preadditive.isLimitForkOfKernelFork
{C : Type u} →
[inst : CategoryTheory.Category.{v, u} C] →
[inst_1 : CategoryTheory.Preadditive C] →
{X Y : C} →
{f g : X ⟶ Y} →
{c : CategoryTheory.Limits.KernelFork (f - g)} →
CategoryTheory.Limits.IsLimit c →
CategoryTheory.Limits.IsLimit (CategoryTheory.Preadditive.forkOfKernelFork c)A kernel of f - g is an equalizer of f and g.
- Defined in
- Mathlib.CategoryTheory.Preadditive.Basic
- Cited by
- 4 results in Mathlib
- Foundations
- Depth 32 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
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.Preadditivestatement and proof · cited by 3,309
- CategoryTheory.Limits.WalkingParallelPairstatement · cited by 781
- CategoryTheory.Limits.parallelPairstatement · cited by 766
- CategoryTheory.Limits.IsLimitstatement and proof · cited by 664
- CategoryTheory.Limits.IsLimit.liftproof · cited by 167
- CategoryTheory.Limits.KernelForkstatement and proof · cited by 108
- CategoryTheory.Limits.Forkproof · cited by 85
- CategoryTheory.Preadditive.forkOfKernelForkstatement and proof · cited by 8
- CategoryTheory.Preadditive.kernelForkOfForkproof · cited by 7
- CategoryTheory.Limits.Fork.IsLimit.mk'proof · cited by 1
Cited by5
Results whose statement or proof uses this declaration.
- CategoryTheory.Limits.binaryBiconeOfIsSplitEpiOfKernelproof · cited by 5
- CategoryTheory.Preadditive.hasEqualizer_of_hasKernelproof · cited by 2
- CategoryTheory.Functor.preservesEqualizer_of_preservesKernelsproof · cited by 1
- CategoryTheory.Limits.binaryBiconeOfIsSplitEpiOfKernel_fststatement · cited by 0
- CategoryTheory.Preadditive.isLimitForkOfKernelFork_liftstatement · cited by 0