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

@[simp]

theorem MonoidHom.fromMultiplicativeIntEquiv_apply (α : Type u) [Group α] (φ : Multiplicative ℤ →* α) : (MonoidHom.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 ℤ) →* α) : (MonoidHom.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 ℤ)) : ((MonoidHom.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 : α) : (AddMonoidHom.fromIntEquiv α).symm x = (zmultiplesHom α) x

@[simp]

theorem AddMonoidHom.fromIntEquiv_apply (α : Type u) [AddGroup α] (φ : ℤ →+ α) : (AddMonoidHom.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} ℤ →+ α) : (AddMonoidHom.fromULiftIntEquiv α) a✝ = a✝ (AddEquiv.ulift.symm 1)

@[simp]

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

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

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

Equations

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

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

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

Equations

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

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

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

Equations

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

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

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

Equations

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

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