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ᵒᵖ ⥤ Grp.{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

    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