# mathlib3documentation

algebra.category.Ring.constructions

# Constructions of (co)limits in CommRing #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

• tensor product is the pushout
• Z is the initial object
• 0 is the strict terminal object
• cartesian product is the product
• ring_hom.eq_locus is the equalizer
def CommRing.pushout_cocone {R A B : CommRing} (f : R A) (g : R B) :

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

Equations
• = let _inst : A := , _inst_1 : B := in
@[simp]
theorem CommRing.pushout_cocone_inl {R A B : CommRing} (f : R A) (g : R B) :
.inl = let _inst : A := , _inst_1 : B := in algebra.tensor_product.include_left.to_ring_hom
@[simp]
theorem CommRing.pushout_cocone_inr {R A B : CommRing} (f : R A) (g : R B) :
.inr = let _inst : A := , _inst_1 : B := in algebra.tensor_product.include_right.to_ring_hom
@[simp]
theorem CommRing.pushout_cocone_X {R A B : CommRing} (f : R A) (g : R B) :
.X = let _inst : A := , _inst_1 : B := in CommRing.of A B)
def CommRing.pushout_cocone_is_colimit {R A B : CommRing} (f : R A) (g : R B) :

Verify that the pushout_cocone is indeed the colimit.

Equations

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

Equations
@[protected, instance]

ℤ is the initial object of CommRing.

Equations
def CommRing.prod_fan (A B : CommRing) :

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

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

The product in CommRing is the cartesian product.

Equations
def CommRing.equalizer_fork {A B : CommRing} (f g : A B) :

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

Equations
def CommRing.equalizer_fork_is_limit {A B : CommRing} (f g : A B) :

The equalizer in CommRing is the equalizer as sets.

Equations
• = (λ (s : , _, _⟩)
@[protected, instance]
def CommRing.ι.is_local_ring_hom {A B : CommRing} (f g : A B) :
@[protected, instance]
@[protected, instance]
def CommRing.pullback_cone {A B C : CommRing} (f : A C) (g : B C) :

In the category of CommRing, the pullback of f : A ⟶ C and g : B ⟶ C is the eq_locus of the two maps A × B ⟶ C. This is the constructed pullback cone.

Equations
def CommRing.pullback_cone_is_limit {A B C : CommRing} (f : A C) (g : B C) :

The constructed pullback cone is indeed the limit.

Equations