mathlib3 documentation

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.

source
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
source
@[protected, instance]
def Mon.colimits.prequotient.inhabited {J : Type v} [category_theory.small_category J] (F : J ⥤ Mon) :
inhabited (Mon.colimits.prequotient F)
Equations
source
inductive Mon.colimits.relation {J : Type v} [category_theory.small_category J] (F : J ⥤ Mon) :
Mon.colimits.prequotient F → Mon.colimits.prequotient F → Prop

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.

source
@[instance]
def Mon.colimits.colimit_setoid {J : Type v} [category_theory.small_category J] (F : J ⥤ Mon) :
setoid (Mon.colimits.prequotient F)

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

Equations
source
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
source
@[protected, instance]
def Mon.colimits.colimit_type.inhabited {J : Type v} [category_theory.small_category J] (F : J ⥤ Mon) :
inhabited (Mon.colimits.colimit_type F)
source
@[protected, instance]
def Mon.colimits.monoid_colimit_type {J : Type v} [category_theory.small_category J] (F : J ⥤ Mon) :
monoid (Mon.colimits.colimit_type F)
Equations
source
@[simp]
theorem Mon.colimits.quot_one {J : Type v} [category_theory.small_category J] (F : J ⥤ Mon) :
quot.mk setoid.r Mon.colimits.prequotient.one = 1
source
@[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
source
def Mon.colimits.colimit {J : Type v} [category_theory.small_category J] (F : J ⥤ Mon) :
Mon

The bundled monoid giving the colimit of a diagram.

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

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

Equations
source
def Mon.colimits.cocone_morphism {J : Type v} [category_theory.small_category J] (F : J ⥤ Mon) (j : J) :
F.obj j ⟶ Mon.colimits.colimit F

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

Equations
source
@[simp]
theorem Mon.colimits.cocone_naturality {J : Type v} [category_theory.small_category J] (F : J ⥤ Mon) {j j' : J} (f : j ⟶ j') :
F.map f ≫ Mon.colimits.cocone_morphism F j' = Mon.colimits.cocone_morphism F j
source
@[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)) :
⇑(Mon.colimits.cocone_morphism F j') (⇑(F.map f) x) = ⇑(Mon.colimits.cocone_morphism F j) x
source
def Mon.colimits.colimit_cocone {J : Type v} [category_theory.small_category J] (F : J ⥤ Mon) :
category_theory.limits.cocone F

The cocone over the proposed colimit monoid.

Equations
source
@[simp]
def Mon.colimits.desc_fun_lift {J : Type v} [category_theory.small_category J] (F : J ⥤ Mon) (s : category_theory.limits.cocone F) :
Mon.colimits.prequotient F → ↥(s.X)

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

Equations
source
def Mon.colimits.desc_fun {J : Type v} [category_theory.small_category J] (F : J ⥤ Mon) (s : category_theory.limits.cocone F) :
Mon.colimits.colimit_type F → ↥(s.X)

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

Equations
source
def Mon.colimits.desc_morphism {J : Type v} [category_theory.small_category J] (F : J ⥤ Mon) (s : category_theory.limits.cocone F) :
Mon.colimits.colimit F ⟶ s.X

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

Equations
source
def Mon.colimits.colimit_is_colimit {J : Type v} [category_theory.small_category J] (F : J ⥤ Mon) :
category_theory.limits.is_colimit (Mon.colimits.colimit_cocone F)

Evidence that the proposed colimit is the colimit.

Equations
source
@[protected, instance]
def Mon.colimits.has_colimits_Mon  :
category_theory.limits.has_colimits Mon