Documentation

Mathlib.Algebra.Category.Grp.EquivalenceGroupAddGroup

Equivalence between Group and AddGroup #

This file contains two equivalences:

@[simp]
theorem Grp.toAddGrp_map {X : Grp} {Y : Grp} (a : X →* Y) :
Grp.toAddGrp.map a = MonoidHom.toAdditive a
@[simp]
theorem Grp.toAddGrp_obj (X : Grp) :

The functor GrpAddGrp by sending X ↦ Additive X and f ↦ f.

Equations
Instances For
    @[simp]
    theorem CommGrp.toAddCommGrp_map {X : CommGrp} {Y : CommGrp} (a : X →* Y) :
    CommGrp.toAddCommGrp.map a = MonoidHom.toAdditive a

    The functor CommGrpAddCommGrp by sending X ↦ Additive X and f ↦ f.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      @[simp]
      theorem AddGrp.toGrp_map {X : AddGrp} {Y : AddGrp} (a : X →+ Y) :
      AddGrp.toGrp.map a = AddMonoidHom.toMultiplicative a
      @[simp]

      The functor AddGrpGrp by sending X ↦ Multiplicative Y and f ↦ f.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        @[simp]
        theorem AddCommGrp.toCommGrp_map {X : AddCommGrp} {Y : AddCommGrp} (a : X →+ Y) :
        AddCommGrp.toCommGrp.map a = AddMonoidHom.toMultiplicative a

        The functor AddCommGrpCommGrp by sending X ↦ Multiplicative Y and f ↦ f.

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

          The equivalence of categories between Grp and AddGrp

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

            The equivalence of categories between CommGrp and AddCommGrp.

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