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

def AddMonCat.adjoinZero : CategoryTheory.Functor AddSemigrp AddMonCat

The functor of adjoining a neutral element zero to a semigroup

Equations

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

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)

@[simp]

theorem MonCat.adjoinOne_obj (S : Semigrp) : MonCat.adjoinOne.obj S = MonCat.of (WithOne ↑S)

@[simp]

theorem MonCat.adjoinOne_map : ∀ {X Y : Semigrp} (f : ↑X →ₙ* ↑Y), MonCat.adjoinOne.map f = WithOne.map f

@[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

def MonCat.adjoinOne : CategoryTheory.Functor Semigrp MonCat

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 }

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)

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)

instance AddMonCat.hasForgetToAddSemigroup : CategoryTheory.HasForget₂ AddMonCat AddSemigrp

Equations

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

instance MonCat.hasForgetToSemigroup : CategoryTheory.HasForget₂ MonCat Semigrp

Equations

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

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)

def AddMonCat.adjoinZeroAdj : AddMonCat.adjoinZero ⊣ CategoryTheory.forget₂ AddMonCat AddSemigrp

The adjoinZero-forgetful adjunction from AddSemigrp to AddMonCat

Equations

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

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)

def MonCat.adjoinOneAdj : MonCat.adjoinOne ⊣ CategoryTheory.forget₂ MonCat Semigrp

The adjoinOne-forgetful adjunction from Semigrp to MonCat.

Equations

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

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

• MonCat.free = { obj := fun (α : Type u) => MonCat.of (FreeMonoid α), map := fun {X Y : Type u} => FreeMonoid.map, map_id := MonCat.free.proof_1, map_comp := @MonCat.free.proof_2 }

def MonCat.adj : MonCat.free ⊣ CategoryTheory.forget MonCat

The free-forgetful adjunction for monoids.

Equations

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

instance MonCat.instIsRightAdjointForget : (CategoryTheory.forget MonCat).IsRightAdjoint

Equations

• MonCat.instIsRightAdjointForget = ⋯