The category of (commutative) (additive) monoids 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.
An alias for AddMonCat.{max u v}
, to deal around unification issues.
Instances For
The flat sections of a functor into AddMonCat
form an additive submonoid of all sections.
Instances For
The flat sections of a functor into MonCat
form a submonoid of all sections.
Instances For
limit.π (F ⋙ forget AddMonCat) j
as an AddMonoidHom
.
Instances For
limit.π (F ⋙ forget MonCat) j
as a MonoidHom
.
Instances For
(Internal use only; use the limits API.)
Instances For
Construction of a limit cone in MonCat
.
(Internal use only; use the limits API.)
Instances For
(Internal use only; use the limits API.)
Instances For
Witness that the limit cone in MonCat
is a limit cone.
(Internal use only; use the limits API.)
Instances For
The category of additive monoids has all limits.
The category of monoids has all limits.
The forgetful functor from additive monoids to types preserves all limits.
This means the underlying type of a limit can be computed as a limit in the category of types.
The forgetful functor from monoids to types preserves all limits.
This means the underlying type of a limit can be computed as a limit in the category of types.
An alias for AddCommMonCat.{max u v}
, to deal around unification issues.
Instances For
An alias for CommMonCat.{max u v}
, to deal around unification issues.
Instances For
We show that the forgetful functor AddCommMonCat ⥤ AddMonCat
creates limits.
All we need to do is notice that the limit point has an AddCommMonoid
instance available,
and then reuse the existing limit.
We show that the forgetful functor CommMonCat ⥤ MonCat
creates limits.
All we need to do is notice that the limit point has a CommMonoid
instance available,
and then reuse the existing limit.
A choice of limit cone for a functor into AddCommMonCat
.
(Generally, you'll just want to use limit F
.)
Instances For
A choice of limit cone for a functor into CommMonCat
.
(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 chosen cone is a limit cone.
(Generally, you'll just want to use limit.cone F
.)
Instances For
The category of additive commutative monoids has all limits.
The category of commutative monoids has all limits.
The forgetful functor from additive
commutative monoids to additive monoids preserves all limits.
This means the underlying type of a limit can be computed as a limit in the category of additive
monoids.
The forgetful functor from commutative monoids to monoids preserves all limits.
This means the underlying type of a limit can be computed as a limit in the category of monoids.
The forgetful functor from additive commutative monoids to types preserves all
limits.
This means the underlying type of a limit can be computed as a limit in the category of types.
The forgetful functor from commutative monoids to types preserves all limits.
This means the underlying type of a limit can be computed as a limit in the category of types.