Documentation

Mathlib.Algebra.Category.GroupCat.Basic

Category instances for Group, AddGroup, CommGroup, and AddCommGroup. #

We introduce the bundled categories:

def AddGroupCat :
Type (u + 1)

The category of additive groups and group morphisms

Equations
Instances For
    def GroupCat :
    Type (u + 1)

    The category of groups and group morphisms.

    Equations
    Instances For
      Equations
      • One or more equations did not get rendered due to their size.
      instance GroupCat.instGroupα (X : GroupCat) :
      Group X
      Equations
      Equations
      • AddGroupCat.instCoeFunHomAddGroupCatToQuiverToCategoryStructInstAddGroupCatLargeCategoryForAllαAddGroup = { coe := fun (f : X →+ Y) => f }
      Equations
      • GroupCat.instCoeFunHomGroupCatToQuiverToCategoryStructInstGroupCatLargeCategoryForAllαGroup = { coe := fun (f : X →* Y) => f }
      instance AddGroupCat.instFunLike (X : AddGroupCat) (Y : AddGroupCat) :
      FunLike (X Y) X Y
      Equations
      instance GroupCat.instFunLike (X : GroupCat) (Y : GroupCat) :
      FunLike (X Y) X Y
      Equations
      @[simp]
      theorem AddGroupCat.coe_comp {X : AddGroupCat} {Y : AddGroupCat} {Z : AddGroupCat} {f : X Y} {g : Y Z} :
      @[simp]
      theorem GroupCat.coe_comp {X : GroupCat} {Y : GroupCat} {Z : GroupCat} {f : X Y} {g : Y Z} :
      @[simp]
      theorem GroupCat.forget_map {X : GroupCat} {Y : GroupCat} (f : X Y) :
      theorem AddGroupCat.ext {X : AddGroupCat} {Y : AddGroupCat} {f : X Y} {g : X Y} (w : ∀ (x : X), f x = g x) :
      f = g
      theorem GroupCat.ext {X : GroupCat} {Y : GroupCat} {f : X Y} {g : X Y} (w : ∀ (x : X), f x = g x) :
      f = g

      Construct a bundled AddGroup from the underlying type and typeclass.

      Equations
      Instances For
        def GroupCat.of (X : Type u) [Group X] :

        Construct a bundled Group from the underlying type and typeclass.

        Equations
        Instances For
          @[simp]
          theorem AddGroupCat.coe_of (R : Type u) [AddGroup R] :
          (AddGroupCat.of R) = R
          @[simp]
          theorem GroupCat.coe_of (R : Type u) [Group R] :
          (GroupCat.of R) = R
          @[simp]
          theorem AddGroupCat.zero_apply (G : AddGroupCat) (H : AddGroupCat) (g : G) :
          0 g = 0
          @[simp]
          theorem GroupCat.one_apply (G : GroupCat) (H : GroupCat) (g : G) :
          1 g = 1
          def AddGroupCat.ofHom {X : Type u} {Y : Type u} [AddGroup X] [AddGroup Y] (f : X →+ Y) :

          Typecheck an AddMonoidHom as a morphism in AddGroup.

          Equations
          Instances For
            def GroupCat.ofHom {X : Type u} {Y : Type u} [Group X] [Group Y] (f : X →* Y) :

            Typecheck a MonoidHom as a morphism in GroupCat.

            Equations
            Instances For
              theorem AddGroupCat.ofHom_apply {X : Type u_1} {Y : Type u_1} [AddGroup X] [AddGroup Y] (f : X →+ Y) (x : X) :
              theorem GroupCat.ofHom_apply {X : Type u_1} {Y : Type u_1} [Group X] [Group Y] (f : X →* Y) (x : X) :
              (GroupCat.ofHom f) x = f x
              instance AddGroupCat.ofUnique (G : Type u_1) [AddGroup G] [i : Unique G] :
              Equations
              instance GroupCat.ofUnique (G : Type u_1) [Group G] [i : Unique G] :
              Equations
              def AddCommGroupCat :
              Type (u + 1)

              The category of additive commutative groups and group morphisms.

              Equations
              Instances For
                def CommGroupCat :
                Type (u + 1)

                The category of commutative groups and group morphisms.

                Equations
                Instances For
                  @[inline, reducible]
                  abbrev Ab :
                  Type (u_1 + 1)

                  Ab is an abbreviation for AddCommGroup, for the sake of mathematicians' sanity.

                  Equations
                  Instances For
                    Equations
                    • One or more equations did not get rendered due to their size.
                    Equations
                    • AddCommGroupCat.instCoeFunHomAddCommGroupCatToQuiverToCategoryStructInstAddCommGroupCatLargeCategoryForAllαAddCommGroup = { coe := fun (f : X →+ Y) => f }
                    Equations
                    • CommGroupCat.instCoeFunHomCommGroupCatToQuiverToCategoryStructInstCommGroupCatLargeCategoryForAllαCommGroup = { coe := fun (f : X →* Y) => f }
                    Equations
                    instance CommGroupCat.instFunLike (X : CommGroupCat) (Y : CommGroupCat) :
                    FunLike (X Y) X Y
                    Equations
                    @[simp]
                    @[simp]
                    theorem CommGroupCat.coe_comp {X : CommGroupCat} {Y : CommGroupCat} {Z : CommGroupCat} {f : X Y} {g : Y Z} :
                    theorem AddCommGroupCat.ext {X : AddCommGroupCat} {Y : AddCommGroupCat} {f : X Y} {g : X Y} (w : ∀ (x : X), f x = g x) :
                    f = g
                    theorem CommGroupCat.ext {X : CommGroupCat} {Y : CommGroupCat} {f : X Y} {g : X Y} (w : ∀ (x : X), f x = g x) :
                    f = g

                    Construct a bundled AddCommGroup from the underlying type and typeclass.

                    Equations
                    Instances For

                      Construct a bundled CommGroup from the underlying type and typeclass.

                      Equations
                      Instances For
                        Equations
                        • One or more equations did not get rendered due to their size.
                        Equations
                        • One or more equations did not get rendered due to their size.
                        @[simp]
                        theorem AddCommGroupCat.zero_apply (G : AddCommGroupCat) (H : AddCommGroupCat) (g : G) :
                        0 g = 0
                        @[simp]
                        theorem CommGroupCat.one_apply (G : CommGroupCat) (H : CommGroupCat) (g : G) :
                        1 g = 1

                        Typecheck an AddMonoidHom as a morphism in AddCommGroup.

                        Equations
                        Instances For

                          Typecheck a MonoidHom as a morphism in CommGroup.

                          Equations
                          Instances For
                            @[simp]
                            theorem AddCommGroupCat.ofHom_apply {X : Type u_1} {Y : Type u_1} [AddCommGroup X] [AddCommGroup Y] (f : X →+ Y) (x : X) :
                            @[simp]
                            theorem CommGroupCat.ofHom_apply {X : Type u_1} {Y : Type u_1} [CommGroup X] [CommGroup Y] (f : X →* Y) (x : X) :

                            Any element of an abelian group gives a unique morphism from sending 1 to that element.

                            Equations
                            Instances For
                              @[simp]
                              theorem AddCommGroupCat.asHom_apply {G : AddCommGroupCat} (g : G) (i : ) :
                              def AddEquiv.toAddGroupCatIso {X : AddGroupCat} {Y : AddGroupCat} (e : X ≃+ Y) :
                              X Y

                              Build an isomorphism in the category AddGroup from an AddEquiv between AddGroups.

                              Equations
                              Instances For
                                def MulEquiv.toGroupCatIso {X : GroupCat} {Y : GroupCat} (e : X ≃* Y) :
                                X Y

                                Build an isomorphism in the category GroupCat from a MulEquiv between Groups.

                                Equations
                                Instances For

                                  Build an isomorphism in the category AddCommGroupCat from an AddEquiv between AddCommGroups.

                                  Equations
                                  Instances For
                                    def MulEquiv.toCommGroupCatIso {X : CommGroupCat} {Y : CommGroupCat} (e : X ≃* Y) :
                                    X Y

                                    Build an isomorphism in the category CommGroupCat from a MulEquiv between CommGroups.

                                    Equations
                                    Instances For

                                      Build an addEquiv from an isomorphism in the category AddGroup

                                      Equations
                                      Instances For
                                        def CategoryTheory.Iso.groupIsoToMulEquiv {X : GroupCat} {Y : GroupCat} (i : X Y) :
                                        X ≃* Y

                                        Build a MulEquiv from an isomorphism in the category GroupCat.

                                        Equations
                                        Instances For

                                          Build an AddEquiv from an isomorphism in the category AddCommGroup.

                                          Equations
                                          Instances For

                                            Build a MulEquiv from an isomorphism in the category CommGroup.

                                            Equations
                                            Instances For
                                              def addEquivIsoAddGroupIso {X : AddGroupCat} {Y : AddGroupCat} :
                                              X ≃+ Y X Y

                                              "additive equivalences between add_groups are the same as (isomorphic to) isomorphisms in AddGroup

                                              Equations
                                              • One or more equations did not get rendered due to their size.
                                              Instances For
                                                def mulEquivIsoGroupIso {X : GroupCat} {Y : GroupCat} :
                                                X ≃* Y X Y

                                                multiplicative equivalences between Groups are the same as (isomorphic to) isomorphisms in GroupCat

                                                Equations
                                                Instances For

                                                  additive equivalences between AddCommGroups are the same as (isomorphic to) isomorphisms in AddCommGroup

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

                                                    multiplicative equivalences between comm_groups are the same as (isomorphic to) isomorphisms in CommGroup

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

                                                      The (bundled) group of automorphisms of a type is isomorphic to the (bundled) group of permutations.

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

                                                        The (unbundled) group of automorphisms of a type is mul_equiv to the (unbundled) group of permutations.

                                                        Equations
                                                        Instances For
                                                          abbrev GroupCatMaxAux :
                                                          Type ((max u1 u2) + 1)

                                                          An alias for AddGroupCat.{max u v}, to deal around unification issues.

                                                          Equations
                                                          Instances For
                                                            @[inline, reducible]
                                                            abbrev GroupCatMax :
                                                            Type ((max u1 u2) + 1)

                                                            An alias for GroupCat.{max u v}, to deal around unification issues.

                                                            Equations
                                                            Instances For
                                                              @[inline, reducible]
                                                              abbrev AddGroupCatMax :
                                                              Type ((max u1 u2) + 1)

                                                              An alias for AddGroupCat.{max u v}, to deal around unification issues.

                                                              Equations
                                                              Instances For
                                                                abbrev AddCommGroupCatMaxAux :
                                                                Type ((max u1 u2) + 1)

                                                                An alias for AddCommGroupCat.{max u v}, to deal around unification issues.

                                                                Equations
                                                                Instances For
                                                                  @[inline, reducible]
                                                                  abbrev CommGroupCatMax :
                                                                  Type ((max u1 u2) + 1)

                                                                  An alias for CommGroupCat.{max u v}, to deal around unification issues.

                                                                  Equations
                                                                  Instances For
                                                                    @[inline, reducible]
                                                                    abbrev AddCommGroupCatMax :
                                                                    Type ((max u1 u2) + 1)

                                                                    An alias for AddCommGroupCat.{max u v}, to deal around unification issues.

                                                                    Equations
                                                                    Instances For