Documentation

Mathlib.Algebra.Category.MonCat.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 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.

source
inductive MonCat.Colimits.Prequotient {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J MonCat) :
Type v

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

Instances For
    source
    instance MonCat.Colimits.instInhabitedPrequotient {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J MonCat) :
    Inhabited (MonCat.Colimits.Prequotient F)
    Equations
    source
    inductive MonCat.Colimits.Relation {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J MonCat) :
    MonCat.Colimits.Prequotient F → MonCat.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.

    Instances For
      source
      instance MonCat.Colimits.colimitSetoid {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J MonCat) :
      Setoid (MonCat.Colimits.Prequotient F)

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

      Equations
      source
      def MonCat.Colimits.ColimitType {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J MonCat) :
      Type v

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

      Equations
      Instances For
        source
        instance MonCat.Colimits.instInhabitedColimitType {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J MonCat) :
        Inhabited (MonCat.Colimits.ColimitType F)
        Equations
        source
        instance MonCat.Colimits.monoidColimitType {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J MonCat) :
        Monoid (MonCat.Colimits.ColimitType F)
        Equations
        source
        @[simp]
        theorem MonCat.Colimits.quot_one {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J MonCat) :
        Quot.mk (⇑(MonCat.Colimits.colimitSetoid F)) MonCat.Colimits.Prequotient.one = 1
        source
        @[simp]
        theorem MonCat.Colimits.quot_mul {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J MonCat) (x : MonCat.Colimits.Prequotient F) (y : MonCat.Colimits.Prequotient F) :
        Quot.mk (⇑(MonCat.Colimits.colimitSetoid F)) (x.mul y) = Quot.mk (⇑(MonCat.Colimits.colimitSetoid F)) x * Quot.mk (⇑(MonCat.Colimits.colimitSetoid F)) y
        source
        def MonCat.Colimits.colimit {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J MonCat) :
        MonCat

        The bundled monoid giving the colimit of a diagram.

        Equations
        Instances For
          source
          def MonCat.Colimits.coconeFun {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J MonCat) (j : J) (x : ↑(F.obj j)) :
          MonCat.Colimits.ColimitType F

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

          Equations
          Instances For
            source
            def MonCat.Colimits.coconeMorphism {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J MonCat) (j : J) :
            F.obj j ⟶ MonCat.Colimits.colimit F

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

            Equations
            Instances For
              source
              @[simp]
              theorem MonCat.Colimits.cocone_naturality {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J MonCat) {j : J} {j' : J} (f : j ⟶ j') :
              CategoryTheory.CategoryStruct.comp (F.map f) (MonCat.Colimits.coconeMorphism F j') = MonCat.Colimits.coconeMorphism F j
              source
              @[simp]
              theorem MonCat.Colimits.cocone_naturality_components {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J MonCat) (j : J) (j' : J) (f : j ⟶ j') (x : ↑(F.obj j)) :
              (MonCat.Colimits.coconeMorphism F j') ((F.map f) x) = (MonCat.Colimits.coconeMorphism F j) x
              source
              def MonCat.Colimits.colimitCocone {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J MonCat) :
              CategoryTheory.Limits.Cocone F

              The cocone over the proposed colimit monoid.

              Equations
              Instances For
                source
                def MonCat.Colimits.descFunLift {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J MonCat) (s : CategoryTheory.Limits.Cocone F) :
                MonCat.Colimits.Prequotient F → ↑s.pt

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

                Equations
                Instances For
                  source
                  def MonCat.Colimits.descFun {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J MonCat) (s : CategoryTheory.Limits.Cocone F) :
                  MonCat.Colimits.ColimitType F → ↑s.pt

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

                  Equations
                  Instances For
                    source
                    def MonCat.Colimits.descMorphism {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J MonCat) (s : CategoryTheory.Limits.Cocone F) :
                    MonCat.Colimits.colimit F ⟶ s.pt

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

                    Equations
                    Instances For
                      source
                      def MonCat.Colimits.colimitIsColimit {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J MonCat) :
                      CategoryTheory.Limits.IsColimit (MonCat.Colimits.colimitCocone F)

                      Evidence that the proposed colimit is the colimit.

                      Equations
                      Instances For
                        source
                        instance MonCat.Colimits.hasColimits_monCat :
                        CategoryTheory.Limits.HasColimits MonCat
                        Equations