The forgetful functor from (commutative) (additive) groups preserves filtered colimits. #
Forgetful functors from algebraic categories usually don't preserve colimits. However, they tend to preserve filtered colimits.
In this file, we start with a small filtered category J
and a functor F : J ⥤ GroupCat
.
We show that the colimit of F ⋙ forget₂ GroupCat MonCat
(in MonCat
) carries the structure of a
group,
thereby showing that the forgetful functor forget₂ GroupCat MonCat
preserves filtered colimits.
In particular, this implies that forget GroupCat
preserves filtered colimits.
Similarly for AddGroupCat
, CommGroupCat
and AddCommGroupCat
.
The colimit of F ⋙ forget₂ AddGroupCat AddMonCat
in the category AddMonCat
.
In the following, we will show that this has the structure of an additive group.
Equations
Instances For
The colimit of F ⋙ forget₂ GroupCat MonCat
in the category MonCat
.
In the following, we will show that this has the structure of a group.
Equations
Instances For
The canonical projection into the colimit, as a quotient type.
Equations
Instances For
The canonical projection into the colimit, as a quotient type.
Equations
Instances For
The "unlifted" version of negation in the colimit.
Equations
- AddGroupCat.FilteredColimits.colimitNegAux F x = AddGroupCat.FilteredColimits.G.mk F { fst := x.fst, snd := -x.snd }
Instances For
The "unlifted" version of taking inverses in the colimit.
Equations
- GroupCat.FilteredColimits.colimitInvAux F x = GroupCat.FilteredColimits.G.mk F { fst := x.fst, snd := x.snd⁻¹ }
Instances For
Negation in the colimit. See also colimitNegAux
.
Equations
- AddGroupCat.FilteredColimits.colimitNeg F = { neg := fun (x : ↑(AddGroupCat.FilteredColimits.G F)) => Quot.lift (AddGroupCat.FilteredColimits.colimitNegAux F) ⋯ x }
Taking inverses in the colimit. See also colimitInvAux
.
Equations
- GroupCat.FilteredColimits.colimitInv F = { inv := fun (x : ↑(GroupCat.FilteredColimits.G F)) => Quot.lift (GroupCat.FilteredColimits.colimitInvAux F) ⋯ x }
Equations
- AddGroupCat.FilteredColimits.colimitAddGroup F = let __src := AddGroupCat.FilteredColimits.colimitNeg F; let __src_1 := (AddGroupCat.FilteredColimits.G F).str; AddGroup.mk ⋯
Equations
- GroupCat.FilteredColimits.colimitGroup F = let __src := GroupCat.FilteredColimits.colimitInv F; let __src_1 := (GroupCat.FilteredColimits.G F).str; Group.mk ⋯
The bundled additive group giving the filtered colimit of a diagram.
Equations
Instances For
The bundled group giving the filtered colimit of a diagram.
Equations
Instances For
The cocone over the proposed colimit additive group.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The cocone over the proposed colimit group.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The proposed colimit cocone is a colimit in AddGroup
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The proposed colimit cocone is a colimit in GroupCat
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
The colimit of F ⋙ forget₂ AddCommGroupCat AddGroupCat
in the category AddGroupCat
.
In the following, we will show that this has the structure of a commutative additive group.
Equations
Instances For
The colimit of F ⋙ forget₂ CommGroupCat GroupCat
in the category GroupCat
.
In the following, we will show that this has the structure of a commutative group.
Equations
Instances For
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
The bundled additive commutative group giving the filtered colimit of a diagram.
Equations
Instances For
The bundled commutative group giving the filtered colimit of a diagram.
Equations
Instances For
The cocone over the proposed colimit additive commutative group.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The cocone over the proposed colimit commutative group.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The proposed colimit cocone is a colimit in AddCommGroup
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The proposed colimit cocone is a colimit in CommGroupCat
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.