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.

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

Equations

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

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

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

Equations

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

instance SemiRingCat.limitSemiring {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J SemiRingCatMax) : Semiring (CategoryTheory.Limits.Types.limitCone (CategoryTheory.Functor.comp F (CategoryTheory.forget SemiRingCat))).pt

Equations

• SemiRingCat.limitSemiring F = Subsemiring.toSemiring (SemiRingCat.sectionsSubsemiring F)

def SemiRingCat.limitπRingHom {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J SemiRingCatMax) (j : J) : (CategoryTheory.Limits.Types.limitCone (CategoryTheory.Functor.comp F (CategoryTheory.forget SemiRingCat))).pt →+* (CategoryTheory.Functor.comp F (CategoryTheory.forget SemiRingCat)).obj j

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

Equations

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

def SemiRingCat.HasLimits.limitCone {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J SemiRingCatMax) : CategoryTheory.Limits.Cone F

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

Equations

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

def SemiRingCat.HasLimits.limitConeIsLimit {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J SemiRingCatMax) : CategoryTheory.Limits.IsLimit (SemiRingCat.HasLimits.limitCone F)

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

instance SemiRingCat.hasLimitsOfSize : CategoryTheory.Limits.HasLimitsOfSize.{v, v, max u v, max (u + 1) (v + 1)} SemiRingCatMax

The category of rings has all limits.

Equations

• SemiRingCat.hasLimitsOfSize = SemiRingCat.hasLimitsOfSize.proof_1

instance SemiRingCat.hasLimits : CategoryTheory.Limits.HasLimits SemiRingCat

Equations

• SemiRingCat.hasLimits = SemiRingCat.hasLimitsOfSize

def SemiRingCat.forget₂AddCommMonPreservesLimitsAux {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J SemiRingCatMax) : CategoryTheory.Limits.IsLimit ((CategoryTheory.forget₂ SemiRingCat AddCommMonCat).mapCone (SemiRingCat.HasLimits.limitCone F))

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

Equations

• SemiRingCat.forget₂AddCommMonPreservesLimitsAux F = AddCommMonCat.limitConeIsLimit (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ SemiRingCat AddCommMonCat))

instance SemiRingCat.forget₂AddCommMonPreservesLimitsOfSize : CategoryTheory.Limits.PreservesLimitsOfSize.{v, v, max u v, max u v, max (u + 1) (v + 1), max (u + 1) (v + 1)} (CategoryTheory.forget₂ SemiRingCat AddCommMonCat)

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

Equations

• SemiRingCat.forget₂AddCommMonPreservesLimitsOfSize = CategoryTheory.Limits.PreservesLimitsOfSize.mk

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

Equations

• SemiRingCat.forget₂AddCommMonPreservesLimits = SemiRingCat.forget₂AddCommMonPreservesLimitsOfSize

def SemiRingCat.forget₂MonPreservesLimitsAux {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J SemiRingCatMax) : CategoryTheory.Limits.IsLimit ((CategoryTheory.forget₂ SemiRingCat MonCat).mapCone (SemiRingCat.HasLimits.limitCone F))

An auxiliary declaration to speed up typechecking.

Equations

• SemiRingCat.forget₂MonPreservesLimitsAux F = MonCat.HasLimits.limitConeIsLimit (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ SemiRingCat MonCat))

instance SemiRingCat.forget₂MonPreservesLimitsOfSize : CategoryTheory.Limits.PreservesLimitsOfSize.{v, v, max u v, max u v, max (u + 1) (v + 1), max (u + 1) (v + 1)} (CategoryTheory.forget₂ SemiRingCat MonCat)

The forgetful functor from semirings to monoids preserves all limits.

Equations

• SemiRingCat.forget₂MonPreservesLimitsOfSize = CategoryTheory.Limits.PreservesLimitsOfSize.mk

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

Equations

• SemiRingCat.forget₂MonPreservesLimits = SemiRingCat.forget₂MonPreservesLimitsOfSize

instance SemiRingCat.forgetPreservesLimitsOfSize : CategoryTheory.Limits.PreservesLimitsOfSize.{v, v, max u v, max u v, max (u + 1) (v + 1), max (u + 1) (v + 1)} (CategoryTheory.forget SemiRingCat)

