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 ⥤ SemiRingCat. We show that the colimit of F ⋙ forget₂ SemiRingCat MonCat (in MonCat) carries the structure of a semiring, thereby showing that the forgetful functor forget₂ SemiRingCat MonCat preserves filtered colimits. In particular, this implies that forget SemiRingCat preserves filtered colimits. Similarly for CommSemiRingCat, RingCat and CommRingCat.

instance SemiRingCat.FilteredColimits.semiringObj {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J SemiRingCat) (j : J) : Semiring (((F.comp (CategoryTheory.forget₂ SemiRingCat MonCat)).comp (CategoryTheory.forget MonCat)).obj j)

Equations

• SemiRingCat.FilteredColimits.semiringObj F j = inferInstance

@[reducible, inline]

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

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 (F.comp (CategoryTheory.forget₂ SemiRingCat MonCat))

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

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 SemiRingCat) [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.descAddMonoidHom {J : Type v} [CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J SemiRingCat} [CategoryTheory.IsFiltered J] (t : CategoryTheory.Limits.Cocone F) : ↑(R F) →+ ↑t.pt

Auxiliary definition for colimitCoconeIsColimit.

Equations

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

theorem SemiRingCat.FilteredColimits.colimitCoconeIsColimit.descAddMonoidHom_quotMk {J : Type v} [CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J SemiRingCat} [CategoryTheory.IsFiltered J] (t : CategoryTheory.Limits.Cocone F) {j : J} (x : ↑(F.obj j)) : (descAddMonoidHom t) (Quot.mk ((F.comp (CategoryTheory.forget₂ SemiRingCat MonCat)).comp (CategoryTheory.forget MonCat)).ColimitTypeRel ⟨j, x⟩) = (CategoryTheory.ConcreteCategory.hom (t.ι.app j)) x

def SemiRingCat.FilteredColimits.colimitCoconeIsColimit.descMonoidHom {J : Type v} [CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J SemiRingCat} [CategoryTheory.IsFiltered J] (t : CategoryTheory.Limits.Cocone F) : ↑(R F) →* ↑t.pt

Auxiliary definition for colimitCoconeIsColimit.

Equations

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

theorem SemiRingCat.FilteredColimits.colimitCoconeIsColimit.descMonoidHom_quotMk {J : Type v} [CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J SemiRingCat} [CategoryTheory.IsFiltered J] (t : CategoryTheory.Limits.Cocone F) {j : J} (x : ↑(F.obj j)) : (descMonoidHom t) (Quot.mk ((F.comp (CategoryTheory.forget₂ SemiRingCat MonCat)).comp (CategoryTheory.forget MonCat)).ColimitTypeRel ⟨j, x⟩) = (CategoryTheory.ConcreteCategory.hom (t.ι.app j)) x

theorem SemiRingCat.FilteredColimits.colimitCoconeIsColimit.descMonoidHom_apply_eq {J : Type v} [CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J SemiRingCat} [CategoryTheory.IsFiltered J] (t : CategoryTheory.Limits.Cocone F) (x : ↑(R F)) : (descMonoidHom t) x = (descAddMonoidHom t) x

def SemiRingCat.FilteredColimits.colimitCoconeIsColimit {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J SemiRingCat) [CategoryTheory.IsFiltered J] : CategoryTheory.Limits.IsColimit (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₂Mon_preservesFilteredColimits : CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget₂ SemiRingCat MonCat)

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

@[reducible, inline]

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

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 (F.comp (CategoryTheory.forget₂ CommSemiRingCat SemiRingCat))

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

Equations

• CommSemiRingCat.FilteredColimits.colimitCommSemiring F = { toSemiring := (CommSemiRingCat.FilteredColimits.R F).semiring, mul_comm := ⋯ }

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 (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₂SemiRing_preservesFilteredColimits : CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget₂ CommSemiRingCat SemiRingCat)

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

@[reducible, inline]

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 (F.comp (CategoryTheory.forget₂ RingCat SemiRingCat))

instance RingCat.FilteredColimits.colimitRing {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J RingCat) : Ring ↑(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 (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₂SemiRing_preservesFilteredColimits : CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget₂ RingCat SemiRingCat)

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

@[reducible, inline]

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 (F.comp (CategoryTheory.forget₂ CommRingCat RingCat))

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

Equations

• CommRingCat.FilteredColimits.colimitCommRing F = { toRing := (CommRingCat.FilteredColimits.R F).ring, mul_comm := ⋯ }

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 (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₂Ring_preservesFilteredColimits : CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget₂ CommRingCat RingCat)

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

theorem CommRingCat.FilteredColimits.nontrivial {J : Type v} [CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CommRingCat} [CategoryTheory.IsFilteredOrEmpty J] [∀ (i : J), Nontrivial ↑(F.obj i)] {c : CategoryTheory.Limits.Cocone F} (hc : CategoryTheory.Limits.IsColimit c) : Nontrivial ↑c.pt

instance CommRingCat.FilteredColimits.instNontrivialCarrierColimitOfIsFilteredOrEmptyOfObj {J : Type v} [CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CommRingCat} [CategoryTheory.IsFilteredOrEmpty J] [CategoryTheory.Limits.HasColimit F] [∀ (i : J), Nontrivial ↑(F.obj i)] : Nontrivial ↑(CategoryTheory.Limits.colimit F)