# Documentation

Mathlib.Algebra.Category.Ring.Constructions

# 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 object
• 0 is the strict terminal object
• cartesian product is the product
• RingHom.eqLocus is the equalizer
def CommRingCat.pushoutCocone {R : CommRingCat} {A : CommRingCat} {B : CommRingCat} (f : R A) (g : R B) :

The explicit cocone with tensor products as the fibered product in CommRingCat.

Instances For
@[simp]
theorem CommRingCat.pushoutCocone_inl {R : CommRingCat} {A : CommRingCat} {B : CommRingCat} (f : R A) (g : R B) :
= Algebra.TensorProduct.includeLeftRingHom
@[simp]
theorem CommRingCat.pushoutCocone_inr {R : CommRingCat} {A : CommRingCat} {B : CommRingCat} (f : R A) (g : R B) :
= Algebra.TensorProduct.includeRight
@[simp]
theorem CommRingCat.pushoutCocone_pt {R : CommRingCat} {A : CommRingCat} {B : CommRingCat} (f : R A) (g : R B) :
().pt = CommRingCat.of (TensorProduct R A B)
def CommRingCat.pushoutCoconeIsColimit {R : CommRingCat} {A : CommRingCat} {B : CommRingCat} (f : R A) (g : R B) :

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
@[simp]
theorem CommRingCat.prodFan_pt (A : CommRingCat) (B : CommRingCat) :
().pt = CommRingCat.of (A × B)

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
def CommRingCat.equalizerFork {A : CommRingCat} {B : CommRingCat} (f : A B) (g : A B) :

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

Instances For
def CommRingCat.equalizerForkIsLimit {A : CommRingCat} {B : CommRingCat} (f : A B) (g : A B) :

The equalizer in CommRingCat is the equalizer as sets.

Instances For
def CommRingCat.pullbackCone {A : CommRingCat} {B : CommRingCat} {C : CommRingCat} (f : A C) (g : B C) :

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
def CommRingCat.pullbackConeIsLimit {A : CommRingCat} {B : CommRingCat} {C : CommRingCat} (f : A C) (g : B C) :

The constructed pullback cone is indeed the limit.

Instances For