mathlib documentation

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.

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.

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.

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.

The bundled ring giving the filtered colimit of a diagram.

Equations

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.

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

Equations