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 #

theorem AddMonCat.adjoinZero.proof_2 :
∀ {X Y Z : AddSemigrp} (f : AddHom X Y) (g : AddHom Y Z), WithZero.map (g.comp f) = (WithZero.map g).comp (WithZero.map f)

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
    @[simp]
    theorem AddMonCat.adjoinZero_map :
    ∀ {X Y : AddSemigrp} (f : AddHom X Y), AddMonCat.adjoinZero.map f = WithZero.map f
    @[simp]
    theorem MonCat.adjoinOne_map :
    ∀ {X Y : Semigrp} (f : X →ₙ* Y), MonCat.adjoinOne.map f = WithOne.map f

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

    Equations
    Instances For
      theorem AddMonCat.hasForgetToAddSemigroup.proof_3 :
      { obj := fun (M : AddMonCat) => AddSemigrp.of M, map := fun {X Y : AddMonCat} => AddMonoidHom.toAddHom, map_id := , map_comp := }.comp (CategoryTheory.forget AddSemigrp) = { obj := fun (M : AddMonCat) => AddSemigrp.of M, map := fun {X Y : AddMonCat} => AddMonoidHom.toAddHom, map_id := , map_comp := }.comp (CategoryTheory.forget AddSemigrp)
      Equations
      • One or more equations did not get rendered due to their size.
      theorem AddMonCat.hasForgetToAddSemigroup.proof_1 (X : AddMonCat) :
      { obj := fun (M : AddMonCat) => AddSemigrp.of M, map := fun {X Y : AddMonCat} => AddMonoidHom.toAddHom }.map (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id ({ obj := fun (M : AddMonCat) => AddSemigrp.of M, map := fun {X Y : AddMonCat} => AddMonoidHom.toAddHom }.obj X)
      theorem AddMonCat.hasForgetToAddSemigroup.proof_2 {X : AddMonCat} {Y : AddMonCat} {Z : AddMonCat} (f : X Y) (g : Y Z) :
      { obj := fun (M : AddMonCat) => AddSemigrp.of M, map := fun {X Y : AddMonCat} => AddMonoidHom.toAddHom }.map (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp ({ obj := fun (M : AddMonCat) => AddSemigrp.of M, map := fun {X Y : AddMonCat} => AddMonoidHom.toAddHom }.map f) ({ obj := fun (M : AddMonCat) => AddSemigrp.of M, map := fun {X Y : AddMonCat} => AddMonoidHom.toAddHom }.map g)
      Equations
      • One or more equations did not get rendered due to their size.

      The adjoinZero-forgetful adjunction from AddSemigrp to AddMonCat

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        theorem AddMonCat.adjoinZeroAdj.proof_2 {X : AddSemigrp} {Y : AddMonCat} {Y' : AddMonCat} (f : AddMonCat.adjoinZero.obj X Y) (g : Y Y') :
        ((fun (S : AddSemigrp) (M : AddMonCat) => WithZero.lift.symm) X Y') (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (((fun (S : AddSemigrp) (M : AddMonCat) => WithZero.lift.symm) X Y) f) ((CategoryTheory.forget₂ AddMonCat AddSemigrp).map g)
        theorem AddMonCat.adjoinZeroAdj.proof_1 {S : AddSemigrp} {T : AddSemigrp} {M : AddMonCat} (f : S T) (g : T (CategoryTheory.forget₂ AddMonCat AddSemigrp).obj M) :
        ((fun (S : AddSemigrp) (M : AddMonCat) => WithZero.lift.symm) S M).symm (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (AddMonCat.adjoinZero.map f) (((fun (S : AddSemigrp) (M : AddMonCat) => WithZero.lift.symm) T M).symm g)

        The adjoinOne-forgetful adjunction from Semigrp to MonCat.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For

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

          Equations
          Instances For

            The free-forgetful adjunction for monoids.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For