# mathlib3documentation

algebra.category.Ring.limits

# The category of (commutative) rings has all limits #

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

Further, these limits are preserved by the forgetful functor --- that is, the underlying types are just the limits in the category of types.

Some definitions may be extremely slow to elaborate, when the target type to be constructed is complicated and when the type of the term given in the definition is also complicated and does not obviously match the target type. In this case, instead of just giving the term, prefixing it with by apply may speed up things considerably as the types are not elaborated in the same order.

@[protected, instance]
def SemiRing.semiring_obj {J : Type v} (F : J SemiRing) (j : J) :
Equations
def SemiRing.sections_subsemiring {J : Type v} (F : J SemiRing) :
subsemiring (Π (j : J), (F.obj j))

The flat sections of a functor into SemiRing form a subsemiring of all sections.

Equations
@[protected, instance]
Equations
def SemiRing.limit_π_ring_hom {J : Type v} (F : J SemiRing) (j : J) :

limit.π (F ⋙ forget SemiRing) j as a ring_hom.

Equations

Construction of a limit cone in SemiRing. (Internal use only; use the limits API.)

Equations

Witness that the limit cone in SemiRing is a limit cone. (Internal use only; use the limits API.)

Equations
@[protected, instance, irreducible]

The category of rings has all limits.

@[protected, instance]

An auxiliary declaration to speed up typechecking.

Equations
@[protected, instance]

The forgetful functor from semirings to additive commutative monoids preserves all limits.

Equations
@[protected, instance]
Equations

An auxiliary declaration to speed up typechecking.

Equations
@[protected, instance]

The forgetful functor from semirings to monoids preserves all limits.

Equations
@[protected, instance]
Equations
@[protected, instance]

The forgetful functor from semirings to types preserves all limits.

Equations
@[protected, instance]
Equations
@[protected, instance]
def CommSemiRing.comm_semiring_obj {J : Type v} (F : J CommSemiRing) (j : J) :
Equations
@[protected, instance]
Equations
@[protected, instance]

We show that the forgetful functor CommSemiRingSemiRing creates limits.

All we need to do is notice that the limit point has a comm_semiring instance available, and then reuse the existing limit.

Equations
noncomputable def CommSemiRing.limit_cone {J : Type v} (F : J CommSemiRing) :

A choice of limit cone for a functor into CommSemiRing. (Generally, you'll just want to use limit F.)

Equations
noncomputable def CommSemiRing.limit_cone_is_limit {J : Type v} (F : J CommSemiRing) :

The chosen cone is a limit cone. (Generally, you'll just want to use limit.cone F.)

Equations
@[protected, instance, irreducible]

The category of rings has all limits.

@[protected, instance]
@[protected, instance]

The forgetful functor from rings to semirings preserves all limits.

Equations
@[protected, instance]
Equations
@[protected, instance]

The forgetful functor from rings to types preserves all limits. (That is, the underlying types could have been computed instead as limits in the category of types.)

Equations
@[protected, instance]
Equations
@[protected, instance]
def Ring.ring_obj {J : Type v} (F : J Ring) (j : J) :
ring .obj j)
Equations
def Ring.sections_subring {J : Type v} (F : J Ring) :
subring (Π (j : J), (F.obj j))

The flat sections of a functor into Ring form a subring of all sections.

Equations
@[protected, instance]
def Ring.limit_ring {J : Type v} (F : J Ring) :
Equations
@[protected, instance]

We show that the forgetful functor CommRingRing creates limits.

All we need to do is notice that the limit point has a ring instance available, and then reuse the existing limit.

Equations
noncomputable def Ring.limit_cone {J : Type v} (F : J Ring) :

A choice of limit cone for a functor into Ring. (Generally, you'll just want to use limit F.)

Equations
noncomputable def Ring.limit_cone_is_limit {J : Type v} (F : J Ring) :

The chosen cone is a limit cone. (Generally, you'll just want to use limit.cone F.)

Equations
@[protected, instance, irreducible]

The category of rings has all limits.

@[protected, instance]
@[protected, instance]

The forgetful functor from rings to semirings preserves all limits.

Equations
@[protected, instance]
Equations
noncomputable def Ring.forget₂_AddCommGroup_preserves_limits_aux {J : Type v} (F : J Ring) :

An auxiliary declaration to speed up typechecking.

Equations
@[protected, instance]

The forgetful functor from rings to additive commutative groups preserves all limits.

Equations
@[protected, instance]
Equations
@[protected, instance]

The forgetful functor from rings to types preserves all limits. (That is, the underlying types could have been computed instead as limits in the category of types.)

Equations
@[protected, instance]
Equations
@[protected, instance]
def CommRing.comm_ring_obj {J : Type v} (F : J CommRing) (j : J) :
Equations
@[protected, instance]
Equations
@[protected, instance]

We show that the forgetful functor CommRingRing creates limits.

All we need to do is notice that the limit point has a comm_ring instance available, and then reuse the existing limit.

Equations
noncomputable def CommRing.limit_cone {J : Type v} (F : J CommRing) :

A choice of limit cone for a functor into CommRing. (Generally, you'll just want to use limit F.)

Equations
noncomputable def CommRing.limit_cone_is_limit {J : Type v} (F : J CommRing) :

The chosen cone is a limit cone. (Generally, you'll just want to use limit.cone F.)

Equations
@[protected, instance, irreducible]

The category of commutative rings has all limits.

@[protected, instance]
@[protected, instance]

The forgetful functor from commutative rings to rings preserves all limits. (That is, the underlying rings could have been computed instead as limits in the category of rings.)

Equations
@[protected, instance]
Equations

An auxiliary declaration to speed up typechecking.

Equations
@[protected, instance]

The forgetful functor from commutative rings to commutative semirings preserves all limits. (That is, the underlying commutative semirings could have been computed instead as limits in the category of commutative semirings.)

Equations
@[protected, instance]
Equations
@[protected, instance]

The forgetful functor from commutative rings to types preserves all limits. (That is, the underlying types could have been computed instead as limits in the category of types.)

Equations
@[protected, instance]
Equations