Documentation

Mathlib.Algebra.Category.Ring.Colimits

The category of commutative rings has all colimits. #

This file uses a "pre-automated" approach, just as for Mathlib/Algebra/Category/MonCat/Colimits.lean. It is a very uniform approach, that conceivably could be synthesised directly by a tactic that analyses the shape of CommRing and RingHom.

We build the colimit of a diagram in RingCat by constructing the free ring on the disjoint union of all the rings in the diagram, then taking the quotient by the ring laws within each ring, and the identifications given by the morphisms in the diagram.

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

Instances For

    The Relation on Prequotient saying when two expressions are equal because of the ring laws, or because one element is mapped to another by a morphism in the diagram.

    Instances For

      The setoid corresponding to commutative expressions modulo monoid Relations and identifications.

      Equations
      @[simp]
      theorem RingCat.Colimits.quot_zero {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J RingCat) :
      Quot.mk Setoid.r RingCat.Colimits.Prequotient.zero = 0
      @[simp]
      theorem RingCat.Colimits.quot_one {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J RingCat) :
      Quot.mk Setoid.r RingCat.Colimits.Prequotient.one = 1

      The bundled ring giving the colimit of a diagram.

      Equations
      Instances For

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

        Equations
        Instances For

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

          Equations
          Instances For
            @[simp]

            The cocone over the proposed colimit ring.

            Equations
            Instances For

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

              Equations
              Instances For

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

                Equations
                Instances For

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

                  Equations
                  Instances For

                    Evidence that the proposed colimit is the colimit.

                    Equations
                    Instances For

                      We build the colimit of a diagram in CommRingCat by constructing the free commutative ring on the disjoint union of all the commutative rings in the diagram, then taking the quotient by the commutative ring laws within each commutative ring, and the identifications given by the morphisms in the diagram.

                      The Relation on Prequotient saying when two expressions are equal because of the commutative ring laws, or because one element is mapped to another by a morphism in the diagram.

                      Instances For

                        The setoid corresponding to commutative expressions modulo monoid Relations and identifications.

                        Equations
                        @[simp]
                        theorem CommRingCat.Colimits.quot_zero {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommRingCat) :
                        Quot.mk Setoid.r CommRingCat.Colimits.Prequotient.zero = 0
                        @[simp]
                        theorem CommRingCat.Colimits.quot_one {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommRingCat) :
                        Quot.mk Setoid.r CommRingCat.Colimits.Prequotient.one = 1

                        The function from a given commutative ring in the diagram to the colimit commutative ring.

                        Equations
                        Instances For

                          The ring homomorphism from a given commutative ring in the diagram to the colimit commutative ring.

                          Equations
                          Instances For

                            The cocone over the proposed colimit commutative ring.

                            Equations
                            Instances For

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

                              Equations
                              Instances For

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

                                Equations
                                Instances For

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

                                  Equations
                                  Instances For