The category of R-algebras has all limits #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
Further, these limits are preserved by the forgetful functor --- that is, the underlying types are just the limits in the category of types.
@[protected, instance]
def
Algebra.semiring_obj
{R : Type u}
[comm_ring R]
{J : Type v}
[category_theory.small_category J]
(F : J ⥤ Algebra R)
(j : J) :
semiring ((F ⋙ category_theory.forget (Algebra R)).obj j)
Equations
@[protected, instance]
def
Algebra.algebra_obj
{R : Type u}
[comm_ring R]
{J : Type v}
[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 v}
[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
- Algebra.sections_subalgebra F = {carrier := (SemiRing.sections_subsemiring (F ⋙ category_theory.forget₂ (Algebra R) Ring ⋙ category_theory.forget₂ Ring SemiRing)).carrier, mul_mem' := _, one_mem' := _, add_mem' := _, zero_mem' := _, algebra_map_mem' := _}
@[protected, instance]
def
Algebra.limit_semiring
{R : Type u}
[comm_ring R]
{J : Type v}
[category_theory.small_category J]
(F : J ⥤ Algebra R) :
Equations
@[protected, instance]
def
Algebra.limit_algebra
{R : Type u}
[comm_ring R]
{J : Type v}
[category_theory.small_category J]
(F : J ⥤ Algebra R) :
Equations
def
Algebra.limit_π_alg_hom
{R : Type u}
[comm_ring R]
{J : Type v}
[category_theory.small_category J]
(F : J ⥤ Algebra R)
(j : J) :
(category_theory.limits.types.limit_cone (F ⋙ category_theory.forget (Algebra R))).X →ₐ[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_cone
{R : Type u}
[comm_ring R]
{J : Type v}
[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_cone F = {X := Algebra.of R (category_theory.limits.types.limit_cone (F ⋙ category_theory.forget (Algebra R))).X (Algebra.limit_algebra F), π := {app := Algebra.limit_π_alg_hom F, naturality' := _}}
def
Algebra.has_limits.limit_cone_is_limit
{R : Type u}
[comm_ring R]
{J : Type v}
[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_cone_is_limit F = category_theory.limits.is_limit.of_faithful (category_theory.forget (Algebra R)) (category_theory.limits.types.limit_cone_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' := _}) _
@[protected, instance, irreducible]
The category of R-algebras has all limits.
@[protected, instance]
@[protected, instance]
The forgetful functor from R-algebras to rings preserves all limits.
Equations
- Algebra.forget₂_Ring_preserves_limits_of_size = {preserves_limits_of_shape := λ (J : Type v) (𝒥 : category_theory.category J), {preserves_limit := λ (F : J ⥤ Algebra R), category_theory.limits.preserves_limit_of_preserves_limit_cone (Algebra.has_limits.limit_cone_is_limit F) (Ring.limit_cone_is_limit (F ⋙ category_theory.forget₂ (Algebra R) Ring))}}
@[protected, instance]
@[protected, instance]
The forgetful functor from R-algebras to R-modules preserves all limits.
Equations
- Algebra.forget₂_Module_preserves_limits_of_size = {preserves_limits_of_shape := λ (J : Type v) (𝒥 : category_theory.category J), {preserves_limit := λ (F : J ⥤ Algebra R), category_theory.limits.preserves_limit_of_preserves_limit_cone (Algebra.has_limits.limit_cone_is_limit F) (Module.has_limits.limit_cone_is_limit (F ⋙ category_theory.forget₂ (Algebra R) (Module R)))}}
@[protected, instance]
@[protected, instance]
The forgetful functor from R-algebras to types preserves all limits.
Equations
- Algebra.forget_preserves_limits_of_size = {preserves_limits_of_shape := λ (J : Type v) (𝒥 : category_theory.category J), {preserves_limit := λ (F : J ⥤ Algebra R), category_theory.limits.preserves_limit_of_preserves_limit_cone (Algebra.has_limits.limit_cone_is_limit F) (category_theory.limits.types.limit_cone_is_limit (F ⋙ category_theory.forget (Algebra R)))}}
@[protected, instance]