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
🔸 coverage
def MonCat.adjoinOne :
CategoryTheory.Functor Semigrp MonCat

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

Instances For
    source
    🔸 coverage
    def AddMonCat.adjoinZero :
    CategoryTheory.Functor AddSemigrp AddMonCat

    The functor of adjoining a neutral element zero to a semigroup

    Instances For
      source
      📐 coverage
      @[simp]
      theorem AddMonCat.adjoinZero_obj_coe (S : AddSemigrp) :
      ↑(adjoinZero.obj S) = WithZero ↑S
      source
      📐 coverage
      @[simp]
      theorem MonCat.adjoinOne_map {X✝ Y✝ : Semigrp} (f : X✝ ⟶ Y✝) :
      adjoinOne.map f = ofHom (WithOne.mapMulHom (Semigrp.Hom.hom f))
      source
      📐 coverage
      @[simp]
      theorem AddMonCat.adjoinZero_map {X✝ Y✝ : AddSemigrp} (f : X✝ ⟶ Y✝) :
      adjoinZero.map f = ofHom (WithZero.mapAddHom (AddSemigrp.Hom.hom f))
      source
      📐 coverage
      @[simp]
      theorem MonCat.adjoinOne_obj_coe (S : Semigrp) :
      ↑(adjoinOne.obj S) = WithOne ↑S
      source
      🔸 coverage
      @[implicit_reducible]
      instance MonCat.hasForgetToSemigroup :
      CategoryTheory.HasForget₂ MonCat Semigrp
      source
      🔸 coverage
      @[implicit_reducible]
      instance AddMonCat.hasForgetToAddSemigroup :
      CategoryTheory.HasForget₂ AddMonCat AddSemigrp
      source
      🔸 coverage
      def MonCat.adjoinOneAdj :
      adjoinOne ⊣ CategoryTheory.forget₂ MonCat Semigrp

      The adjoinOne-forgetful adjunction from Semigrp to MonCat.

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

        The adjoinZero-forgetful adjunction from AddSemigrp to AddMonCat

        Instances For
          source
          🔸 coverage
          def MonCat.free :
          CategoryTheory.Functor (Type u) MonCat

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

          Instances For
            source
            🔸 coverage
            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.

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

              The free-forgetful adjunction for monoids.

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

                The free-forgetful adjunction for additive monoids.

                Instances For
                  source
                  📐 coverage
                  instance MonCat.instIsRightAdjointForgetMonoidHomCarrier :
                  (CategoryTheory.forget MonCat).IsRightAdjoint
                  source
                  🔸 coverage
                  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.

                  Instances For
                    source
                    📐 coverage
                    @[simp]
                    theorem AddCommMonCat.free_obj_coe (α : Type u) :
                    ↑(free.obj α) = (α →₀ ℕ)
                    source
                    📐 coverage
                    @[simp]
                    theorem AddCommMonCat.free_map {X✝ Y✝ : Type u} (f : X✝ ⟶ Y✝) :
                    free.map f = ofHom (Finsupp.mapDomain.addMonoidHom f)
                    source
                    🔸 coverage
                    noncomputable def AddCommMonCat.adj :
                    free ⊣ CategoryTheory.forget AddCommMonCat

                    The free-forgetful adjunction for commutative monoids.

                    Instances For
                      source
                      📐 coverage
                      instance AddCommMonCat.instIsLeftAdjointFree :
                      free.IsLeftAdjoint
                      source
                      📐 coverage
                      instance AddCommMonCat.instIsRightAdjointForgetAddMonoidHomCarrier :
                      (CategoryTheory.forget AddCommMonCat).IsRightAdjoint
                      source
                      📐 coverage
                      instance CommMonCat.instIsRightAdjointForgetMonoidHomCarrier :
                      (CategoryTheory.forget CommMonCat).IsRightAdjoint