# 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
• arbitrary direct product of a family of rings is the product object (Pi object)
• RingHom.eqLocus is the equalizer
noncomputable 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.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CommRingCat.pushoutCocone_inl {R : CommRingCat} {A : CommRingCat} {B : CommRingCat} (f : R A) (g : R B) :
.inl = Algebra.TensorProduct.includeLeftRingHom
@[simp]
theorem CommRingCat.pushoutCocone_inr {R : CommRingCat} {A : CommRingCat} {B : CommRingCat} (f : R A) (g : R B) :
.inr = Algebra.TensorProduct.includeRight.toRingHom
@[simp]
theorem CommRingCat.pushoutCocone_pt {R : CommRingCat} {A : CommRingCat} {B : CommRingCat} (f : R A) (g : R B) :
.pt = CommRingCat.of (TensorProduct R A B)
noncomputable def CommRingCat.pushoutCoconeIsColimit {R : CommRingCat} {A : CommRingCat} {B : CommRingCat} (f : R A) (g : R B) :

Verify that the pushout_cocone is indeed the colimit.

Equations
• One or more equations did not get rendered due to their size.
Instances For
noncomputable def CommRingCat.punitIsTerminal :

The trivial ring is the (strict) terminal object of CommRingCat.

Equations
Instances For
noncomputable def CommRingCat.zIsInitial :

ℤ is the initial object of CommRingCat.

Equations
Instances For
noncomputable def CommRingCat.prodFan (A : CommRingCat) (B : CommRingCat) :

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

Equations
• A.prodFan B =
Instances For
@[simp]
theorem CommRingCat.prodFan_pt (A : CommRingCat) (B : CommRingCat) :
(A.prodFan B).pt = CommRingCat.of (A × B)

The product in CommRingCat is the cartesian product.

Equations
• One or more equations did not get rendered due to their size.
Instances For
noncomputable def CommRingCat.piFan {ι : Type u} (R : ) :

The categorical product of rings is the cartesian product of rings. This is its Fan.

Equations
Instances For
@[simp]
theorem CommRingCat.piFan_pt {ι : Type u} (R : ) :
.pt = CommRingCat.of ((i : ι) → (R i))
noncomputable def CommRingCat.piFanIsLimit {ι : Type u} (R : ) :

The categorical product of rings is the cartesian product of rings.

Equations
• One or more equations did not get rendered due to their size.
Instances For
noncomputable def CommRingCat.piIsoPi {ι : Type u} (R : ) :
R CommRingCat.of ((i : ι) → (R i))

The categorical product and the usual product agrees

Equations
Instances For
noncomputable def RingEquiv.piEquivPi {ι : Type u} (R : ιType u) [(i : ι) → CommRing (R i)] :
( fun (i : ι) => CommRingCat.of (R i)) ≃+* ((i : ι) → R i)

The categorical product and the usual product agrees

Equations
Instances For
noncomputable 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.

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

The equalizer in CommRingCat is the equalizer as sets.

Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
• =
Equations
• =
noncomputable 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.

Equations
• One or more equations did not get rendered due to their size.
Instances For
noncomputable def CommRingCat.pullbackConeIsLimit {A : CommRingCat} {B : CommRingCat} {C : CommRingCat} (f : A C) (g : B C) :

The constructed pullback cone is indeed the limit.

Equations
• One or more equations did not get rendered due to their size.
Instances For