Documentation

Mathlib.Algebra.Category.Grp.EquivalenceGroupAddGroup

Equivalence between Group and AddGroup #

This file contains two equivalences:

source
def Grp.toAddGrp :
CategoryTheory.Functor Grp AddGrp

The functor Grp ⥤ AddGrp by sending X ↦ Additive X and f ↦ f.

Equations
    Instances For
      source
      @[simp]
      theorem Grp.toAddGrp_obj_coe (X : Grp) :
      ↑(toAddGrp.obj X) = Additive ↑X
      source
      @[simp]
      theorem Grp.toAddGrp_map {x✝ x✝¹ : Grp} (f : x✝ ⟶ x✝¹) :
      toAddGrp.map f = AddGrp.ofHom (MonoidHom.toAdditive (Hom.hom f))
      source
      def CommGrp.toAddCommGrp :
      CategoryTheory.Functor CommGrp AddCommGrp

      The functor CommGrp ⥤ AddCommGrp by sending X ↦ Additive X and f ↦ f.

      Equations
        Instances For
          source
          @[simp]
          theorem CommGrp.toAddCommGrp_obj_coe (X : CommGrp) :
          ↑(toAddCommGrp.obj X) = Additive ↑X
          source
          @[simp]
          theorem CommGrp.toAddCommGrp_map {x✝ x✝¹ : CommGrp} (f : x✝ ⟶ x✝¹) :
          toAddCommGrp.map f = AddCommGrp.ofHom (MonoidHom.toAdditive (Hom.hom f))
          source
          def AddGrp.toGrp :
          CategoryTheory.Functor AddGrp Grp

          The functor AddGrp ⥤ Grp by sending X ↦ Multiplicative X and f ↦ f.

          Equations
            Instances For
              source
              @[simp]
              theorem AddGrp.toGrp_map {x✝ x✝¹ : AddGrp} (f : x✝ ⟶ x✝¹) :
              toGrp.map f = Grp.ofHom (AddMonoidHom.toMultiplicative (Hom.hom f))
              source
              @[simp]
              theorem AddGrp.toGrp_obj_coe (X : AddGrp) :
              ↑(toGrp.obj X) = Multiplicative ↑X
              source
              def AddCommGrp.toCommGrp :
              CategoryTheory.Functor AddCommGrp CommGrp

              The functor AddCommGrp ⥤ CommGrp by sending X ↦ Multiplicative X and f ↦ f.

              Equations
                Instances For
                  source
                  @[simp]
                  theorem AddCommGrp.toCommGrp_map {x✝ x✝¹ : AddCommGrp} (f : x✝ ⟶ x✝¹) :
                  toCommGrp.map f = CommGrp.ofHom (AddMonoidHom.toMultiplicative (Hom.hom f))
                  source
                  @[simp]
                  theorem AddCommGrp.toCommGrp_obj_coe (X : AddCommGrp) :
                  ↑(toCommGrp.obj X) = Multiplicative ↑X
                  source
                  def groupAddGroupEquivalence :
                  Grp ≌ AddGrp

                  The equivalence of categories between Grp and AddGrp

                  Equations
                    Instances For
                      source
                      @[simp]
                      theorem groupAddGroupEquivalence_functor :
                      groupAddGroupEquivalence.functor = Grp.toAddGrp
                      source
                      @[simp]
                      theorem groupAddGroupEquivalence_inverse :
                      groupAddGroupEquivalence.inverse = AddGrp.toGrp
                      source
                      @[simp]
                      theorem groupAddGroupEquivalence_counitIso :
                      groupAddGroupEquivalence.counitIso = CategoryTheory.Iso.refl (AddGrp.toGrp.comp Grp.toAddGrp)
                      source
                      @[simp]
                      theorem groupAddGroupEquivalence_unitIso :
                      groupAddGroupEquivalence.unitIso = CategoryTheory.Iso.refl (CategoryTheory.Functor.id Grp)
                      source
                      def commGroupAddCommGroupEquivalence :
                      CommGrp ≌ AddCommGrp

                      The equivalence of categories between CommGrp and AddCommGrp.

                      Equations
                        Instances For
                          source
                          @[simp]
                          theorem commGroupAddCommGroupEquivalence_counitIso :
                          commGroupAddCommGroupEquivalence.counitIso = CategoryTheory.Iso.refl (AddCommGrp.toCommGrp.comp CommGrp.toAddCommGrp)
                          source
                          @[simp]
                          theorem commGroupAddCommGroupEquivalence_unitIso :
                          commGroupAddCommGroupEquivalence.unitIso = CategoryTheory.Iso.refl (CategoryTheory.Functor.id CommGrp)
                          source
                          @[simp]
                          theorem commGroupAddCommGroupEquivalence_functor :
                          commGroupAddCommGroupEquivalence.functor = CommGrp.toAddCommGrp
                          source
                          @[simp]
                          theorem commGroupAddCommGroupEquivalence_inverse :
                          commGroupAddCommGroupEquivalence.inverse = AddCommGrp.toCommGrp