mathlib documentation

algebra.category.Semigroup.basic

Category instances for has_mul, has_add, semigroup and add_semigroup #

We introduce the bundled categories:

This closely follows algebra.category.Mon.basic.

TODO #

def AddMagma  :
Type (u+1)

The category of additive magmas and additive magma morphisms.

def Magma  :
Type (u+1)

The category of magmas and magma morphisms.

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

def Magma.of_hom {X Y : Type u} [has_mul X] [has_mul Y] (f : mul_hom X 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 : add_hom X Y) :

Typecheck a add_hom as a morphism in AddMagma.

@[instance]
@[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] :
def AddSemigroup  :
Type (u+1)

The category of additive semigroups and semigroup morphisms.

def Semigroup  :
Type (u+1)

The category of semigroups and semigroup morphisms.

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

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

Typecheck a add_hom as a morphism in AddSemigroup.

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

Typecheck a mul_hom as a morphism in Semigroup.

Equations
@[instance]
Equations
@[simp]
theorem AddSemigroup.coe_of (R : Type u) [add_semigroup R] :
@[simp]
theorem Semigroup.coe_of (R : Type u) [semigroup R] :
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.

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

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.

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] :

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

Equations

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.