mathlib documentation

algebra.category.Ring.constructions

Constructions of (co)limits in CommRing #

In this file we provide the explicit (co)cones for various (co)limits in CommRing, including

@[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

The product in CommRing is the cartesian product. This is the binary fan.

Equations
@[simp]
theorem CommRing.prod_fan_X (A B : CommRing) :

The equalizer in CommRing is the equalizer as sets. This is the equalizer fork.

Equations
@[protected, instance]