The category of (commutative) rings has all limits

Further, these limits are preserved by the forgetful functor --- that is, the underlying types are just the limits in the category of types.

def LibraryNote.«change_elaboration_strategy_with_`by_apply`» : Batteries.Util.LibraryNote

Some definitions may be extremely slow to elaborate, when the target type to be constructed is complicated and when the type of the term given in the definition is also complicated and does not obviously match the target type. In this case, instead of just giving the term, prefixing it with by apply may speed up things considerably as the types are not elaborated in the same order.

@[implicit_reducible]

instance SemiRingCat.semiringObj {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J SemiRingCat) (j : J) : Semiring ((F.comp (CategoryTheory.forget SemiRingCat)).obj j)

def SemiRingCat.sectionsSubsemiring {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J SemiRingCat) : Subsemiring ((j : J) → ↑(F.obj j))

The flat sections of a functor into SemiRingCat form a subsemiring of all sections.

@[implicit_reducible]

instance SemiRingCat.sectionsSemiring {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J SemiRingCat) : Semiring ↑(F.comp (CategoryTheory.forget SemiRingCat)).sections

@[implicit_reducible]

noncomputable instance SemiRingCat.limitSemiring {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J SemiRingCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget SemiRingCat)).sections] : Semiring (CategoryTheory.Limits.Types.Small.limitCone (F.comp (CategoryTheory.forget SemiRingCat))).pt

noncomputable def SemiRingCat.limitπRingHom {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J SemiRingCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget SemiRingCat)).sections] (j : J) : (CategoryTheory.Limits.Types.Small.limitCone (F.comp (CategoryTheory.forget SemiRingCat))).pt →+* (F.comp (CategoryTheory.forget SemiRingCat)).obj j

limit.π (F ⋙ forget SemiRingCat) j as a RingHom.

noncomputable def SemiRingCat.HasLimits.limitCone {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J SemiRingCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget SemiRingCat)).sections] : CategoryTheory.Limits.Cone F

Construction of a limit cone in SemiRingCat. (Internal use only; use the limits API.)

noncomputable def SemiRingCat.HasLimits.limitConeIsLimit {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J SemiRingCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget SemiRingCat)).sections] : CategoryTheory.Limits.IsLimit (limitCone F)

Witness that the limit cone in SemiRingCat is a limit cone. (Internal use only; use the limits API.)

instance SemiRingCat.hasLimit {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J SemiRingCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget SemiRingCat)).sections] : CategoryTheory.Limits.HasLimit F

If (F ⋙ forget SemiRingCat).sections is u-small, F has a limit.

instance SemiRingCat.hasLimitsOfShape {J : Type v} [CategoryTheory.Category.{w, v} J] [Small.{u, v} J] : CategoryTheory.Limits.HasLimitsOfShape J SemiRingCat

If J is u-small, SemiRingCat.{u} has limits of shape J.

instance SemiRingCat.hasLimitsOfSize [UnivLE.{v, u}] : CategoryTheory.Limits.HasLimitsOfSize.{w, v, u, u + 1} SemiRingCat

The category of rings has all limits.

instance SemiRingCat.hasLimits : CategoryTheory.Limits.HasLimits SemiRingCat

noncomputable def SemiRingCat.forget₂AddCommMonPreservesLimitsAux {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J SemiRingCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget SemiRingCat)).sections] : CategoryTheory.Limits.IsLimit ((CategoryTheory.forget₂ SemiRingCat AddCommMonCat).mapCone (HasLimits.limitCone F))

Auxiliary lemma to prove the cone induced by limitCone is a limit cone.

instance SemiRingCat.forget₂AddCommMon_preservesLimitsOfSize [UnivLE.{v, u}] : CategoryTheory.Limits.PreservesLimitsOfSize.{w, v, u, u, u + 1, u + 1} (CategoryTheory.forget₂ SemiRingCat AddCommMonCat)

The forgetful functor from semirings to additive commutative monoids preserves all limits.

instance SemiRingCat.forget₂AddCommMon_preservesLimits : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget₂ SemiRingCat AddCommMonCat)

