Constructions of (co)limits in CommRingCat
#
In this file we provide the explicit (co)cones for various (co)limits in CommRingCat
, including
- tensor product is the pushout
Z
is the initial object0
is the strict terminal object- cartesian product is the product
RingHom.eqLocus
is the equalizer
The explicit cocone with tensor products as the fibered product in CommRingCat
.
Instances For
Verify that the pushout_cocone
is indeed the colimit.
Instances For
The trivial ring is the (strict) terminal object of CommRingCat
.
Instances For
ℤ
is the initial object of CommRingCat
.
Instances For
The product in CommRingCat
is the cartesian product. This is the binary fan.
Instances For
The product in CommRingCat
is the cartesian product.
Instances For
The equalizer in CommRingCat
is the equalizer as sets. This is the equalizer fork.
Instances For
The equalizer in CommRingCat
is the equalizer as sets.
Instances For
In the category of CommRingCat
, the pullback of f : A ⟶ C
and g : B ⟶ C
is the eqLocus
of the two maps A × B ⟶ C
. This is the constructed pullback cone.
Instances For
The constructed pullback cone is indeed the limit.