Documentation

Mathlib.Algebra.Category.Grp.Adjunctions

Adjunctions regarding the category of (abelian) groups #

This file contains construction of basic adjunctions concerning the category of groups and the category of abelian groups.

Main definitions #

Main statements #

The free functor Type u ⥤ AddCommGroup sending a type X to the free abelian group with generators x : X.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    @[simp]
    theorem AddCommGrp.free_map_coe {α : Type u} {β : Type u} {f : αβ} (x : FreeAbelianGroup α) :
    (AddCommGrp.free.map f) x = f <$> x

    The free-forgetful adjunction for abelian groups.

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

      The free functor Type u ⥤ Group sending a type X to the free group with generators x : X.

      Equations
      Instances For

        The free-forgetful adjunction for groups.

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

          The abelianization functor GroupCommGroup sending a group G to its abelianization Gᵃᵇ.

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

            The abelianization-forgetful adjuction from Group to CommGroup.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              @[simp]
              theorem MonCat.units_obj (R : MonCat) :
              MonCat.units.obj R = Grp.of (↑R)ˣ
              @[simp]
              theorem MonCat.units_map :
              ∀ {X Y : MonCat} (f : X Y), MonCat.units.map f = Grp.ofHom (Units.map f)

              The functor taking a monoid to its subgroup of units.

              Equations
              Instances For

                The forgetful-units adjunction between Grp and MonCat.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  @[simp]
                  theorem CommMonCat.units_map :
                  ∀ {X Y : CommMonCat} (f : X Y), CommMonCat.units.map f = CommGrp.ofHom (Units.map f)

                  The functor taking a monoid to its subgroup of units.

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

                    The forgetful-units adjunction between CommGrp and CommMonCat.

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