Documentation

Mathlib.Algebra.Category.MonCat.FilteredColimits

The forgetful functor from (commutative) (additive) monoids 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 ⥤ MonCat. We then construct a monoid structure on the colimit of F ⋙ forget MonCat (in Type), thereby showing that the forgetful functor forget MonCat preserves filtered colimits. Similarly for AddMonCat, CommMonCat and AddCommMonCat.

@[reducible, inline]

The colimit of F ⋙ forget AddMon in the category of types. In the following, we will construct an additive monoid structure on M.

Equations
Instances For
    @[reducible, inline]

    The colimit of F ⋙ forget MonCat in the category of types. In the following, we will construct a monoid structure on M.

    Equations
    Instances For
      @[reducible, inline]

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

      Equations
      Instances For
        @[reducible, inline]

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

        Equations
        Instances For
          theorem AddMonCat.FilteredColimits.M.mk_eq {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddMonCatMax) (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 MonCat.FilteredColimits.M.mk_eq {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J MonCatMax) (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) :

          As J is nonempty, we can pick an arbitrary object j₀ : J. We use this object to define the "zero" in the colimit as the equivalence class of ⟨j₀, 0 : F.obj j₀⟩.

          Equations

          As J is nonempty, we can pick an arbitrary object j₀ : J. We use this object to define the "one" in the colimit as the equivalence class of ⟨j₀, 1 : F.obj j₀⟩.

          Equations

          The definition of the "zero" in the colimit is independent of the chosen object of J. In particular, this lemma allows us to "unfold" the definition of colimit_zero at a custom chosen object j.

          The definition of the "one" in the colimit is independent of the chosen object of J. In particular, this lemma allows us to "unfold" the definition of colimit_one at a custom chosen object j.

          noncomputable def AddMonCat.FilteredColimits.colimitAddAux {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddMonCatMax) [CategoryTheory.IsFiltered J] (x : (j : J) × (F.obj j)) (y : (j : J) × (F.obj j)) :

          The "unlifted" version of addition in the colimit. To add two dependent pairs ⟨j₁, x⟩ and ⟨j₂, y⟩, we pass to a common successor of j₁ and j₂ (given by IsFiltered.max) and add them there.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            noncomputable def MonCat.FilteredColimits.colimitMulAux {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J MonCatMax) [CategoryTheory.IsFiltered J] (x : (j : J) × (F.obj j)) (y : (j : J) × (F.obj j)) :

            The "unlifted" version of multiplication in the colimit. To multiply two dependent pairs ⟨j₁, x⟩ and ⟨j₂, y⟩, we pass to a common successor of j₁ and j₂ (given by IsFiltered.max) and multiply them there.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For

              Addition in the colimit is well-defined in the left argument.

              Multiplication in the colimit is well-defined in the left argument.

              Addition in the colimit is well-defined in the right argument.

              Multiplication in the colimit is well-defined in the right argument.

              theorem AddMonCat.FilteredColimits.colimit_add_mk_eq {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddMonCatMax) [CategoryTheory.IsFiltered J] (x : (j : J) × (F.obj j)) (y : (j : J) × (F.obj j)) (k : J) (f : x.fst k) (g : y.fst k) :

              Addition in the colimit is independent of the chosen "maximum" in the filtered category. In particular, this lemma allows us to "unfold" the definition of the addition of x and y, using a custom object k and morphisms f : x.1 ⟶ k and g : y.1 ⟶ k.

              theorem MonCat.FilteredColimits.colimit_mul_mk_eq {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J MonCatMax) [CategoryTheory.IsFiltered J] (x : (j : J) × (F.obj j)) (y : (j : J) × (F.obj j)) (k : J) (f : x.fst k) (g : y.fst k) :

              Multiplication in the colimit is independent of the chosen "maximum" in the filtered category. In particular, this lemma allows us to "unfold" the definition of the multiplication of x and y, using a custom object k and morphisms f : x.1 ⟶ k and g : y.1 ⟶ k.

              The bundled additive monoid giving the filtered colimit of a diagram.

              Equations
              Instances For

                The bundled monoid giving the filtered colimit of a diagram.

                Equations
                Instances For
                  theorem AddMonCat.FilteredColimits.coconeMorphism.proof_2 {J : Type u_2} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddMonCatMax) [CategoryTheory.IsFiltered J] (j : J) (x : (F.obj j)) (y : (F.obj j)) :
                  { toFun := (CategoryTheory.Limits.Types.TypeMax.colimitCocone (F.comp (CategoryTheory.forget AddMonCat))).app j, map_zero' := }.toFun (x + y) = { toFun := (CategoryTheory.Limits.Types.TypeMax.colimitCocone (F.comp (CategoryTheory.forget AddMonCat))).app j, map_zero' := }.toFun x + { toFun := (CategoryTheory.Limits.Types.TypeMax.colimitCocone (F.comp (CategoryTheory.forget AddMonCat))).app j, map_zero' := }.toFun y

                  The additive monoid homomorphism from a given additive monoid in the diagram to the colimit additive monoid.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For

                    The monoid homomorphism from a given monoid in the diagram to the colimit monoid.

                    Equations
                    Instances For

                      Given a cocone t of F, the induced additive monoid homomorphism from the colimit to the cocone point. As a function, this is simply given by the induced map of the corresponding cocone in Type. The only thing left to see is that it is an additive monoid homomorphism.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For

                        Given a cocone t of F, the induced monoid homomorphism from the colimit to the cocone point. As a function, this is simply given by the induced map of the corresponding cocone in Type. The only thing left to see is that it is a monoid homomorphism.

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

                          The colimit of F ⋙ forget₂ AddCommMonCat AddMonCat in the category AddMonCat. In the following, we will show that this has the structure of a commutative additive monoid.

                          Equations
                          Instances For
                            @[reducible, inline]

                            The colimit of F ⋙ forget₂ CommMonCat MonCat in the category MonCat. In the following, we will show that this has the structure of a commutative monoid.

                            Equations
                            Instances For

                              The bundled additive commutative monoid giving the filtered colimit of a diagram.

                              Equations
                              Instances For

                                The bundled commutative monoid giving the filtered colimit of a diagram.

                                Equations
                                Instances For

                                  The cocone over the proposed colimit additive commutative monoid.

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For

                                    The cocone over the proposed colimit commutative monoid.

                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For

                                      The proposed colimit cocone is a colimit in AddCommMonCat.

                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For

                                        The proposed colimit cocone is a colimit in CommMonCat.

                                        Equations
                                        • One or more equations did not get rendered due to their size.
                                        Instances For