Documentation

Mathlib.Algebra.Category.MonCat.ForgetCorepresentable

The forgetful functor is corepresentable #

The forgetful functor AddCommMonCat.{u} ⥤ Type u is corepresentable by ULift ℕ. Similar results are obtained for the variants CommMonCat, AddMonCat and MonCat.

(ULift ℕ →+ G) ≃ G #

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

source
def uliftMultiplesHom (M : Type u) [AddMonoid M] :
M ≃ (ULift.{u, 0} ℕ →+ M)

Monoid homomorphisms from ULift ℕ are defined by the image of 1.

Equations
    Instances For
      source
      @[simp]
      theorem uliftMultiplesHom_apply_apply (M : Type u) [AddMonoid M] (a✝ : M) (a✝¹ : ULift.{u, 0} ℕ) :
      ((uliftMultiplesHom M) a✝) a✝¹ = AddEquiv.ulift a✝¹ • a✝
      source
      @[simp]
      theorem uliftMultiplesHom_symm_apply (M : Type u) [AddMonoid M] (a✝ : ULift.{u, 0} ℕ →+ M) :
      (uliftMultiplesHom M).symm a✝ = a✝ (AddEquiv.ulift.symm 1)
      source
      def uliftPowersHom (M : Type u) [Monoid M] :
      M ≃ (ULift.{u, 0} (Multiplicative ℕ) →* M)

      Monoid homomorphisms from ULift (Multiplicative ℕ) are defined by the image of Multiplicative.ofAdd 1.

      Equations
        Instances For
          source
          @[simp]
          theorem uliftPowersHom_symm_apply (M : Type u) [Monoid M] (a✝ : ULift.{u, 0} (Multiplicative ℕ) →* M) :
          (uliftPowersHom M).symm a✝ = a✝ (MulEquiv.ulift.symm (Multiplicative.ofAdd 1))
          source
          @[simp]
          theorem uliftPowersHom_apply_apply (M : Type u) [Monoid M] (a✝ : M) (a✝¹ : ULift.{u, 0} (Multiplicative ℕ)) :
          ((uliftPowersHom M) a✝) a✝¹ = a✝ ^ Multiplicative.toAdd (MulEquiv.ulift a✝¹)
          source
          @[deprecated powersHom (since := "2025-05-11")]
          def MonoidHom.fromMultiplicativeNatEquiv (α : Type u) [Monoid α] :
          (Multiplicative ℕ →* α) ≃ α

          The equivalence (Multiplicative ℕ →* α) ≃ α for any monoid α.

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

              The equivalence (ULift (Multiplicative ℕ) →* α) ≃ α for any monoid α.

              Equations
                Instances For
                  source
                  @[deprecated multiplesHom (since := "2025-05-11")]
                  def AddMonoidHom.fromNatEquiv (α : Type u) [AddMonoid α] :
                  (ℕ →+ α) ≃ α

                  The equivalence (ℕ →+ α) ≃ α for any additive monoid α.

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

                      The equivalence (ULift ℕ →+ α) ≃ α for any additive monoid α.

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

                          The forgetful functor MonCat.{u} ⥤ Type u is corepresentable.

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

                              The forgetful functor CommMonCat.{u} ⥤ Type u is corepresentable.

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

                                  The forgetful functor AddMonCat.{u} ⥤ Type u is corepresentable.

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

                                      The forgetful functor AddCommMonCat.{u} ⥤ Type u is corepresentable.

                                      Equations
                                        Instances For
                                          source
                                          instance MonCat.forget_isCorepresentable :
                                          (CategoryTheory.forget MonCat).IsCorepresentable
                                          source
                                          instance CommMonCat.forget_isCorepresentable :
                                          (CategoryTheory.forget CommMonCat).IsCorepresentable
                                          source
                                          instance AddMonCat.forget_isCorepresentable :
                                          (CategoryTheory.forget AddMonCat).IsCorepresentable
                                          source
                                          instance AddCommMonCat.forget_isCorepresentable :
                                          (CategoryTheory.forget AddCommMonCat).IsCorepresentable