Documentation

Mathlib.Algebra.Category.Grp.ForgetCorepresentable

The forget functor is corepresentable #

It is shown that the forget functor AddCommGrpCat.{u} ⥤ Type u is corepresentable by ULift ℤ. Similar results are obtained for the variants CommGrpCat, AddGrpCat and GrpCat.

(ULift ℤ →+ G) ≃ G #

These universe-monomorphic variants of zmultiplesHom/zpowersHom are put here since they shouldn't be useful outside of category theory.

source
def uliftZMultiplesHom (G : Type u) [AddGroup G] :
G ≃ (ULift.{u, 0} ℤ →+ G)

The equivalence (ULift ℤ →+ G) ≃ G for any additive group G.

Equations
    Instances For
      source
      @[simp]
      theorem uliftZMultiplesHom_symm_apply (G : Type u) [AddGroup G] (a✝ : ULift.{u, 0} ℤ →+ G) :
      (uliftZMultiplesHom G).symm a✝ = a✝ (AddEquiv.ulift.symm 1)
      source
      @[simp]
      theorem uliftZMultiplesHom_apply_apply (G : Type u) [AddGroup G] (a✝ : G) (a✝¹ : ULift.{u, 0} ℤ) :
      ((uliftZMultiplesHom G) a✝) a✝¹ = AddEquiv.ulift a✝¹ • a✝
      source
      def uliftZPowersHom (G : Type u) [Group G] :
      G ≃ (ULift.{u, 0} (Multiplicative ℤ) →* G)

      The equivalence (ULift (Multiplicative ℤ) →* G) ≃ G for any group G.

      Equations
        Instances For
          source
          @[simp]
          theorem uliftZPowersHom_symm_apply (G : Type u) [Group G] (a✝ : ULift.{u, 0} (Multiplicative ℤ) →* G) :
          (uliftZPowersHom G).symm a✝ = a✝ (MulEquiv.ulift.symm (Multiplicative.ofAdd 1))
          source
          @[simp]
          theorem uliftZPowersHom_apply_apply (G : Type u) [Group G] (a✝ : G) (a✝¹ : ULift.{u, 0} (Multiplicative ℤ)) :
          ((uliftZPowersHom G) a✝) a✝¹ = a✝ ^ Multiplicative.toAdd (MulEquiv.ulift a✝¹)
          source
          def GrpCat.coyonedaObjIsoForget :
          CategoryTheory.coyoneda.obj (Opposite.op (of (ULift.{u, 0} (Multiplicative ℤ)))) ≅ CategoryTheory.forget GrpCat

          The forget functor GrpCat.{u} ⥤ Type u is corepresentable.

          Equations
            Instances For
              source
              def CommGrpCat.coyonedaObjIsoForget :
              CategoryTheory.coyoneda.obj (Opposite.op (of (ULift.{u, 0} (Multiplicative ℤ)))) ≅ CategoryTheory.forget CommGrpCat

              The forget functor CommGrpCat.{u} ⥤ Type u is corepresentable.

              Equations
                Instances For
                  source
                  def AddGrpCat.coyonedaObjIsoForget :
                  CategoryTheory.coyoneda.obj (Opposite.op (of (ULift.{u, 0} ℤ))) ≅ CategoryTheory.forget AddGrpCat

                  The forget functor AddGrpCat.{u} ⥤ Type u is corepresentable.

                  Equations
                    Instances For
                      source
                      def AddCommGrpCat.coyonedaObjIsoForget :
                      CategoryTheory.coyoneda.obj (Opposite.op (of (ULift.{u, 0} ℤ))) ≅ CategoryTheory.forget AddCommGrpCat

                      The forget functor AddCommGrpCat.{u} ⥤ Type u is corepresentable.

                      Equations
                        Instances For
                          source
                          instance GrpCat.forget_isCorepresentable :
                          (CategoryTheory.forget GrpCat).IsCorepresentable
                          source
                          instance CommGrpCat.forget_isCorepresentable :
                          (CategoryTheory.forget CommGrpCat).IsCorepresentable
                          source
                          instance AddGrpCat.forget_isCorepresentable :
                          (CategoryTheory.forget AddGrpCat).IsCorepresentable
                          source
                          instance AddCommGrpCat.forget_isCorepresentable :
                          (CategoryTheory.forget AddCommGrpCat).IsCorepresentable