The category of R-algebras 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 AlgebraCat.semiringObj {R : Type u} [CommRing R] {J : Type v} [CategoryTheory.Category.{t, v} J] (F : CategoryTheory.Functor J (AlgebraCat R)) (j : J) : Semiring ((CategoryTheory.Functor.comp F (CategoryTheory.forget (AlgebraCat R))).obj j)

Equations

• AlgebraCat.semiringObj F j = inferInstanceAs (Semiring ↑(F.obj j))

instance AlgebraCat.algebraObj {R : Type u} [CommRing R] {J : Type v} [CategoryTheory.Category.{t, v} J] (F : CategoryTheory.Functor J (AlgebraCat R)) (j : J) : Algebra R ((CategoryTheory.Functor.comp F (CategoryTheory.forget (AlgebraCat R))).obj j)

Equations

• AlgebraCat.algebraObj F j = inferInstanceAs (Algebra R ↑(F.obj j))

def AlgebraCat.sectionsSubalgebra {R : Type u} [CommRing R] {J : Type v} [CategoryTheory.Category.{t, v} J] (F : CategoryTheory.Functor J (AlgebraCat R)) : Subalgebra R ((j : J) → ↑(F.obj j))

The flat sections of a functor into AlgebraCat R form a submodule of all sections.

Equations

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

instance AlgebraCat.instRingElemForAllObjToQuiverToCategoryStructTypeToQuiverToCategoryStructTypesToPrefunctorCompAlgebraCatInstCategoryAlgebraCatForgetInstConcreteCategoryAlgebraCatInstCategoryAlgebraCatSections {R : Type u} [CommRing R] {J : Type v} [CategoryTheory.Category.{t, v} J] (F : CategoryTheory.Functor J (AlgebraCat R)) : Ring ↑(CategoryTheory.Functor.sections (CategoryTheory.Functor.comp F (CategoryTheory.forget (AlgebraCat R))))

Equations

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

instance AlgebraCat.instAlgebraElemForAllObjToQuiverToCategoryStructTypeToQuiverToCategoryStructTypesToPrefunctorCompAlgebraCatInstCategoryAlgebraCatForgetInstConcreteCategoryAlgebraCatInstCategoryAlgebraCatSectionsToCommSemiringToSemiringInstRingElemForAllObjToQuiverToCategoryStructTypeToQuiverToCategoryStructTypesToPrefunctorCompAlgebraCatInstCategoryAlgebraCatForgetInstConcreteCategoryAlgebraCatInstCategoryAlgebraCatSections {R : Type u} [CommRing R] {J : Type v} [CategoryTheory.Category.{t, v} J] (F : CategoryTheory.Functor J (AlgebraCat R)) : Algebra R ↑(CategoryTheory.Functor.sections (CategoryTheory.Functor.comp F (CategoryTheory.forget (AlgebraCat R))))

Equations

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

instance AlgebraCat.instSmallSubtypeForAllCarrierObjToQuiverToCategoryStructAlgebraCatToQuiverToCategoryStructInstCategoryAlgebraCatToPrefunctorMemSubalgebraToCommSemiringSemiringToSemiringIsRingAlgebraIsAlgebraInstMembershipInstSetLikeSubalgebraSectionsSubalgebra {R : Type u} [CommRing R] {J : Type v} [CategoryTheory.Category.{t, v} J] (F : CategoryTheory.Functor J (AlgebraCat R)) [Small.{w, max v w} ↑(CategoryTheory.Functor.sections (CategoryTheory.Functor.comp F (CategoryTheory.forget (AlgebraCat R))))] : Small.{w, max v w} ↥(AlgebraCat.sectionsSubalgebra F)

Equations

• ⋯ = ⋯

instance AlgebraCat.limitSemiring {R : Type u} [CommRing R] {J : Type v} [CategoryTheory.Category.{t, v} J] (F : CategoryTheory.Functor J (AlgebraCat R)) [Small.{w, max v w} ↑(CategoryTheory.Functor.sections (CategoryTheory.Functor.comp F (CategoryTheory.forget (AlgebraCat R))))] : Ring (CategoryTheory.Limits.Types.Small.limitCone (CategoryTheory.Functor.comp F (CategoryTheory.forget (AlgebraCat R)))).pt

Equations

