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 ⥤ Grp
.
We show that the colimit of F ⋙ forget₂ Grp MonCat
(in MonCat
) carries the structure of a
group,
thereby showing that the forgetful functor forget₂ Grp MonCat
preserves filtered colimits.
In particular, this implies that forget Grp
preserves filtered colimits.
Similarly for AddGrp
, CommGrp
and AddCommGrp
.
The colimit of F ⋙ forget₂ Grp MonCat
in the category MonCat
.
In the following, we will show that this has the structure of a group.
Equations
Instances For
The colimit of F ⋙ forget₂ AddGrp AddMonCat
in the category AddMonCat
.
In the following, we will show that this has the structure of an additive 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 taking inverses in the colimit.
Equations
Instances For
The "unlifted" version of negation in the colimit.
Equations
Instances For
Taking inverses in the colimit. See also colimitInvAux
.
Equations
- Grp.FilteredColimits.colimitInv F = { inv := fun (x : ↑(Grp.FilteredColimits.G F)) => Quot.lift (Grp.FilteredColimits.colimitInvAux F) ⋯ x }
Negation in the colimit. See also colimitNegAux
.
Equations
- AddGrp.FilteredColimits.colimitNeg F = { neg := fun (x : ↑(AddGrp.FilteredColimits.G F)) => Quot.lift (AddGrp.FilteredColimits.colimitNegAux F) ⋯ x }
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 group giving the filtered colimit of a diagram.
Equations
Instances For
The bundled additive group giving the filtered colimit of a diagram.
Equations
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 cocone over the proposed colimit additive group.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The proposed colimit cocone is a colimit in Grp
.
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 colimit of F ⋙ forget₂ CommGrp Grp
in the category Grp
.
In the following, we will show that this has the structure of a commutative group.
Equations
Instances For
The colimit of F ⋙ forget₂ AddCommGrp AddGrp
in the category AddGrp
.
In the following, we will show that this has the structure of a commutative additive group.
Equations
Instances For
Equations
- CommGrp.FilteredColimits.colimitCommGroup F = { toGroup := (CommGrp.FilteredColimits.G F).str, mul_comm := ⋯ }
Equations
- AddCommGrp.FilteredColimits.colimitAddCommGroup F = { toAddGroup := (AddCommGrp.FilteredColimits.G F).str, add_comm := ⋯ }
The bundled commutative group giving the filtered colimit of a diagram.
Equations
Instances For
The bundled additive commutative group giving the filtered colimit of a diagram.
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 cocone over the proposed colimit additive 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 CommGrp
.
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.