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.

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

Instances For

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

    Instances For

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

      Instances For