mathlib documentation

algebra.category.Ring.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.

@[protected, instance]
Equations
def SemiRing.sections_subsemiring {J : Type v} [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
@[protected, instance]

The category of rings has all limits.

@[protected, instance]

We show that the forgetful functor CommSemiRingSemiRing 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

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

Equations
@[protected, instance]

The category of rings has all limits.

@[protected, instance]

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
@[protected, instance]
def Ring.ring_obj {J : Type v} [category_theory.small_category J] (F : J Ring) (j : J) :
Equations
def Ring.sections_subring {J : Type v} [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
@[protected, instance]

We show that the forgetful functor CommRingRing 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
noncomputable def Ring.limit_cone {J : Type v} [category_theory.small_category J] (F : J Ring) :

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

Equations

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

Equations
@[protected, instance]

The category of rings has all limits.

@[protected, instance]

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
@[protected, instance]
Equations
@[protected, instance]

We show that the forgetful functor CommRingRing 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

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

Equations
@[protected, instance]

The category of commutative rings has all limits.

@[protected, instance]

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
@[protected, instance]

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
@[protected, instance]

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