noncomputable def SemiRingCat.forget₂MonPreservesLimitsAux {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J SemiRingCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget SemiRingCat)).sections] : CategoryTheory.Limits.IsLimit ((CategoryTheory.forget₂ SemiRingCat MonCat).mapCone (HasLimits.limitCone F))

An auxiliary declaration to speed up typechecking.

instance SemiRingCat.forget₂Mon_preservesLimitsOfSize [UnivLE.{v, u}] : CategoryTheory.Limits.PreservesLimitsOfSize.{w, v, u, u, u + 1, u + 1} (CategoryTheory.forget₂ SemiRingCat MonCat)

The forgetful functor from semirings to monoids preserves all limits.

instance SemiRingCat.forget₂Mon_preservesLimits : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget₂ SemiRingCat MonCat)

instance SemiRingCat.forget_preservesLimitsOfSize [UnivLE.{v, u}] : CategoryTheory.Limits.PreservesLimitsOfSize.{w, v, u, u, u + 1, u + 1} (CategoryTheory.forget SemiRingCat)

The forgetful functor from semirings to types preserves all limits.

instance SemiRingCat.forget_preservesLimits : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget SemiRingCat)

@[implicit_reducible]

instance CommSemiRingCat.commSemiringObj {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J CommSemiRingCat) (j : J) : CommSemiring ((F.comp (CategoryTheory.forget CommSemiRingCat)).obj j)

@[implicit_reducible]

noncomputable instance CommSemiRingCat.limitCommSemiring {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J CommSemiRingCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget CommSemiRingCat)).sections] : CommSemiring (CategoryTheory.Limits.Types.Small.limitCone (F.comp (CategoryTheory.forget CommSemiRingCat))).pt

@[implicit_reducible]

noncomputable instance CommSemiRingCat.instCreatesLimitSemiRingCatForget₂RingHomCarrierCarrier {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J CommSemiRingCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget CommSemiRingCat)).sections] : CategoryTheory.CreatesLimit F (CategoryTheory.forget₂ CommSemiRingCat SemiRingCat)

We show that the forgetful functor CommSemiRingCat ⥤ SemiRingCat creates limits.

All we need to do is notice that the limit point has a CommSemiring instance available, and then reuse the existing limit.

noncomputable def CommSemiRingCat.limitCone {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J CommSemiRingCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget CommSemiRingCat)).sections] : CategoryTheory.Limits.Cone F

A choice of limit cone for a functor into CommSemiRingCat. (Generally, you'll just want to use limit F.)

noncomputable def CommSemiRingCat.limitConeIsLimit {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J CommSemiRingCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget CommSemiRingCat)).sections] : CategoryTheory.Limits.IsLimit (limitCone F)

The chosen cone is a limit cone. (Generally, you'll just want to use limit.cone F.)

instance CommSemiRingCat.hasLimit {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J CommSemiRingCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget CommSemiRingCat)).sections] : CategoryTheory.Limits.HasLimit F

If (F ⋙ forget CommSemiRingCat).sections is u-small, F has a limit.

instance CommSemiRingCat.hasLimitsOfShape {J : Type v} [CategoryTheory.Category.{w, v} J] [Small.{u, v} J] : CategoryTheory.Limits.HasLimitsOfShape J CommSemiRingCat

If J is u-small, CommSemiRingCat.{u} has limits of shape J.

instance CommSemiRingCat.hasLimitsOfSize [UnivLE.{v, u}] : CategoryTheory.Limits.HasLimitsOfSize.{w, v, u, u + 1} CommSemiRingCat

The category of rings has all limits.

instance CommSemiRingCat.hasLimits : CategoryTheory.Limits.HasLimits CommSemiRingCat

instance CommSemiRingCat.forget₂SemiRing_preservesLimitsOfSize [UnivLE.{v, u}] : CategoryTheory.Limits.PreservesLimitsOfSize.{w, v, u, u, u + 1, u + 1} (CategoryTheory.forget₂ CommSemiRingCat SemiRingCat)

The forgetful functor from rings to semirings preserves all limits.

instance CommSemiRingCat.forget₂SemiRing_preservesLimits : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget₂ CommSemiRingCat SemiRingCat)

