# mathlibdocumentation

algebra.category.CommRing.filtered_colimits

# The forgetful functor from (commutative) (semi-) rings preserves filtered colimits. #

Forgetful functors from algebraic categories usually don't preserve colimits. However, they tend to preserve filtered colimits.

In this file, we start with a small filtered category J and a functor F : J ⥤ SemiRing. We show that the colimit of F ⋙ forget₂ SemiRing Mon (in Mon) carries the structure of a semiring, thereby showing that the forgetful functor forget₂ SemiRing Mon preserves filtered colimits. In particular, this implies that forget SemiRing preserves filtered colimits. Similarly for CommSemiRing, Ring and CommRing.

@[instance]
def SemiRing.filtered_colimits.semiring_obj {J : Type v} (F : J SemiRing) (j : J) :
Equations
def SemiRing.filtered_colimits.R {J : Type v} (F : J SemiRing)  :

The colimit of F ⋙ forget₂ SemiRing Mon in the category Mon. In the following, we will show that this has the structure of a semiring.

@[instance]
Equations

The bundled semiring giving the filtered colimit of a diagram.

Equations

The cocone over the proposed colimit semiring.

Equations

The proposed colimit cocone is a colimit in SemiRing.

Equations
@[instance]
Equations
@[instance]
Equations

The colimit of F ⋙ forget₂ CommSemiRing SemiRing in the category SemiRing. In the following, we will show that this has the structure of a commutative semiring.

@[instance]
Equations

The bundled commutative semiring giving the filtered colimit of a diagram.

Equations

The cocone over the proposed colimit commutative semiring.

Equations

The proposed colimit cocone is a colimit in CommSemiRing.

Equations
@[instance]
Equations
def Ring.filtered_colimits.R {J : Type v} (F : J Ring) :

The colimit of F ⋙ forget₂ Ring SemiRing in the category SemiRing. In the following, we will show that this has the structure of a ring.

@[instance]
def Ring.filtered_colimits.colimit_ring {J : Type v} (F : J Ring) :
Equations
def Ring.filtered_colimits.colimit {J : Type v} (F : J Ring) :

The bundled ring giving the filtered colimit of a diagram.

Equations
def Ring.filtered_colimits.colimit_cocone {J : Type v} (F : J Ring) :

The cocone over the proposed colimit ring.

Equations

The proposed colimit cocone is a colimit in Ring.

Equations
@[instance]
Equations
@[instance]
Equations
def CommRing.filtered_colimits.R {J : Type v} (F : J CommRing) :

The colimit of F ⋙ forget₂ CommRing Ring in the category Ring. In the following, we will show that this has the structure of a commutative ring.

@[instance]
Equations

The bundled commutative ring giving the filtered colimit of a diagram.

Equations

The cocone over the proposed colimit commutative ring.

Equations

The proposed colimit cocone is a colimit in CommRing.

Equations
@[instance]
Equations
@[instance]
Equations