# mathlib3documentation

algebra.category.Mon.colimits

# The category of monoids has all colimits. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

We do this construction knowing nothing about monoids. In particular, I want to claim that this file could be produced by a python script that just looks at the output of #print monoid:

-- structure monoid : Type u → Type u -- fields: -- monoid.mul : Π {α : Type u} [c : monoid α], α → α → α -- monoid.mul_assoc : ∀ {α : Type u} [c : monoid α] (a b c_1 : α), a * b * c_1 = a * (b * c_1) -- monoid.one : Π (α : Type u) [c : monoid α], α -- monoid.one_mul : ∀ {α : Type u} [c : monoid α] (a : α), 1 * a = a -- monoid.mul_one : ∀ {α : Type u} [c : monoid α] (a : α), a * 1 = a

and if we'd fed it the output of #print comm_ring, this file would instead build colimits of commutative rings.

A slightly bolder claim is that we could do this with tactics, as well.

We build the colimit of a diagram in Mon by constructing the free monoid on the disjoint union of all the monoids in the diagram, then taking the quotient by the monoid laws within each monoid, and the identifications given by the morphisms in the diagram.

inductive Mon.colimits.prequotient {J : Type v} (F : J Mon) :

An inductive type representing all monoid expressions (without relations) on a collection of types indexed by the objects of J.

Instances for Mon.colimits.prequotient
@[protected, instance]
Equations
inductive Mon.colimits.relation {J : Type v} (F : J Mon) :

The relation on prequotient saying when two expressions are equal because of the monoid laws, or because one element is mapped to another by a morphism in the diagram.

@[instance]
def Mon.colimits.colimit_setoid {J : Type v} (F : J Mon) :

The setoid corresponding to monoid expressions modulo monoid relations and identifications.

Equations
def Mon.colimits.colimit_type {J : Type v} (F : J Mon) :

The underlying type of the colimit of a diagram in Mon.

Equations
Instances for Mon.colimits.colimit_type
@[protected, instance]
@[protected, instance]
def Mon.colimits.monoid_colimit_type {J : Type v} (F : J Mon) :
Equations
@[simp]
theorem Mon.colimits.quot_one {J : Type v} (F : J Mon) :
= 1
@[simp]
theorem Mon.colimits.quot_mul {J : Type v} (F : J Mon) (x y : Mon.colimits.prequotient F) :
quot.mk setoid.r (x.mul y) = quot.mk setoid.r x * quot.mk setoid.r y
def Mon.colimits.colimit {J : Type v} (F : J Mon) :

The bundled monoid giving the colimit of a diagram.

Equations
def Mon.colimits.cocone_fun {J : Type v} (F : J Mon) (j : J) (x : (F.obj j)) :

The function from a given monoid in the diagram to the colimit monoid.

Equations
def Mon.colimits.cocone_morphism {J : Type v} (F : J Mon) (j : J) :
F.obj j

The monoid homomorphism from a given monoid in the diagram to the colimit monoid.

Equations
@[simp]
theorem Mon.colimits.cocone_naturality {J : Type v} (F : J Mon) {j j' : J} (f : j j') :
@[simp]
theorem Mon.colimits.cocone_naturality_components {J : Type v} (F : J Mon) (j j' : J) (f : j j') (x : (F.obj j)) :
((F.map f) x) =
def Mon.colimits.colimit_cocone {J : Type v} (F : J Mon) :

The cocone over the proposed colimit monoid.

Equations
@[simp]
def Mon.colimits.desc_fun_lift {J : Type v} (F : J Mon)  :

The function from the free monoid on the diagram to the cone point of any other cocone.

Equations
def Mon.colimits.desc_fun {J : Type v} (F : J Mon)  :

The function from the colimit monoid to the cone point of any other cocone.

Equations
• = quot.lift _
def Mon.colimits.desc_morphism {J : Type v} (F : J Mon)  :

The monoid homomorphism from the colimit monoid to the cone point of any other cocone.

Equations

Evidence that the proposed colimit is the colimit.

Equations
@[protected, instance]