Adjunctions regarding the category of monoids #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

source

def adjoin_one :

Semigroup ⥤ Mon

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

Equations

adjoin_one = {obj := λ (S : Semigroup), Mon.of (with_one ↥S), map := λ (X Y : Semigroup), with_one.map, map_id' := adjoin_one._proof_1, map_comp' := adjoin_one._proof_2}

source

@[simp]

theorem adjoin_one_map (X Y : Semigroup) (f : ↥X →ₙ* ↥Y) :

adjoin_one.map f = with_one.map f

source

@[simp]

theorem adjoin_zero_obj (S : AddSemigroup) :

adjoin_zero.obj S = AddMon.of (with_zero ↥S)

source

@[simp]

theorem adjoin_zero_map (X Y : AddSemigroup) (f : add_hom ↥X ↥Y) :

adjoin_zero.map f = with_zero.map f

source

def adjoin_zero :

AddSemigroup ⥤ AddMon

The functor of adjoining a neutral element zero to a semigroup

Equations

adjoin_zero = {obj := λ (S : AddSemigroup), AddMon.of (with_zero ↥S), map := λ (X Y : AddSemigroup), with_zero.map, map_id' := adjoin_zero._proof_1, map_comp' := adjoin_zero._proof_2}

source

@[simp]

theorem adjoin_one_obj (S : Semigroup) :

adjoin_one.obj S = Mon.of (with_one ↥S)

source

@[protected, instance]

def has_forget_to_Semigroup :

category_theory.has_forget₂ Mon Semigroup

Equations

has_forget_to_Semigroup = {forget₂ := {obj := λ (M : Mon), Semigroup.of ↥M, map := λ (M N : Mon), monoid_hom.to_mul_hom, map_id' := has_forget_to_Semigroup._proof_1, map_comp' := has_forget_to_Semigroup._proof_2}, forget_comp := has_forget_to_Semigroup._proof_3}

source

@[protected, instance]

def has_forget_to_AddSemigroup :

category_theory.has_forget₂ AddMon AddSemigroup

Equations

has_forget_to_AddSemigroup = {forget₂ := {obj := λ (M : AddMon), AddSemigroup.of ↥M, map := λ (M N : AddMon), add_monoid_hom.to_add_hom, map_id' := has_forget_to_AddSemigroup._proof_1, map_comp' := has_forget_to_AddSemigroup._proof_2}, forget_comp := has_forget_to_AddSemigroup._proof_3}

source

def adjoin_zero_adj :

adjoin_zero ⊣ category_theory.forget₂ AddMon AddSemigroup

The adjoin_one-forgetful adjunction from AddSemigroup to AddMon

Equations

adjoin_zero_adj = category_theory.adjunction.mk_of_hom_equiv {hom_equiv := λ (S : AddSemigroup) (M : AddMon), with_zero.lift.symm, hom_equiv_naturality_left_symm' := adjoin_zero_adj._proof_1, hom_equiv_naturality_right' := adjoin_zero_adj._proof_2}

source

def adjoin_one_adj :

adjoin_one ⊣ category_theory.forget₂ Mon Semigroup

The adjoin_one-forgetful adjunction from Semigroup to Mon.

Equations

adjoin_one_adj = category_theory.adjunction.mk_of_hom_equiv {hom_equiv := λ (S : Semigroup) (M : Mon), with_one.lift.symm, hom_equiv_naturality_left_symm' := adjoin_one_adj._proof_1, hom_equiv_naturality_right' := adjoin_one_adj._proof_2}

source

def free :

Type u ⥤ Mon

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

Equations

free = {obj := λ (α : Type u), Mon.of (free_monoid α), map := λ (X Y : Type u), free_monoid.map, map_id' := free._proof_1, map_comp' := free._proof_2}

source

def adj :

free ⊣ category_theory.forget Mon

The free-forgetful adjunction for monoids.

Equations

adj = category_theory.adjunction.mk_of_hom_equiv {hom_equiv := λ (X : Type u) (G : Mon), free_monoid.lift.symm, hom_equiv_naturality_left_symm' := adj._proof_1, hom_equiv_naturality_right' := adj._proof_2}

source

@[protected, instance]

def category_theory.forget.category_theory.is_right_adjoint :

category_theory.is_right_adjoint (category_theory.forget Mon)

Equations

category_theory.forget.category_theory.is_right_adjoint = {left := free, adj := adj}