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.
- of : Π {J : Type v} [_inst_1 : category_theory.small_category J] (F : J ⥤ Mon) (j : J), ↥(F.obj j) → Mon.colimits.prequotient F
- one : Π {J : Type v} [_inst_1 : category_theory.small_category J] (F : J ⥤ Mon), Mon.colimits.prequotient F
- mul : Π {J : Type v} [_inst_1 : category_theory.small_category J] (F : J ⥤ Mon), Mon.colimits.prequotient F → Mon.colimits.prequotient F → Mon.colimits.prequotient F
An inductive type representing all monoid expressions (without relations)
on a collection of types indexed by the objects of J.
Equations
- refl : ∀ {J : Type v} [_inst_1 : category_theory.small_category J] (F : J ⥤ Mon) (x : Mon.colimits.prequotient F), Mon.colimits.relation F x x
- symm : ∀ {J : Type v} [_inst_1 : category_theory.small_category J] (F : J ⥤ Mon) (x y : Mon.colimits.prequotient F), Mon.colimits.relation F x y → Mon.colimits.relation F y x
- trans : ∀ {J : Type v} [_inst_1 : category_theory.small_category J] (F : J ⥤ Mon) (x y z : Mon.colimits.prequotient F), Mon.colimits.relation F x y → Mon.colimits.relation F y z → Mon.colimits.relation F x z
- map : ∀ {J : Type v} [_inst_1 : category_theory.small_category J] (F : J ⥤ Mon) (j j' : J) (f : j ⟶ j') (x : ↥(F.obj j)), Mon.colimits.relation F (Mon.colimits.prequotient.of j' (⇑(F.map f) x)) (Mon.colimits.prequotient.of j x)
- mul : ∀ {J : Type v} [_inst_1 : category_theory.small_category J] (F : J ⥤ Mon) (j : J) (x y : ↥(F.obj j)), Mon.colimits.relation F (Mon.colimits.prequotient.of j (x * y)) ((Mon.colimits.prequotient.of j x).mul (Mon.colimits.prequotient.of j y))
- one : ∀ {J : Type v} [_inst_1 : category_theory.small_category J] (F : J ⥤ Mon) (j : J), Mon.colimits.relation F (Mon.colimits.prequotient.of j 1) Mon.colimits.prequotient.one
- mul_1 : ∀ {J : Type v} [_inst_1 : category_theory.small_category J] (F : J ⥤ Mon) (x x' y : Mon.colimits.prequotient F), Mon.colimits.relation F x x' → Mon.colimits.relation F (x.mul y) (x'.mul y)
- mul_2 : ∀ {J : Type v} [_inst_1 : category_theory.small_category J] (F : J ⥤ Mon) (x y y' : Mon.colimits.prequotient F), Mon.colimits.relation F y y' → Mon.colimits.relation F (x.mul y) (x.mul y')
- mul_assoc : ∀ {J : Type v} [_inst_1 : category_theory.small_category J] (F : J ⥤ Mon) (x y z : Mon.colimits.prequotient F), Mon.colimits.relation F ((x.mul y).mul z) (x.mul (y.mul z))
- one_mul : ∀ {J : Type v} [_inst_1 : category_theory.small_category J] (F : J ⥤ Mon) (x : Mon.colimits.prequotient F), Mon.colimits.relation F (Mon.colimits.prequotient.one.mul x) x
- mul_one : ∀ {J : Type v} [_inst_1 : category_theory.small_category J] (F : J ⥤ Mon) (x : Mon.colimits.prequotient F), Mon.colimits.relation F (x.mul Mon.colimits.prequotient.one) x
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.
The setoid corresponding to monoid expressions modulo monoid relations and identifications.
Equations
- Mon.colimits.colimit_setoid F = {r := Mon.colimits.relation F, iseqv := _}
The underlying type of the colimit of a diagram in Mon.
Equations
Equations
- Mon.colimits.monoid_colimit_type F = {mul := quot.lift (λ (x : Mon.colimits.prequotient F), quot.lift (λ (y : Mon.colimits.prequotient F), quot.mk setoid.r (x.mul y)) _) _, mul_assoc := _, one := quot.mk setoid.r Mon.colimits.prequotient.one, one_mul := _, mul_one := _}
The bundled monoid giving the colimit of a diagram.
Equations
The function from a given monoid in the diagram to the colimit monoid.
Equations
- Mon.colimits.cocone_fun F j x = quot.mk setoid.r (Mon.colimits.prequotient.of j x)
The monoid homomorphism from a given monoid in the diagram to the colimit monoid.
Equations
- Mon.colimits.cocone_morphism F j = {to_fun := Mon.colimits.cocone_fun F j, map_one' := _, map_mul' := _}
The cocone over the proposed colimit monoid.
Equations
- Mon.colimits.colimit_cocone F = {X := Mon.colimits.colimit F, ι := {app := Mon.colimits.cocone_morphism F, naturality' := _}}
The function from the free monoid on the diagram to the cone point of any other cocone.
Equations
- Mon.colimits.desc_fun_lift F s (x.mul y) = Mon.colimits.desc_fun_lift F s x * Mon.colimits.desc_fun_lift F s y
- Mon.colimits.desc_fun_lift F s Mon.colimits.prequotient.one = 1
- Mon.colimits.desc_fun_lift F s (Mon.colimits.prequotient.of j x) = ⇑(s.ι.app j) x
The function from the colimit monoid to the cone point of any other cocone.
Equations
- Mon.colimits.desc_fun F s = quot.lift (Mon.colimits.desc_fun_lift F s) _
The monoid homomorphism from the colimit monoid to the cone point of any other cocone.
Equations
- Mon.colimits.desc_morphism F s = {to_fun := Mon.colimits.desc_fun F s, map_one' := _, map_mul' := _}
Evidence that the proposed colimit is the colimit.
Equations
- Mon.colimits.colimit_is_colimit F = {desc := λ (s : category_theory.limits.cocone F), Mon.colimits.desc_morphism F s, fac' := _, uniq' := _}
Equations
- Mon.colimits.has_colimits_Mon = {has_colimits_of_shape := λ (J : Type u_1) (𝒥 : category_theory.small_category J), {has_colimit := λ (F : J ⥤ Mon), {cocone := Mon.colimits.colimit_cocone F, is_colimit := Mon.colimits.colimit_is_colimit F}}}