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

Type (max u_1 u_2)

add_monoid_hom doesn't actually assume associativity. This alias is needed to make the category theory machinery work.

def Mon.assoc_monoid_hom (M : Type u_1) (N : Type u_2) [monoid M] [monoid N] :
Type (max u_1 u_2)

monoid_hom doesn't actually assume associativity. This alias is needed to make the category theory machinery work.

@[instance]
Equations
@[instance]
@[instance]
@[instance]
@[instance]
@[instance]
@[instance]
@[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
@[instance]
@[instance]
@[instance]
@[instance]
@[instance]
@[instance]
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
@[simp]
theorem add_equiv.to_Mon_iso_hom {X Y : Type u} [add_monoid X] [add_monoid Y] (e : X ≃+ Y) :
@[simp]
theorem add_equiv.to_Mon_iso_neg {X Y : Type u} [add_monoid X] [add_monoid Y] (e : X ≃+ Y) :
def mul_equiv.to_Mon_iso {X Y : Type u} [monoid X] [monoid Y] (e : X ≃* Y) :

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

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

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

@[simp]
theorem mul_equiv.to_Mon_iso_hom {X Y : Type u} [monoid X] [monoid Y] (e : X ≃* Y) :
def mul_equiv.to_CommMon_iso {X Y : Type u} [comm_monoid X] [comm_monoid Y] (e : X ≃* Y) :

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

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

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

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.