# mathlibdocumentation

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} (F : J ) (j : J) :
semiring ((F .obj j)
Equations
@[protected, instance]
def Algebra.algebra_obj {R : Type u} [comm_ring R] {J : Type v} (F : J ) (j : J) :
((F .obj j)
Equations
def Algebra.sections_subalgebra {R : Type u} [comm_ring R] {J : Type v} (F : J ) :
(Π (j : J), (F.obj j))

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

Equations
@[protected, instance]
def Algebra.limit_semiring {R : Type u} [comm_ring R] {J : Type v} (F : J ) :
Equations
@[protected, instance]
def Algebra.limit_algebra {R : Type u} [comm_ring R] {J : Type v} (F : J ) :
Equations
def Algebra.limit_π_alg_hom {R : Type u} [comm_ring R] {J : Type v} (F : J ) (j : J) :
→ₐ[R] (F .obj j

limit.π (F ⋙ forget (Algebra R)) j as a alg_hom.

Equations
def Algebra.has_limits.limit_cone {R : Type u} [comm_ring R] {J : Type v} (F : J ) :

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

Equations
def Algebra.has_limits.limit_cone_is_limit {R : Type u} [comm_ring R] {J : Type v} (F : J ) :

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

Equations
@[protected, instance, irreducible]
def Algebra.has_limits_of_size {R : Type u} [comm_ring R] :

The category of R-algebras has all limits.

@[protected, instance]
def Algebra.has_limits {R : Type u} [comm_ring R] :
@[protected, instance]
noncomputable def Algebra.forget₂_Ring_preserves_limits_of_size {R : Type u} [comm_ring R] :

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

Equations
@[protected, instance]
noncomputable def Algebra.forget₂_Ring_preserves_limits {R : Type u} [comm_ring R] :
Equations
@[protected, instance]

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

Equations
@[protected, instance]
Equations
@[protected, instance]

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

Equations
@[protected, instance]
def Algebra.forget_preserves_limits {R : Type u} [comm_ring R] :
Equations