Theorems · Definition · commutative algebra
CommRingCat.pushoutCoconeIsColimit
(R A B : Type u) →
[inst : CommRing R] →
[inst_1 : CommRing A] →
[inst_2 : CommRing B] →
[inst_3 : Algebra R A] →
[inst_4 : Algebra R B] → CategoryTheory.Limits.IsColimit (CommRingCat.pushoutCocone R A B)Verify that the pushout_cocone is indeed the colimit.
- Cited by
- 5 results in Mathlib
- Foundations
- Depth 84 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites21
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CommRingstatement and proof · cited by 17,173
- Algebrastatement and proof · cited by 11,388
- RingHomproof · cited by 10,189
- Algebra.algebraMapstatement and proof · cited by 4,706
- AlgHomproof · cited by 3,236
- CommRingCatstatement · cited by 2,333
- CategoryTheory.Limits.Cocone.ptproof · cited by 1,354
- CategoryTheory.Limits.WalkingPairstatement · cited by 1,319
- CommRingCat.carrierproof · cited by 1,096
- CategoryTheory.Limits.IsColimitstatement · cited by 773
- AlgHom.toRingHomproof · cited by 490
- CommRingCat.Hom.homproof · cited by 432
Cited by6
Results whose statement or proof uses this declaration.
- AlgebraicGeometry.pullbackSpecIsoproof · cited by 26
- CommRingCat.isPushout_tensorProductproof · cited by 7
- AlgebraicGeometry.pullbackSpecIso_inv_fstproof · cited by 7
- AlgebraicGeometry.pullbackSpecIso_inv_sndproof · cited by 6
- RingHom.IsStableUnderBaseChange.pushout_inlproof · cited by 1
- CommRingCat.nontrivial_of_isPushout_of_isFieldproof · cited by 0