Documentation

Mathlib.Algebra.Category.MonCat.ForgetCorepresentable

The forget 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.

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

Equations
Instances For
    @[simp]
    theorem uliftMultiplesHom_apply_apply (M : Type u) [AddMonoid M] (a✝ : M) (a✝¹ : ULift.{u, 0} ) :
    ((uliftMultiplesHom M) a✝) a✝¹ = AddEquiv.ulift a✝¹ a✝

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

    Equations
    Instances For
      @[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✝¹)
      @[deprecated powersHom (since := "2025-05-11")]

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

      Equations
      Instances For
        @[deprecated uliftPowersHom (since := "2025-05-11")]

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

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

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

          Equations
          Instances For
            @[deprecated uliftMultiplesHom (since := "2025-05-11")]

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

            Equations
            Instances For

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

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For

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

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For

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

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For

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

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For