The category of (commutative) (additive) groups 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.
Equations
- GrpCat.groupObj F j = inferInstanceAs (Group ↑(F.obj j))
Equations
- AddGrpCat.addGroupObj F j = inferInstanceAs (AddGroup ↑(F.obj j))
The flat sections of a functor into GrpCat
form a subgroup of all sections.
Equations
- GrpCat.sectionsSubgroup F = { carrier := (F.comp (CategoryTheory.forget GrpCat)).sections, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }
Instances For
The flat sections of a functor into AddGrpCat
form an additive subgroup of all sections.
Equations
- AddGrpCat.sectionsAddSubgroup F = { carrier := (F.comp (CategoryTheory.forget AddGrpCat)).sections, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }
Instances For
Equations
Equations
The projection from Functor.sections
to a factor as a MonoidHom
.
Equations
- GrpCat.sectionsπMonoidHom F j = { toFun := fun (x : ↑(F.comp (CategoryTheory.forget GrpCat)).sections) => ↑x j, map_one' := ⋯, map_mul' := ⋯ }
Instances For
The projection from Functor.sections
to a factor as an AddMonoidHom
.
Equations
- AddGrpCat.sectionsπAddMonoidHom F j = { toFun := fun (x : ↑(F.comp (CategoryTheory.forget AddGrpCat)).sections) => ↑x j, map_zero' := ⋯, map_add' := ⋯ }
Instances For
Equations
Equations
We show that the forgetful functor GrpCat ⥤ MonCat
creates limits.
All we need to do is notice that the limit point has a Group
instance available, and then reuse
the existing limit.
Equations
- One or more equations did not get rendered due to their size.
We show that the forgetful functor AddGrpCat ⥤ AddMonCat
creates limits.
All we need to do is notice that the limit point has an AddGroup
instance available, and then
reuse the existing limit.
Equations
- One or more equations did not get rendered due to their size.
A choice of limit cone for a functor into GrpCat
.
(Generally, you'll just want to use limit F
.)
Equations
Instances For
A choice of limit cone for a functor into GrpCat
.
(Generally, you'll just want to use limit F
.)
Equations
Instances For
The chosen cone is a limit cone.
(Generally, you'll just want to use limit.cone F
.)
Equations
Instances For
The chosen cone is a limit cone.
(Generally, you'll just want to use limit.cone F
.)
Equations
Instances For
If (F ⋙ forget GrpCat).sections
is u
-small, F
has a limit.
If (F ⋙ forget AddGrpCat).sections
is u
-small, F
has a limit.
A functor F : J ⥤ GrpCat.{u}
has a limit iff (F ⋙ forget GrpCat).sections
is
u
-small.
A functor F : J ⥤ AddGrpCat.{u}
has a limit iff
(F ⋙ forget AddGrpCat).sections
is u
-small.
If J
is u
-small, GrpCat.{u}
has limits of shape J
.
If J
is u
-small, AddGrpCat.{u}
has limits of shape J
.
The category of groups has all limits.
The category of additive groups has all limits.
The forgetful functor from groups to monoids preserves all limits.
This means the underlying monoid of a limit can be computed as a limit in the category of monoids.
The forgetful functor from additive groups to additive monoids preserves all limits.
This means the underlying additive monoid of a limit can be computed as a limit in the category of additive monoids.
If J
is u
-small, the forgetful functor from GrpCat.{u}
preserves limits of shape J
.
If J
is u
-small, the forgetful functor from AddGrpCat.{u}
preserves limits
of shape J
.
The forgetful functor from groups 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 additive groups to types preserves all limits.
This means the underlying type of a limit can be computed as a limit in the category of types.
Equations
- GrpCat.forget_createsLimitsOfShape = { CreatesLimit := fun {K : CategoryTheory.Functor J GrpCat} => inferInstance }
Equations
- AddGrpCat.forget_createsLimitsOfShape = { CreatesLimit := fun {K : CategoryTheory.Functor J AddGrpCat} => inferInstance }
The forgetful functor from groups to types creates all limits.
Equations
- GrpCat.forget_createsLimitsOfSize = { CreatesLimitsOfShape := fun {J : Type ?u.6} [CategoryTheory.Category.{?u.4, ?u.6} J] => inferInstance }
The forgetful functor from additive groups to types creates all limits.
Equations
- AddGrpCat.forget_createsLimitsOfSize = { CreatesLimitsOfShape := fun {J : Type ?u.6} [CategoryTheory.Category.{?u.4, ?u.6} J] => inferInstance }
Equations
- CommGrpCat.commGroupObj F j = inferInstanceAs (CommGroup ↑(F.obj j))
Equations
- AddCommGrpCat.addCommGroupObj F j = inferInstanceAs (AddCommGroup ↑(F.obj j))
We show that the forgetful functor CommGrpCat ⥤ GrpCat
creates limits.
All we need to do is notice that the limit point has a CommGroup
instance available,
and then reuse the existing limit.
Equations
- One or more equations did not get rendered due to their size.
We show that the forgetful functor AddCommGrpCat ⥤ AddGrpCat
creates limits.
All we need to do is notice that the limit point has an AddCommGroup
instance available,
and then reuse the existing limit.
Equations
- One or more equations did not get rendered due to their size.
A choice of limit cone for a functor into CommGrpCat
.
(Generally, you'll just want to use limit F
.)
Equations
Instances For
A choice of limit cone for a functor into AddCommGrpCat
.
(Generally, you'll just want to use limit F
.)
Equations
Instances For
The chosen cone is a limit cone.
(Generally, you'll just want to use limit.cone F
.)
Equations
Instances For
The chosen cone is a limit cone.
(Generally, you'll just want to use limit.cone F
.)
Equations
Instances For
If (F ⋙ forget CommGrpCat).sections
is u
-small, F
has a limit.
If (F ⋙ forget AddCommGrpCat).sections
is u
-small, F
has a limit.
A functor F : J ⥤ CommGrpCat.{u}
has a limit iff (F ⋙ forget CommGrpCat).sections
is
u
-small.
A functor F : J ⥤ AddCommGrpCat.{u}
has a limit iff
(F ⋙ forget AddCommGrpCat).sections
is u
-small.
If J
is u
-small, CommGrpCat.{u}
has limits of shape J
.
If J
is u
-small, AddCommGrpCat.{u}
has limits of shape J
.
The category of commutative groups has all limits.
The category of additive commutative groups has all limits.
The forgetful functor from commutative groups to groups preserves all limits. (That is, the underlying group could have been computed instead as limits in the category of groups.)
The forgetful functor from additive commutative groups to additive groups preserves all limits. (That is, the underlying group could have been computed instead as limits in the category of additive groups.)
An auxiliary declaration to speed up typechecking.
Equations
Instances For
An auxiliary declaration to speed up typechecking.
Equations
Instances For
If J
is u
-small, the forgetful functor from CommGrpCat.{u}
to CommMonCat.{u}
preserves limits of shape J
.
If J
is u
-small, the forgetful functor from AddCommGrpCat.{u}
to AddCommMonCat.{u}
preserves limits of shape J
.
The forgetful functor from commutative groups to commutative monoids preserves all limits. (That is, the underlying commutative monoids could have been computed instead as limits in the category of commutative monoids.)
The forgetful functor from additive commutative groups to additive commutative monoids preserves all limits. (That is, the underlying additive commutative monoids could have been computed instead as limits in the category of additive commutative monoids.)
If J
is u
-small, the forgetful functor from CommGrpCat.{u}
preserves limits of
shape J
.
If J
is u
-small, the forgetful functor from AddCommGrpCat.{u}
preserves limits of shape J
.
The forgetful functor from commutative groups to types preserves all limits. (That is, the underlying types could have been computed instead as limits in the category of types.)
The forgetful functor from additive commutative groups to types preserves all limits. (That is, the underlying types could have been computed instead as limits in the category of types.)
Equations
- CommGrpCat.forget_createsLimitsOfShape J = { CreatesLimit := fun {K : CategoryTheory.Functor J CommGrpCat} => inferInstance }
Equations
- AddCommGrpCat.forget_createsLimitsOfShape J = { CreatesLimit := fun {K : CategoryTheory.Functor J AddCommGrpCat} => inferInstance }
The forgetful functor from commutative groups to types creates all limits.
Equations
- CommGrpCat.forget_createsLimitsOfSize = { CreatesLimitsOfShape := fun {J : Type ?u.6} [CategoryTheory.Category.{?u.4, ?u.6} J] => inferInstance }
The forgetful functor from additive commutative groups to types creates all limits.
Equations
- AddCommGrpCat.forget_createsLimitsOfSize = { CreatesLimitsOfShape := fun {J : Type ?u.6} [CategoryTheory.Category.{?u.4, ?u.6} J] => inferInstance }
The categorical kernel of a morphism in AddCommGrpCat
agrees with the usual group-theoretical kernel.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The categorical kernel inclusion for f : G ⟶ H
, as an object over G
,
agrees with the AddSubgroup.subtype
map.