Documentation

Mathlib.Algebra.Category.MonCat.Limits

The category of (commutative) (additive) monoids 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.

@[reducible, inline]
abbrev AddMonCatMax :
Type ((max u1 u2) + 1)

An alias for AddMonCat.{max u v}, to deal around unification issues.

Equations
Instances For
    @[reducible, inline]
    abbrev MonCatMax :
    Type ((max u1 u2) + 1)

    An alias for MonCat.{max u v}, to deal around unification issues.

    Equations
    Instances For
      theorem AddMonCat.sectionsAddSubmonoid.proof_2 {J : Type u_2} [CategoryTheory.Category.{u_1, u_2} J] (F : CategoryTheory.Functor J AddMonCat) {j : J} {j' : J} (f : j j') :
      (F.map f) 0 = 0

      The flat sections of a functor into AddMonCat form an additive submonoid of all sections.

      Equations
      Instances For
        theorem AddMonCat.sectionsAddSubmonoid.proof_1 {J : Type u_3} [CategoryTheory.Category.{u_2, u_3} J] (F : CategoryTheory.Functor J AddMonCat) {a : (j : J) → (F.obj j)} {b : (j : J) → (F.obj j)} (ah : a (F.comp (CategoryTheory.forget AddMonCat)).sections) (bh : b (F.comp (CategoryTheory.forget AddMonCat)).sections) {j : J} {j' : J} (f : j j') :
        (F.comp (CategoryTheory.forget AddMonCat)).map f ((a + b) j) = (a + b) j'

        The flat sections of a functor into MonCat form a submonoid of all sections.

        Equations
        Instances For
          theorem AddMonCat.limitπAddMonoidHom.proof_2 {J : Type u_3} [CategoryTheory.Category.{u_1, u_3} J] (F : CategoryTheory.Functor J AddMonCat) [Small.{u_2, max u_2 u_3} (F.comp (CategoryTheory.forget AddMonCat)).sections] (j : J) :
          ∀ (x x_1 : (CategoryTheory.Limits.Types.Small.limitCone (F.comp (CategoryTheory.forget AddMonCat))).pt), { toFun := (CategoryTheory.Limits.Types.Small.limitCone (F.comp (CategoryTheory.forget AddMonCat))).app j, map_zero' := }.toFun (x + x_1) = { toFun := (CategoryTheory.Limits.Types.Small.limitCone (F.comp (CategoryTheory.forget AddMonCat))).app j, map_zero' := }.toFun x + { toFun := (CategoryTheory.Limits.Types.Small.limitCone (F.comp (CategoryTheory.forget AddMonCat))).app j, map_zero' := }.toFun x_1

          limit.π (F ⋙ forget AddMonCat) j as an AddMonoidHom.

          Equations
          Instances For

            limit.π (F ⋙ forget MonCat) j as a MonoidHom.

            Equations
            Instances For

              (Internal use only; use the limits API.)

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

                Construction of a limit cone in MonCat. (Internal use only; use the limits API.)

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

                  (Internal use only; use the limits API.)

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    theorem AddMonCat.HasLimits.limitConeIsLimit.proof_4 {J : Type u_3} [CategoryTheory.Category.{u_1, u_3} J] (F : CategoryTheory.Functor J AddMonCat) [Small.{u_2, max u_2 u_3} (F.comp (CategoryTheory.forget AddMonCat)).sections] (s : CategoryTheory.Limits.Cone F) :
                    (CategoryTheory.forget AddMonCat).map ((fun (s : CategoryTheory.Limits.Cone F) => { toFun := fun (v : ((CategoryTheory.forget AddMonCat).mapCone s).pt) => (equivShrink (F.comp (CategoryTheory.forget AddMonCat)).sections).1 fun (j : J) => ((CategoryTheory.forget AddMonCat).mapCone s).app j v, , map_zero' := , map_add' := }) s) = (CategoryTheory.forget AddMonCat).map ((fun (s : CategoryTheory.Limits.Cone F) => { toFun := fun (v : ((CategoryTheory.forget AddMonCat).mapCone s).pt) => (equivShrink (F.comp (CategoryTheory.forget AddMonCat)).sections).1 fun (j : J) => ((CategoryTheory.forget AddMonCat).mapCone s).app j v, , map_zero' := , map_add' := }) s)
                    theorem AddMonCat.HasLimits.limitConeIsLimit.proof_3 {J : Type u_3} [CategoryTheory.Category.{u_2, u_3} J] (F : CategoryTheory.Functor J AddMonCat) [Small.{u_1, max u_1 u_3} (F.comp (CategoryTheory.forget AddMonCat)).sections] (s : CategoryTheory.Limits.Cone F) (x : s.pt) (y : s.pt) :
                    { toFun := fun (v : ((CategoryTheory.forget AddMonCat).mapCone s).pt) => (equivShrink (F.comp (CategoryTheory.forget AddMonCat)).sections).1 fun (j : J) => ((CategoryTheory.forget AddMonCat).mapCone s).app j v, , map_zero' := }.toFun (x + y) = { toFun := fun (v : ((CategoryTheory.forget AddMonCat).mapCone s).pt) => (equivShrink (F.comp (CategoryTheory.forget AddMonCat)).sections).1 fun (j : J) => ((CategoryTheory.forget AddMonCat).mapCone s).app j v, , map_zero' := }.toFun x + { toFun := fun (v : ((CategoryTheory.forget AddMonCat).mapCone s).pt) => (equivShrink (F.comp (CategoryTheory.forget AddMonCat)).sections).1 fun (j : J) => ((CategoryTheory.forget AddMonCat).mapCone s).app j v, , map_zero' := }.toFun y

                    Witness that the limit cone in MonCat is a limit cone. (Internal use only; use the limits API.)

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

                      If (F ⋙ forget AddMonCat).sections is u-small, F has a limit.

                      Equations
                      • =

                      If (F ⋙ forget MonCat).sections is u-small, F has a limit.

                      Equations
                      • =

                      If J is u-small, AddMonCat.{u} has limits of shape J.

                      Equations
                      • =

                      If J is u-small, MonCat.{u} has limits of shape J.

                      Equations
                      • =

                      The category of additive monoids has all limits.

                      Equations
                      • =

                      The category of monoids has all limits.

                      Equations
                      • =

                      If J is u-small, the forgetful functor from AddMonCat.{u}

                      preserves limits of shape J.

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

                      If J is u-small, the forgetful functor from MonCat.{u} preserves limits of shape J.

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

                      The forgetful functor from additive monoids 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
                      • One or more equations did not get rendered due to their size.

                      The forgetful functor from monoids 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
                      • One or more equations did not get rendered due to their size.
                      @[reducible, inline]
                      abbrev AddCommMonCatMax :
                      Type ((max u1 u2) + 1)

                      An alias for AddCommMonCat.{max u v}, to deal around unification issues.

                      Equations
                      Instances For
                        @[reducible, inline]
                        abbrev CommMonCatMax :
                        Type ((max u1 u2) + 1)

                        An alias for CommMonCat.{max u v}, to deal around unification issues.

                        Equations
                        Instances For

                          We show that the forgetful functor AddCommMonCatAddMonCat creates limits.

                          All we need to do is notice that the limit point has an AddCommMonoid 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 CommMonCatMonCat creates limits.

                          All we need to do is notice that the limit point has a CommMonoid 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 CommMonCat. (Generally, you'll just want to use limit F.)

                          Equations
                          Instances For

                            If (F ⋙ forget AddCommMonCat).sections is u-small, F has a limit.

                            Equations
                            • =

                            If (F ⋙ forget CommMonCat).sections is u-small, F has a limit.

                            Equations
                            • =

                            If J is u-small, AddCommMonCat.{u} has limits of shape J.

                            Equations
                            • =

                            If J is u-small, CommMonCat.{u} has limits of shape J.

                            Equations
                            • =

                            The category of additive commutative monoids has all limits.

                            Equations
                            • =

                            The category of commutative monoids has all limits.

                            Equations
                            • =

                            The forgetful functor from additive commutative monoids to additive monoids preserves all limits.

                            This means the underlying type of a limit can be computed as a limit in the category of additive

                            monoids.

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

                            The forgetful functor from commutative monoids to monoids preserves all limits.

                            This means the underlying type of a limit can be computed as a limit in the category of monoids.

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

                            If J is u-small, the forgetful functor from AddCommMonCat.{u}

                            preserves limits of shape J.

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

                            If J is u-small, the forgetful functor from CommMonCat.{u} preserves limits of shape J.

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

                            The forgetful functor from additive commutative monoids 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
                            • One or more equations did not get rendered due to their size.

                            The forgetful functor from commutative monoids 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
                            • One or more equations did not get rendered due to their size.