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 adjoinZero.proof_1 : ∀ (x : AddSemigroupCat), WithZero.map (AddHom.id ↑x) = AddMonoidHom.id (WithZero ↑x)

def adjoinZero : CategoryTheory.Functor AddSemigroupCat AddMonCat

The functor of adjoining a neutral element zero to a semigroup

Equations

• adjoinZero = CategoryTheory.Functor.mk { obj := fun (S : AddSemigroupCat) => AddMonCat.of (WithZero ↑S), map := fun {X Y : AddSemigroupCat} => WithZero.map }

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.toPrefunctor.map f = WithZero.map f

@[simp]

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

@[simp]

theorem adjoinZero_obj (S : AddSemigroupCat) : adjoinZero.toPrefunctor.obj S = AddMonCat.of (WithZero ↑S)

@[simp]

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

def adjoinOne : CategoryTheory.Functor SemigroupCat MonCat

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

Equations

• adjoinOne = CategoryTheory.Functor.mk { obj := fun (S : SemigroupCat) => MonCat.of (WithOne ↑S), map := fun {X Y : SemigroupCat} => WithOne.map }

theorem hasForgetToAddSemigroup.proof_1 (X : AddMonCat) : { obj := fun (M : AddMonCat) => AddSemigroupCat.of ↑M, map := fun {X Y : AddMonCat} => AddMonoidHom.toAddHom }.map (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id ({ obj := fun (M : AddMonCat) => AddSemigroupCat.of ↑M, map := fun {X Y : AddMonCat} => AddMonoidHom.toAddHom }.obj X)

theorem hasForgetToAddSemigroup.proof_2 {X : AddMonCat} {Y : AddMonCat} {Z : AddMonCat} (f : X ⟶ Y) (g : Y ⟶ Z) : { obj := fun (M : AddMonCat) => AddSemigroupCat.of ↑M, map := fun {X Y : AddMonCat} => AddMonoidHom.toAddHom }.map (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp ({ obj := fun (M : AddMonCat) => AddSemigroupCat.of ↑M, map := fun {X Y : AddMonCat} => AddMonoidHom.toAddHom }.map f) ({ obj := fun (M : AddMonCat) => AddSemigroupCat.of ↑M, map := fun {X Y : AddMonCat} => AddMonoidHom.toAddHom }.map g)

instance hasForgetToAddSemigroup : CategoryTheory.HasForget₂ AddMonCat AddSemigroupCat

Equations

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

theorem hasForgetToAddSemigroup.proof_3 : CategoryTheory.Functor.comp (CategoryTheory.Functor.mk { obj := fun (M : AddMonCat) => AddSemigroupCat.of ↑M, map := fun {X Y : AddMonCat} => AddMonoidHom.toAddHom }) (CategoryTheory.forget AddSemigroupCat) = CategoryTheory.Functor.comp (CategoryTheory.Functor.mk { obj := fun (M : AddMonCat) => AddSemigroupCat.of ↑M, map := fun {X Y : AddMonCat} => AddMonoidHom.toAddHom }) (CategoryTheory.forget AddSemigroupCat)

instance hasForgetToSemigroup : CategoryTheory.HasForget₂ MonCat SemigroupCat

Equations

• hasForgetToSemigroup = CategoryTheory.HasForget₂.mk (CategoryTheory.Functor.mk { obj := fun (M : MonCat) => SemigroupCat.of ↑M, map := fun {X Y : MonCat} => MonoidHom.toMulHom })

theorem adjoinZeroAdj.proof_1 {S : AddSemigroupCat} {T : AddSemigroupCat} {M : AddMonCat} (f : S ⟶ T) (g : T ⟶ (CategoryTheory.forget₂ AddMonCat AddSemigroupCat).toPrefunctor.obj M) : ((fun (S : AddSemigroupCat) (M : AddMonCat) => WithZero.lift.symm) S M).symm (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (adjoinZero.toPrefunctor.map f) (((fun (S : AddSemigroupCat) (M : AddMonCat) => WithZero.lift.symm) T M).symm g)

theorem adjoinZeroAdj.proof_2 {X : AddSemigroupCat} {Y : AddMonCat} {Y' : AddMonCat} (f : adjoinZero.toPrefunctor.obj X ⟶ Y) (g : Y ⟶ Y') : ((fun (S : AddSemigroupCat) (M : AddMonCat) => WithZero.lift.symm) X Y') (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (((fun (S : AddSemigroupCat) (M : AddMonCat) => WithZero.lift.symm) X Y) f) ((CategoryTheory.forget₂ AddMonCat AddSemigroupCat).toPrefunctor.map g)

def adjoinZeroAdj : adjoinZero ⊣ CategoryTheory.forget₂ AddMonCat AddSemigroupCat

The adjoinZero-forgetful adjunction from AddSemigroupCat to AddMonCat

Equations

• adjoinZeroAdj = CategoryTheory.Adjunction.mkOfHomEquiv (CategoryTheory.Adjunction.CoreHomEquiv.mk fun (S : AddSemigroupCat) (M : AddMonCat) => WithZero.lift.symm)

def adjoinOneAdj : adjoinOne ⊣ CategoryTheory.forget₂ MonCat SemigroupCat

The adjoinOne-forgetful adjunction from SemigroupCat to MonCat.

Equations

• adjoinOneAdj = CategoryTheory.Adjunction.mkOfHomEquiv (CategoryTheory.Adjunction.CoreHomEquiv.mk fun (S : SemigroupCat) (M : MonCat) => WithOne.lift.symm)

def free : CategoryTheory.Functor (Type u) MonCat

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

Equations

• free = CategoryTheory.Functor.mk { obj := fun (α : Type u) => MonCat.of (FreeMonoid α), map := fun {X Y : Type u} => FreeMonoid.map }

def adj : free ⊣ CategoryTheory.forget MonCat

The free-forgetful adjunction for monoids.

Equations

• adj = CategoryTheory.Adjunction.mkOfHomEquiv (CategoryTheory.Adjunction.CoreHomEquiv.mk fun (X : Type u) (G : MonCat) => FreeMonoid.lift.symm)

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

Equations

• instIsRightAdjointTypeTypesMonCatInstMonCatLargeCategoryForgetConcreteCategory = { left := free, adj := adj }