Documentation

Mathlib.Algebra.Category.Grp.Basic

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

We introduce the bundled categories:

def AddGrp :
Type (u + 1)

The category of additive groups and group morphisms

Equations
Instances For
    def Grp :
    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.
      Equations
      Equations
      instance AddGrp.instGroupα (X : AddGrp) :
      Equations
      • X.instGroupα = X.str
      instance Grp.instGroupα (X : Grp) :
      Group X
      Equations
      • X.instGroupα = X.str
      instance AddGrp.instCoeFunHomForallαAddGroup {X : AddGrp} {Y : AddGrp} :
      CoeFun (X Y) fun (x : X Y) => XY
      Equations
      • AddGrp.instCoeFunHomForallαAddGroup = { coe := fun (f : X →+ Y) => f }
      instance Grp.instCoeFunHomForallαGroup {X : Grp} {Y : Grp} :
      CoeFun (X Y) fun (x : X Y) => XY
      Equations
      • Grp.instCoeFunHomForallαGroup = { coe := fun (f : X →* Y) => f }
      instance AddGrp.instFunLike (X : AddGrp) (Y : AddGrp) :
      FunLike (X Y) X Y
      Equations
      • X.instFunLike Y = inferInstance
      instance Grp.instFunLike (X : Grp) (Y : Grp) :
      FunLike (X Y) X Y
      Equations
      • X.instFunLike Y = inferInstance
      @[simp]
      @[simp]
      theorem AddGrp.coe_comp {X : AddGrp} {Y : AddGrp} {Z : AddGrp} {f : X Y} {g : Y Z} :
      @[simp]
      theorem Grp.coe_comp {X : Grp} {Y : Grp} {Z : Grp} {f : X Y} {g : Y Z} :
      theorem Grp.comp_def {X : Grp} {Y : Grp} {Z : Grp} {f : X Y} {g : Y Z} :
      @[simp]
      theorem Grp.forget_map {X : Grp} {Y : Grp} (f : X Y) :
      theorem AddGrp.ext {X : AddGrp} {Y : AddGrp} {f : X Y} {g : X Y} (w : ∀ (x : X), f x = g x) :
      f = g
      theorem Grp.ext_iff {X : Grp} {Y : Grp} {f : X Y} {g : X Y} :
      f = g ∀ (x : X), f x = g x
      theorem AddGrp.ext_iff {X : AddGrp} {Y : AddGrp} {f : X Y} {g : X Y} :
      f = g ∀ (x : X), f x = g x
      theorem Grp.ext {X : Grp} {Y : Grp} {f : X Y} {g : X Y} (w : ∀ (x : X), f x = g x) :
      f = g
      def AddGrp.of (X : Type u) [AddGroup X] :

      Construct a bundled AddGroup from the underlying type and typeclass.

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

        Construct a bundled Group from the underlying type and typeclass.

        Equations
        Instances For
          @[simp]
          theorem AddGrp.coe_of (R : Type u) [AddGroup R] :
          (AddGrp.of R) = R
          @[simp]
          theorem Grp.coe_of (R : Type u) [Group R] :
          (Grp.of R) = R
          @[simp]
          theorem AddGrp.coe_comp' {G : Type u_1} {H : Type u_1} {K : Type u_1} [AddGroup G] [AddGroup H] [AddGroup K] (f : G →+ H) (g : H →+ K) :
          @[simp]
          theorem Grp.coe_comp' {G : Type u_1} {H : Type u_1} {K : Type u_1} [Group G] [Group H] [Group K] (f : G →* H) (g : H →* K) :
          @[simp]
          theorem Grp.coe_id' {G : Type u_1} [Group G] :
          instance AddGrp.instZeroHom (G : AddGrp) (H : AddGrp) :
          Zero (G H)
          Equations
          • G.instZeroHom H = inferInstance
          instance Grp.instOneHom (G : Grp) (H : Grp) :
          One (G H)
          Equations
          • G.instOneHom H = inferInstance
          @[simp]
          theorem AddGrp.zero_apply (G : AddGrp) (H : AddGrp) (g : G) :
          0 g = 0
          @[simp]
          theorem Grp.one_apply (G : Grp) (H : Grp) (g : G) :
          1 g = 1
          def AddGrp.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 Grp.ofHom {X : Type u} {Y : Type u} [Group X] [Group Y] (f : X →* Y) :

            Typecheck a MonoidHom as a morphism in Grp.

            Equations
            Instances For
              theorem AddGrp.ofHom_apply {X : Type u_1} {Y : Type u_1} [AddGroup X] [AddGroup Y] (f : X →+ Y) (x : X) :
              (AddGrp.ofHom f) x = f x
              theorem Grp.ofHom_apply {X : Type u_1} {Y : Type u_1} [Group X] [Group Y] (f : X →* Y) (x : X) :
              (Grp.ofHom f) x = f x
              instance AddGrp.ofUnique (G : Type u_1) [AddGroup G] [i : Unique G] :
              Equations
              instance Grp.ofUnique (G : Type u_1) [Group G] [i : Unique G] :
              Unique (Grp.of G)
              Equations

              Universe lift functor for additive groups.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                theorem AddGrp.uliftFunctor.proof_1 (X : AddGrp) :
                { obj := fun (X : AddGrp) => AddGrp.of (ULift.{u_2, u_1} X), map := fun {X Y : AddGrp} (f : X Y) => AddGrp.ofHom (AddEquiv.ulift.symm.toAddMonoidHom.comp (AddMonoidHom.comp f AddEquiv.ulift.toAddMonoidHom)) }.map (CategoryTheory.CategoryStruct.id X) = { obj := fun (X : AddGrp) => AddGrp.of (ULift.{u_2, u_1} X), map := fun {X Y : AddGrp} (f : X Y) => AddGrp.ofHom (AddEquiv.ulift.symm.toAddMonoidHom.comp (AddMonoidHom.comp f AddEquiv.ulift.toAddMonoidHom)) }.map (CategoryTheory.CategoryStruct.id X)
                theorem AddGrp.uliftFunctor.proof_2 {X : AddGrp} {Y : AddGrp} {Z : AddGrp} (f : X Y) (g : Y Z) :
                { obj := fun (X : AddGrp) => AddGrp.of (ULift.{u_2, u_1} X), map := fun {X Y : AddGrp} (f : X Y) => AddGrp.ofHom (AddEquiv.ulift.symm.toAddMonoidHom.comp (AddMonoidHom.comp f AddEquiv.ulift.toAddMonoidHom)) }.map (CategoryTheory.CategoryStruct.comp f g) = { obj := fun (X : AddGrp) => AddGrp.of (ULift.{u_2, u_1} X), map := fun {X Y : AddGrp} (f : X Y) => AddGrp.ofHom (AddEquiv.ulift.symm.toAddMonoidHom.comp (AddMonoidHom.comp f AddEquiv.ulift.toAddMonoidHom)) }.map (CategoryTheory.CategoryStruct.comp f g)
                @[simp]
                theorem AddGrp.uliftFunctor_map {X : AddGrp} {Y : AddGrp} (f : X Y) :
                AddGrp.uliftFunctor.map f = AddGrp.ofHom (AddEquiv.ulift.symm.toAddMonoidHom.comp (AddMonoidHom.comp f AddEquiv.ulift.toAddMonoidHom))
                @[simp]
                theorem Grp.uliftFunctor_map {X : Grp} {Y : Grp} (f : X Y) :
                Grp.uliftFunctor.map f = Grp.ofHom (MulEquiv.ulift.symm.toMonoidHom.comp (MonoidHom.comp f MulEquiv.ulift.toMonoidHom))

                Universe lift functor for groups.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  def AddCommGrp :
                  Type (u + 1)

                  The category of additive commutative groups and group morphisms.

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

                    The category of commutative groups and group morphisms.

                    Equations
                    Instances For
                      @[reducible, inline]
                      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
                        Equations
                        • X.addCommGroupInstance = X.str
                        Equations
                        • X.commGroupInstance = X.str
                        instance AddCommGrp.instCoeFunHomForallαAddCommGroup {X : AddCommGrp} {Y : AddCommGrp} :
                        CoeFun (X Y) fun (x : X Y) => XY
                        Equations
                        • AddCommGrp.instCoeFunHomForallαAddCommGroup = { coe := fun (f : X →+ Y) => f }
                        instance CommGrp.instCoeFunHomForallαCommGroup {X : CommGrp} {Y : CommGrp} :
                        CoeFun (X Y) fun (x : X Y) => XY
                        Equations
                        • CommGrp.instCoeFunHomForallαCommGroup = { coe := fun (f : X →* Y) => f }
                        instance AddCommGrp.instFunLike (X : AddCommGrp) (Y : AddCommGrp) :
                        FunLike (X Y) X Y
                        Equations
                        • X.instFunLike Y = inferInstance
                        instance CommGrp.instFunLike (X : CommGrp) (Y : CommGrp) :
                        FunLike (X Y) X Y
                        Equations
                        • X.instFunLike Y = inferInstance
                        @[simp]
                        theorem AddCommGrp.coe_comp {X : AddCommGrp} {Y : AddCommGrp} {Z : AddCommGrp} {f : X Y} {g : Y Z} :
                        @[simp]
                        theorem CommGrp.coe_comp {X : CommGrp} {Y : CommGrp} {Z : CommGrp} {f : X Y} {g : Y Z} :
                        @[simp]
                        @[simp]
                        theorem CommGrp.forget_map {X : CommGrp} {Y : CommGrp} (f : X Y) :
                        theorem AddCommGrp.ext {X : AddCommGrp} {Y : AddCommGrp} {f : X Y} {g : X Y} (w : ∀ (x : X), f x = g x) :
                        f = g
                        theorem CommGrp.ext_iff {X : CommGrp} {Y : CommGrp} {f : X Y} {g : X Y} :
                        f = g ∀ (x : X), f x = g x
                        theorem AddCommGrp.ext_iff {X : AddCommGrp} {Y : AddCommGrp} {f : X Y} {g : X Y} :
                        f = g ∀ (x : X), f x = g x
                        theorem CommGrp.ext {X : CommGrp} {Y : CommGrp} {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
                          def CommGrp.of (G : Type u) [CommGroup G] :

                          Construct a bundled CommGroup from the underlying type and typeclass.

                          Equations
                          Instances For
                            @[simp]
                            theorem AddCommGrp.coe_of (R : Type u) [AddCommGroup R] :
                            (AddCommGrp.of R) = R
                            @[simp]
                            theorem CommGrp.coe_of (R : Type u) [CommGroup R] :
                            (CommGrp.of R) = R
                            @[simp]
                            theorem AddCommGrp.coe_comp' {G : Type u_1} {H : Type u_1} {K : Type u_1} [AddCommGroup G] [AddCommGroup H] [AddCommGroup K] (f : G →+ H) (g : H →+ K) :
                            @[simp]
                            theorem CommGrp.coe_comp' {G : Type u_1} {H : Type u_1} {K : Type u_1} [CommGroup G] [CommGroup H] [CommGroup K] (f : G →* H) (g : H →* K) :
                            instance AddCommGrp.ofUnique (G : Type u_1) [AddCommGroup G] [i : Unique G] :
                            Equations
                            instance CommGrp.ofUnique (G : Type u_1) [CommGroup G] [i : Unique G] :
                            Equations
                            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.
                            Equations
                            • G.instZeroHom H = inferInstance
                            instance CommGrp.instOneHom (G : CommGrp) (H : CommGrp) :
                            One (G H)
                            Equations
                            • G.instOneHom H = inferInstance
                            @[simp]
                            theorem AddCommGrp.zero_apply (G : AddCommGrp) (H : AddCommGrp) (g : G) :
                            0 g = 0
                            @[simp]
                            theorem CommGrp.one_apply (G : CommGrp) (H : CommGrp) (g : G) :
                            1 g = 1

                            Typecheck an AddMonoidHom as a morphism in AddCommGroup.

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

                              Typecheck a MonoidHom as a morphism in CommGroup.

                              Equations
                              Instances For
                                @[simp]
                                theorem AddCommGrp.ofHom_apply {X : Type u_1} {Y : Type u_1} [AddCommGroup X] [AddCommGroup Y] (f : X →+ Y) (x : X) :
                                @[simp]
                                theorem CommGrp.ofHom_apply {X : Type u_1} {Y : Type u_1} [CommGroup X] [CommGroup Y] (f : X →* Y) (x : X) :
                                (CommGrp.ofHom f) x = f x
                                theorem AddCommGrp.uliftFunctor.proof_1 (X : AddCommGrp) :
                                { obj := fun (X : AddCommGrp) => AddCommGrp.of (ULift.{u_2, u_1} X), map := fun {X Y : AddCommGrp} (f : X Y) => AddCommGrp.ofHom (AddEquiv.ulift.symm.toAddMonoidHom.comp (AddMonoidHom.comp f AddEquiv.ulift.toAddMonoidHom)) }.map (CategoryTheory.CategoryStruct.id X) = { obj := fun (X : AddCommGrp) => AddCommGrp.of (ULift.{u_2, u_1} X), map := fun {X Y : AddCommGrp} (f : X Y) => AddCommGrp.ofHom (AddEquiv.ulift.symm.toAddMonoidHom.comp (AddMonoidHom.comp f AddEquiv.ulift.toAddMonoidHom)) }.map (CategoryTheory.CategoryStruct.id X)
                                theorem AddCommGrp.uliftFunctor.proof_2 {X : AddCommGrp} {Y : AddCommGrp} {Z : AddCommGrp} (f : X Y) (g : Y Z) :
                                { obj := fun (X : AddCommGrp) => AddCommGrp.of (ULift.{u_2, u_1} X), map := fun {X Y : AddCommGrp} (f : X Y) => AddCommGrp.ofHom (AddEquiv.ulift.symm.toAddMonoidHom.comp (AddMonoidHom.comp f AddEquiv.ulift.toAddMonoidHom)) }.map (CategoryTheory.CategoryStruct.comp f g) = { obj := fun (X : AddCommGrp) => AddCommGrp.of (ULift.{u_2, u_1} X), map := fun {X Y : AddCommGrp} (f : X Y) => AddCommGrp.ofHom (AddEquiv.ulift.symm.toAddMonoidHom.comp (AddMonoidHom.comp f AddEquiv.ulift.toAddMonoidHom)) }.map (CategoryTheory.CategoryStruct.comp f g)

                                Universe lift functor for additive commutative groups.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  @[simp]
                                  theorem CommGrp.uliftFunctor_map {X : CommGrp} {Y : CommGrp} (f : X Y) :
                                  CommGrp.uliftFunctor.map f = CommGrp.ofHom (MulEquiv.ulift.symm.toMonoidHom.comp (MonoidHom.comp f MulEquiv.ulift.toMonoidHom))
                                  @[simp]
                                  theorem AddCommGrp.uliftFunctor_map {X : AddCommGrp} {Y : AddCommGrp} (f : X Y) :
                                  AddCommGrp.uliftFunctor.map f = AddCommGrp.ofHom (AddEquiv.ulift.symm.toAddMonoidHom.comp (AddMonoidHom.comp f AddEquiv.ulift.toAddMonoidHom))

                                  Universe lift functor for commutative groups.

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

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

                                    Equations
                                    Instances For
                                      @[simp]
                                      theorem AddCommGrp.asHom_apply {G : AddCommGrp} (g : G) (i : ) :
                                      theorem AddCommGrp.int_hom_ext {G : AddCommGrp} (f : AddCommGrp.of G) (g : AddCommGrp.of G) (w : f 1 = g 1) :
                                      f = g
                                      theorem AddEquiv.toAddGrpIso.proof_2 {X : AddGrp} {Y : AddGrp} (e : X ≃+ Y) :
                                      def AddEquiv.toAddGrpIso {X : AddGrp} {Y : AddGrp} (e : X ≃+ Y) :
                                      X Y

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

                                      Equations
                                      • e.toAddGrpIso = { hom := e.toAddMonoidHom, inv := e.symm.toAddMonoidHom, hom_inv_id := , inv_hom_id := }
                                      Instances For
                                        theorem AddEquiv.toAddGrpIso.proof_1 {X : AddGrp} {Y : AddGrp} (e : X ≃+ Y) :
                                        @[simp]
                                        theorem MulEquiv.toGrpIso_hom {X : Grp} {Y : Grp} (e : X ≃* Y) :
                                        e.toGrpIso.hom = e.toMonoidHom
                                        @[simp]
                                        theorem MulEquiv.toGrpIso_inv {X : Grp} {Y : Grp} (e : X ≃* Y) :
                                        e.toGrpIso.inv = e.symm.toMonoidHom
                                        @[simp]
                                        theorem AddEquiv.toAddGrpIso_inv {X : AddGrp} {Y : AddGrp} (e : X ≃+ Y) :
                                        e.toAddGrpIso.inv = e.symm.toAddMonoidHom
                                        @[simp]
                                        theorem AddEquiv.toAddGrpIso_hom {X : AddGrp} {Y : AddGrp} (e : X ≃+ Y) :
                                        e.toAddGrpIso.hom = e.toAddMonoidHom
                                        def MulEquiv.toGrpIso {X : Grp} {Y : Grp} (e : X ≃* Y) :
                                        X Y

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

                                        Equations
                                        • e.toGrpIso = { hom := e.toMonoidHom, inv := e.symm.toMonoidHom, hom_inv_id := , inv_hom_id := }
                                        Instances For
                                          def AddEquiv.toAddCommGrpIso {X : AddCommGrp} {Y : AddCommGrp} (e : X ≃+ Y) :
                                          X Y

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

                                          Equations
                                          • e.toAddCommGrpIso = { hom := e.toAddMonoidHom, inv := e.symm.toAddMonoidHom, hom_inv_id := , inv_hom_id := }
                                          Instances For
                                            @[simp]
                                            theorem AddEquiv.toAddCommGrpIso_hom {X : AddCommGrp} {Y : AddCommGrp} (e : X ≃+ Y) :
                                            e.toAddCommGrpIso.hom = e.toAddMonoidHom
                                            @[simp]
                                            theorem AddEquiv.toAddCommGrpIso_inv {X : AddCommGrp} {Y : AddCommGrp} (e : X ≃+ Y) :
                                            e.toAddCommGrpIso.inv = e.symm.toAddMonoidHom
                                            @[simp]
                                            theorem MulEquiv.toCommGrpIso_inv {X : CommGrp} {Y : CommGrp} (e : X ≃* Y) :
                                            e.toCommGrpIso.inv = e.symm.toMonoidHom
                                            @[simp]
                                            theorem MulEquiv.toCommGrpIso_hom {X : CommGrp} {Y : CommGrp} (e : X ≃* Y) :
                                            e.toCommGrpIso.hom = e.toMonoidHom
                                            def MulEquiv.toCommGrpIso {X : CommGrp} {Y : CommGrp} (e : X ≃* Y) :
                                            X Y

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

                                            Equations
                                            • e.toCommGrpIso = { hom := e.toMonoidHom, inv := e.symm.toMonoidHom, hom_inv_id := , inv_hom_id := }
                                            Instances For
                                              def CategoryTheory.Iso.addGroupIsoToAddEquiv {X : AddGrp} {Y : AddGrp} (i : X Y) :
                                              X ≃+ Y

                                              Build an addEquiv from an isomorphism in the category AddGroup

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

                                                Build a MulEquiv from an isomorphism in the category Grp.

                                                Equations
                                                Instances For

                                                  Build an AddEquiv from an isomorphism in the category AddCommGroup.

                                                  Equations
                                                  Instances For
                                                    @[simp]
                                                    theorem CategoryTheory.Iso.addCommGroupIsoToAddEquiv_symm_apply {X : AddCommGrp} {Y : AddCommGrp} (i : X Y) (a : Y) :
                                                    i.addCommGroupIsoToAddEquiv.symm a = i.inv a
                                                    @[simp]
                                                    theorem CategoryTheory.Iso.commGroupIsoToMulEquiv_apply {X : CommGrp} {Y : CommGrp} (i : X Y) (a : X) :
                                                    i.commGroupIsoToMulEquiv a = i.hom a
                                                    @[simp]
                                                    theorem CategoryTheory.Iso.addCommGroupIsoToAddEquiv_apply {X : AddCommGrp} {Y : AddCommGrp} (i : X Y) (a : X) :
                                                    i.addCommGroupIsoToAddEquiv a = i.hom a
                                                    @[simp]
                                                    theorem CategoryTheory.Iso.commGroupIsoToMulEquiv_symm_apply {X : CommGrp} {Y : CommGrp} (i : X Y) (a : Y) :
                                                    i.commGroupIsoToMulEquiv.symm a = i.inv a

                                                    Build a MulEquiv from an isomorphism in the category CommGroup.

                                                    Equations
                                                    Instances For
                                                      theorem addEquivIsoAddGroupIso.proof_1 {X : AddGrp} {Y : AddGrp} :
                                                      (CategoryTheory.CategoryStruct.comp (fun (e : X ≃+ Y) => e.toAddGrpIso) fun (i : X Y) => i.addGroupIsoToAddEquiv) = CategoryTheory.CategoryStruct.id (X ≃+ Y)
                                                      def addEquivIsoAddGroupIso {X : AddGrp} {Y : AddGrp} :
                                                      X ≃+ Y X Y

                                                      Additive equivalences between AddGroups are the same as (isomorphic to) isomorphisms in AddGrp.

                                                      Equations
                                                      • addEquivIsoAddGroupIso = { hom := fun (e : X ≃+ Y) => e.toAddGrpIso, inv := fun (i : X Y) => i.addGroupIsoToAddEquiv, hom_inv_id := , inv_hom_id := }
                                                      Instances For
                                                        theorem addEquivIsoAddGroupIso.proof_2 {X : AddGrp} {Y : AddGrp} :
                                                        (CategoryTheory.CategoryStruct.comp (fun (i : X Y) => i.addGroupIsoToAddEquiv) fun (e : X ≃+ Y) => e.toAddGrpIso) = CategoryTheory.CategoryStruct.id (X Y)
                                                        def mulEquivIsoGroupIso {X : Grp} {Y : Grp} :
                                                        X ≃* Y X Y

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

                                                        Equations
                                                        • mulEquivIsoGroupIso = { hom := fun (e : X ≃* Y) => e.toGrpIso, inv := fun (i : X Y) => i.groupIsoToMulEquiv, hom_inv_id := , inv_hom_id := }
                                                        Instances For
                                                          theorem addEquivIsoAddCommGroupIso.proof_1 {X : AddCommGrp} {Y : AddCommGrp} :
                                                          (CategoryTheory.CategoryStruct.comp (fun (e : X ≃+ Y) => e.toAddCommGrpIso) fun (i : X Y) => i.addCommGroupIsoToAddEquiv) = CategoryTheory.CategoryStruct.comp (fun (e : X ≃+ Y) => e.toAddCommGrpIso) fun (i : X Y) => i.addCommGroupIsoToAddEquiv

                                                          Additive equivalences between AddCommGroups are the same as (isomorphic to) isomorphisms in AddCommGrp.

                                                          Equations
                                                          • addEquivIsoAddCommGroupIso = { hom := fun (e : X ≃+ Y) => e.toAddCommGrpIso, inv := fun (i : X Y) => i.addCommGroupIsoToAddEquiv, hom_inv_id := , inv_hom_id := }
                                                          Instances For
                                                            theorem addEquivIsoAddCommGroupIso.proof_2 {X : AddCommGrp} {Y : AddCommGrp} :
                                                            (CategoryTheory.CategoryStruct.comp (fun (i : X Y) => i.addCommGroupIsoToAddEquiv) fun (e : X ≃+ Y) => e.toAddCommGrpIso) = CategoryTheory.CategoryStruct.comp (fun (i : X Y) => i.addCommGroupIsoToAddEquiv) fun (e : X ≃+ Y) => e.toAddCommGrpIso
                                                            def mulEquivIsoCommGroupIso {X : CommGrp} {Y : CommGrp} :
                                                            X ≃* Y X Y

                                                            Multiplicative equivalences between CommGroups are the same as (isomorphic to) isomorphisms in CommGrp.

                                                            Equations
                                                            • mulEquivIsoCommGroupIso = { hom := fun (e : X ≃* Y) => e.toCommGrpIso, inv := fun (i : X Y) => i.commGroupIsoToMulEquiv, hom_inv_id := , inv_hom_id := }
                                                            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 MulEquiv to the (unbundled) group of permutations.

                                                                Equations
                                                                • CategoryTheory.Aut.mulEquivPerm = CategoryTheory.Aut.isoPerm.groupIsoToMulEquiv
                                                                Instances For
                                                                  @[reducible, inline]
                                                                  abbrev GrpMaxAux :
                                                                  Type ((max u1 u2) + 1)

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

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

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

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

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

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

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

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

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

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

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

                                                                            Equations
                                                                            Instances For

                                                                              @[simp] lemmas for MonoidHom.comp and categorical identities.

                                                                              @[simp]
                                                                              theorem AddMonoidHom.comp_id_addGrp {G : AddGrp} {H : Type u} [AddGroup H] (f : G →+ H) :
                                                                              @[simp]
                                                                              theorem MonoidHom.comp_id_grp {G : Grp} {H : Type u} [Group H] (f : G →* H) :
                                                                              @[simp]
                                                                              @[simp]
                                                                              @[simp]
                                                                              theorem MonoidHom.comp_id_commGrp {G : CommGrp} {H : Type u} [CommGroup H] (f : G →* H) :