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.

def MonoidHom.fromMultiplicativeNatEquiv (α : Type u) [Monoid α] : (Multiplicative ℕ →* α) ≃ α

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

Equations

• MonoidHom.fromMultiplicativeNatEquiv α = { toFun := fun (φ : Multiplicative ℕ →* α) => φ (Multiplicative.ofAdd 1), invFun := fun (x : α) => (powersHom α) x, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem MonoidHom.fromMultiplicativeNatEquiv_symm_apply (α : Type u) [Monoid α] (x : α) : (fromMultiplicativeNatEquiv α).symm x = (powersHom α) x

@[simp]

theorem MonoidHom.fromMultiplicativeNatEquiv_apply (α : Type u) [Monoid α] (φ : Multiplicative ℕ →* α) : (fromMultiplicativeNatEquiv α) φ = φ (Multiplicative.ofAdd 1)

def MonoidHom.fromULiftMultiplicativeNatEquiv (α : Type u) [Monoid α] : (ULift.{u, 0} (Multiplicative ℕ) →* α) ≃ α

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

Equations

• MonoidHom.fromULiftMultiplicativeNatEquiv α = (MonoidHom.precompEquiv MulEquiv.ulift.symm α).trans (MonoidHom.fromMultiplicativeNatEquiv α)

@[simp]

theorem MonoidHom.fromULiftMultiplicativeNatEquiv_apply (α : Type u) [Monoid α] (a✝ : ULift.{u, 0} (Multiplicative ℕ) →* α) : (fromULiftMultiplicativeNatEquiv α) a✝ = a✝ (MulEquiv.ulift.symm (Multiplicative.ofAdd 1))

@[simp]

theorem MonoidHom.fromULiftMultiplicativeNatEquiv_symm_apply_apply (α : Type u) [Monoid α] (a✝ : α) (a✝¹ : ULift.{u, 0} (Multiplicative ℕ)) : ((fromULiftMultiplicativeNatEquiv α).symm a✝) a✝¹ = a✝ ^ Multiplicative.toAdd (MulEquiv.ulift a✝¹)

def AddMonoidHom.fromNatEquiv (α : Type u) [AddMonoid α] : (ℕ →+ α) ≃ α

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

Equations

• AddMonoidHom.fromNatEquiv α = { toFun := fun (φ : ℕ →+ α) => φ 1, invFun := fun (x : α) => (multiplesHom α) x, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem AddMonoidHom.fromNatEquiv_apply (α : Type u) [AddMonoid α] (φ : ℕ →+ α) : (fromNatEquiv α) φ = φ 1

@[simp]

theorem AddMonoidHom.fromNatEquiv_symm_apply (α : Type u) [AddMonoid α] (x : α) : (fromNatEquiv α).symm x = (multiplesHom α) x

def AddMonoidHom.fromULiftNatEquiv (α : Type u) [AddMonoid α] : (ULift.{u, 0} ℕ →+ α) ≃ α

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

Equations

• AddMonoidHom.fromULiftNatEquiv α = (AddMonoidHom.precompEquiv AddEquiv.ulift.symm α).trans (AddMonoidHom.fromNatEquiv α)

@[simp]

theorem AddMonoidHom.fromULiftNatEquiv_apply (α : Type u) [AddMonoid α] (a✝ : ULift.{u, 0} ℕ →+ α) : (fromULiftNatEquiv α) a✝ = a✝ (AddEquiv.ulift.symm 1)

@[simp]

theorem AddMonoidHom.fromULiftNatEquiv_symm_apply_apply (α : Type u) [AddMonoid α] (a✝ : α) (a✝¹ : ULift.{u, 0} ℕ) : ((fromULiftNatEquiv α).symm a✝) a✝¹ = AddEquiv.ulift a✝¹ • a✝

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

• MonCat.coyonedaObjIsoForget = CategoryTheory.NatIso.ofComponents (fun (M : MonCat) => (MonoidHom.fromULiftMultiplicativeNatEquiv ↑M).toIso) @MonCat.coyonedaObjIsoForget.proof_1

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

• CommMonCat.coyonedaObjIsoForget = CategoryTheory.NatIso.ofComponents (fun (M : CommMonCat) => (MonoidHom.fromULiftMultiplicativeNatEquiv ↑M).toIso) @CommMonCat.coyonedaObjIsoForget.proof_1

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

• AddMonCat.coyonedaObjIsoForget = CategoryTheory.NatIso.ofComponents (fun (M : AddMonCat) => (AddMonoidHom.fromULiftNatEquiv ↑M).toIso) @AddMonCat.coyonedaObjIsoForget.proof_1

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

• AddCommMonCat.coyonedaObjIsoForget = CategoryTheory.NatIso.ofComponents (fun (M : AddCommMonCat) => (AddMonoidHom.fromULiftNatEquiv ↑M).toIso) @AddCommMonCat.coyonedaObjIsoForget.proof_1

instance MonCat.forget_isCorepresentable : (CategoryTheory.forget MonCat).IsCorepresentable

instance CommMonCat.forget_isCorepresentable : (CategoryTheory.forget CommMonCat).IsCorepresentable

instance AddMonCat.forget_isCorepresentable : (CategoryTheory.forget AddMonCat).IsCorepresentable

instance AddCommMonCat.forget_isCorepresentable : (CategoryTheory.forget AddCommMonCat).IsCorepresentable