mathlib documentation

algebra.category.Mon.colimits

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 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} [category_theory.small_category J] (F : J Mon) :
Type v

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

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]

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

Equations
def Mon.colimits.colimit_type {J : Type v} [category_theory.small_category J] (F : J Mon) :
Type v

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

Equations
Instances for Mon.colimits.colimit_type
@[simp]
theorem Mon.colimits.quot_mul {J : Type v} [category_theory.small_category J] (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

The bundled monoid giving the colimit of a diagram.

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

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

Equations

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

Equations
@[simp]
theorem Mon.colimits.cocone_naturality_components {J : Type v} [category_theory.small_category J] (F : J Mon) (j j' : J) (f : j j') (x : (F.obj j)) :
@[simp]

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

Equations

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

Equations

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

Equations