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
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem Grp.toAddGrp_map {x✝ x✝¹ : Grp} (f : x✝ ⟶ x✝¹) :
    toAddGrp.map f = AddGrp.ofHom (MonoidHom.toAdditive (Hom.hom f))
    source
    @[simp]
    theorem Grp.toAddGrp_obj_coe (X : Grp) :
    ↑(toAddGrp.obj X) = Additive ↑X
    source
    def CommGrp.toAddCommGrp :
    CategoryTheory.Functor CommGrp AddCommGrp

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

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem CommGrp.toAddCommGrp_map {x✝ x✝¹ : CommGrp} (f : x✝ ⟶ x✝¹) :
      toAddCommGrp.map f = AddCommGrp.ofHom (MonoidHom.toAdditive (Hom.hom f))
      source
      @[simp]
      theorem CommGrp.toAddCommGrp_obj_coe (X : CommGrp) :
      ↑(toAddCommGrp.obj X) = Additive ↑X
      source
      def AddGrp.toGrp :
      CategoryTheory.Functor AddGrp Grp

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

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem AddGrp.toGrp_obj_coe (X : AddGrp) :
        ↑(toGrp.obj X) = Multiplicative ↑X
        source
        @[simp]
        theorem AddGrp.toGrp_map {x✝ x✝¹ : AddGrp} (f : x✝ ⟶ x✝¹) :
        toGrp.map f = Grp.ofHom (AddMonoidHom.toMultiplicative (Hom.hom f))
        source
        def AddCommGrp.toCommGrp :
        CategoryTheory.Functor AddCommGrp CommGrp

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

        Equations
        • One or more equations did not get rendered due to their size.
        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
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[simp]
            theorem groupAddGroupEquivalence_functor :
            groupAddGroupEquivalence.functor = Grp.toAddGrp
            source
            @[simp]
            theorem groupAddGroupEquivalence_inverse :
            groupAddGroupEquivalence.inverse = AddGrp.toGrp
            source
            @[simp]
            theorem groupAddGroupEquivalence_unitIso :
            groupAddGroupEquivalence.unitIso = CategoryTheory.Iso.refl (CategoryTheory.Functor.id Grp)
            source
            @[simp]
            theorem groupAddGroupEquivalence_counitIso :
            groupAddGroupEquivalence.counitIso = CategoryTheory.Iso.refl (AddGrp.toGrp.comp Grp.toAddGrp)
            source
            def commGroupAddCommGroupEquivalence :
            CommGrp ≌ AddCommGrp

            The equivalence of categories between CommGrp and AddCommGrp.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              @[simp]
              theorem commGroupAddCommGroupEquivalence_inverse :
              commGroupAddCommGroupEquivalence.inverse = AddCommGrp.toCommGrp
              source
              @[simp]
              theorem commGroupAddCommGroupEquivalence_unitIso :
              commGroupAddCommGroupEquivalence.unitIso = CategoryTheory.Iso.refl (CategoryTheory.Functor.id CommGrp)
              source
              @[simp]
              theorem commGroupAddCommGroupEquivalence_counitIso :
              commGroupAddCommGroupEquivalence.counitIso = CategoryTheory.Iso.refl (AddCommGrp.toCommGrp.comp CommGrp.toAddCommGrp)
              source
              @[simp]
              theorem commGroupAddCommGroupEquivalence_functor :
              commGroupAddCommGroupEquivalence.functor = CommGrp.toAddCommGrp