mathlib documentation

algebra.category.Algebra.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.

@[protected, instance]
def Algebra.semiring_obj {R : Type u} [comm_ring R] {J : Type v} [category_theory.small_category J] (F : J Algebra R) (j : J) :
Equations
@[protected, instance]
def Algebra.algebra_obj {R : Type u} [comm_ring R] {J : Type v} [category_theory.small_category J] (F : J Algebra R) (j : J) :
Equations
def Algebra.sections_subalgebra {R : Type u} [comm_ring R] {J : Type v} [category_theory.small_category J] (F : J Algebra R) :
subalgebra R (Π (j : J), (F.obj j))

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

Equations

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

Equations
@[protected, instance, irreducible]

The category of R-algebras has all limits.

@[protected, instance]