Documentation

Mathlib.Algebra.Category.Grp.Limits

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

Equations

The flat sections of a functor into Grp form a subgroup of all sections.

Equations
Instances For

    The flat sections of a functor into AddGrp form an additive subgroup of all sections.

    Equations
    Instances For
      def Grp.sectionsπMonoidHom {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J Grp) (j : J) :
      (F.comp (CategoryTheory.forget Grp)).sections →* (F.obj j)

      The projection from Functor.sections to a factor as a MonoidHom.

      Equations
      Instances For

        The projection from Functor.sections to a factor as an AddMonoidHom.

        Equations
        Instances For

          We show that the forgetful functor GrpMonCat creates limits.

          All we need to do is notice that the limit point has a Group 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 AddGrpAddMonCat creates limits.

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

          Equations
          Instances For

            A choice of limit cone for a functor into Grp. (Generally, you'll just want to use limit F.)

            Equations
            Instances For

              The chosen cone is a limit cone. (Generally, you'll just want to use limit.cone F.)

              Equations
              Instances For

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

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

                A functor F : J ⥤ Grp.{u} has a limit iff (F ⋙ forget Grp).sections is u-small.

                A functor F : J ⥤ AddGrp.{u} has a limit iff (F ⋙ forget AddGrp).sections is u-small.

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

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

                The forgetful functor from groups to monoids preserves all limits.

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

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

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

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

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

                preserves limits of shape J.

                The forgetful functor from groups to types preserves all limits.

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

                The forgetful functor from additive groups 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
                Equations

                The forgetful functor from groups to types creates all limits.

                Equations

                The forgetful functor from additive groups to types creates all limits.

                Equations

                We show that the forgetful functor CommGrpGrp creates limits.

                All we need to do is notice that the limit point has a CommGroup 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 AddCommGrpAddGrp creates limits.

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

                Equations
                Instances For

                  A choice of limit cone for a functor into AddCommGrp. (Generally, you'll just want to use limit F.)

                  Equations
                  Instances For

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

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

                    A functor F : J ⥤ CommGrp.{u} has a limit iff (F ⋙ forget CommGrp).sections is u-small.

                    A functor F : J ⥤ AddCommGrp.{u} has a limit iff (F ⋙ forget AddCommGrp).sections is u-small.

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

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

                    The category of additive commutative groups has all limits.

                    The forgetful functor from commutative groups to groups preserves all limits. (That is, the underlying group could have been computed instead as limits in the category of groups.)

                    The forgetful functor from additive commutative groups to additive groups preserves all limits. (That is, the underlying group could have been computed instead as limits in the category of additive groups.)

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

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

                    The forgetful functor from commutative groups to commutative monoids preserves all limits. (That is, the underlying commutative monoids could have been computed instead as limits in the category of commutative monoids.)

                    The forgetful functor from additive commutative groups to additive commutative monoids preserves all limits. (That is, the underlying additive commutative monoids could have been computed instead as limits in the category of additive commutative monoids.)

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

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

                    preserves limits of shape J.

                    The forgetful functor from commutative groups to types preserves all limits. (That is, the underlying types could have been computed instead as limits in the category of types.)

                    The forgetful functor from additive commutative groups to types preserves all limits. (That is, the underlying types could have been computed instead as limits in the category of types.)

                    The forgetful functor from commutative groups to types creates all limits.

                    Equations

                    The forgetful functor from additive commutative groups to types creates all limits.

                    Equations

                    The categorical kernel of a morphism in AddCommGrp agrees with the usual group-theoretical kernel.

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

                      The categorical kernel inclusion for f : G ⟶ H, as an object over G, agrees with the AddSubgroup.subtype map.

                      Equations
                      Instances For