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.
      Equations
      Equations
      • X.instGroupα = X.str
      instance GroupCat.instGroupα (X : GroupCat) :
      Group X
      Equations
      • X.instGroupα = X.str
      instance AddGroupCat.instCoeFunHomForallαAddGroup {X : AddGroupCat} {Y : AddGroupCat} :
      CoeFun (X Y) fun (x : X Y) => XY
      Equations
      • AddGroupCat.instCoeFunHomForallαAddGroup = { coe := fun (f : X →+ Y) => f }
      instance GroupCat.instCoeFunHomForallαGroup {X : GroupCat} {Y : GroupCat} :
      CoeFun (X Y) fun (x : X Y) => XY
      Equations
      • GroupCat.instCoeFunHomForallαGroup = { coe := fun (f : X →* Y) => f }
      instance AddGroupCat.instFunLike (X : AddGroupCat) (Y : AddGroupCat) :
      FunLike (X Y) X Y
      Equations
      • X.instFunLike Y = let_fun this := inferInstance; this
      instance GroupCat.instFunLike (X : GroupCat) (Y : GroupCat) :
      FunLike (X Y) X Y
      Equations
      • X.instFunLike Y = let_fun this := inferInstance; this
      @[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
          Equations
          • G.instZeroHom H = inferInstance
          instance GroupCat.instOneHom (G : GroupCat) (H : GroupCat) :
          One (G H)
          Equations
          • G.instOneHom H = inferInstance
          @[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
                  @[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
                    • X.addCommGroupInstance = X.str
                    Equations
                    • X.commGroupInstance = X.str
                    instance AddCommGroupCat.instCoeFunHomForallαAddCommGroup {X : AddCommGroupCat} {Y : AddCommGroupCat} :
                    CoeFun (X Y) fun (x : X Y) => XY
                    Equations
                    • AddCommGroupCat.instCoeFunHomForallαAddCommGroup = { coe := fun (f : X →+ Y) => f }
                    instance CommGroupCat.instCoeFunHomForallαCommGroup {X : CommGroupCat} {Y : CommGroupCat} :
                    CoeFun (X Y) fun (x : X Y) => XY
                    Equations
                    • CommGroupCat.instCoeFunHomForallαCommGroup = { coe := fun (f : X →* Y) => f }
                    Equations
                    • X.instFunLike Y = let_fun this := inferInstance; this
                    instance CommGroupCat.instFunLike (X : CommGroupCat) (Y : CommGroupCat) :
                    FunLike (X Y) X Y
                    Equations
                    • X.instFunLike Y = let_fun this := inferInstance; this
                    @[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.
                        Equations
                        • G.instZeroHom H = inferInstance
                        Equations
                        • G.instOneHom H = inferInstance
                        @[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
                              • e.toAddGroupCatIso = { hom := e.toAddMonoidHom, inv := e.symm.toAddMonoidHom, hom_inv_id := , inv_hom_id := }
                              Instances For
                                @[simp]
                                theorem MulEquiv.toGroupCatIso_inv {X : GroupCat} {Y : GroupCat} (e : X ≃* Y) :
                                e.toGroupCatIso.inv = e.symm.toMonoidHom
                                @[simp]
                                theorem MulEquiv.toGroupCatIso_hom {X : GroupCat} {Y : GroupCat} (e : X ≃* Y) :
                                e.toGroupCatIso.hom = e.toMonoidHom
                                @[simp]
                                theorem AddEquiv.toAddGroupCatIso_inv {X : AddGroupCat} {Y : AddGroupCat} (e : X ≃+ Y) :
                                e.toAddGroupCatIso.inv = e.symm.toAddMonoidHom
                                @[simp]
                                theorem AddEquiv.toAddGroupCatIso_hom {X : AddGroupCat} {Y : AddGroupCat} (e : X ≃+ Y) :
                                e.toAddGroupCatIso.hom = e.toAddMonoidHom
                                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
                                • e.toGroupCatIso = { hom := e.toMonoidHom, inv := e.symm.toMonoidHom, hom_inv_id := , inv_hom_id := }
                                Instances For

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

                                  Equations
                                  • e.toAddCommGroupCatIso = { hom := e.toAddMonoidHom, inv := e.symm.toAddMonoidHom, hom_inv_id := , inv_hom_id := }
                                  Instances For
                                    @[simp]
                                    theorem AddEquiv.toAddCommGroupCatIso_hom {X : AddCommGroupCat} {Y : AddCommGroupCat} (e : X ≃+ Y) :
                                    e.toAddCommGroupCatIso.hom = e.toAddMonoidHom
                                    @[simp]
                                    theorem AddEquiv.toAddCommGroupCatIso_inv {X : AddCommGroupCat} {Y : AddCommGroupCat} (e : X ≃+ Y) :
                                    e.toAddCommGroupCatIso.inv = e.symm.toAddMonoidHom
                                    @[simp]
                                    theorem MulEquiv.toCommGroupCatIso_inv {X : CommGroupCat} {Y : CommGroupCat} (e : X ≃* Y) :
                                    e.toCommGroupCatIso.inv = e.symm.toMonoidHom
                                    @[simp]
                                    theorem MulEquiv.toCommGroupCatIso_hom {X : CommGroupCat} {Y : CommGroupCat} (e : X ≃* Y) :
                                    e.toCommGroupCatIso.hom = e.toMonoidHom
                                    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
                                    • e.toCommGroupCatIso = { hom := e.toMonoidHom, inv := e.symm.toMonoidHom, hom_inv_id := , inv_hom_id := }
                                    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
                                            @[simp]
                                            theorem CategoryTheory.Iso.addCommGroupIsoToAddEquiv_symm_apply {X : AddCommGroupCat} {Y : AddCommGroupCat} (i : X Y) (a : Y) :
                                            i.addCommGroupIsoToAddEquiv.symm a = i.inv a
                                            @[simp]
                                            theorem CategoryTheory.Iso.addCommGroupIsoToAddEquiv_apply {X : AddCommGroupCat} {Y : AddCommGroupCat} (i : X Y) (a : X) :
                                            i.addCommGroupIsoToAddEquiv a = i.hom a
                                            @[simp]
                                            theorem CategoryTheory.Iso.commGroupIsoToMulEquiv_apply {X : CommGroupCat} {Y : CommGroupCat} (i : X Y) (a : X) :
                                            i.commGroupIsoToMulEquiv a = i.hom a
                                            @[simp]
                                            theorem CategoryTheory.Iso.commGroupIsoToMulEquiv_symm_apply {X : CommGroupCat} {Y : CommGroupCat} (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_2 {X : AddGroupCat} {Y : AddGroupCat} :
                                              (CategoryTheory.CategoryStruct.comp (fun (i : X Y) => i.addGroupIsoToAddEquiv) fun (e : X ≃+ Y) => e.toAddGroupCatIso) = CategoryTheory.CategoryStruct.id (X Y)
                                              theorem addEquivIsoAddGroupIso.proof_1 {X : AddGroupCat} {Y : AddGroupCat} :
                                              (CategoryTheory.CategoryStruct.comp (fun (e : X ≃+ Y) => e.toAddGroupCatIso) fun (i : X Y) => i.addGroupIsoToAddEquiv) = CategoryTheory.CategoryStruct.id (X ≃+ Y)
                                              def addEquivIsoAddGroupIso {X : AddGroupCat} {Y : AddGroupCat} :
                                              X ≃+ Y X Y

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

                                              Equations
                                              • addEquivIsoAddGroupIso = { hom := fun (e : X ≃+ Y) => e.toAddGroupCatIso, inv := fun (i : X Y) => i.addGroupIsoToAddEquiv, hom_inv_id := , inv_hom_id := }
                                              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
                                                • mulEquivIsoGroupIso = { hom := fun (e : X ≃* Y) => e.toGroupCatIso, inv := fun (i : X Y) => i.groupIsoToMulEquiv, hom_inv_id := , inv_hom_id := }
                                                Instances For
                                                  theorem addEquivIsoAddCommGroupIso.proof_1 {X : AddCommGroupCat} {Y : AddCommGroupCat} :
                                                  (CategoryTheory.CategoryStruct.comp (fun (e : X ≃+ Y) => e.toAddCommGroupCatIso) fun (i : X Y) => i.addCommGroupIsoToAddEquiv) = CategoryTheory.CategoryStruct.comp (fun (e : X ≃+ Y) => e.toAddCommGroupCatIso) fun (i : X Y) => i.addCommGroupIsoToAddEquiv
                                                  theorem addEquivIsoAddCommGroupIso.proof_2 {X : AddCommGroupCat} {Y : AddCommGroupCat} :
                                                  (CategoryTheory.CategoryStruct.comp (fun (i : X Y) => i.addCommGroupIsoToAddEquiv) fun (e : X ≃+ Y) => e.toAddCommGroupCatIso) = CategoryTheory.CategoryStruct.comp (fun (i : X Y) => i.addCommGroupIsoToAddEquiv) fun (e : X ≃+ Y) => e.toAddCommGroupCatIso

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

                                                  Equations
                                                  • addEquivIsoAddCommGroupIso = { hom := fun (e : X ≃+ Y) => e.toAddCommGroupCatIso, inv := fun (i : X Y) => i.addCommGroupIsoToAddEquiv, hom_inv_id := , inv_hom_id := }
                                                  Instances For

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

                                                    Equations
                                                    • mulEquivIsoCommGroupIso = { hom := fun (e : X ≃* Y) => e.toCommGroupCatIso, 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
                                                          abbrev GroupCatMaxAux :
                                                          Type ((max u1 u2) + 1)

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

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

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

                                                            Equations
                                                            Instances For
                                                              @[reducible, inline]
                                                              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
                                                                  @[reducible, inline]
                                                                  abbrev CommGroupCatMax :
                                                                  Type ((max u1 u2) + 1)

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

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

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

                                                                    Equations
                                                                    Instances For