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 #

The functor of adjoining a neutral element zero to a semigroup

Instances For
    theorem adjoinZero.proof_2 :
    ∀ {X Y Z : AddSemigroupCat} (f : AddHom X Y) (g : AddHom Y Z), WithZero.map (AddHom.comp g f) = AddMonoidHom.comp (WithZero.map g) (WithZero.map f)
    @[simp]
    theorem adjoinZero_map :
    ∀ {X Y : AddSemigroupCat} (f : AddHom X Y), adjoinZero.map f = WithZero.map f
    @[simp]
    theorem adjoinOne_map :
    ∀ {X Y : SemigroupCat} (f : X →ₙ* Y), adjoinOne.map f = WithOne.map f
    @[simp]

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

    Instances For
      theorem hasForgetToAddSemigroup.proof_1 (X : AddMonCat) :
      { obj := fun M => AddSemigroupCat.of M, map := fun {X Y} => AddMonoidHom.toAddHom }.map (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id ({ obj := fun M => AddSemigroupCat.of M, map := fun {X Y} => AddMonoidHom.toAddHom }.obj X)
      theorem hasForgetToAddSemigroup.proof_2 {X : AddMonCat} {Y : AddMonCat} {Z : AddMonCat} (f : X Y) (g : Y Z) :
      { obj := fun M => AddSemigroupCat.of M, map := fun {X Y} => AddMonoidHom.toAddHom }.map (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp ({ obj := fun M => AddSemigroupCat.of M, map := fun {X Y} => AddMonoidHom.toAddHom }.map f) ({ obj := fun M => AddSemigroupCat.of M, map := fun {X Y} => AddMonoidHom.toAddHom }.map g)
      theorem adjoinZeroAdj.proof_1 {S : AddSemigroupCat} {T : AddSemigroupCat} {M : AddMonCat} (f : S T) (g : T (CategoryTheory.forget₂ AddMonCat AddSemigroupCat).obj M) :
      ((fun S M => WithZero.lift.symm) S M).symm (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (adjoinZero.map f) (((fun S M => WithZero.lift.symm) T M).symm g)
      theorem adjoinZeroAdj.proof_2 {X : AddSemigroupCat} {Y : AddMonCat} {Y' : AddMonCat} (f : adjoinZero.obj X Y) (g : Y Y') :
      ↑((fun S M => WithZero.lift.symm) X Y') (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (↑((fun S M => WithZero.lift.symm) X Y) f) ((CategoryTheory.forget₂ AddMonCat AddSemigroupCat).map g)

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

      Instances For

        The free-forgetful adjunction for monoids.

        Instances For