Documentation

Mathlib.Algebra.Category.MonCat.Adjunctions

Adjunctions regarding the category of monoids #

This file proves the adjunction between adjoining a unit to a semigroup and the forgetful functor from monoids to semigroups.

TODO #

source
def MonCat.adjoinOne :
CategoryTheory.Functor Semigrp MonCat

The functor of adjoining a neutral element one to a semigroup.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def AddMonCat.adjoinZero :
    CategoryTheory.Functor AddSemigrp AddMonCat

    The functor of adjoining a neutral element zero to a semigroup

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem MonCat.adjoinOne_map {X✝ Y✝ : Semigrp} (f : X✝ ⟶ Y✝) :
      adjoinOne.map f = ofHom (WithOne.map (Semigrp.Hom.hom f))
      source
      @[simp]
      theorem MonCat.adjoinOne_obj_coe (S : Semigrp) :
      ↑(adjoinOne.obj S) = WithOne ↑S
      source
      @[simp]
      theorem AddMonCat.adjoinZero_map {X✝ Y✝ : AddSemigrp} (f : X✝ ⟶ Y✝) :
      adjoinZero.map f = ofHom (WithZero.map (AddSemigrp.Hom.hom f))
      source
      @[simp]
      theorem AddMonCat.adjoinZero_obj_coe (S : AddSemigrp) :
      ↑(adjoinZero.obj S) = WithZero ↑S
      source
      instance MonCat.hasForgetToSemigroup :
      CategoryTheory.HasForget₂ MonCat Semigrp
      Equations
      • One or more equations did not get rendered due to their size.
      source
      instance AddMonCat.hasForgetToAddSemigroup :
      CategoryTheory.HasForget₂ AddMonCat AddSemigrp
      Equations
      • One or more equations did not get rendered due to their size.
      source
      def MonCat.adjoinOneAdj :
      adjoinOne ⊣ CategoryTheory.forget₂ MonCat Semigrp

      The adjoinOne-forgetful adjunction from Semigrp to MonCat.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def AddMonCat.adjoinZeroAdj :
        adjoinZero ⊣ CategoryTheory.forget₂ AddMonCat AddSemigrp

        The adjoinZero-forgetful adjunction from AddSemigrp to AddMonCat

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def MonCat.free :
          CategoryTheory.Functor (Type u) MonCat

          The free functor Type u ⥤ MonCat sending a type X to the free monoid on X.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def AddMonCat.free :
            CategoryTheory.Functor (Type u) AddMonCat

            The free functor Type u ⥤ AddMonCat sending a type X to the free monoid on X.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              def MonCat.adj :
              free ⊣ CategoryTheory.forget MonCat

              The free-forgetful adjunction for monoids.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                def AddMonCat.adj :
                free ⊣ CategoryTheory.forget AddMonCat

                The free-forgetful adjunction for additive monoids.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  instance MonCat.instIsRightAdjointForget :
                  (CategoryTheory.forget MonCat).IsRightAdjoint
                  source
                  noncomputable def AddCommMonCat.free :
                  CategoryTheory.Functor (Type u) AddCommMonCat

                  The free functor Type u ⥤ AddCommMonCat sending a type X to the free commutative monoid on X.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    @[simp]
                    theorem AddCommMonCat.free_obj_coe (α : Type u) :
                    ↑(free.obj α) = (α →₀ ℕ)
                    source
                    @[simp]
                    theorem AddCommMonCat.free_map {X✝ Y✝ : Type u} (f : X✝ ⟶ Y✝) :
                    free.map f = ofHom (Finsupp.mapDomain.addMonoidHom f)
                    source
                    noncomputable def AddCommMonCat.adj :
                    free ⊣ CategoryTheory.forget AddCommMonCat

                    The free-forgetful adjunction for commutative monoids.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      source
                      instance AddCommMonCat.instIsLeftAdjointFree :
                      free.IsLeftAdjoint
                      source
                      instance AddCommMonCat.instIsRightAdjointForget :
                      (CategoryTheory.forget AddCommMonCat).IsRightAdjoint
                      source
                      instance CommMonCat.instIsRightAdjointForget :
                      (CategoryTheory.forget CommMonCat).IsRightAdjoint