instance CommSemiRingCat.forget_preservesLimitsOfSize [UnivLE.{v, u}] : CategoryTheory.Limits.PreservesLimitsOfSize.{w, v, u, u, u + 1, u + 1} (CategoryTheory.forget CommSemiRingCat)

The forgetful functor from rings to types preserves all limits. (That is, the underlying types could have been computed instead as limits in the category of types.)

instance CommSemiRingCat.forget_preservesLimits : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget CommSemiRingCat)

@[implicit_reducible]

instance RingCat.ringObj {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J RingCat) (j : J) : Ring ((F.comp (CategoryTheory.forget RingCat)).obj j)

def RingCat.sectionsSubring {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J RingCat) : Subring ((j : J) → ↑(F.obj j))

The flat sections of a functor into RingCat form a subring of all sections.

@[implicit_reducible]

noncomputable instance RingCat.limitRing {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J RingCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget RingCat)).sections] : Ring (CategoryTheory.Limits.Types.Small.limitCone (F.comp (CategoryTheory.forget RingCat))).pt

@[implicit_reducible]

noncomputable instance RingCat.instCreatesLimitSemiRingCatForget₂RingHomCarrierCarrier {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J RingCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget RingCat)).sections] : CategoryTheory.CreatesLimit F (CategoryTheory.forget₂ RingCat SemiRingCat)

We show that the forgetful functor CommRingCat ⥤ RingCat creates limits.

All we need to do is notice that the limit point has a Ring instance available, and then reuse the existing limit.

noncomputable def RingCat.limitCone {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J RingCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget RingCat)).sections] : CategoryTheory.Limits.Cone F

A choice of limit cone for a functor into RingCat. (Generally, you'll just want to use limit F.)

noncomputable def RingCat.limitConeIsLimit {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J RingCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget RingCat)).sections] : CategoryTheory.Limits.IsLimit (limitCone F)

The chosen cone is a limit cone. (Generally, you'll just want to use limit.cone F.)

instance RingCat.hasLimit {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J RingCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget RingCat)).sections] : CategoryTheory.Limits.HasLimit F

If (F ⋙ forget RingCat).sections is u-small, F has a limit.

instance RingCat.hasLimitsOfShape {J : Type v} [CategoryTheory.Category.{w, v} J] [Small.{u, v} J] : CategoryTheory.Limits.HasLimitsOfShape J RingCat

If J is u-small, RingCat.{u} has limits of shape J.

instance RingCat.hasLimitsOfSize [UnivLE.{v, u}] : CategoryTheory.Limits.HasLimitsOfSize.{w, v, u, u + 1} RingCat

The category of rings has all limits.

instance RingCat.hasLimits : CategoryTheory.Limits.HasLimits RingCat

instance RingCat.forget₂SemiRing_preservesLimitsOfSize [UnivLE.{v, u}] : CategoryTheory.Limits.PreservesLimitsOfSize.{w, v, u, u, u + 1, u + 1} (CategoryTheory.forget₂ RingCat SemiRingCat)

The forgetful functor from rings to semirings preserves all limits.

instance RingCat.forget₂SemiRing_preservesLimits : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget₂ RingCat SemiRingCat)

noncomputable def RingCat.forget₂AddCommGroupPreservesLimitsAux {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J RingCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget RingCat)).sections] : CategoryTheory.Limits.IsLimit ((CategoryTheory.forget₂ RingCat AddCommGrpCat).mapCone (limitCone F))

An auxiliary declaration to speed up typechecking.

instance RingCat.forget₂AddCommGroup_preservesLimitsOfSize [UnivLE.{v, u}] : CategoryTheory.Limits.PreservesLimitsOfSize.{v, v, u, u, u + 1, u + 1} (CategoryTheory.forget₂ RingCat AddCommGrpCat)

The forgetful functor from rings to additive commutative groups preserves all limits.

instance RingCat.forget₂AddCommGroup_preservesLimits : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget₂ RingCat AddCommGrpCat)

instance RingCat.forget_preservesLimitsOfSize [UnivLE.{v, u}] : CategoryTheory.Limits.PreservesLimitsOfSize.{v, v, u, u, u + 1, u + 1} (CategoryTheory.forget RingCat)

The forgetful functor from rings to types preserves all limits. (That is, the underlying types could have been computed instead as limits in the category of types.)

