Documentation

Mathlib.CategoryTheory.SingleObj

Single-object category #

Single object category with a given monoid of endomorphisms. It is defined to facilitate transferring some definitions and lemmas (e.g., conjugacy etc.) from category theory to monoids and groups.

Main definitions #

Given a type α with a monoid structure, SingleObj α is Unit type with Category structure such that End (SingleObj α).star is the monoid α. This can be extended to a functor MonCat ⥤ Cat.

If α is a group, then SingleObj α is a groupoid.

An element x : α can be reinterpreted as an element of End (SingleObj.star α) using SingleObj.toEnd.

Implementation notes #

@[inline, reducible]

Abbreviation that allows writing CategoryTheory.SingleObj rather than Quiver.SingleObj.

Instances For

    One and flip (*) become id and comp for morphisms of the single object category.

    Monoid laws become category laws for the single object category.

    @[inline, reducible]

    Abbreviation that allows writing CategoryTheory.SingleObj.star rather than Quiver.SingleObj.star.

    Instances For

      The endomorphisms monoid of the only object in SingleObj α is equivalent to the original monoid α.

      Instances For

        There is a 1-1 correspondence between monoid homomorphisms α → β and functors between the corresponding single-object categories. It means that SingleObj is a fully faithful functor.

        See https://stacks.math.columbia.edu/tag/001F -- although we do not characterize when the functor is full or faithful.

        Instances For
          @[simp]
          theorem CategoryTheory.SingleObj.differenceFunctor_map {C : Type u_1} {G : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [Group G] (f : CG) {x : C} {y : C} :
          ∀ (x : x y), (CategoryTheory.SingleObj.differenceFunctor f).map x = f y * (f x)⁻¹

          Given a function f : C → G from a category to a group, we get a functor C ⥤ G sending any morphism x ⟶ y to f y * (f x)⁻¹.

          Instances For
            @[reducible]

            Reinterpret a monoid homomorphism f : α → β as a functor (single_obj α) ⥤ (single_obj β). See also CategoryTheory.SingleObj.mapHom for an equivalence between these types.

            Instances For

              The units in a monoid are (multiplicatively) equivalent to the automorphisms of star when we think of the monoid as a single-object category.

              Instances For
                @[simp]
                theorem Units.toAut_hom (α : Type u) [Monoid α] (x : αˣ) :
                (↑(Units.toAut α) x).hom = ↑(CategoryTheory.SingleObj.toEnd α) x
                @[simp]
                theorem Units.toAut_inv (α : Type u) [Monoid α] (x : αˣ) :

                The fully faithful functor from MonCat to Cat.

                Instances For