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

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

      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.

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

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

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

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

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

            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) (coconeMorphism F j') = 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)) :
              (CategoryTheory.ConcreteCategory.hom (coconeMorphism F j')) ((CategoryTheory.ConcreteCategory.hom (F.map f)) x) = (CategoryTheory.ConcreteCategory.hom (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.

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

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

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

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

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

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

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

                      Evidence that the proposed colimit is the colimit.

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

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

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

                            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.

                            Instances For
                              source
                              @[implicit_reducible]
                              instance CommRingCat.Colimits.ColimitType.instZero {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommRingCat) :
                              Zero (ColimitType F)
                              source
                              @[implicit_reducible]
                              instance CommRingCat.Colimits.ColimitType.instAdd {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommRingCat) :
                              Add (ColimitType F)
                              source
                              @[implicit_reducible]
                              instance CommRingCat.Colimits.ColimitType.instNeg {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommRingCat) :
                              Neg (ColimitType F)
                              source
                              @[implicit_reducible]
                              instance CommRingCat.Colimits.ColimitType.AddGroup {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommRingCat) :
                              _root_.AddGroup (ColimitType F)
                              source
                              @[implicit_reducible]
                              instance CommRingCat.Colimits.InhabitedColimitType {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommRingCat) :
                              Inhabited (ColimitType F)
                              source
                              @[implicit_reducible]
                              instance CommRingCat.Colimits.ColimitType.AddGroupWithOne {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommRingCat) :
                              _root_.AddGroupWithOne (ColimitType F)
                              source
                              @[implicit_reducible]
                              instance CommRingCat.Colimits.instCommRingColimitType {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommRingCat) :
                              CommRing (ColimitType F)
                              source
                              @[simp]
                              theorem CommRingCat.Colimits.quot_zero {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommRingCat) :
                              Quot.mk (⇑(colimitSetoid F)) Prequotient.zero = 0
                              source
                              @[simp]
                              theorem CommRingCat.Colimits.quot_one {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommRingCat) :
                              Quot.mk (⇑(colimitSetoid F)) Prequotient.one = 1
                              source
                              @[simp]
                              theorem CommRingCat.Colimits.quot_neg {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommRingCat) (x : Prequotient F) :
                              Quot.mk (⇑(colimitSetoid F)) x.neg = -have this := Quot.mk (⇑(colimitSetoid F)) x; this
                              source
                              @[simp]
                              theorem CommRingCat.Colimits.quot_add {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommRingCat) (x y : Prequotient F) :
                              Quot.mk (⇑(colimitSetoid F)) (x.add y) = (have this := Quot.mk (⇑(colimitSetoid F)) x; this) + have this := Quot.mk (⇑(colimitSetoid F)) y; this
                              source
                              @[simp]
                              theorem CommRingCat.Colimits.quot_mul {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommRingCat) (x y : Prequotient F) :
                              Quot.mk (⇑(colimitSetoid F)) (x.mul y) = (have this := Quot.mk (⇑(colimitSetoid F)) x; this) * have this := Quot.mk (⇑(colimitSetoid F)) y; this
                              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.

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

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

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

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

                                  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) (coconeMorphism F j') = 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)) :
                                    (CategoryTheory.ConcreteCategory.hom (coconeMorphism F j')) ((CategoryTheory.ConcreteCategory.hom (F.map f)) x) = (CategoryTheory.ConcreteCategory.hom (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.

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

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

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

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

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

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

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

                                            Evidence that the proposed colimit is the colimit.

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