The forgetful functor from semirings to types preserves all limits.

Equations

• SemiRingCat.forgetPreservesLimitsOfSize = CategoryTheory.Limits.PreservesLimitsOfSize.mk

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

Equations

• SemiRingCat.forgetPreservesLimits = SemiRingCat.forgetPreservesLimitsOfSize

@[inline, reducible]

abbrev CommSemiRingCatMax : Type ((max u1 u2) + 1)

An alias for CommSemiring.{max u v}, to deal with unification issues.

Equations

• CommSemiRingCatMax = CommSemiRingCat

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

Equations

• CommSemiRingCat.commSemiringObj F j = let_fun this := inferInstance; this

instance CommSemiRingCat.limitCommSemiring {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommSemiRingCatMax) : CommSemiring (CategoryTheory.Limits.Types.limitCone (CategoryTheory.Functor.comp F (CategoryTheory.forget CommSemiRingCat))).pt

Equations

• CommSemiRingCat.limitCommSemiring F = Subsemiring.toCommSemiring (SemiRingCat.sectionsSubsemiring (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ CommSemiRingCat SemiRingCat)))

def CommSemiRingCat.limitCone {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommSemiRingCatMax) : CategoryTheory.Limits.Cone F

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

Equations

• CommSemiRingCat.limitCone F = CategoryTheory.liftLimit (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ CommSemiRingCatMax SemiRingCatMax)))

def CommSemiRingCat.limitConeIsLimit {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommSemiRingCatMax) : CategoryTheory.Limits.IsLimit (CommSemiRingCat.limitCone F)

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

Equations

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

instance CommSemiRingCat.hasLimitsOfSize : CategoryTheory.Limits.HasLimitsOfSize.{v, v, max u v, max (u + 1) (v + 1)} CommSemiRingCatMax

The category of rings has all limits.

Equations

• CommSemiRingCat.hasLimitsOfSize = CommSemiRingCat.hasLimitsOfSize.proof_1

instance CommSemiRingCat.hasLimits : CategoryTheory.Limits.HasLimits CommSemiRingCat

Equations

• CommSemiRingCat.hasLimits = CommSemiRingCat.hasLimitsOfSize

instance CommSemiRingCat.forget₂SemiRingPreservesLimitsOfSize : CategoryTheory.Limits.PreservesLimitsOfSize.{v, v, max u v, max u v, max (u + 1) (v + 1), max (u + 1) (v + 1)} (CategoryTheory.forget₂ CommSemiRingCat SemiRingCat)

The forgetful functor from rings to semirings preserves all limits.

Equations

• CommSemiRingCat.forget₂SemiRingPreservesLimitsOfSize = CategoryTheory.Limits.PreservesLimitsOfSize.mk

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

Equations

• CommSemiRingCat.forget₂SemiRingPreservesLimits = CommSemiRingCat.forget₂SemiRingPreservesLimitsOfSize

instance CommSemiRingCat.forgetPreservesLimitsOfSize : CategoryTheory.Limits.PreservesLimitsOfSize.{v, v, max u v, max u v, max (u + 1) (v + 1), max (u + 1) (v + 1)} (CategoryTheory.forget CommSemiRingCatMax)

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

Equations

• CommSemiRingCat.forgetPreservesLimitsOfSize = CategoryTheory.Limits.PreservesLimitsOfSize.mk

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

Equations

• CommSemiRingCat.forgetPreservesLimits = CommSemiRingCat.forgetPreservesLimitsOfSize

@[inline, reducible]

abbrev RingCatMax : Type ((max u1 u2) + 1)

An alias for RingCat.{max u v}, to deal around unification issues.

Equations

• RingCatMax = RingCat

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

Equations

• RingCat.ringObj F j = let_fun this := inferInstance; this

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

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

Equations

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

instance RingCat.limitRing {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J RingCatMax) : Ring (CategoryTheory.Limits.Types.limitCone (CategoryTheory.Functor.comp F (CategoryTheory.forget RingCatMax))).pt

Equations

• RingCat.limitRing F = Subring.toRing (RingCat.sectionsSubring F)