instance RingCat.forget_preservesLimits : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget RingCat)

@[implicit_reducible]

instance CommRingCat.commRingObj {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J CommRingCat) (j : J) : CommRing ((F.comp (CategoryTheory.forget CommRingCat)).obj j)

@[implicit_reducible]

noncomputable instance CommRingCat.limitCommRing {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J CommRingCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget CommRingCat)).sections] : CommRing (CategoryTheory.Limits.Types.Small.limitCone (F.comp (CategoryTheory.forget CommRingCat))).pt

@[implicit_reducible]

noncomputable instance CommRingCat.instCreatesLimitRingCatForget₂RingHomCarrierCarrier {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J CommRingCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget CommRingCat)).sections] : CategoryTheory.CreatesLimit F (CategoryTheory.forget₂ CommRingCat RingCat)

We show that the forgetful functor CommRingCat ⥤ RingCat creates limits.

All we need to do is notice that the limit point has a CommRing instance available, and then reuse the existing limit.

noncomputable def CommRingCat.limitCone {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J CommRingCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget CommRingCat)).sections] : CategoryTheory.Limits.Cone F

A choice of limit cone for a functor into CommRingCat. (Generally, you'll just want to use limit F.)

noncomputable def CommRingCat.limitConeIsLimit {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J CommRingCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget CommRingCat)).sections] : CategoryTheory.Limits.IsLimit (limitCone F)

The chosen cone is a limit cone. (Generally, you'll just want to use limit.cone F.)

instance CommRingCat.hasLimit {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J CommRingCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget CommRingCat)).sections] : CategoryTheory.Limits.HasLimit F

If (F ⋙ forget CommRingCat).sections is u-small, F has a limit.

instance CommRingCat.hasLimitsOfShape {J : Type v} [CategoryTheory.Category.{w, v} J] [Small.{u, v} J] : CategoryTheory.Limits.HasLimitsOfShape J CommRingCat

If J is u-small, CommRingCat.{u} has limits of shape J.

instance CommRingCat.hasLimitsOfSize [UnivLE.{v, u}] : CategoryTheory.Limits.HasLimitsOfSize.{w, v, u, u + 1} CommRingCat

The category of commutative rings has all limits.

instance CommRingCat.hasLimits : CategoryTheory.Limits.HasLimits CommRingCat

instance CommRingCat.forget₂Ring_preservesLimitsOfSize [UnivLE.{v, u}] : CategoryTheory.Limits.PreservesLimitsOfSize.{w, v, u, u, u + 1, u + 1} (CategoryTheory.forget₂ CommRingCat RingCat)

The forgetful functor from commutative rings to rings preserves all limits. (That is, the underlying rings could have been computed instead as limits in the category of rings.)

instance CommRingCat.forget₂Ring_preservesLimits : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget₂ CommRingCat RingCat)

noncomputable def CommRingCat.forget₂CommSemiRingPreservesLimitsAux {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J CommRingCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget CommRingCat)).sections] : CategoryTheory.Limits.IsLimit ((CategoryTheory.forget₂ CommRingCat CommSemiRingCat).mapCone (limitCone F))

An auxiliary declaration to speed up typechecking.

instance CommRingCat.forget₂CommSemiRing_preservesLimitsOfSize [UnivLE.{v, u}] : CategoryTheory.Limits.PreservesLimitsOfSize.{w, v, u, u, u + 1, u + 1} (CategoryTheory.forget₂ CommRingCat CommSemiRingCat)

The forgetful functor from commutative rings to commutative semirings preserves all limits. (That is, the underlying commutative semirings could have been computed instead as limits in the category of commutative semirings.)

instance CommRingCat.forget₂CommSemiRing_preservesLimits : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget₂ CommRingCat CommSemiRingCat)

instance CommRingCat.forget_preservesLimitsOfSize [UnivLE.{v, u}] : CategoryTheory.Limits.PreservesLimitsOfSize.{w, v, u, u, u + 1, u + 1} (CategoryTheory.forget CommRingCat)

The forgetful functor from commutative rings to types preserves all limits. (That is, the underlying types could have been computed instead as limits in the category of types.)

instance CommRingCat.forget_preservesLimits : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget CommRingCat)