Documentation

Mathlib.Algebra.Category.GroupCat.FilteredColimits

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
    @[inline, reducible]

    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
      @[inline, reducible]

      The canonical projection into the colimit, as a quotient type.

      Equations
      Instances For
        theorem AddGroupCat.FilteredColimits.G.mk_eq {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J AddGroupCat) (x : (j : J) × (F.obj j)) (y : (j : J) × (F.obj j)) (h : ∃ (k : J) (f : x.fst k) (g : y.fst k), (F.map f) x.snd = (F.map g) y.snd) :
        theorem GroupCat.FilteredColimits.G.mk_eq {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J GroupCat) (x : (j : J) × (F.obj j)) (y : (j : J) × (F.obj j)) (h : ∃ (k : J) (f : x.fst k) (g : y.fst k), (F.map f) x.snd = (F.map g) y.snd) :

        The "unlifted" version of negation in the colimit.

        Equations
        Instances For

          The "unlifted" version of taking inverses in the colimit.

          Equations
          Instances For

            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.

                        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
                          @[inline, reducible]

                          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 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.