mathlib documentation

algebra.category.Mon.basic

Category instances for monoid, add_monoid, comm_monoid, and add_comm_monoid.

We introduce the bundled categories:

def Mon  :
Type (u+1)

The category of monoids and monoid morphisms.

Equations
def AddMon  :
Type (u+1)

The category of additive monoids and monoid morphisms.

@[instance]

Equations
def AddMon.of (M : Type u) [add_monoid M] :

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]

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

Equations
@[instance]

@[simp]
theorem AddMon.coe_of (R : Type u) [add_monoid R] :

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

def AddCommMon  :
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
def AddCommMon.of (M : Type u) [add_comm_monoid M] :

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
@[simp]
theorem AddCommMon.coe_of (R : Type u) [add_comm_monoid R] :

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

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
def add_equiv.to_AddMon_iso {X Y : Type u} [add_monoid X] [add_monoid Y] :
X ≃+ Y(AddMon.of X AddMon.of Y)

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

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

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

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

Equations

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

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

@[simp]

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

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

Equations

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

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.