Documentation

Mathlib.Algebra.Category.AlgCat.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.

source
instance AlgCat.semiringObj {R : Type u} [CommRing R] {J : Type v} [CategoryTheory.Category.{t, v} J] (F : CategoryTheory.Functor J (AlgCat R)) (j : J) :
Semiring ((F.comp (CategoryTheory.forget (AlgCat R))).obj j)
Equations
    source
    instance AlgCat.algebraObj {R : Type u} [CommRing R] {J : Type v} [CategoryTheory.Category.{t, v} J] (F : CategoryTheory.Functor J (AlgCat R)) (j : J) :
    Algebra R ((F.comp (CategoryTheory.forget (AlgCat R))).obj j)
    Equations
      source
      def AlgCat.sectionsSubalgebra {R : Type u} [CommRing R] {J : Type v} [CategoryTheory.Category.{t, v} J] (F : CategoryTheory.Functor J (AlgCat R)) :
      Subalgebra R ((j : J) → ↑(F.obj j))

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

      Equations
        Instances For
          source
          instance AlgCat.instRingElemForallObjCompForgetSections {R : Type u} [CommRing R] {J : Type v} [CategoryTheory.Category.{t, v} J] (F : CategoryTheory.Functor J (AlgCat R)) :
          Ring ↑(F.comp (CategoryTheory.forget (AlgCat R))).sections
          Equations
            source
            instance AlgCat.instAlgebraElemForallObjCompForgetSections {R : Type u} [CommRing R] {J : Type v} [CategoryTheory.Category.{t, v} J] (F : CategoryTheory.Functor J (AlgCat R)) :
            Algebra R ↑(F.comp (CategoryTheory.forget (AlgCat R))).sections
            Equations
              source
              instance AlgCat.instSmallSubtypeForallCarrierObjMemSubalgebraSectionsSubalgebra {R : Type u} [CommRing R] {J : Type v} [CategoryTheory.Category.{t, v} J] (F : CategoryTheory.Functor J (AlgCat R)) [Small.{w, max v w} ↑(F.comp (CategoryTheory.forget (AlgCat R))).sections] :
              Small.{w, max v w} ↥(sectionsSubalgebra F)
              source
              instance AlgCat.limitSemiring {R : Type u} [CommRing R] {J : Type v} [CategoryTheory.Category.{t, v} J] (F : CategoryTheory.Functor J (AlgCat R)) [Small.{w, max v w} ↑(F.comp (CategoryTheory.forget (AlgCat R))).sections] :
              Ring (CategoryTheory.Limits.Types.Small.limitCone (F.comp (CategoryTheory.forget (AlgCat R)))).pt
              Equations
                source
                instance AlgCat.limitAlgebra {R : Type u} [CommRing R] {J : Type v} [CategoryTheory.Category.{t, v} J] (F : CategoryTheory.Functor J (AlgCat R)) [Small.{w, max v w} ↑(F.comp (CategoryTheory.forget (AlgCat R))).sections] :
                Algebra R (CategoryTheory.Limits.Types.Small.limitCone (F.comp (CategoryTheory.forget (AlgCat R)))).pt
                Equations
                  source
                  def AlgCat.limitπAlgHom {R : Type u} [CommRing R] {J : Type v} [CategoryTheory.Category.{t, v} J] (F : CategoryTheory.Functor J (AlgCat R)) [Small.{w, max v w} ↑(F.comp (CategoryTheory.forget (AlgCat R))).sections] (j : J) :
                  (CategoryTheory.Limits.Types.Small.limitCone (F.comp (CategoryTheory.forget (AlgCat R)))).pt →ₐ[R] (F.comp (CategoryTheory.forget (AlgCat R))).obj j

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

                  Equations
                    Instances For
                      source
                      def AlgCat.HasLimits.limitCone {R : Type u} [CommRing R] {J : Type v} [CategoryTheory.Category.{t, v} J] (F : CategoryTheory.Functor J (AlgCat R)) [Small.{w, max v w} ↑(F.comp (CategoryTheory.forget (AlgCat R))).sections] :
                      CategoryTheory.Limits.Cone F

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

                      Equations
                        Instances For
                          source
                          def AlgCat.HasLimits.limitConeIsLimit {R : Type u} [CommRing R] {J : Type v} [CategoryTheory.Category.{t, v} J] (F : CategoryTheory.Functor J (AlgCat R)) [Small.{w, max v w} ↑(F.comp (CategoryTheory.forget (AlgCat R))).sections] :
                          CategoryTheory.Limits.IsLimit (limitCone F)

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

                          Equations
                            Instances For
                              source
                              theorem AlgCat.hasLimitsOfSize {R : Type u} [CommRing R] [UnivLE.{v, w}] :
                              CategoryTheory.Limits.HasLimitsOfSize.{t, v, w, max (w + 1) u} (AlgCat R)

                              The category of R-algebras has all limits.

                              source
                              instance AlgCat.hasLimits {R : Type u} [CommRing R] :
                              CategoryTheory.Limits.HasLimits (AlgCat R)
                              source
                              instance AlgCat.forget₂Ring_preservesLimitsOfSize {R : Type u} [CommRing R] [UnivLE.{v, w}] :
                              CategoryTheory.Limits.PreservesLimitsOfSize.{t, v, w, w, max u (w + 1), w + 1} (CategoryTheory.forget₂ (AlgCat R) RingCat)

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

                              source
                              instance AlgCat.forget₂Ring_preservesLimits {R : Type u} [CommRing R] :
                              CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget₂ (AlgCat R) RingCat)
                              source
                              instance AlgCat.forget₂Module_preservesLimitsOfSize {R : Type u} [CommRing R] [UnivLE.{v, w}] :
                              CategoryTheory.Limits.PreservesLimitsOfSize.{t, v, w, w, max u (w + 1), max u (w + 1)} (CategoryTheory.forget₂ (AlgCat R) (ModuleCat R))

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

                              source
                              instance AlgCat.forget₂Module_preservesLimits {R : Type u} [CommRing R] :
                              CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget₂ (AlgCat R) (ModuleCat R))
                              source
                              instance AlgCat.forget_preservesLimitsOfSize {R : Type u} [CommRing R] [UnivLE.{v, w}] :
                              CategoryTheory.Limits.PreservesLimitsOfSize.{t, v, w, w, max u (w + 1), w + 1} (CategoryTheory.forget (AlgCat R))

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

                              source
                              instance AlgCat.forget_preservesLimits {R : Type u} [CommRing R] :
                              CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget (AlgCat R))