# The category of monoids has all colimits. #

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 what Lean 3's #print monoid printed a long time ago (it no longer looks like this due to the addition of npow fields):

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


and if we'd fed it the output of Lean 3's #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.

Note: Monoid and CommRing are no longer flat structures in Mathlib4, and so #print Monoid gives the less clear

inductive Monoid.{u} : Type u → Type u
number of parameters: 1
constructors:
Monoid.mk : {M : Type u} →
[toSemigroup : Semigroup M] →
[toOne : One M] →
(∀ (a : M), 1 * a = a) →
(∀ (a : M), a * 1 = a) →
(npow : ℕ → M → M) →
autoParam (∀ (x : M), npow 0 x = 1) _auto✝ →
autoParam (∀ (n : ℕ) (x : M), npow (n + 1) x = x * npow n x) _auto✝¹ → Monoid M


We build the colimit of a diagram in MonCat 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 MonCat.Colimits.Prequotient {J : Type v} (F : ) :

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

• of: {J : Type v} → [inst : ] → {F : } → (j : J) → (F.obj j)
• one: {J : Type v} → [inst : ] →
• mul: {J : Type v} → [inst : ] →
Instances For
Equations
• = { default := MonCat.Colimits.Prequotient.one }
inductive MonCat.Colimits.Relation {J : Type v} (F : ) :

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.

Instances For
instance MonCat.Colimits.colimitSetoid {J : Type v} (F : ) :

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

Equations
• = { r := , iseqv := }
def MonCat.Colimits.ColimitType {J : Type v} (F : ) :

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

Equations
Instances For
Equations
• = id inferInstance
instance MonCat.Colimits.monoidColimitType {J : Type v} (F : ) :
Equations
@[simp]
theorem MonCat.Colimits.quot_one {J : Type v} (F : ) :
Quot.mk Setoid.r MonCat.Colimits.Prequotient.one = 1
@[simp]
theorem MonCat.Colimits.quot_mul {J : Type v} (F : ) (x : ) (y : ) :
Quot.mk Setoid.r (x.mul y) = Quot.mk Setoid.r x * Quot.mk Setoid.r y
def MonCat.Colimits.colimit {J : Type v} (F : ) :

The bundled monoid giving the colimit of a diagram.

Equations
• = { α := , str := inferInstance }
Instances For
def MonCat.Colimits.coconeFun {J : Type v} (F : ) (j : J) (x : (F.obj j)) :

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

Equations
Instances For
def MonCat.Colimits.coconeMorphism {J : Type v} (F : ) (j : J) :
F.obj j

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

Equations
• = { toFun := , map_one' := , map_mul' := }
Instances For
@[simp]
theorem MonCat.Colimits.cocone_naturality {J : Type v} (F : ) {j : J} {j' : J} (f : j j') :
@[simp]
theorem MonCat.Colimits.cocone_naturality_components {J : Type v} (F : ) (j : J) (j' : J) (f : j j') (x : (F.obj j)) :
((F.map f) x) =

The cocone over the proposed colimit monoid.

Equations
• = { pt := , ι := { app := , naturality := } }
Instances For
def MonCat.Colimits.descFunLift {J : Type v} (F : ) (s : ) :
s.pt

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

Equations
Instances For
def MonCat.Colimits.descFun {J : Type v} (F : ) (s : ) :
s.pt

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

Equations
Instances For
def MonCat.Colimits.descMorphism {J : Type v} (F : ) (s : ) :
s.pt

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

Equations
• = { toFun := , map_one' := , map_mul' := }
Instances For

Evidence that the proposed colimit is the colimit.

Equations
• = { desc := fun (s : ) => , fac := , uniq := }
Instances For