Documentation

Mathlib.CategoryTheory.Monoidal.Cartesian.Grp_

Yoneda embedding of Grp C #

We show that group objects are exactly those whose yoneda presheaf is a presheaf of groups, by constructing the yoneda embedding Grp C ⥤ Cᵒᵖ ⥤ GrpCat.{v} and showing that it is fully faithful and its (essential) image is the representable functors.

def Grp.homMk {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G H : C} [GrpObj G] [GrpObj H] (f : G H) [IsMonHom f] :
{ X := G, grp := inst✝ } { X := H, grp := inst✝¹ }

Construct a morphism G ⟶ H of Grp C C from a map f : G ⟶ H and a IsMonHom f instance.

Equations
Instances For
    @[deprecated Grp.homMk (since := "2025-10-13")]
    def Grp_.homMk {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G H : C} [GrpObj G] [GrpObj H] (f : G H) [IsMonHom f] :
    { X := G, grp := inst✝ } { X := H, grp := inst✝¹ }

    Alias of Grp.homMk.


    Construct a morphism G ⟶ H of Grp C C from a map f : G ⟶ H and a IsMonHom f instance.

    Equations
    Instances For
      @[deprecated Grp.homMk_hom' (since := "2025-10-13")]

      Alias of Grp.homMk_hom'.

      If X represents a presheaf of monoids, then X is a monoid object.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        @[deprecated GrpObj.ofRepresentableBy (since := "2025-09-13")]

        Alias of GrpObj.ofRepresentableBy.


        If X represents a presheaf of monoids, then X is a monoid object.

        Equations
        Instances For
          @[reducible, inline]

          If G is a group object, then Hom(X, G) has a group structure.

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

            If G is a group object, then Hom(-, G) is a presheaf of groups.

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

              If X represents a presheaf of groups F, then Hom(-, X) is isomorphic to F as a presheaf of groups.

              Equations
              Instances For

                The yoneda embedding of Grp_C into presheaves of groups.

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

                  The yoneda embedding for Grp_C is fully faithful.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    @[deprecated GrpObj.inv_comp (since := "2025-09-13")]

                    Alias of GrpObj.inv_comp.

                    @[deprecated GrpObj.div_comp (since := "2025-09-13")]

                    Alias of GrpObj.div_comp.

                    @[deprecated GrpObj.zpow_comp (since := "2025-09-13")]

                    Alias of GrpObj.zpow_comp.

                    @[deprecated GrpObj.comp_inv (since := "2025-09-13")]

                    Alias of GrpObj.comp_inv.

                    @[deprecated GrpObj.comp_div (since := "2025-09-13")]

                    Alias of GrpObj.comp_div.

                    @[deprecated GrpObj.comp_zpow (since := "2025-09-13")]

                    Alias of GrpObj.comp_zpow.

                    @[deprecated GrpObj.inv_eq_inv (since := "2025-09-13")]

                    Alias of GrpObj.inv_eq_inv.

                    @[reducible, inline]

                    If G is a commutative group object, then Hom(X, G) has a commutative group structure.

                    Equations
                    Instances For