# Documentation

Mathlib.Algebra.Category.AlgebraCat.Limits

# 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} [] {J : Type v} (F : ) (j : J) :
Semiring (().obj j)
instance AlgebraCat.algebraObj {R : Type u} [] {J : Type v} (F : ) (j : J) :
Algebra R (().obj j)
def AlgebraCat.sectionsSubalgebra {R : Type u} [] {J : Type v} (F : ) :
Subalgebra R ((j : J) → ↑(F.obj j))

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

Instances For
instance AlgebraCat.limitSemiring {R : Type u} [] {J : Type v} (F : ) :
instance AlgebraCat.limitAlgebra {R : Type u} [] {J : Type v} (F : ) :
def AlgebraCat.limitπAlgHom {R : Type u} [] {J : Type v} (F : ) (j : J) :

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

Instances For
def AlgebraCat.HasLimits.limitCone {R : Type u} [] {J : Type v} (F : ) :

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

Instances For
def AlgebraCat.HasLimits.limitConeIsLimit {R : Type u} [] {J : Type v} (F : ) :

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

Instances For
theorem AlgebraCat.hasLimitsOfSize {R : Type u} [] :

The category of R-algebras has all limits.

instance AlgebraCat.hasLimits {R : Type u} [] :

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

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

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