# mathlibdocumentation

algebra.category.Semigroup.basic

# Category instances for has_mul, has_add, semigroup and add_semigroup #

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)

The category of additive magmas and additive magma morphisms.

Equations
def Magma  :
Type (u+1)

The category of magmas and magma morphisms.

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

Construct a bundled Magma from the underlying type and typeclass.

Equations
def AddMagma.of (M : Type u) [has_add M] :

Construct a bundled AddMagma from the underlying type and typeclass.

Equations
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
def AddMagma.of_hom {X Y : Type u} [has_add X] [has_add Y] (f : Y) :

Typecheck a add_hom as a morphism in AddMagma.

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

The category of additive semigroups and semigroup morphisms.

Equations
def Semigroup  :
Type (u+1)

The category of semigroups and semigroup morphisms.

Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
def Semigroup.has_coe_to_sort  :
(Type u_1)
Equations
@[protected, instance]
(Type u_1)
Equations
def AddSemigroup.of (M : Type u)  :

Construct a bundled AddSemigroup from the underlying type and typeclass.

Equations
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.

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

Typecheck a mul_hom as a morphism in Semigroup.

Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[simp]
theorem AddSemigroup.coe_of (R : Type u)  :
= R
@[simp]
theorem Semigroup.coe_of (R : Type u) [semigroup R] :
@[protected, instance]
Equations
@[protected, instance]
Equations
def add_equiv.to_AddMagma_iso {X Y : Type u} [has_add X] [has_add Y] (e : X ≃+ Y) :

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

Equations
@[simp]
theorem add_equiv.to_AddMagma_iso_hom {X Y : Type u} [has_add X] [has_add Y] (e : X ≃+ Y) :
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]
theorem add_equiv.to_AddMagma_iso_neg {X Y : Type u} [has_add X] [has_add Y] (e : X ≃+ Y) :
@[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.

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

Equations

Build a mul_equiv from an isomorphism in the category Semigroup.

Equations

Build an add_equiv from an isomorphism in the category AddSemigroup.

Equations
X ≃+ Y

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

Equations
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
def add_equiv_iso_AddSemigroup_iso {X Y : Type u}  :
X ≃+ Y

additive equivalences between add_semigroups are the same as (isomorphic to) isomorphisms in AddSemigroup

Equations
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]

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.