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.

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

Equations
Instances For

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

    Equations
    Instances For

      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 GrpCatMonCat 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 AddGrpCatAddMonCat 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 functor F : J ⥤ GrpCat.{u} has a limit iff (F ⋙ forget GrpCat).sections is u-small.

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

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

          If J is u-small, AddGrpCat.{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 GrpCat.{u} preserves limits of shape J.

          If J is u-small, the forgetful functor from AddGrpCat.{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.

          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 CommGrpCatGrpCat 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 AddCommGrpCatAddGrpCat 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 functor F : J ⥤ CommGrpCat.{u} has a limit iff (F ⋙ forget CommGrpCat).sections is u-small.

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

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

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

          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 CommGrpCat.{u} to CommMonCat.{u} preserves limits of shape J.

          If J is u-small, the forgetful functor from AddCommGrpCat.{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 CommGrpCat.{u} preserves limits of shape J.

          If J is u-small, the forgetful functor from AddCommGrpCat.{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 AddCommGrpCat 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