The forget functor is corepresentable

It is shown that the forget functor AddCommGrp.{u} ⥤ Type u is corepresentable by ULift ℤ. Similar results are obtained for the variants CommGrp, AddGrp and Grp.

def MonoidHom.fromMultiplicativeIntEquiv (α : Type u) [Group α] : (Multiplicative ℤ →* α) ≃ α

The equivalence (Multiplicative ℤ →* α) ≃ α for any group α.

Equations

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

@[simp]

theorem MonoidHom.fromMultiplicativeIntEquiv_symm_apply (α : Type u) [Group α] (x : α) : (fromMultiplicativeIntEquiv α).symm x = (zpowersHom α) x

@[simp]

theorem MonoidHom.fromMultiplicativeIntEquiv_apply (α : Type u) [Group α] (φ : Multiplicative ℤ →* α) : (fromMultiplicativeIntEquiv α) φ = φ (Multiplicative.ofAdd 1)

def MonoidHom.fromULiftMultiplicativeIntEquiv (α : Type u) [Group α] : (ULift.{u, 0} (Multiplicative ℤ) →* α) ≃ α

The equivalence (ULift (Multiplicative ℤ) →* α) ≃ α for any group α.

Equations

• MonoidHom.fromULiftMultiplicativeIntEquiv α = (MonoidHom.precompEquiv MulEquiv.ulift.symm α).trans (MonoidHom.fromMultiplicativeIntEquiv α)

@[simp]

theorem MonoidHom.fromULiftMultiplicativeIntEquiv_apply (α : Type u) [Group α] (a✝ : ULift.{u, 0} (Multiplicative ℤ) →* α) : (fromULiftMultiplicativeIntEquiv α) a✝ = a✝ (MulEquiv.ulift.symm (Multiplicative.ofAdd 1))

@[simp]

theorem MonoidHom.fromULiftMultiplicativeIntEquiv_symm_apply_apply (α : Type u) [Group α] (a✝ : α) (a✝¹ : ULift.{u, 0} (Multiplicative ℤ)) : ((fromULiftMultiplicativeIntEquiv α).symm a✝) a✝¹ = a✝ ^ Multiplicative.toAdd (MulEquiv.ulift a✝¹)

def AddMonoidHom.fromIntEquiv (α : Type u) [AddGroup α] : (ℤ →+ α) ≃ α

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

Equations

• AddMonoidHom.fromIntEquiv α = { toFun := fun (φ : ℤ →+ α) => φ 1, invFun := fun (x : α) => (zmultiplesHom α) x, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem AddMonoidHom.fromIntEquiv_symm_apply (α : Type u) [AddGroup α] (x : α) : (fromIntEquiv α).symm x = (zmultiplesHom α) x

@[simp]

theorem AddMonoidHom.fromIntEquiv_apply (α : Type u) [AddGroup α] (φ : ℤ →+ α) : (fromIntEquiv α) φ = φ 1

def AddMonoidHom.fromULiftIntEquiv (α : Type u) [AddGroup α] : (ULift.{u, 0} ℤ →+ α) ≃ α

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

Equations

• AddMonoidHom.fromULiftIntEquiv α = (AddMonoidHom.precompEquiv AddEquiv.ulift.symm α).trans (AddMonoidHom.fromIntEquiv α)

@[simp]

theorem AddMonoidHom.fromULiftIntEquiv_apply (α : Type u) [AddGroup α] (a✝ : ULift.{u, 0} ℤ →+ α) : (fromULiftIntEquiv α) a✝ = a✝ (AddEquiv.ulift.symm 1)

@[simp]

theorem AddMonoidHom.fromULiftIntEquiv_symm_apply_apply (α : Type u) [AddGroup α] (a✝ : α) (a✝¹ : ULift.{u, 0} ℤ) : ((fromULiftIntEquiv α).symm a✝) a✝¹ = AddEquiv.ulift a✝¹ • a✝

def Grp.coyonedaObjIsoForget : CategoryTheory.coyoneda.obj (Opposite.op (of (ULift.{u, 0} (Multiplicative ℤ)))) ≅ CategoryTheory.forget Grp

The forget functor Grp.{u} ⥤ Type u is corepresentable.

Equations

• One or more equations did not get rendered due to their size.

def CommGrp.coyonedaObjIsoForget : CategoryTheory.coyoneda.obj (Opposite.op (of (ULift.{u, 0} (Multiplicative ℤ)))) ≅ CategoryTheory.forget CommGrp

The forget functor CommGrp.{u} ⥤ Type u is corepresentable.

Equations

• One or more equations did not get rendered due to their size.

def AddGrp.coyonedaObjIsoForget : CategoryTheory.coyoneda.obj (Opposite.op (of (ULift.{u, 0} ℤ))) ≅ CategoryTheory.forget AddGrp

The forget functor AddGrp.{u} ⥤ Type u is corepresentable.

Equations

• One or more equations did not get rendered due to their size.

def AddCommGrp.coyonedaObjIsoForget : CategoryTheory.coyoneda.obj (Opposite.op (of (ULift.{u, 0} ℤ))) ≅ CategoryTheory.forget AddCommGrp

The forget functor AddCommGrp.{u} ⥤ Type u is corepresentable.

Equations

• One or more equations did not get rendered due to their size.

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

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

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

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