• AlgebraCat.limitSemiring F = inferInstanceAs (Ring (Shrink.{w, max v w} ↥(AlgebraCat.sectionsSubalgebra F)))

instance AlgebraCat.limitAlgebra {R : Type u} [CommRing R] {J : Type v} [CategoryTheory.Category.{t, v} J] (F : CategoryTheory.Functor J (AlgebraCat R)) [Small.{w, max v w} ↑(CategoryTheory.Functor.sections (CategoryTheory.Functor.comp F (CategoryTheory.forget (AlgebraCat R))))] : Algebra R (CategoryTheory.Limits.Types.Small.limitCone (CategoryTheory.Functor.comp F (CategoryTheory.forget (AlgebraCat R)))).pt

Equations

• AlgebraCat.limitAlgebra F = inferInstanceAs (Algebra R (Shrink.{w, max v w} ↥(AlgebraCat.sectionsSubalgebra F)))

def AlgebraCat.limitπAlgHom {R : Type u} [CommRing R] {J : Type v} [CategoryTheory.Category.{t, v} J] (F : CategoryTheory.Functor J (AlgebraCat R)) [Small.{w, max v w} ↑(CategoryTheory.Functor.sections (CategoryTheory.Functor.comp F (CategoryTheory.forget (AlgebraCat R))))] (j : J) : (CategoryTheory.Limits.Types.Small.limitCone (CategoryTheory.Functor.comp F (CategoryTheory.forget (AlgebraCat R)))).pt →ₐ[R] (CategoryTheory.Functor.comp F (CategoryTheory.forget (AlgebraCat R))).obj j

limit.π (F ⋙ forget (AlgebraCat R)) j as a AlgHom.

Equations

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

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

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

Equations

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

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

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

Equations

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

theorem AlgebraCat.hasLimitsOfSize {R : Type u} [CommRing R] [UnivLE.{v, w} ] : CategoryTheory.Limits.HasLimitsOfSize.{t, v, w, max (w + 1) u} (AlgebraCat R)

The category of R-algebras has all limits.

instance AlgebraCat.hasLimits {R : Type u} [CommRing R] : CategoryTheory.Limits.HasLimits (AlgebraCat R)

Equations

• ⋯ = ⋯

instance AlgebraCat.forget₂RingPreservesLimitsOfSize {R : Type u} [CommRing R] [UnivLE.{v, w} ] : CategoryTheory.Limits.PreservesLimitsOfSize.{t, v, w, w, max u (w + 1), w + 1} (CategoryTheory.forget₂ (AlgebraCat R) RingCat)

The forgetful functor from R-algebras to rings preserves all limits.

Equations

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

instance AlgebraCat.forget₂RingPreservesLimits {R : Type u} [CommRing R] : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget₂ (AlgebraCat R) RingCat)

Equations

• AlgebraCat.forget₂RingPreservesLimits = AlgebraCat.forget₂RingPreservesLimitsOfSize

instance AlgebraCat.forget₂ModulePreservesLimitsOfSize {R : Type u} [CommRing R] [UnivLE.{v, w} ] : CategoryTheory.Limits.PreservesLimitsOfSize.{t, v, w, w, max u (w + 1), max u (w + 1)} (CategoryTheory.forget₂ (AlgebraCat R) (ModuleCat R))

The forgetful functor from R-algebras to R-modules preserves all limits.

Equations

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

instance AlgebraCat.forget₂ModulePreservesLimits {R : Type u} [CommRing R] : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget₂ (AlgebraCat R) (ModuleCat R))

Equations

• AlgebraCat.forget₂ModulePreservesLimits = AlgebraCat.forget₂ModulePreservesLimitsOfSize

instance AlgebraCat.forgetPreservesLimitsOfSize {R : Type u} [CommRing R] [UnivLE.{v, w} ] : CategoryTheory.Limits.PreservesLimitsOfSize.{t, v, w, w, max u (w + 1), w + 1} (CategoryTheory.forget (AlgebraCat R))

The forgetful functor from R-algebras to types preserves all limits.

Equations

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

instance AlgebraCat.forgetPreservesLimits {R : Type u} [CommRing R] : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget (AlgebraCat R))

Equations

• AlgebraCat.forgetPreservesLimits = AlgebraCat.forgetPreservesLimitsOfSize