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 AddGrp form an additive subgroup of all sections.

Equations
Instances For
    theorem AddGrp.sectionsAddSubgroup.proof_3 {J : Type u_3} [CategoryTheory.Category.{u_2, u_3} J] (F : CategoryTheory.Functor J AddGrp) {a : (j : J) → (F.obj j)} (ah : a { carrier := (F.comp (CategoryTheory.forget AddGrp)).sections, add_mem' := , zero_mem' := }.carrier) (j : J) (j' : J) (f : j j') :
    (F.comp (CategoryTheory.forget AddGrp)).map f ((-a) j) = (-a) j'

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

    Equations
    Instances For
      theorem AddGrp.sectionsπAddMonoidHom.proof_2 {J : Type u_2} [CategoryTheory.Category.{u_3, u_2} J] (F : CategoryTheory.Functor J AddGrp) (j : J) :
      ∀ (x x_1 : (F.comp (CategoryTheory.forget AddGrp)).sections), { toFun := fun (x : (F.comp (CategoryTheory.forget AddGrp)).sections) => x j, map_zero' := }.toFun (x + x_1) = { toFun := fun (x : (F.comp (CategoryTheory.forget AddGrp)).sections) => x j, map_zero' := }.toFun (x + x_1)
      theorem AddGrp.sectionsπAddMonoidHom.proof_1 {J : Type u_3} [CategoryTheory.Category.{u_2, u_3} J] (F : CategoryTheory.Functor J AddGrp) (j : J) :
      (fun (x : (F.comp (CategoryTheory.forget AddGrp)).sections) => x j) 0 = (fun (x : (F.comp (CategoryTheory.forget AddGrp)).sections) => x j) 0

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

      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

          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.

          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.

          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 AddGrp).sections is u-small, F has a limit.

                Equations
                • =

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

                Equations
                • =

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

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

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

                Equations
                • =

                If J is u-small, Grp.{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 AddGrp.{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 Grp.{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

                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
                theorem AddCommGrp.Forget₂.createsLimit.proof_5 {J : Type u_3} [CategoryTheory.Category.{u_1, u_3} J] (F : CategoryTheory.Functor J AddCommGrp) (c : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.forget₂ AddCommGrp AddGrp))) (hc : CategoryTheory.Limits.IsLimit c) (this : Small.{u_2, max u_2 u_3} (F.comp (CategoryTheory.forget AddCommGrp)).sections) (this : Small.{u_2, max u_2 u_3} ((F.comp ((CategoryTheory.forget₂ AddCommGrp AddGrp).comp (CategoryTheory.forget₂ AddGrp AddMonCat))).comp (CategoryTheory.forget AddMonCat)).sections) (this : Small.{u_2, max u_2 u_3} ((F.comp (CategoryTheory.forget₂ AddCommGrp AddGrp)).comp (CategoryTheory.forget AddGrp)).sections) (s : CategoryTheory.Limits.Cone F) :

                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.

                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.

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

                Equations
                Instances For

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

                  Equations
                  Instances For

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

                    Equations
                    • =

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

                    Equations
                    • =

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

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

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

                    Equations
                    • =

                    If J is u-small, CommGrp.{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
                    • =
                    Equations
                    • One or more equations did not get rendered due to their size.
                    Equations
                    Equations

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

                    Equations

                    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

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

                    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

                    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