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_symm_apply (M : Type u) [AddMonoid M] (a✝ : ULift.{u, 0} ℕ →+ M) :
    (uliftMultiplesHom M).symm a✝ = a✝ (AddEquiv.ulift.symm 1)
    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
    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_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
      @[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
      @[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
              • One or more equations did not get rendered due to their size.
              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
                • One or more equations did not get rendered due to their size.
                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
                  • One or more equations did not get rendered due to their size.
                  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
                    • One or more equations did not get rendered due to their size.
                    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