Theorems · Definition · category theory
CommRingCat.Under.equalizerForkIsLimit
{R : CommRingCat} →
{A B : CategoryTheory.Under R} → (f g : A ⟶ B) → CategoryTheory.Limits.IsLimit (CommRingCat.Under.equalizerFork f g)The canonical fork on f g : A ⟶ B is limiting.
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 81 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites14
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Quiver.Homstatement and proof · cited by 32,603
- CommRingCatstatement and proof · cited by 2,333
- CategoryTheory.Limits.WalkingParallelPairstatement · cited by 781
- CategoryTheory.Limits.parallelPairstatement · cited by 766
- CategoryTheory.Limits.IsLimitstatement · cited by 664
- CategoryTheory.Understatement and proof · cited by 276
- Equiv.invFunproof · cited by 163
- CategoryTheory.Under.forgetproof · cited by 90
- CategoryTheory.Under.Hom.rightproof · cited by 67
- CategoryTheory.Limits.isLimitOfReflectsproof · cited by 18
- CategoryTheory.Limits.isLimitMapConeForkEquivproof · cited by 3
- CommRingCat.Under.equalizerForkstatement · cited by 3
Cited by3
Results whose statement or proof uses this declaration.
- CommRingCat.Under.equalizerFork'IsLimitproof · cited by 0
- RingHom.HasEqualizers.isClosedUnderLimitsOfShapeproof · cited by 0