Theorems · Definition · category theory
CategoryTheory.Limits.multiequalizer
{C : Type u} →
[inst : CategoryTheory.Category.{v, u} C] →
{J : CategoryTheory.Limits.MulticospanShape} →
(I : CategoryTheory.Limits.MulticospanIndex J C) → [CategoryTheory.Limits.HasMultiequalizer I] → CThe multiequalizer of I : MulticospanIndex J C.
- Cited by
- 33 results in Mathlib
- Foundations
- Depth 18 from the axioms · uses propext, Classical.choice
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
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.limitproof · cited by 346
- CategoryTheory.Limits.MulticospanIndex.multicospanproof · cited by 167
- CategoryTheory.Limits.MulticospanShapestatement and proof · cited by 160
- CategoryTheory.Limits.MulticospanIndexstatement and proof · cited by 101
- CategoryTheory.Limits.HasMultiequalizerstatement and proof · cited by 88
Cited by43
Results whose statement or proof uses this declaration.
- CategoryTheory.Limits.Multiequalizer.ιstatement · cited by 37
- CategoryTheory.GrothendieckTopology.diagramproof · cited by 29
- CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjproof · cited by 26
- CategoryTheory.Limits.end_proof · cited by 20
- CategoryTheory.Limits.Multiequalizer.liftstatement · cited by 18
- CategoryTheory.Limits.Multiequalizer.hom_extstatement and proof · cited by 12
- CategoryTheory.Meq.equivstatement · cited by 8
- CategoryTheory.Limits.Multiequalizer.lift_ιstatement · cited by 8
- CategoryTheory.GrothendieckTopology.toPlus_naturalityproof · cited by 6
- CategoryTheory.GrothendieckTopology.Cover.toMultiequalizerstatement · cited by 6
- CategoryTheory.GrothendieckTopology.plusMap_toPlusproof · cited by 5
- CategoryTheory.Meq.equiv_symm_eq_applystatement · cited by 4