Theorems · Definition · category theory
CommAlgCat.binaryCofanIsColimit
{R : Type u} → [inst : CommRing R] → (A B : CommAlgCat R) → CategoryTheory.Limits.IsColimit (A.binaryCofan B)Verify that the pushout cocone is indeed the colimit.
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 83 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CommRing
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites16
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Quiver.Homproof · cited by 32,603
- CategoryTheory.CategoryStruct.compproof · cited by 17,999
- CommRingstatement and proof · cited by 17,173
- CategoryTheory.Discretestatement · cited by 2,447
- CategoryTheory.Limits.Cocone.ptproof · cited by 1,354
- CategoryTheory.Limits.WalkingPairstatement · cited by 1,319
- CategoryTheory.Limits.IsColimitstatement · cited by 773
- CategoryTheory.Limits.pairstatement · cited by 536
- CommAlgCatstatement and proof · cited by 96
- CategoryTheory.Limits.BinaryCofan.inrproof · cited by 51
- CategoryTheory.Limits.BinaryCofan.inlproof · cited by 51
- Algebra.TensorProduct.liftproof · cited by 46
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.