Documentation

Mathlib.Algebra.Category.Grp.Colimits

The category of additive commutative groups has all colimits. #

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

TODO: In fact, in AddCommGrp there is a much nicer model of colimits as quotients of finitely supported functions, and we really should implement this as well (or instead).

We build the colimit of a diagram in AddCommGrp by constructing the free group on the disjoint union of all the abelian groups in the diagram, then taking the quotient by the abelian group laws within each abelian group, and the identifications given by the morphisms in the diagram.

source
inductive AddCommGrp.Colimits.Prequotient {J : Type u} [CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J AddCommGrp) :
Type (max (max u v) w)

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

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

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

    Instances For
      source
      instance AddCommGrp.Colimits.colimitSetoid {J : Type u} [CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J AddCommGrp) :
      Setoid (AddCommGrp.Colimits.Prequotient F)

      The setoid corresponding to group expressions modulo abelian group relations and identifications.

      Equations
      source
      def AddCommGrp.Colimits.ColimitType {J : Type u} [CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J AddCommGrp) :
      Type (max u v w)

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

      Equations
      Instances For
        source
        instance AddCommGrp.Colimits.instZeroColimitType {J : Type u} [CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J AddCommGrp) :
        Zero (AddCommGrp.Colimits.ColimitType F)
        Equations
        source
        instance AddCommGrp.Colimits.instNegColimitType {J : Type u} [CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J AddCommGrp) :
        Neg (AddCommGrp.Colimits.ColimitType F)
        Equations
        source
        instance AddCommGrp.Colimits.instAddColimitType {J : Type u} [CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J AddCommGrp) :
        Add (AddCommGrp.Colimits.ColimitType F)
        Equations
        source
        instance AddCommGrp.Colimits.instAddCommGroupColimitType {J : Type u} [CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J AddCommGrp) :
        AddCommGroup (AddCommGrp.Colimits.ColimitType F)
        Equations
        source
        instance AddCommGrp.Colimits.ColimitTypeInhabited {J : Type u} [CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J AddCommGrp) :
        Inhabited (AddCommGrp.Colimits.ColimitType F)
        Equations
        source
        @[simp]
        theorem AddCommGrp.Colimits.quot_zero {J : Type u} [CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J AddCommGrp) :
        Quot.mk (⇑(AddCommGrp.Colimits.colimitSetoid F)) AddCommGrp.Colimits.Prequotient.zero = 0
        source
        @[simp]
        theorem AddCommGrp.Colimits.quot_neg {J : Type u} [CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J AddCommGrp) (x : AddCommGrp.Colimits.Prequotient F) :
        Quot.mk (⇑(AddCommGrp.Colimits.colimitSetoid F)) x.neg = -Quot.mk (⇑(AddCommGrp.Colimits.colimitSetoid F)) x
        source
        @[simp]
        theorem AddCommGrp.Colimits.quot_add {J : Type u} [CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J AddCommGrp) (x y : AddCommGrp.Colimits.Prequotient F) :
        Quot.mk (⇑(AddCommGrp.Colimits.colimitSetoid F)) (x.add y) = Quot.mk (⇑(AddCommGrp.Colimits.colimitSetoid F)) x + Quot.mk (⇑(AddCommGrp.Colimits.colimitSetoid F)) y
        source
        def AddCommGrp.Colimits.colimit {J : Type u} [CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J AddCommGrp) :
        AddCommGrp

        The bundled abelian group giving the colimit of a diagram.

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

          The function from a given abelian group in the diagram to the colimit abelian group.

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

            The group homomorphism from a given abelian group in the diagram to the colimit abelian group.

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

              The cocone over the proposed colimit abelian group.

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

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

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

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

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

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

                    Equations
                    Instances For
                      source
                      def AddCommGrp.Colimits.colimitCoconeIsColimit {J : Type u} [CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J AddCommGrp) :
                      CategoryTheory.Limits.IsColimit (AddCommGrp.Colimits.colimitCocone F)

                      Evidence that the proposed colimit is the colimit.

                      Equations
                      Instances For
                        source
                        theorem AddCommGrp.hasColimit {J : Type u} [CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J AddCommGrp) :
                        CategoryTheory.Limits.HasColimit F
                        source
                        theorem AddCommGrp.hasColimitsOfShape (J : Type u) [CategoryTheory.Category.{v, u} J] :
                        CategoryTheory.Limits.HasColimitsOfShape J AddCommGrp
                        source
                        theorem AddCommGrp.hasColimitsOfSize :
                        CategoryTheory.Limits.HasColimitsOfSize.{v, u, max (max u v) w, max (max (u + 1) (v + 1)) (w + 1)} AddCommGrp
                        source
                        instance AddCommGrp.hasColimits :
                        CategoryTheory.Limits.HasColimits AddCommGrp
                        source
                        instance AddCommGrp.instHasColimitsOfSizeAddCommGrpMax :
                        CategoryTheory.Limits.HasColimitsOfSize.{v, v, max u v, max (u + 1) (v + 1)} AddCommGrpMax
                        source
                        instance AddCommGrp.instHasColimitsOfSizeAddCommGrpMax_1 :
                        CategoryTheory.Limits.HasColimitsOfSize.{u, u, max u v, max (u + 1) (v + 1)} AddCommGrpMax
                        source
                        instance AddCommGrp.instHasColimitsOfSizeAddCommGrpMax_2 :
                        CategoryTheory.Limits.HasColimitsOfSize.{u, v, max u v, max (u + 1) (v + 1)} AddCommGrpMax
                        source
                        instance AddCommGrp.instHasColimitsOfSizeAddCommGrpMax_3 :
                        CategoryTheory.Limits.HasColimitsOfSize.{v, u, max u v, max (u + 1) (v + 1)} AddCommGrpMax
                        source
                        instance AddCommGrp.instHasColimitsOfSize :
                        CategoryTheory.Limits.HasColimitsOfSize.{0, 0, u, u + 1} AddCommGrp
                        source
                        noncomputable def AddCommGrp.cokernelIsoQuotient {G H : AddCommGrp} (f : G ⟶ H) :
                        CategoryTheory.Limits.cokernel f ≅ AddCommGrp.of (↑H ⧸ AddMonoidHom.range f)

                        The categorical cokernel of a morphism in AddCommGrp agrees with the usual group-theoretical quotient.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For