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
- Grp.groupObj F j = inferInstanceAs (Group ↑(F.obj j))
Equations
- AddGrp.addGroupObj F j = inferInstanceAs (AddGroup ↑(F.obj j))
The flat sections of a functor into Grp
form a subgroup of all sections.
Equations
- Grp.sectionsSubgroup F = { carrier := (F.comp (CategoryTheory.forget Grp)).sections, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }
Instances For
The flat sections of a functor into AddGrp
form an additive subgroup of all sections.
Equations
- AddGrp.sectionsAddSubgroup F = { carrier := (F.comp (CategoryTheory.forget AddGrp)).sections, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }
Instances For
Equations
- Grp.sectionsGroup F = (Grp.sectionsSubgroup F).toGroup
Equations
- AddGrp.sectionsAddGroup F = (AddGrp.sectionsAddSubgroup F).toAddGroup
The projection from Functor.sections
to a factor as a MonoidHom
.
Equations
- Grp.sectionsπMonoidHom F j = { toFun := fun (x : ↑(F.comp (CategoryTheory.forget Grp)).sections) => ↑x j, map_one' := ⋯, map_mul' := ⋯ }
Instances For
The projection from Functor.sections
to a factor as an AddMonoidHom
.
Equations
- AddGrp.sectionsπAddMonoidHom F j = { toFun := fun (x : ↑(F.comp (CategoryTheory.forget AddGrp)).sections) => ↑x j, map_zero' := ⋯, map_add' := ⋯ }
Instances For
Equations
- Grp.limitGroup F = inferInstanceAs (Group (Shrink.{?u.41, max ?u.41 ?u.42} ↑(F.comp (CategoryTheory.forget Grp)).sections))
Equations
- AddGrp.limitAddGroup F = inferInstanceAs (AddGroup (Shrink.{?u.41, max ?u.41 ?u.42} ↑(F.comp (CategoryTheory.forget AddGrp)).sections))
We show that the forgetful functor Grp ⥤ 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 AddGrp ⥤ 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 Grp
.
(Generally, you'll just want to use limit F
.)
Equations
Instances For
A choice of limit cone for a functor into Grp
.
(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 Grp).sections
is u
-small, F
has a limit.
If (F ⋙ forget AddGrp).sections
is u
-small, F
has a limit.
A functor F : J ⥤ Grp.{u}
has a limit iff (F ⋙ forget Grp).sections
is
u
-small.
A functor F : J ⥤ AddGrp.{u}
has a limit iff
(F ⋙ forget AddGrp).sections
is u
-small.
If J
is u
-small, Grp.{u}
has limits of shape J
.
If J
is u
-small, AddGrp.{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 Grp.{u}
preserves limits of shape J
.
If J
is u
-small, the forgetful functor from AddGrp.{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
- Grp.forget_createsLimitsOfShape = { CreatesLimit := fun {K : CategoryTheory.Functor J Grp} => inferInstance }
Equations
- AddGrp.forget_createsLimitsOfShape = { CreatesLimit := fun {K : CategoryTheory.Functor J AddGrp} => inferInstance }
The forgetful functor from groups to types creates all limits.
Equations
- Grp.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
- AddGrp.forget_createsLimitsOfSize = { CreatesLimitsOfShape := fun {J : Type ?u.6} [CategoryTheory.Category.{?u.4, ?u.6} J] => inferInstance }
Equations
- CommGrp.commGroupObj F j = inferInstanceAs (CommGroup ↑(F.obj j))
Equations
- AddCommGrp.addCommGroupObj F j = inferInstanceAs (AddCommGroup ↑(F.obj j))
Equations
- CommGrp.limitCommGroup F = inferInstanceAs (CommGroup (Shrink.{?u.41, max ?u.41 ?u.42} ↑(F.comp (CategoryTheory.forget CommGrp)).sections))
Equations
- AddCommGrp.limitAddCommGroup F = inferInstanceAs (AddCommGroup (Shrink.{?u.41, max ?u.41 ?u.42} ↑(F.comp (CategoryTheory.forget AddCommGrp)).sections))
We show that the forgetful functor CommGrp ⥤ Grp
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 AddCommGrp ⥤ AddGrp
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 CommGrp
.
(Generally, you'll just want to use limit F
.)
Equations
Instances For
A choice of limit cone for a functor into AddCommGrp
.
(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 CommGrp).sections
is u
-small, F
has a limit.
If (F ⋙ forget AddCommGrp).sections
is u
-small, F
has a limit.
A functor F : J ⥤ CommGrp.{u}
has a limit iff (F ⋙ forget CommGrp).sections
is
u
-small.
A functor F : J ⥤ AddCommGrp.{u}
has a limit iff
(F ⋙ forget AddCommGrp).sections
is u
-small.
If J
is u
-small, CommGrp.{u}
has limits of shape J
.
If J
is u
-small, AddCommGrp.{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 CommGrp.{u}
to CommMonCat.{u}
preserves limits of shape J
.
If J
is u
-small, the forgetful functor from AddCommGrp.{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 CommGrp.{u}
preserves limits of
shape J
.
If J
is u
-small, the forgetful functor from AddCommGrp.{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
- CommGrp.forget_createsLimitsOfShape J = { CreatesLimit := fun {K : CategoryTheory.Functor J CommGrp} => inferInstance }
Equations
- AddCommGrp.forget_createsLimitsOfShape J = { CreatesLimit := fun {K : CategoryTheory.Functor J AddCommGrp} => inferInstance }
The forgetful functor from commutative groups to types creates all limits.
Equations
- CommGrp.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
- AddCommGrp.forget_createsLimitsOfSize = { CreatesLimitsOfShape := fun {J : Type ?u.6} [CategoryTheory.Category.{?u.4, ?u.6} J] => inferInstance }
The categorical kernel of a morphism in AddCommGrp
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.