Documentation

Mathlib.Algebra.Category.GroupCat.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 AddGroupCat form an additive subgroup of all sections.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    theorem AddGroupCat.sectionsAddSubgroup.proof_3 {J : Type u_3} [CategoryTheory.Category.{u_2, u_3} J] (F : CategoryTheory.Functor J AddGroupCat) {a : (j : J) → (F.obj j)} (ah : a { toAddSubsemigroup := { carrier := CategoryTheory.Functor.sections (CategoryTheory.Functor.comp F (CategoryTheory.forget AddGroupCat)), add_mem' := }, zero_mem' := }.carrier) (j : J) (j' : J) (f : j j') :

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

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

      We show that the forgetful functor AddGroupCatAddMonCat 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.

      We show that the forgetful functor GroupCatMonCat 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.

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

      Equations
      • =

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

      Equations
      • =

      The category of additive groups has all limits.

      Equations
      • =

      The category of groups has all limits.

      Equations
      • =

      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.

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

      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.

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

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

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

      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
      • One or more equations did not get rendered due to their size.

      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.

      Equations
      • One or more equations did not get rendered due to their size.
      theorem AddCommGroupCat.Forget₂.createsLimit.proof_4 {J : Type u_3} [CategoryTheory.Category.{u_1, u_3} J] (F : CategoryTheory.Functor J AddCommGroupCat) [Small.{u_2, max u_2 u_3} (CategoryTheory.Functor.sections (CategoryTheory.Functor.comp F (CategoryTheory.forget AddCommGroupCat)))] (c' : CategoryTheory.Limits.Cone (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ AddCommGroupCat AddGroupCat))) (t : CategoryTheory.Limits.IsLimit c') (s : CategoryTheory.Limits.Cone F) :

      We show that the forgetful functor AddCommGroupCatAddGroupCat 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.

      We show that the forgetful functor CommGroupCatGroupCat 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.

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

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

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

        Equations
        • =

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

        Equations
        • =

        The category of additive commutative groups has all limits.

        Equations
        • =

        The category of commutative groups has all limits.

        Equations
        • =

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

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

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

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

        If J is u-small, the forgetful functor from AddCommGroupCat.{u} to 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 CommGroupCat.{u} to 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 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.)

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

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

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

        If J is u-small, the forgetful functor from AddCommGroupCat.{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 CommGroupCat.{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 groups to types preserves all limits. (That is, the underlying types could have been computed instead as limits in the category of types.)

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

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

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

        The categorical kernel of a morphism in AddCommGroupCat 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 subtype map.

          Equations
          Instances For