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
.
Equations
- SemiRingCat.FilteredColimits.semiringObj F j = let_fun this := inferInstance; this
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.
Equations
Instances For
Equations
- One or more equations did not get rendered due to their size.
The bundled semiring giving the filtered colimit of a diagram.
Equations
Instances For
The cocone over the proposed colimit semiring.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The proposed colimit cocone is a colimit in SemiRing
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
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.
Equations
Instances For
Equations
- One or more equations did not get rendered due to their size.
The bundled commutative semiring giving the filtered colimit of a diagram.
Equations
Instances For
The cocone over the proposed colimit commutative semiring.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The proposed colimit cocone is a colimit in CommSemiRing
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
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.
Equations
Instances For
Equations
- One or more equations did not get rendered due to their size.
The bundled ring giving the filtered colimit of a diagram.
Equations
Instances For
The cocone over the proposed colimit ring.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The proposed colimit cocone is a colimit in Ring
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
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.
Equations
Instances For
Equations
- One or more equations did not get rendered due to their size.
The bundled commutative ring giving the filtered colimit of a diagram.
Equations
Instances For
The cocone over the proposed colimit commutative ring.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The proposed colimit cocone is a colimit in CommRing
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.