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.

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
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
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
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
source
@[deprecated multiplesHom (since := "2025-05-11")]
def AddMonoidHom.fromNatEquiv (α : Type u) [AddMonoid α] :
(ℕ →+ α) ≃ α

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

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

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

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