# mathlibdocumentation

algebra.category.Mon.basic

We introduce the bundled categories:

• Mon
• AddMon
• CommMon
• AddCommMon along with the relevant forgetful functors between them.
def Mon  :
Type (u+1)

The category of monoids and monoid morphisms.

Equations
Type (u+1)

The category of additive monoids and monoid morphisms.

@[instance]

Equations
@[instance]

Construct a bundled Mon from the underlying type and typeclass.

def Mon.of (M : Type u) [monoid M] :

Construct a bundled Mon from the underlying type and typeclass.

Equations
@[instance]

Equations
@[instance]

@[instance]
def Mon.monoid (M : Mon) :

Equations
@[instance]

@[simp]

@[simp]
theorem Mon.coe_of (R : Type u) [monoid R] :
(Mon.of R) = R

Type (u+1)

The category of additive commutative monoids and monoid morphisms.

def CommMon  :
Type (u+1)

The category of commutative monoids and monoid morphisms.

Equations
@[instance]

Equations
def AddCommMon.of (M : Type u)  :

Construct a bundled AddCommMon from the underlying type and typeclass.

def CommMon.of (M : Type u) [comm_monoid M] :

Construct a bundled CommMon from the underlying type and typeclass.

Equations
@[instance]

Equations
@[instance]

@[instance]

Equations
@[instance]

@[simp]
theorem AddCommMon.coe_of (R : Type u)  :
= R

@[simp]
theorem CommMon.coe_of (R : Type u) [comm_monoid R] :

@[instance]

@[instance]

Equations
def mul_equiv.to_Mon_iso {X Y : Type u} [monoid X] [monoid Y] :
X ≃* Y(Mon.of X Mon.of Y)

Build an isomorphism in the category Mon from a mul_equiv between monoids.

Equations
X ≃+ Y

Build an isomorphism in the category AddMon from an add_equiv between add_monoids.

@[simp]

@[simp]
theorem mul_equiv.to_Mon_iso_hom {X Y : Type u} [monoid X] [monoid Y] {e : X ≃* Y} :

@[simp]
theorem mul_equiv.to_Mon_iso_inv {X Y : Type u} [monoid X] [monoid Y] {e : X ≃* Y} :

@[simp]

def mul_equiv.to_CommMon_iso {X Y : Type u} [comm_monoid X] [comm_monoid Y] :
X ≃* Y

Build an isomorphism in the category CommMon from a mul_equiv between comm_monoids.

Equations
X ≃+ Y

Build an isomorphism in the category AddCommMon from an add_equiv between add_comm_monoids.

@[simp]
theorem add_equiv.to_AddCommMon_iso_hom {X Y : Type u} {e : X ≃+ Y} :

@[simp]
theorem mul_equiv.to_CommMon_iso_hom {X Y : Type u} [comm_monoid X] [comm_monoid Y] {e : X ≃* Y} :

@[simp]
theorem mul_equiv.to_CommMon_iso_inv {X Y : Type u} [comm_monoid X] [comm_monoid Y] {e : X ≃* Y} :

@[simp]
theorem add_equiv.to_AddCommMon_iso_inv {X Y : Type u} {e : X ≃+ Y} :

Build an add_equiv from an isomorphism in the category AddMon.

Build a mul_equiv from an isomorphism in the category Mon.

Equations

Build an add_equiv from an isomorphism in the category AddCommMon.

Build a mul_equiv from an isomorphism in the category CommMon.

Equations
def mul_equiv_iso_Mon_iso {X Y : Type u} [monoid X] [monoid Y] :
X ≃* Y

multiplicative equivalences between monoids are the same as (isomorphic to) isomorphisms in Mon

Equations
X ≃+ Y

additive equivalences between add_monoids are the same as (isomorphic to) isomorphisms in AddMon

def mul_equiv_iso_CommMon_iso {X Y : Type u} [comm_monoid X] [comm_monoid Y] :
X ≃* Y

multiplicative equivalences between comm_monoids are the same as (isomorphic to) isomorphisms in CommMon

Equations
additive equivalences between add_comm_monoids are the same as (isomorphic to) isomorphisms in AddCommMon
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.