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.
The flat sections of a functor into SemiRingCat
form a subsemiring of all sections.
Instances For
limit.π (F ⋙ forget SemiRingCat) j
as a RingHom
.
Instances For
Construction of a limit cone in SemiRingCat
.
(Internal use only; use the limits API.)
Instances For
Witness that the limit cone in SemiRingCat
is a limit cone.
(Internal use only; use the limits API.)
Instances For
The category of rings has all limits.
Auxiliary lemma to prove the cone induced by limitCone
is a limit cone.
Instances For
The forgetful functor from semirings to additive commutative monoids preserves all limits.
An auxiliary declaration to speed up typechecking.
Instances For
The forgetful functor from semirings to monoids preserves all limits.
The forgetful functor from semirings to types preserves all limits.
An alias for CommSemiring.{max u v}
, to deal with unification issues.
Instances For
We show that the forgetful functor CommSemiRingCat ⥤ SemiRingCat
creates limits.
All we need to do is notice that the limit point has a CommSemiring
instance available,
and then reuse the existing limit.
A choice of limit cone for a functor into CommSemiRingCat
.
(Generally, you'll just want to use limit F
.)
Instances For
The chosen cone is a limit cone.
(Generally, you'll just want to use limit.cone F
.)
Instances For
The category of rings has all limits.
The forgetful functor from rings to semirings preserves all limits.
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.)
An alias for RingCat.{max u v}
, to deal around unification issues.
Instances For
The flat sections of a functor into RingCat
form a subring of all sections.
Instances For
We show that the forgetful functor CommRingCat ⥤ RingCat
creates limits.
All we need to do is notice that the limit point has a Ring
instance available,
and then reuse the existing limit.
A choice of limit cone for a functor into RingCat
.
(Generally, you'll just want to use limit F
.)
Instances For
The chosen cone is a limit cone.
(Generally, you'll just want to use limit.cone F
.)
Instances For
The category of rings has all limits.
The forgetful functor from rings to semirings preserves all limits.
An auxiliary declaration to speed up typechecking.
Instances For
The forgetful functor from rings to additive commutative groups preserves all limits.
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.)
An alias for CommRingCat.{max u v}
, to deal around unification issues.
Instances For
We show that the forgetful functor CommRingCat ⥤ RingCat
creates limits.
All we need to do is notice that the limit point has a CommRing
instance available,
and then reuse the existing limit.
A choice of limit cone for a functor into CommRingCat
.
(Generally, you'll just want to use limit F
.)
Instances For
The chosen cone is a limit cone.
(Generally, you'll just want to use limit.cone F
.)
Instances For
The category of commutative rings has all limits.
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.)
An auxiliary declaration to speed up typechecking.
Instances For
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.)
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.)