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.

def AddMon.assoc_add_monoid_hom (M : Type u_1) (N : Type u_2) [add_monoid M] [add_monoid N] :
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
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
def AddMon.of_hom {X Y : Type u} [add_monoid X] [add_monoid Y] (f : X →+ Y) :

Typecheck a add_monoid_hom as a morphism in AddMon.

def Mon.of_hom {X Y : Type u} [monoid X] [monoid Y] (f : X →* Y) :

Typecheck a monoid_hom as a morphism in Mon.

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] :
@[simp]
theorem add_equiv.to_AddMon_iso_hom {X Y : Type u} [add_monoid X] [add_monoid Y] (e : X ≃+ Y) :
@[simp]
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) :
def add_equiv.to_AddMon_iso {X Y : Type u} [add_monoid X] [add_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]
@[simp]
theorem mul_equiv.to_CommMon_iso_hom {X Y : Type u} [comm_monoid X] [comm_monoid Y] (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] :

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.