Documentation

Mathlib.Algebra.Category.Grp.ForgetCorepresentable

The forget functor is corepresentable #

It is shown that the forget functor AddCommGrp.{u} ⥤ Type u is corepresentable by ULift ℤ. Similar results are obtained for the variants CommGrp, AddGrp and Grp.

(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 Grp.coyonedaObjIsoForget :
                          CategoryTheory.coyoneda.obj (Opposite.op (of (ULift.{u, 0} (Multiplicative ℤ)))) ≅ CategoryTheory.forget Grp

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

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

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

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

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

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

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

                                      Equations
                                        Instances For
                                          source
                                          instance Grp.forget_isCorepresentable :
                                          (CategoryTheory.forget Grp).IsCorepresentable
                                          source
                                          instance CommGrp.forget_isCorepresentable :
                                          (CategoryTheory.forget CommGrp).IsCorepresentable
                                          source
                                          instance AddGrp.forget_isCorepresentable :
                                          (CategoryTheory.forget AddGrp).IsCorepresentable
                                          source
                                          instance AddCommGrp.forget_isCorepresentable :
                                          (CategoryTheory.forget AddCommGrp).IsCorepresentable