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
      • One or more equations did not get rendered due to their size.
      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
        • One or more equations did not get rendered due to their size.
        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
          • One or more equations did not get rendered due to their size.
          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
            • One or more equations did not get rendered due to their size.
            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