Theorems · Definition · commutative algebra
CommRingCat.pullbackConeIsLimit
{A B C : CommRingCat} → (f : A ⟶ C) → (g : B ⟶ C) → CategoryTheory.Limits.IsLimit (CommRingCat.pullbackCone f g)The constructed pullback cone is indeed the limit.
- Cited by
- 4 results in Mathlib
- Foundations
- Depth 33 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites20
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.WalkingPairstatement · cited by 1,319
- CommRingCat.carrierproof · cited by 1,096
- RingHom.compproof · cited by 899
- CategoryTheory.Limits.IsLimitstatement · cited by 664
- CategoryTheory.Limits.WalkingCospanstatement · cited by 496
- CategoryTheory.Limits.cospanstatement · cited by 467
- CommRingCat.Hom.homproof · cited by 432
- CommRingCat.ofHomproof · cited by 259
- CategoryTheory.Limits.PullbackConeproof · cited by 136
- CategoryTheory.Limits.PullbackCone.fstproof · cited by 118
Cited by5
Results whose statement or proof uses this declaration.
- TopCat.Sheaf.objSupIsoProdEqLocusproof · cited by 6
- TopCat.Sheaf.objSupIsoProdEqLocus_inv_fstproof · cited by 1
- TopCat.Sheaf.objSupIsoProdEqLocus_inv_sndproof · cited by 1
- TopCat.Sheaf.objSupIsoProdEqLocus_hom_fstproof · cited by 0
- TopCat.Sheaf.objSupIsoProdEqLocus_hom_sndproof · cited by 0