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
      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