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 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.

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

    Instances For
      @[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 bundled commutative ring giving the colimit of a diagram.

      Instances For

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

        Instances For

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

          Instances For
            @[simp]

            The cocone over the proposed colimit commutative ring.

            Instances For

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

              Instances For

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

                Instances For