mathlib documentation

algebra.category.CommRing.limits

The category of (commutative) rings 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
@[protected, instance]
def SemiRing.semiring_obj {J : Type u} [category_theory.small_category J] (F : J ⥤ SemiRing) (j : J) :
semiring ((F ⋙ category_theory.forget SemiRing).obj j)
Equations
source
def SemiRing.sections_subsemiring {J : Type u} [category_theory.small_category J] (F : J ⥤ SemiRing) :
subsemiring (Π (j : J), ↥(F.obj j))

The flat sections of a functor into SemiRing form a subsemiring of all sections.

Equations
source
@[protected, instance]
def SemiRing.limit_semiring {J : Type u} [category_theory.small_category J] (F : J ⥤ SemiRing) :
semiring (category_theory.limits.types.limit_cone (F ⋙ category_theory.forget SemiRing)).X
Equations
source
def SemiRing.limit_π_ring_hom {J : Type u} [category_theory.small_category J] (F : J ⥤ SemiRing) (j : J) :
(category_theory.limits.types.limit_cone (F ⋙ category_theory.forget SemiRing)).X →+* (F ⋙ category_theory.forget SemiRing).obj j

limit.π (F ⋙ forget SemiRing) j as a ring_hom.

Equations
source
def SemiRing.has_limits.limit_cone {J : Type u} [category_theory.small_category J] (F : J ⥤ SemiRing) :
category_theory.limits.cone F

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

Equations
source
def SemiRing.has_limits.limit_cone_is_limit {J : Type u} [category_theory.small_category J] (F : J ⥤ SemiRing) :
category_theory.limits.is_limit (SemiRing.has_limits.limit_cone F)

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

Equations
source
@[protected, instance]
def SemiRing.has_limits  :
category_theory.limits.has_limits SemiRing

The category of rings has all limits.

source
def SemiRing.forget₂_AddCommMon_preserves_limits_aux {J : Type u} [category_theory.small_category J] (F : J ⥤ SemiRing) :
category_theory.limits.is_limit ((category_theory.forget₂ SemiRing AddCommMon).map_cone (SemiRing.has_limits.limit_cone F))

An auxiliary declaration to speed up typechecking.

Equations
source
@[protected, instance]
def SemiRing.forget₂_AddCommMon_preserves_limits  :
category_theory.limits.preserves_limits (category_theory.forget₂ SemiRing AddCommMon)

The forgetful functor from semirings to additive commutative monoids preserves all limits.

Equations
source
def SemiRing.forget₂_Mon_preserves_limits_aux {J : Type u} [category_theory.small_category J] (F : J ⥤ SemiRing) :
category_theory.limits.is_limit ((category_theory.forget₂ SemiRing Mon).map_cone (SemiRing.has_limits.limit_cone F))

An auxiliary declaration to speed up typechecking.

Equations
source
@[protected, instance]
def SemiRing.forget₂_Mon_preserves_limits  :
category_theory.limits.preserves_limits (category_theory.forget₂ SemiRing Mon)

The forgetful functor from semirings to monoids preserves all limits.

Equations
source
@[protected, instance]
def SemiRing.forget_preserves_limits  :
category_theory.limits.preserves_limits (category_theory.forget SemiRing)

The forgetful functor from semirings to types preserves all limits.

Equations
source
@[protected, instance]
def CommSemiRing.comm_semiring_obj {J : Type u} [category_theory.small_category J] (F : J ⥤ CommSemiRing) (j : J) :
comm_semiring ((F ⋙ category_theory.forget CommSemiRing).obj j)
Equations
source
@[protected, instance]
def CommSemiRing.limit_comm_semiring {J : Type u} [category_theory.small_category J] (F : J ⥤ CommSemiRing) :
comm_semiring (category_theory.limits.types.limit_cone (F ⋙ category_theory.forget CommSemiRing)).X
Equations
source
@[protected, instance]
def CommSemiRing.category_theory.forget₂.category_theory.creates_limit {J : Type u} [category_theory.small_category J] (F : J ⥤ CommSemiRing) :
category_theory.creates_limit F (category_theory.forget₂ CommSemiRing SemiRing)

We show that the forgetful functor CommSemiRing ⥤ SemiRing creates limits.

All we need to do is notice that the limit point has a comm_semiring instance available, and then reuse the existing limit.

Equations
source
def CommSemiRing.limit_cone {J : Type u} [category_theory.small_category J] (F : J ⥤ CommSemiRing) :
category_theory.limits.cone F

