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.

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

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

Instances For
    source
    instance CommRingCat.Colimits.instInhabitedPrequotient {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommRingCat) :
    Inhabited (CommRingCat.Colimits.Prequotient F)
    Equations
    source
    inductive CommRingCat.Colimits.Relation {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommRingCat) :
    CommRingCat.Colimits.Prequotient F → CommRingCat.Colimits.Prequotient F → Prop

    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
      source
      instance CommRingCat.Colimits.colimitSetoid {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommRingCat) :
      Setoid (CommRingCat.Colimits.Prequotient F)

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

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

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

      Equations
      Instances For
        source
        instance CommRingCat.Colimits.ColimitType.AddGroup {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommRingCat) :
        AddGroup (CommRingCat.Colimits.ColimitType F)
        Equations
        source
        instance CommRingCat.Colimits.InhabitedColimitType {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommRingCat) :
        Inhabited (CommRingCat.Colimits.ColimitType F)
        Equations
        source
        instance CommRingCat.Colimits.ColimitType.AddGroupWithOne {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommRingCat) :
        AddGroupWithOne (CommRingCat.Colimits.ColimitType F)
        Equations
        • One or more equations did not get rendered due to their size.
        source
        instance CommRingCat.Colimits.instCommRingColimitType {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommRingCat) :
        CommRing (CommRingCat.Colimits.ColimitType F)
        Equations
        source
        @[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
        source
        @[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
        source
        @[simp]
        theorem CommRingCat.Colimits.quot_neg {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommRingCat) (x : CommRingCat.Colimits.Prequotient F) :
        Quot.mk Setoid.r (CommRingCat.Colimits.Prequotient.neg x) = -Quot.mk Setoid.r x
        source
        @[simp]
        theorem CommRingCat.Colimits.quot_add {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommRingCat) (x : CommRingCat.Colimits.Prequotient F) (y : CommRingCat.Colimits.Prequotient F) :
        Quot.mk Setoid.r (CommRingCat.Colimits.Prequotient.add x y) = Quot.mk Setoid.r x + Quot.mk Setoid.r y
        source
        @[simp]
        theorem CommRingCat.Colimits.quot_mul {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommRingCat) (x : CommRingCat.Colimits.Prequotient F) (y : CommRingCat.Colimits.Prequotient F) :
        Quot.mk Setoid.r (CommRingCat.Colimits.Prequotient.mul x y) = Quot.mk Setoid.r x * Quot.mk Setoid.r y
        source
        def CommRingCat.Colimits.colimit {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommRingCat) :
        CommRingCat

        The bundled commutative ring giving the colimit of a diagram.

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

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

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

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

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              @[simp]
              theorem CommRingCat.Colimits.cocone_naturality {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommRingCat) {j : J} {j' : J} (f : j ⟶ j') :
              CategoryTheory.CategoryStruct.comp (F.toPrefunctor.map f) (CommRingCat.Colimits.coconeMorphism F j') = CommRingCat.Colimits.coconeMorphism F j
              source
              @[simp]
              theorem CommRingCat.Colimits.cocone_naturality_components {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommRingCat) (j : J) (j' : J) (f : j ⟶ j') (x : ↑(F.toPrefunctor.obj j)) :
              (CommRingCat.Colimits.coconeMorphism F j') ((F.toPrefunctor.map f) x) = (CommRingCat.Colimits.coconeMorphism F j) x
              source
              def CommRingCat.Colimits.colimitCocone {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommRingCat) :
              CategoryTheory.Limits.Cocone F

              The cocone over the proposed colimit commutative ring.

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

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

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

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

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    def CommRingCat.Colimits.descMorphism {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommRingCat) (s : CategoryTheory.Limits.Cocone F) :
                    CommRingCat.Colimits.colimit F ⟶ s.pt

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

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      source
                      def CommRingCat.Colimits.colimitIsColimit {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommRingCat) :
                      CategoryTheory.Limits.IsColimit (CommRingCat.Colimits.colimitCocone F)

                      Evidence that the proposed colimit is the colimit.

                      Equations
                      Instances For
                        source
                        instance CommRingCat.Colimits.hasColimits_commRingCat :
                        CategoryTheory.Limits.HasColimits CommRingCat
                        Equations