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
    Instances For
      source
      def AddMonCat.adjoinZero :
      CategoryTheory.Functor AddSemigrp AddMonCat

      The functor of adjoining a neutral element zero to a semigroup

      Equations
        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
            source
            instance AddMonCat.hasForgetToAddSemigroup :
            CategoryTheory.HasForget₂ AddMonCat AddSemigrp
            Equations
              source
              def MonCat.adjoinOneAdj :
              adjoinOne ⊣ CategoryTheory.forget₂ MonCat Semigrp

              The adjoinOne-forgetful adjunction from Semigrp to MonCat.

              Equations
                Instances For
                  source
                  def AddMonCat.adjoinZeroAdj :
                  adjoinZero ⊣ CategoryTheory.forget₂ AddMonCat AddSemigrp

                  The adjoinZero-forgetful adjunction from AddSemigrp to AddMonCat

                  Equations
                    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
                        Instances For
                          source
                          def AddMonCat.free :
                          CategoryTheory.Functor (Type u) AddMonCat

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

                          Equations
                            Instances For
                              source
                              def MonCat.adj :
                              free ⊣ CategoryTheory.forget MonCat

                              The free-forgetful adjunction for monoids.

                              Equations
                                Instances For
                                  source
                                  def AddMonCat.adj :
                                  free ⊣ CategoryTheory.forget AddMonCat

                                  The free-forgetful adjunction for additive monoids.

                                  Equations
                                    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
                                        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
                                            Instances For
                                              source
                                              instance AddCommMonCat.instIsLeftAdjointFree :
                                              free.IsLeftAdjoint
                                              source
                                              instance AddCommMonCat.instIsRightAdjointForget :
                                              (CategoryTheory.forget AddCommMonCat).IsRightAdjoint
                                              source
                                              instance CommMonCat.instIsRightAdjointForget :
                                              (CategoryTheory.forget CommMonCat).IsRightAdjoint