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 ⥤ SemiRingCatMax
.
We show that the colimit of F ⋙ forget₂ SemiRingCatMax MonCat
(in MonCat
)
carries the structure of a semiring, thereby showing that the forgetful functor
forget₂ SemiRingCatMax MonCat
preserves filtered colimits.
In particular, this implies that forget SemiRingCatMax
preserves filtered colimits.
Similarly for CommSemiRingCat
, RingCat
and CommRingCat
.
Equations
- SemiRingCat.FilteredColimits.semiringObj F j = inferInstance
The colimit of F ⋙ forget₂ SemiRingCat MonCat
in the category MonCat
.
In the following, we will show that this has the structure of a semiring.
Equations
Instances For
Equations
- SemiRingCat.FilteredColimits.colimitSemiring F = Semiring.mk ⋯ ⋯ ⋯ ⋯ Monoid.npow ⋯ ⋯
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 SemiRingCat
.
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₂ CommSemiRingCat SemiRingCat
in the category SemiRingCat
.
In the following, we will show that this has the structure of a commutative semiring.
Equations
Instances For
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 CommSemiRingCat
.
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₂ RingCat SemiRingCat
in the category SemiRingCat
.
In the following, we will show that this has the structure of a ring.
Equations
Instances For
Equations
- RingCat.FilteredColimits.colimitRing F = Ring.mk ⋯ SubNegMonoid.zsmul ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
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₂ CommRingCat RingCat
in the category RingCat
.
In the following, we will show that this has the structure of a commutative ring.
Equations
Instances For
Equations
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 CommRingCat
.
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.