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.

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

• AlgCat.semiringObj F j = inferInstanceAs (Semiring ↑(F.obj j))

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

• AlgCat.algebraObj F j = inferInstanceAs (Algebra R ↑(F.obj j))

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

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

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

• AlgCat.instRingElemForallObjCompForgetSections F = inferInstanceAs (Ring ↥(AlgCat.sectionsSubalgebra F))

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

• AlgCat.instAlgebraElemForallObjCompForgetSections F = inferInstanceAs (Algebra R ↥(AlgCat.sectionsSubalgebra F))

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)

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

• AlgCat.limitSemiring F = inferInstanceAs (Ring (Shrink.{?u.74, max ?u.75 ?u.74} ↥(AlgCat.sectionsSubalgebra F)))

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

• AlgCat.limitAlgebra F = inferInstanceAs (Algebra R (Shrink.{?u.73, max ?u.74 ?u.73} ↥(AlgCat.sectionsSubalgebra F)))

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

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

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

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

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

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

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.

instance AlgCat.hasLimits {R : Type u} [CommRing R] : CategoryTheory.Limits.HasLimits (AlgCat R)

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.

instance AlgCat.forget₂Ring_preservesLimits {R : Type u} [CommRing R] : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget₂ (AlgCat R) RingCat)

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.

instance AlgCat.forget₂Module_preservesLimits {R : Type u} [CommRing R] : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget₂ (AlgCat R) (ModuleCat R))

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.

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