instance RingCat.instCreatesLimitRingCatMaxInstRingCatLargeCategorySemiRingCatMaxInstSemiRingCatLargeCategoryForget₂InstConcreteCategoryRingCatInstRingCatLargeCategoryInstConcreteCategorySemiRingCatInstSemiRingCatLargeCategoryHasForgetToSemiRingCat {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J RingCatMax) : CategoryTheory.CreatesLimit F (CategoryTheory.forget₂ RingCatMax SemiRingCatMax)

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.

Equations

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

def RingCat.limitCone {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J RingCatMax) : CategoryTheory.Limits.Cone F

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

Equations

• RingCat.limitCone F = CategoryTheory.liftLimit (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ RingCatMax SemiRingCatMax)))

def RingCat.limitConeIsLimit {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J RingCatMax) : CategoryTheory.Limits.IsLimit (RingCat.limitCone F)

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

Equations

• RingCat.limitConeIsLimit F = CategoryTheory.liftedLimitIsLimit (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ RingCatMax SemiRingCatMax)))

instance RingCat.hasLimitsOfSize : CategoryTheory.Limits.HasLimitsOfSize.{v, v, max u v, max (u + 1) (v + 1)} RingCat

The category of rings has all limits.

Equations

• RingCat.hasLimitsOfSize = RingCat.hasLimitsOfSize.proof_1

instance RingCat.hasLimits : CategoryTheory.Limits.HasLimits RingCat

Equations

• RingCat.hasLimits = RingCat.hasLimitsOfSize

instance RingCat.forget₂SemiRingPreservesLimitsOfSize : CategoryTheory.Limits.PreservesLimitsOfSize.{v, v, max u v, max u v, max (u + 1) (v + 1), max (u + 1) (v + 1)} (CategoryTheory.forget₂ RingCat SemiRingCat)

The forgetful functor from rings to semirings preserves all limits.

Equations

• RingCat.forget₂SemiRingPreservesLimitsOfSize = CategoryTheory.Limits.PreservesLimitsOfSize.mk

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

Equations

• RingCat.forget₂SemiRingPreservesLimits = RingCat.forget₂SemiRingPreservesLimitsOfSize

def RingCat.forget₂AddCommGroupPreservesLimitsAux {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J RingCatMax) : CategoryTheory.Limits.IsLimit ((CategoryTheory.forget₂ RingCatMax AddCommGroupCat).mapCone (RingCat.limitCone F))

An auxiliary declaration to speed up typechecking.

Equations

• RingCat.forget₂AddCommGroupPreservesLimitsAux F = AddCommGroupCat.limitConeIsLimit (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ RingCatMax AddCommGroupCat))

instance RingCat.forget₂AddCommGroupPreservesLimitsOfSize : CategoryTheory.Limits.PreservesLimitsOfSize.{v, v, max u v, max u v, max (u + 1) (v + 1), max (u + 1) (v + 1)} (CategoryTheory.forget₂ RingCatMax AddCommGroupCat)

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

Equations

• RingCat.forget₂AddCommGroupPreservesLimitsOfSize = CategoryTheory.Limits.PreservesLimitsOfSize.mk

instance RingCat.forget₂AddCommGroupPreservesLimits : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget₂ RingCat AddCommGroupCat)

Equations

• RingCat.forget₂AddCommGroupPreservesLimits = RingCat.forget₂AddCommGroupPreservesLimitsOfSize

instance RingCat.forgetPreservesLimitsOfSize : CategoryTheory.Limits.PreservesLimitsOfSize.{v, v, max u v, max u v, max (u + 1) (v + 1), max (u + 1) (v + 1)} (CategoryTheory.forget RingCatMax)

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

Equations

• RingCat.forgetPreservesLimitsOfSize = CategoryTheory.Limits.PreservesLimitsOfSize.mk

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

Equations

• RingCat.forgetPreservesLimits = RingCat.forgetPreservesLimitsOfSize

@[inline, reducible]

abbrev CommRingCatMax : Type ((max u1 u2) + 1)

An alias for CommRingCat.{max u v}, to deal around unification issues.

Equations

• CommRingCatMax = CommRingCat

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

