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.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.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_symm_apply_apply (α : Type u) [Group α] : ∀ (a : α) (a_1 : ULift.{u, 0} (Multiplicative ℤ)), ((MonoidHom.fromULiftMultiplicativeIntEquiv α).symm a) a_1 = a ^ Multiplicative.toAdd (MulEquiv.ulift a_1)

@[simp]

theorem MonoidHom.fromULiftMultiplicativeIntEquiv_apply (α : Type u) [Group α] : ∀ (a : ULift.{u, 0} (Multiplicative ℤ) →* α), (MonoidHom.fromULiftMultiplicativeIntEquiv α) 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_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

@[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

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_symm_apply_apply (α : Type u) [AddGroup α] : ∀ (a : α) (a_1 : ULift.{u, 0} ℤ), ((AddMonoidHom.fromULiftIntEquiv α).symm a) a_1 = AddEquiv.ulift a_1 • a

@[simp]

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

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

Equations

• Grp.forget_isCorepresentable = ⋯

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

Equations

• CommGrp.forget_isCorepresentable = ⋯

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

Equations

• AddGrp.forget_isCorepresentable = ⋯

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

Equations

• AddCommGrp.forget_isCorepresentable = ⋯