# mathlibdocumentation

algebra.category.Semigroup.basic

We introduce the bundled categories:

• Magma
• AddMagma
• Semigroup
• AddSemigroup along with the relevant forgetful functors between them.

This closely follows algebra.category.Mon.basic.

## TODO #

• Limits in these categories
Type (u+1)

def Magma  :
Type (u+1)

The category of magmas and magma morphisms.

Equations
@[instance]
@[instance]
Equations
@[instance]
@[instance]
@[instance]
@[instance]
@[instance]
@[instance]
def Magma.of (M : Type u) [has_mul M] :

Construct a bundled Magma from the underlying type and typeclass.

Equations

Construct a bundled AddMagma from the underlying type and typeclass.

def Magma.of_hom {X Y : Type u} [has_mul X] [has_mul Y] (f : Y) :

Typecheck a mul_hom as a morphism in Magma.

Equations

Typecheck a add_hom as a morphism in AddMagma.

@[instance]
Equations
@[instance]
@[instance]
@[instance]
def Magma.has_mul (M : Magma) :
Equations
@[simp]
theorem Magma.coe_of (R : Type u) [has_mul R] :
@[simp]
Type (u+1)

The category of additive semigroups and semigroup morphisms.

def Semigroup  :
Type (u+1)

The category of semigroups and semigroup morphisms.

Equations
@[instance]
Equations
@[instance]
@[instance]
@[instance]
@[instance]
@[instance]
def AddSemigroup.of (M : Type u)  :

Construct a bundled AddSemigroup from the underlying type and typeclass.

def Semigroup.of (M : Type u) [semigroup M] :

Construct a bundled Semigroup from the underlying type and typeclass.

Equations
def AddSemigroup.of_hom {X Y : Type u} (f : Y) :

Typecheck a add_hom as a morphism in AddSemigroup.

def Semigroup.of_hom {X Y : Type u} [semigroup X] [semigroup Y] (f : Y) :

Typecheck a mul_hom as a morphism in Semigroup.

Equations
@[instance]
@[instance]
Equations
@[instance]
Equations
@[instance]
@[simp]
theorem AddSemigroup.coe_of (R : Type u)  :
= R
@[simp]
theorem Semigroup.coe_of (R : Type u) [semigroup R] :
@[instance]
Equations

Build an isomorphism in the category AddMagma from an add_equiv between has_adds.

@[simp]
def mul_equiv.to_Magma_iso {X Y : Type u} [has_mul X] [has_mul Y] (e : X ≃* Y) :

Build an isomorphism in the category Magma from a mul_equiv between has_muls.

Equations
@[simp]
@[simp]
theorem mul_equiv.to_Magma_iso_inv {X Y : Type u} [has_mul X] [has_mul Y] (e : X ≃* Y) :
@[simp]
theorem mul_equiv.to_Magma_iso_hom {X Y : Type u} [has_mul X] [has_mul Y] (e : X ≃* Y) :
@[simp]
theorem add_equiv.to_AddSemigroup_iso_hom {X Y : Type u} (e : X ≃+ Y) :
@[simp]
theorem mul_equiv.to_Semigroup_iso_hom {X Y : Type u} [semigroup X] [semigroup Y] (e : X ≃* Y) :
def mul_equiv.to_Semigroup_iso {X Y : Type u} [semigroup X] [semigroup Y] (e : X ≃* Y) :

Build an isomorphism in the category Semigroup from a mul_equiv between semigroups.

Equations
@[simp]
theorem add_equiv.to_AddSemigroup_iso_neg {X Y : Type u} (e : X ≃+ Y) :
def add_equiv.to_AddSemigroup_iso {X Y : Type u} (e : X ≃+ Y) :

Build an isomorphism in the category AddSemigroup from an add_equiv between add_semigroups.

@[simp]
theorem mul_equiv.to_Semigroup_iso_inv {X Y : Type u} [semigroup X] [semigroup Y] (e : X ≃* Y) :

Build a mul_equiv from an isomorphism in the category Magma.

Equations

Build an add_equiv from an isomorphism in the category AddMagma.

Build a mul_equiv from an isomorphism in the category Semigroup.

Equations

Build an add_equiv from an isomorphism in the category AddSemigroup.

X ≃+ Y

additive equivalences between has_adds are the same as (isomorphic to) isomorphisms in AddMagma

def mul_equiv_iso_Magma_iso {X Y : Type u} [has_mul X] [has_mul Y] :
X ≃* Y

multiplicative equivalences between has_muls are the same as (isomorphic to) isomorphisms in Magma

Equations
def mul_equiv_iso_Semigroup_iso {X Y : Type u} [semigroup X] [semigroup Y] :
X ≃* Y

multiplicative equivalences between semigroups are the same as (isomorphic to) isomorphisms in Semigroup

Equations
additive equivalences between add_semigroups are the same as (isomorphic to) isomorphisms in AddSemigroup
Once we've shown that the forgetful functors to type reflect isomorphisms, we automatically obtain that the forget₂ functors between our concrete categories reflect isomorphisms.