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