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]
def
Algebra.semiring_obj
{R : Type u}
[comm_ring R]
{J : Type u}
[category_theory.small_category J]
(F : J ⥤ Algebra R)
(j : J) :
semiring ((F ⋙ category_theory.forget (Algebra R)).obj j)
Equations
@[instance]
def
Algebra.algebra_obj
{R : Type u}
[comm_ring R]
{J : Type u}
[category_theory.small_category J]
(F : J ⥤ Algebra R)
(j : J) :
algebra R ((F ⋙ category_theory.forget (Algebra R)).obj j)
Equations
- Algebra.algebra_obj F j = id (F.obj j).is_algebra
def
Algebra.sections_subalgebra
{R : Type u}
[comm_ring R]
{J : Type u}
[category_theory.small_category J]
(F : J ⥤ Algebra R) :
subalgebra R (Π (j : J), ↥(F.obj j))
The flat sections of a functor into Algebra R form a submodule of all sections.
Equations
@[instance]
def
Algebra.limit_semiring
{R : Type u}
[comm_ring R]
{J : Type u}
[category_theory.small_category J]
(F : J ⥤ Algebra R) :
Equations
@[instance]
def
Algebra.limit_algebra
{R : Type u}
[comm_ring R]
{J : Type u}
[category_theory.small_category J]
(F : J ⥤ Algebra R) :
Equations
def
Algebra.limit_π_alg_hom
{R : Type u}
[comm_ring R]
{J : Type u}
[category_theory.small_category J]
(F : J ⥤ Algebra R)
(j : J) :
category_theory.limits.limit (F ⋙ category_theory.forget (Algebra R)) →ₐ[R] (F ⋙ category_theory.forget (Algebra R)).obj j
limit.π (F ⋙ forget (Algebra R)) j as a alg_hom.
Equations
- Algebra.limit_π_alg_hom F j = {to_fun := (SemiRing.limit_π_ring_hom (F ⋙ category_theory.forget₂ (Algebra R) Ring ⋙ category_theory.forget₂ Ring SemiRing) j).to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _}
def
Algebra.has_limits.limit
{R : Type u}
[comm_ring R]
{J : Type u}
[category_theory.small_category J]
(F : J ⥤ Algebra R) :
Construction of a limit cone in Algebra R.
(Internal use only; use the limits API.)
Equations
- Algebra.has_limits.limit F = {X := Algebra.of R (category_theory.limits.limit (F ⋙ category_theory.forget (Algebra R))) (Algebra.limit_algebra F), π := {app := Algebra.limit_π_alg_hom F, naturality' := _}}
def
Algebra.has_limits.limit_is_limit
{R : Type u}
[comm_ring R]
{J : Type u}
[category_theory.small_category J]
(F : J ⥤ Algebra R) :
Witness that the limit cone in Algebra R is a limit cone.
(Internal use only; use the limits API.)
Equations
- Algebra.has_limits.limit_is_limit F = category_theory.limits.is_limit.of_faithful (category_theory.forget (Algebra R)) (category_theory.limits.limit.is_limit (F ⋙ category_theory.forget (Algebra R))) (λ (s : category_theory.limits.cone F), {to_fun := λ (v : ((category_theory.forget (Algebra R)).map_cone s).X), ⟨λ (j : J), ((category_theory.forget (Algebra R)).map_cone s).π.app j v, _⟩, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _}) _
@[instance]
The category of R-algebras has all limits.
Equations
- Algebra.has_limits = {has_limits_of_shape := λ (J : Type u) (𝒥 : category_theory.small_category J), {has_limit := λ (F : J ⥤ Algebra R), {cone := Algebra.has_limits.limit F, is_limit := Algebra.has_limits.limit_is_limit F}}}
@[instance]
The forgetful functor from R-algebras to rings preserves all limits.
Equations
- Algebra.forget₂_Ring_preserves_limits = {preserves_limits_of_shape := λ (J : Type u) (𝒥 : category_theory.small_category J), {preserves_limit := λ (F : J ⥤ Algebra R), category_theory.limits.preserves_limit_of_preserves_limit_cone (category_theory.limits.limit.is_limit F) (category_theory.limits.limit.is_limit (F ⋙ category_theory.forget₂ (Algebra R) Ring))}}
@[instance]
The forgetful functor from R-algebras to R-modules preserves all limits.
Equations
- Algebra.forget₂_Module_preserves_limits = {preserves_limits_of_shape := λ (J : Type u) (𝒥 : category_theory.small_category J), {preserves_limit := λ (F : J ⥤ Algebra R), category_theory.limits.preserves_limit_of_preserves_limit_cone (category_theory.limits.limit.is_limit F) (category_theory.limits.limit.is_limit (F ⋙ category_theory.forget₂ (Algebra R) (Module R)))}}
@[instance]
The forgetful functor from R-algebras to types preserves all limits.
Equations
- Algebra.forget_preserves_limits = {preserves_limits_of_shape := λ (J : Type u) (𝒥 : category_theory.small_category J), {preserves_limit := λ (F : J ⥤ Algebra R), category_theory.limits.preserves_limit_of_preserves_limit_cone (category_theory.limits.limit.is_limit F) (category_theory.limits.limit.is_limit (F ⋙ category_theory.forget (Algebra R)))}}