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.

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

The category of rings has all limits.

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

The category of rings has all limits.

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

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

Equations
@[instance]

The category of rings has all limits.

@[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

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

Equations
@[instance]

The category of commutative rings has all limits.

@[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
@[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
@[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