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
      @[deprecated zpowersHom (since := "2025-05-11")]
      def MonoidHom.fromMultiplicativeIntEquiv (α : Type u) [Group α] :
      (Multiplicative ℤ →* α) ≃ α

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

      Equations
      Instances For
        source
        @[deprecated uliftZPowersHom (since := "2025-05-11")]
        def MonoidHom.fromULiftMultiplicativeIntEquiv (α : Type u) [Group α] :
        (ULift.{u, 0} (Multiplicative ℤ) →* α) ≃ α

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

        Equations
        Instances For
          source
          @[deprecated zmultiplesHom (since := "2025-05-11")]
          def AddMonoidHom.fromIntEquiv (α : Type u) [AddGroup α] :
          (ℤ →+ α) ≃ α

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

          Equations
          Instances For
            source
            @[deprecated uliftZMultiplesHom (since := "2025-05-11")]
            def AddMonoidHom.fromULiftIntEquiv (α : Type u) [AddGroup α] :
            (ULift.{u, 0} ℤ →+ α) ≃ α

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

            Equations
            Instances For
              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