Equations

• CommRingCat.commRingObj F j = let_fun this := inferInstance; this

instance CommRingCat.limitCommRing {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommRingCatMax) : CommRing (CategoryTheory.Limits.Types.limitCone (CategoryTheory.Functor.comp F (CategoryTheory.forget CommRingCatMax))).pt

Equations

• CommRingCat.limitCommRing F = Subring.toCommRing (RingCat.sectionsSubring (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ CommRingCat RingCat)))

instance CommRingCat.instCreatesLimitCommRingCatMaxInstCommRingCatLargeCategoryRingCatMaxInstRingCatLargeCategoryForget₂InstConcreteCategoryCommRingCatInstCommRingCatLargeCategoryInstConcreteCategoryRingCatInstRingCatLargeCategoryHasForgetToRingCat {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommRingCatMax) : CategoryTheory.CreatesLimit F (CategoryTheory.forget₂ CommRingCatMax RingCatMax)

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.

Equations

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

def CommRingCat.limitCone {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommRingCatMax) : CategoryTheory.Limits.Cone F

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

Equations

• CommRingCat.limitCone F = CategoryTheory.liftLimit (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ CommRingCatMax RingCatMax)))

def CommRingCat.limitConeIsLimit {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommRingCatMax) : CategoryTheory.Limits.IsLimit (CommRingCat.limitCone F)

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

Equations

• CommRingCat.limitConeIsLimit F = CategoryTheory.liftedLimitIsLimit (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ CommRingCatMax RingCatMax)))

instance CommRingCat.hasLimitsOfSize : CategoryTheory.Limits.HasLimitsOfSize.{v, v, max u v, max (u + 1) (v + 1)} CommRingCatMax

The category of commutative rings has all limits.

Equations

• CommRingCat.hasLimitsOfSize = CommRingCat.hasLimitsOfSize.proof_1

instance CommRingCat.hasLimits : CategoryTheory.Limits.HasLimits CommRingCat

Equations

• CommRingCat.hasLimits = CommRingCat.hasLimitsOfSize

instance CommRingCat.forget₂RingPreservesLimitsOfSize : CategoryTheory.Limits.PreservesLimitsOfSize.{v, v, max u v, max u v, max (u + 1) (v + 1), max (u + 1) (v + 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.)

Equations

• CommRingCat.forget₂RingPreservesLimitsOfSize = CategoryTheory.Limits.PreservesLimitsOfSize.mk

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

Equations

• CommRingCat.forget₂RingPreservesLimits = CommRingCat.forget₂RingPreservesLimitsOfSize

def CommRingCat.forget₂CommSemiRingPreservesLimitsAux {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommRingCatMax) : CategoryTheory.Limits.IsLimit ((CategoryTheory.forget₂ CommRingCat CommSemiRingCat).mapCone (CommRingCat.limitCone F))

An auxiliary declaration to speed up typechecking.

Equations

• CommRingCat.forget₂CommSemiRingPreservesLimitsAux F = CommSemiRingCat.limitConeIsLimit (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ CommRingCat CommSemiRingCat))

instance CommRingCat.forget₂CommSemiRingPreservesLimitsOfSize : CategoryTheory.Limits.PreservesLimitsOfSize.{v, v, max u v, max u v, max (u + 1) (v + 1), max (u + 1) (v + 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.)

Equations

• CommRingCat.forget₂CommSemiRingPreservesLimitsOfSize = CategoryTheory.Limits.PreservesLimitsOfSize.mk

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

Equations

• CommRingCat.forget₂CommSemiRingPreservesLimits = CommRingCat.forget₂CommSemiRingPreservesLimitsOfSize

instance CommRingCat.forgetPreservesLimitsOfSize : CategoryTheory.Limits.PreservesLimitsOfSize.{v, v, max u v, max u v, max (u + 1) (v + 1), max (u + 1) (v + 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.)

Equations

• CommRingCat.forgetPreservesLimitsOfSize = CategoryTheory.Limits.PreservesLimitsOfSize.mk

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

Equations

• CommRingCat.forgetPreservesLimits = CommRingCat.forgetPreservesLimitsOfSize