Documentation

Mathlib.Algebra.Category.GroupCat.EquivalenceGroupAddGroup

Equivalence between Group and AddGroup #

This file contains two equivalences:

source
@[simp]
theorem GroupCat.toAddGroupCat_obj (X : GroupCat) :
GroupCat.toAddGroupCat.obj X = AddGroupCat.of (Additive ↑X)
source
@[simp]
theorem GroupCat.toAddGroupCat_map {X : GroupCat} {Y : GroupCat} (a : ↑X →* ↑Y) :
GroupCat.toAddGroupCat.map a = MonoidHom.toAdditive a
source
def GroupCat.toAddGroupCat :
CategoryTheory.Functor GroupCat AddGroupCat

The functor Group ⥤ AddGroup 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 CommGroupCat.toAddCommGroupCat_map {X : CommGroupCat} {Y : CommGroupCat} (a : ↑X →* ↑Y) :
    CommGroupCat.toAddCommGroupCat.map a = MonoidHom.toAdditive a
    source
    @[simp]
    theorem CommGroupCat.toAddCommGroupCat_obj (X : CommGroupCat) :
    CommGroupCat.toAddCommGroupCat.obj X = AddCommGroupCat.of (Additive ↑X)
    source
    def CommGroupCat.toAddCommGroupCat :
    CategoryTheory.Functor CommGroupCat AddCommGroupCat

    The functor CommGroup ⥤ AddCommGroup 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 AddGroupCat.toGroupCat_obj (X : AddGroupCat) :
      AddGroupCat.toGroupCat.obj X = GroupCat.of (Multiplicative ↑X)
      source
      @[simp]
      theorem AddGroupCat.toGroupCat_map {X : AddGroupCat} {Y : AddGroupCat} (a : ↑X →+ ↑Y) :
      AddGroupCat.toGroupCat.map a = AddMonoidHom.toMultiplicative a
      source
      def AddGroupCat.toGroupCat :
      CategoryTheory.Functor AddGroupCat GroupCat

      The functor AddGroup ⥤ Group 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 AddCommGroupCat.toCommGroupCat_map {X : AddCommGroupCat} {Y : AddCommGroupCat} (a : ↑X →+ ↑Y) :
        AddCommGroupCat.toCommGroupCat.map a = AddMonoidHom.toMultiplicative a
        source
        @[simp]
        theorem AddCommGroupCat.toCommGroupCat_obj (X : AddCommGroupCat) :
        AddCommGroupCat.toCommGroupCat.obj X = CommGroupCat.of (Multiplicative ↑X)
        source
        def AddCommGroupCat.toCommGroupCat :
        CategoryTheory.Functor AddCommGroupCat CommGroupCat

        The functor AddCommGroup ⥤ CommGroup by sending X ↦ multiplicative Y and f ↦ f.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def groupAddGroupEquivalence :
          GroupCat ≌ AddGroupCat

          The equivalence of categories between Group and AddGroup

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def commGroupAddCommGroupEquivalence :
            CommGroupCat ≌ AddCommGroupCat

            The equivalence of categories between CommGroup and AddCommGroup.

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