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.precompEquiv {α : Type u_1} {β : Type u_2} [Monoid α] [Monoid β] (e : α ≃* β) (γ : Type u_3) [Monoid γ] : (β →* γ) ≃ (α →* γ)

The equivalence (β →* γ) ≃ (α →* γ) obtained by precomposition with a multiplicative equivalence e : α ≃* β.

Equations

• MonoidHom.precompEquiv e γ = { toFun := fun (f : β →* γ) => f.comp ↑e, invFun := fun (g : α →* γ) => g.comp ↑e.symm, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem MonoidHom.precompEquiv_symm_apply {α : Type u_1} {β : Type u_2} [Monoid α] [Monoid β] (e : α ≃* β) (γ : Type u_3) [Monoid γ] (g : α →* γ) : (MonoidHom.precompEquiv e γ).symm g = g.comp ↑e.symm

@[simp]

theorem MonoidHom.precompEquiv_apply {α : Type u_1} {β : Type u_2} [Monoid α] [Monoid β] (e : α ≃* β) (γ : Type u_3) [Monoid γ] (f : β →* γ) : (MonoidHom.precompEquiv e γ) f = f.comp ↑e

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 : α) : (MonoidHom.fromMultiplicativeNatEquiv α).symm x = (powersHom α) x

@[simp]

theorem MonoidHom.fromMultiplicativeNatEquiv_apply (α : Type u) [Monoid α] (φ : Multiplicative ℕ →* α) : (MonoidHom.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_symm_apply_apply (α : Type u) [Monoid α] (a✝ : α) (a✝¹ : ULift.{u, 0} (Multiplicative ℕ)) : ((MonoidHom.fromULiftMultiplicativeNatEquiv α).symm a✝) a✝¹ = a✝ ^ Multiplicative.toAdd (MulEquiv.ulift a✝¹)

@[simp]

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

def AddMonoidHom.precompEquiv {α : Type u_1} {β : Type u_2} [AddMonoid α] [AddMonoid β] (e : α ≃+ β) (γ : Type u_3) [AddMonoid γ] : (β →+ γ) ≃ (α →+ γ)

The equivalence (β →+ γ) ≃ (α →+ γ) obtained by precomposition with an additive equivalence e : α ≃+ β.

Equations

• AddMonoidHom.precompEquiv e γ = { toFun := fun (f : β →+ γ) => f.comp ↑e, invFun := fun (g : α →+ γ) => g.comp ↑e.symm, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem AddMonoidHom.precompEquiv_apply {α : Type u_1} {β : Type u_2} [AddMonoid α] [AddMonoid β] (e : α ≃+ β) (γ : Type u_3) [AddMonoid γ] (f : β →+ γ) : (AddMonoidHom.precompEquiv e γ) f = f.comp ↑e

@[simp]

theorem AddMonoidHom.precompEquiv_symm_apply {α : Type u_1} {β : Type u_2} [AddMonoid α] [AddMonoid β] (e : α ≃+ β) (γ : Type u_3) [AddMonoid γ] (g : α →+ γ) : (AddMonoidHom.precompEquiv e γ).symm g = g.comp ↑e.symm

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_symm_apply (α : Type u) [AddMonoid α] (x : α) : (AddMonoidHom.fromNatEquiv α).symm x = (multiplesHom α) x

@[simp]

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

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_symm_apply_apply (α : Type u) [AddMonoid α] (a✝ : α) (a✝¹ : ULift.{u, 0} ℕ) : ((AddMonoidHom.fromULiftNatEquiv α).symm a✝) a✝¹ = AddEquiv.ulift a✝¹ • a✝

@[simp]

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

def MonCat.coyonedaObjIsoForget : CategoryTheory.coyoneda.obj (Opposite.op (MonCat.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 (CommMonCat.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 (AddMonCat.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 (AddCommMonCat.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