Theorems · Definition · category theory
CategoryTheory.Limits.equalizer
{C : Type u} →
{X Y : C} → [inst : CategoryTheory.Category.{v, u} C] → (f g : X ⟶ Y) → [CategoryTheory.Limits.HasEqualizer f g] → CIf an equalizer of f and g exists, we can access an arbitrary choice of such by
saying equalizer f g.
- Cited by
- 60 results in Mathlib
- Foundations
- Depth 20 from the axioms · uses propext, Classical.choice
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.parallelPairproof · cited by 766
- CategoryTheory.Limits.limitproof · cited by 346
- CategoryTheory.Limits.HasEqualizerstatement and proof · cited by 47
Cited by78
Results whose statement or proof uses this declaration.
- CategoryTheory.Limits.kernelproof · cited by 272
- CategoryTheory.Limits.equalizer.ιstatement · cited by 64
- CategoryTheory.Limits.equalizer.hom_extstatement and proof · cited by 27
- CategoryTheory.Limits.equalizer.liftstatement · cited by 19
- CategoryTheory.Limits.equalizer.conditionstatement · cited by 16
- CategoryTheory.Limits.equalizerPullbackMapIsostatement · cited by 10
- CategoryTheory.Limits.Types.equalizerIsostatement · cited by 7
- CategoryTheory.PreGaloisCategory.evaluation_injective_of_isConnectedproof · cited by 6
- CategoryTheory.Limits.eq_of_epi_equalizerstatement · cited by 6
- CategoryTheory.Limits.equalizerComparisonstatement · cited by 6
- CategoryTheory.Limits.equalizerSubobjectIsostatement · cited by 5
- CategoryTheory.Limits.image.extproof · cited by 4