Theorems · Definition · category theory
CategoryTheory.Limits.HasMultiequalizer
{C : Type u} →
[inst : CategoryTheory.Category.{v, u} C] →
{J : CategoryTheory.Limits.MulticospanShape} → CategoryTheory.Limits.MulticospanIndex J C → PropFor I : MulticospanIndex J C, we say that it has a multiequalizer if the associated
multicospan has a limit.
- Cited by
- 88 results in Mathlib
- Foundations
- Depth 17 from the axioms · uses propext
- Assumes
- CategoryTheory.Category
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
- CategoryTheory.Limits.HasLimitproof · cited by 226
- CategoryTheory.Limits.MulticospanIndex.multicospanproof · cited by 167
- CategoryTheory.Limits.MulticospanShapestatement and proof · cited by 160
- CategoryTheory.Limits.MulticospanIndexstatement and proof · cited by 101
Cited by127
Results whose statement or proof uses this declaration.
- CategoryTheory.GrothendieckTopology.plusObjstatement and proof · cited by 56
- CategoryTheory.Limits.Multiequalizer.ιstatement and proof · cited by 37
- CategoryTheory.Limits.multiequalizerstatement and proof · cited by 33
- CategoryTheory.GrothendieckTopology.sheafifystatement and proof · cited by 32
- CategoryTheory.GrothendieckTopology.diagramstatement and proof · cited by 29
- CategoryTheory.GrothendieckTopology.toPlusstatement and proof · cited by 28
- CategoryTheory.GrothendieckTopology.plusMapstatement and proof · cited by 26
- CategoryTheory.GrothendieckTopology.toSheafifystatement and proof · cited by 19
- CategoryTheory.Limits.Multiequalizer.liftstatement and proof · cited by 18
- CategoryTheory.Limits.HasEndproof · cited by 14
- CategoryTheory.Limits.Multiequalizer.hom_extstatement and proof · cited by 12
- CategoryTheory.GrothendieckTopology.diagramNatTransstatement and proof · cited by 12