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 SemiRingCat.FilteredColimits.semiringObj {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J SemiRingCatMax) (j : J) : Semiring ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ SemiRingCatMax MonCat)) (CategoryTheory.forget MonCat)).obj j)

@[inline, reducible]

abbrev SemiRingCat.FilteredColimits.R {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J SemiRingCatMax) [CategoryTheory.IsFiltered J] : MonCat

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 SemiRingCat.FilteredColimits.colimitSemiring {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J SemiRingCatMax) [CategoryTheory.IsFiltered J] : Semiring ↑(SemiRingCat.FilteredColimits.R F)

def SemiRingCat.FilteredColimits.colimit {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J SemiRingCatMax) [CategoryTheory.IsFiltered J] : SemiRingCatMax

The bundled semiring giving the filtered colimit of a diagram.

def SemiRingCat.FilteredColimits.colimitCocone {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J SemiRingCatMax) [CategoryTheory.IsFiltered J] : CategoryTheory.Limits.Cocone F

The cocone over the proposed colimit semiring.

def SemiRingCat.FilteredColimits.colimitCoconeIsColimit {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J SemiRingCatMax) [CategoryTheory.IsFiltered J] : CategoryTheory.Limits.IsColimit (SemiRingCat.FilteredColimits.colimitCocone F)

The proposed colimit cocone is a colimit in SemiRing.

instance SemiRingCat.FilteredColimits.forget₂MonPreservesFilteredColimits : CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget₂ SemiRingCat MonCat)

instance SemiRingCat.FilteredColimits.forgetPreservesFilteredColimits : CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget SemiRingCat)

@[inline, reducible]

abbrev CommSemiRingCat.FilteredColimits.R {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J CommSemiRingCat) : SemiRingCatMax

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 CommSemiRingCat.FilteredColimits.colimitCommSemiring {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J CommSemiRingCat) : CommSemiring ↑(CommSemiRingCat.FilteredColimits.R F)

def CommSemiRingCat.FilteredColimits.colimit {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J CommSemiRingCat) : CommSemiRingCat

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

def CommSemiRingCat.FilteredColimits.colimitCocone {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J CommSemiRingCat) : CategoryTheory.Limits.Cocone F

The cocone over the proposed colimit commutative semiring.

def CommSemiRingCat.FilteredColimits.colimitCoconeIsColimit {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J CommSemiRingCat) : CategoryTheory.Limits.IsColimit (CommSemiRingCat.FilteredColimits.colimitCocone F)

The proposed colimit cocone is a colimit in CommSemiRing.

instance CommSemiRingCat.FilteredColimits.forget₂SemiRingPreservesFilteredColimits : CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget₂ CommSemiRingCat SemiRingCat)

instance CommSemiRingCat.FilteredColimits.forgetPreservesFilteredColimits : CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget CommSemiRingCat)

@[inline, reducible]

abbrev RingCat.FilteredColimits.R {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J RingCat) : SemiRingCat

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 RingCat.FilteredColimits.colimitRing {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J RingCat) : Ring ↑(RingCat.FilteredColimits.R F)

def RingCat.FilteredColimits.colimit {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J RingCat) : RingCat

The bundled ring giving the filtered colimit of a diagram.

def RingCat.FilteredColimits.colimitCocone {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J RingCat) : CategoryTheory.Limits.Cocone F

The cocone over the proposed colimit ring.

def RingCat.FilteredColimits.colimitCoconeIsColimit {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J RingCat) : CategoryTheory.Limits.IsColimit (RingCat.FilteredColimits.colimitCocone F)

The proposed colimit cocone is a colimit in Ring.

instance RingCat.FilteredColimits.forget₂SemiRingPreservesFilteredColimits : CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget₂ RingCat SemiRingCat)

instance RingCat.FilteredColimits.forgetPreservesFilteredColimits : CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget RingCat)

@[inline, reducible]

abbrev CommRingCat.FilteredColimits.R {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J CommRingCat) : RingCat

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 CommRingCat.FilteredColimits.colimitCommRing {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J CommRingCat) : CommRing ↑(CommRingCat.FilteredColimits.R F)

def CommRingCat.FilteredColimits.colimit {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J CommRingCat) : CommRingCat

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

def CommRingCat.FilteredColimits.colimitCocone {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J CommRingCat) : CategoryTheory.Limits.Cocone F

The cocone over the proposed colimit commutative ring.

def CommRingCat.FilteredColimits.colimitCoconeIsColimit {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J CommRingCat) : CategoryTheory.Limits.IsColimit (CommRingCat.FilteredColimits.colimitCocone F)

The proposed colimit cocone is a colimit in CommRing.

instance CommRingCat.FilteredColimits.forget₂RingPreservesFilteredColimits : CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget₂ CommRingCat RingCat)

instance CommRingCat.FilteredColimits.forgetPreservesFilteredColimits : CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget CommRingCat)