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 #
- free-forgetful adjunction for monoids
- adjunctions related to commutative monoids
theorem
AddMonCat.adjoinZero.proof_1 :
∀ (x : AddSemigrp), WithZero.map (AddHom.id ↑x) = AddMonoidHom.id (WithZero ↑x)
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_obj
(S : AddSemigrp)
:
AddMonCat.adjoinZero.obj S = AddMonCat.of (WithZero ↑S)
@[simp]
theorem
AddMonCat.adjoinZero_map :
∀ {X Y : AddSemigrp} (f : AddHom ↑X ↑Y), AddMonCat.adjoinZero.map f = WithZero.map f
@[simp]
@[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
- MonCat.adjoinOne = { obj := fun (S : Semigrp) => MonCat.of (WithOne ↑S), map := fun {X Y : Semigrp} => WithOne.map, map_id := MonCat.adjoinOne.proof_1, map_comp := @MonCat.adjoinOne.proof_2 }
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 free functor Type u ⥤ MonCat
sending a type X
to the free monoid on X
.
Equations
- MonCat.free = { obj := fun (α : Type ?u.10) => MonCat.of (FreeMonoid α), map := fun {X Y : Type ?u.10} => FreeMonoid.map, map_id := MonCat.free.proof_1, map_comp := @MonCat.free.proof_2 }
Instances For
The free-forgetful adjunction for monoids.
Equations
- One or more equations did not get rendered due to their size.