mathlib documentation

algebra.category.CommRing.pushout

Explicit pushout cocone for CommRing #

In this file we prove that tensor product is indeed the fibered coproduct in CommRing, and provide the explicit pushout cocone.

@[simp]
theorem CommRing.pushout_cocone_X {R A B : CommRing} (f : R A) (g : R B) :

Verify that the pushout_cocone is indeed the colimit.

Equations