A choice of limit cone for a functor into CommSemiRing. (Generally, you'll just want to use limit F.)

Equations
source
def CommSemiRing.limit_cone_is_limit {J : Type u} [category_theory.small_category J] (F : J ⥤ CommSemiRing) :
category_theory.limits.is_limit (CommSemiRing.limit_cone F)

The chosen cone is a limit cone. (Generally, you'll just want to use limit.cone F.)

Equations
source
@[protected, instance]
def CommSemiRing.has_limits  :
category_theory.limits.has_limits CommSemiRing

The category of rings has all limits.

source
@[protected, instance]
def CommSemiRing.forget₂_SemiRing_preserves_limits  :
category_theory.limits.preserves_limits (category_theory.forget₂ CommSemiRing SemiRing)

The forgetful functor from rings to semirings preserves all limits.

Equations
source
@[protected, instance]
def CommSemiRing.forget_preserves_limits  :
category_theory.limits.preserves_limits (category_theory.forget CommSemiRing)

The forgetful functor from rings to types preserves all limits. (That is, the underlying types could have been computed instead as limits in the category of types.)

Equations
source
@[protected, instance]
def Ring.ring_obj {J : Type u} [category_theory.small_category J] (F : J ⥤ Ring) (j : J) :
ring ((F ⋙ category_theory.forget Ring).obj j)
Equations
source
def Ring.sections_subring {J : Type u} [category_theory.small_category J] (F : J ⥤ Ring) :
subring (Π (j : J), ↥(F.obj j))

The flat sections of a functor into Ring form a subring of all sections.

Equations
source
@[protected, instance]
def Ring.limit_ring {J : Type u} [category_theory.small_category J] (F : J ⥤ Ring) :
ring (category_theory.limits.types.limit_cone (F ⋙ category_theory.forget Ring)).X
Equations
source
@[protected, instance]
def Ring.category_theory.forget₂.category_theory.creates_limit {J : Type u} [category_theory.small_category J] (F : J ⥤ Ring) :
category_theory.creates_limit F (category_theory.forget₂ Ring SemiRing)

We show that the forgetful functor CommRing ⥤ Ring creates limits.

All we need to do is notice that the limit point has a ring instance available, and then reuse the existing limit.

Equations
source
def Ring.limit_cone {J : Type u} [category_theory.small_category J] (F : J ⥤ Ring) :
category_theory.limits.cone F

A choice of limit cone for a functor into Ring. (Generally, you'll just want to use limit F.)

Equations
source
def Ring.limit_cone_is_limit {J : Type u} [category_theory.small_category J] (F : J ⥤ Ring) :
category_theory.limits.is_limit (Ring.limit_cone F)

The chosen cone is a limit cone. (Generally, you'll just want to use limit.cone F.)

Equations
source
@[protected, instance]
def Ring.has_limits  :
category_theory.limits.has_limits Ring

The category of rings has all limits.

source
@[protected, instance]
def Ring.forget₂_SemiRing_preserves_limits  :
category_theory.limits.preserves_limits (category_theory.forget₂ Ring SemiRing)

The forgetful functor from rings to semirings preserves all limits.

Equations
source
def Ring.forget₂_AddCommGroup_preserves_limits_aux {J : Type u} [category_theory.small_category J] (F : J ⥤ Ring) :
category_theory.limits.is_limit ((category_theory.forget₂ Ring AddCommGroup).map_cone (Ring.limit_cone F))

An auxiliary declaration to speed up typechecking.

Equations
source
@[protected, instance]
def Ring.forget₂_AddCommGroup_preserves_limits  :
category_theory.limits.preserves_limits (category_theory.forget₂ Ring AddCommGroup)

The forgetful functor from rings to additive commutative groups preserves all limits.

Equations
source
@[protected, instance]
def Ring.forget_preserves_limits  :
category_theory.limits.preserves_limits (category_theory.forget Ring)

The forgetful functor from rings to types preserves all limits. (That is, the underlying types could have been computed instead as limits in the category of types.)

Equations
source
@[protected, instance]
def CommRing.comm_ring_obj {J : Type u} [category_theory.small_category J] (F : J ⥤ CommRing) (j : J) :
comm_ring ((F ⋙ category_theory.forget CommRing).obj j)
Equations
source
@[protected, instance]
def CommRing.limit_comm_ring {J : Type u} [category_theory.small_category J] (F : J ⥤ CommRing) :
comm_ring (category_theory.limits.types.limit_cone (F ⋙ category_theory.forget CommRing)).X
Equations
source
@[protected, instance]
def CommRing.category_theory.forget₂.category_theory.creates_limit {J : Type u} [category_theory.small_category J] (F : J ⥤ CommRing) :
category_theory.creates_limit F (category_theory.forget₂ CommRing Ring)

We show that the forgetful functor CommRing ⥤ Ring creates limits.

All we need to do is notice that the limit point has a comm_ring instance available, and then reuse the existing limit.

Equations
source
def CommRing.limit_cone {J : Type u} [category_theory.small_category J] (F : J ⥤ CommRing) :
category_theory.limits.cone F

A choice of limit cone for a functor into CommRing. (Generally, you'll just want to use limit F.)

Equations
source
def CommRing.limit_cone_is_limit {J : Type u} [category_theory.small_category J] (F : J ⥤ CommRing) :
category_theory.limits.is_limit (CommRing.limit_cone F)

The chosen cone is a limit cone. (Generally, you'll just want to use limit.cone F.)

Equations
source
@[protected, instance]
def CommRing.has_limits  :
category_theory.limits.has_limits CommRing

The category of commutative rings has all limits.

source
@[protected, instance]
def CommRing.forget₂_Ring_preserves_limits  :
category_theory.limits.preserves_limits (category_theory.forget₂ CommRing Ring)

The forgetful functor from commutative rings to rings preserves all limits. (That is, the underlying rings could have been computed instead as limits in the category of rings.)

Equations
source
def CommRing.forget₂_CommSemiRing_preserves_limits_aux {J : Type u} [category_theory.small_category J] (F : J ⥤ CommRing) :
category_theory.limits.is_limit ((category_theory.forget₂ CommRing CommSemiRing).map_cone (CommRing.limit_cone F))

An auxiliary declaration to speed up typechecking.

Equations
source
@[protected, instance]
def CommRing.forget₂_CommSemiRing_preserves_limits  :
category_theory.limits.preserves_limits (category_theory.forget₂ CommRing CommSemiRing)

The forgetful functor from commutative rings to commutative semirings preserves all limits. (That is, the underlying commutative semirings could have been computed instead as limits in the category of commutative semirings.)

Equations
source
@[protected, instance]
def CommRing.forget_preserves_limits  :
category_theory.limits.preserves_limits (category_theory.forget CommRing)

The forgetful functor from commutative rings to types preserves all limits. (That is, the underlying types could have been computed instead as limits in the category of types.)

Equations