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.

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)

Equations

• SemiRingCat.FilteredColimits.semiringObj F j = let_fun this := inferInstance; this

@[inline, reducible]

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

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

• SemiRingCat.FilteredColimits.R F = MonCat.FilteredColimits.colimit (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ SemiRingCatMax MonCatMax))

instance SemiRingCat.FilteredColimits.colimitSemiring {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J SemiRingCatMax) [CategoryTheory.IsFiltered J] : Semiring ↑(SemiRingCat.FilteredColimits.R F)

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• SemiRingCat.FilteredColimits.colimit F = SemiRingCat.of ↑(SemiRingCat.FilteredColimits.R F)

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.

Equations

• One or more equations did not get rendered due to their size.

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 SemiRingCat.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• SemiRingCat.FilteredColimits.forgetPreservesFilteredColimits = CategoryTheory.Limits.compPreservesFilteredColimits (CategoryTheory.forget₂ SemiRingCat MonCat) (CategoryTheory.forget MonCat)

@[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₂ CommSemiRingCat SemiRingCat in the category SemiRingCat. In the following, we will show that this has the structure of a commutative semiring.

Equations

• CommSemiRingCat.FilteredColimits.R F = SemiRingCat.FilteredColimits.colimit (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ CommSemiRingCat SemiRingCat))

instance CommSemiRingCat.FilteredColimits.colimitCommSemiring {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J CommSemiRingCat) : CommSemiring ↑(CommSemiRingCat.FilteredColimits.R F)

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• CommSemiRingCat.FilteredColimits.colimit F = CommSemiRingCat.of ↑(CommSemiRingCat.FilteredColimits.R F)

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.

Equations

• One or more equations did not get rendered due to their size.

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 CommSemiRingCat.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

@[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₂ RingCat SemiRingCat in the category SemiRingCat. In the following, we will show that this has the structure of a ring.

Equations

• RingCat.FilteredColimits.R F = SemiRingCat.FilteredColimits.colimit (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ RingCat SemiRingCat))

instance RingCat.FilteredColimits.colimitRing {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J RingCat) : Ring ↑(RingCat.FilteredColimits.R F)

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• RingCat.FilteredColimits.colimit F = RingCat.of ↑(RingCat.FilteredColimits.R F)

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• RingCat.FilteredColimits.forgetPreservesFilteredColimits = CategoryTheory.Limits.compPreservesFilteredColimits (CategoryTheory.forget₂ RingCat SemiRingCat) (CategoryTheory.forget SemiRingCat)

@[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₂ CommRingCat RingCat in the category RingCat. In the following, we will show that this has the structure of a commutative ring.

Equations

• CommRingCat.FilteredColimits.R F = RingCat.FilteredColimits.colimit (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ CommRingCat RingCat))

instance CommRingCat.FilteredColimits.colimitCommRing {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J CommRingCat) : CommRing ↑(CommRingCat.FilteredColimits.R F)

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• CommRingCat.FilteredColimits.colimit F = CommRingCat.of ↑(CommRingCat.FilteredColimits.R F)

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.

Equations

• One or more equations did not get rendered due to their size.

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 CommRingCat.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• CommRingCat.FilteredColimits.forgetPreservesFilteredColimits = CategoryTheory.Limits.compPreservesFilteredColimits (CategoryTheory.forget₂ CommRingCat RingCat) (CategoryTheory.forget RingCat)