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.

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

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

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

      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.
      Instances For

        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.
        Instances For
          Equations
          • AlgebraCat.forget₂RingPreservesLimits = AlgebraCat.forget₂RingPreservesLimitsOfSize

          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.
          Equations
          • AlgebraCat.forget₂ModulePreservesLimits = AlgebraCat.forget₂ModulePreservesLimitsOfSize

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

          Equations
          • One or more equations did not get rendered due to their size.
          Equations
          • AlgebraCat.forgetPreservesLimits = AlgebraCat.forgetPreservesLimitsOfSize