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.

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

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

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

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

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

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

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

      Equations
      Instances For
        source
        instance RingCat.Colimits.ColimitType.instZero {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J RingCat) :
        Zero (RingCat.Colimits.ColimitType F)
        Equations
        source
        instance RingCat.Colimits.ColimitType.instAdd {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J RingCat) :
        Add (RingCat.Colimits.ColimitType F)
        Equations
        source
        instance RingCat.Colimits.ColimitType.instNeg {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J RingCat) :
        Neg (RingCat.Colimits.ColimitType F)
        Equations
        source
        instance RingCat.Colimits.ColimitType.AddGroup {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J RingCat) :
        AddGroup (RingCat.Colimits.ColimitType F)
        Equations
        source
        instance RingCat.Colimits.InhabitedColimitType {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J RingCat) :
        Inhabited (RingCat.Colimits.ColimitType F)
        Equations
        source
        instance RingCat.Colimits.ColimitType.AddGroupWithOne {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J RingCat) :
        AddGroupWithOne (RingCat.Colimits.ColimitType F)
        Equations
        source
        instance RingCat.Colimits.instRingColimitType {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J RingCat) :
        Ring (RingCat.Colimits.ColimitType F)
        Equations
        source
        @[simp]
        theorem RingCat.Colimits.quot_zero {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J RingCat) :
        Quot.mk (⇑(RingCat.Colimits.colimitSetoid F)) RingCat.Colimits.Prequotient.zero = 0
        source
        @[simp]
        theorem RingCat.Colimits.quot_one {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J RingCat) :
        Quot.mk (⇑(RingCat.Colimits.colimitSetoid F)) RingCat.Colimits.Prequotient.one = 1
        source
        @[simp]
        theorem RingCat.Colimits.quot_neg {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J RingCat) (x : RingCat.Colimits.Prequotient F) :
        Quot.mk (⇑(RingCat.Colimits.colimitSetoid F)) x.neg = -Quot.mk (⇑(RingCat.Colimits.colimitSetoid F)) x
        source
        @[simp]
        theorem RingCat.Colimits.quot_add {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J RingCat) (x y : RingCat.Colimits.Prequotient F) :
        Quot.mk (⇑(RingCat.Colimits.colimitSetoid F)) (x.add y) = Quot.mk (⇑(RingCat.Colimits.colimitSetoid F)) x + Quot.mk (⇑(RingCat.Colimits.colimitSetoid F)) y
        source
        @[simp]
        theorem RingCat.Colimits.quot_mul {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J RingCat) (x y : RingCat.Colimits.Prequotient F) :
        Quot.mk (⇑(RingCat.Colimits.colimitSetoid F)) (x.mul y) = Quot.mk (⇑(RingCat.Colimits.colimitSetoid F)) x * Quot.mk (⇑(RingCat.Colimits.colimitSetoid F)) y
        source
        def RingCat.Colimits.colimit {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J RingCat) :
        RingCat

        The bundled ring giving the colimit of a diagram.

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

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

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

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

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

              The cocone over the proposed colimit ring.

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

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

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

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

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

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

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

                      Evidence that the proposed colimit is the colimit.

                      Equations
                      Instances For
                        source
                        instance RingCat.Colimits.hasColimits_ringCat :
                        CategoryTheory.Limits.HasColimits RingCat
                        Equations

                        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.instZero {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommRingCat) :
                              Zero (CommRingCat.Colimits.ColimitType F)
                              Equations
                              source
                              instance CommRingCat.Colimits.ColimitType.instAdd {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommRingCat) :
                              Add (CommRingCat.Colimits.ColimitType F)
                              Equations
                              source
                              instance CommRingCat.Colimits.ColimitType.instNeg {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommRingCat) :
                              Neg (CommRingCat.Colimits.ColimitType F)
                              Equations
                              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
                              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 (⇑(CommRingCat.Colimits.colimitSetoid F)) 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 (⇑(CommRingCat.Colimits.colimitSetoid F)) 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 (⇑(CommRingCat.Colimits.colimitSetoid F)) x.neg = -Quot.mk (⇑(CommRingCat.Colimits.colimitSetoid F)) x
                              source
                              @[simp]
                              theorem CommRingCat.Colimits.quot_add {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommRingCat) (x y : CommRingCat.Colimits.Prequotient F) :
                              Quot.mk (⇑(CommRingCat.Colimits.colimitSetoid F)) (x.add y) = Quot.mk (⇑(CommRingCat.Colimits.colimitSetoid F)) x + Quot.mk (⇑(CommRingCat.Colimits.colimitSetoid F)) y
                              source
                              @[simp]
                              theorem CommRingCat.Colimits.quot_mul {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommRingCat) (x y : CommRingCat.Colimits.Prequotient F) :
                              Quot.mk (⇑(CommRingCat.Colimits.colimitSetoid F)) (x.mul y) = Quot.mk (⇑(CommRingCat.Colimits.colimitSetoid F)) x * Quot.mk (⇑(CommRingCat.Colimits.colimitSetoid F)) 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.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.obj j ⟶ CommRingCat.Colimits.colimit F

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

                                  Equations
                                  Instances For
                                    source
                                    @[simp]
                                    theorem CommRingCat.Colimits.cocone_naturality {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommRingCat) {j j' : J} (f : j ⟶ j') :
                                    CategoryTheory.CategoryStruct.comp (F.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) (f : j ⟶ j') (x : ↑(F.obj j)) :
                                    (CommRingCat.Colimits.coconeMorphism F j') ((F.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
                                        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
                                          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