# mathlibdocumentation

algebra.category.CommRing.limits

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

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

@[protected, instance]
def SemiRing.semiring_obj {J : Type u} (F : J SemiRing) (j : J) :
Equations
def SemiRing.sections_subsemiring {J : Type u} (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]
def SemiRing.limit_semiring {J : Type u} (F : J SemiRing) :
Equations
def SemiRing.limit_π_ring_hom {J : Type u} (F : J SemiRing) (j : J) :

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

Equations
def SemiRing.has_limits.limit_cone {J : Type u} (F : J SemiRing) :

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]

The category of rings has all limits.

noncomputable def SemiRing.forget₂_AddCommMon_preserves_limits_aux {J : Type u} (F : J SemiRing) :

An auxiliary declaration to speed up typechecking.

Equations
@[protected, instance]

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

Equations

An auxiliary declaration to speed up typechecking.

Equations
@[protected, instance]

The forgetful functor from semirings to monoids preserves all limits.

Equations
@[protected, instance]

The forgetful functor from semirings to types preserves all limits.

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

We show that the forgetful functor CommSemiRing ⥤ SemiRing 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 u} (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 u} (F : J CommSemiRing) :

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

Equations
@[protected, instance]

The category of rings has all limits.

@[protected, instance]

The forgetful functor from rings to semirings preserves all limits.

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]
def Ring.ring_obj {J : Type u} (F : J Ring) (j : J) :
ring .obj j)
Equations
def Ring.sections_subring {J : Type u} (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 u} (F : J Ring) :
Equations
@[protected, instance]
noncomputable def Ring.category_theory.forget₂.category_theory.creates_limit {J : Type u} (F : J Ring) :

We show that the forgetful functor CommRing ⥤ Ring 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 u} (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 u} (F : J Ring) :

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

Equations
@[protected, instance]

The category of rings has all limits.

@[protected, instance]

The forgetful functor from rings to semirings preserves all limits.

Equations
noncomputable def Ring.forget₂_AddCommGroup_preserves_limits_aux {J : Type u} (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]

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]
def CommRing.comm_ring_obj {J : Type u} (F : J CommRing) (j : J) :
Equations
@[protected, instance]
def CommRing.limit_comm_ring {J : Type u} (F : J CommRing) :
Equations
@[protected, instance]

We show that the forgetful functor CommRing ⥤ Ring 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 u} (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 u} (F : J CommRing) :

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

Equations
@[protected, instance]

The category of commutative rings has all limits.

@[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
noncomputable def CommRing.forget₂_CommSemiRing_preserves_limits_aux {J : Type u} (F : J CommRing) :

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]

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