The forget functor is corepresentable

It is shown that the forget functor AddCommGroupCat.{u} ⥤ Type u is corepresentable by ULift ℤ. Similar results are obtained for the variants CommGroupCat, AddGroupCat and GroupCat.

@[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 = MonoidHom.comp g ↑(MulEquiv.symm e)

@[simp]

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

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 : β →* γ) => MonoidHom.comp f ↑e, invFun := fun (g : α →* γ) => MonoidHom.comp g ↑(MulEquiv.symm e), left_inv := ⋯, right_inv := ⋯ }

@[simp]

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

@[simp]

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

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

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

Equations

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

@[simp]

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

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

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

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

Equations

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

@[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 = AddMonoidHom.comp g ↑(AddEquiv.symm e)

@[simp]

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

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

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

@[simp]

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

@[simp]

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

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.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.symm AddEquiv.ulift) 1)

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

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

Equations

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

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

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

Equations

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

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

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

Equations

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

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

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

Equations

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

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

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

Equations

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

instance GroupCat.forget_corepresentable : CategoryTheory.Functor.Corepresentable (CategoryTheory.forget GroupCat)

Equations

• GroupCat.forget_corepresentable = ⋯

instance CommGroupCat.forget_corepresentable : CategoryTheory.Functor.Corepresentable (CategoryTheory.forget CommGroupCat)

Equations

• CommGroupCat.forget_corepresentable = ⋯

instance AddGroupCat.forget_corepresentable : CategoryTheory.Functor.Corepresentable (CategoryTheory.forget AddGroupCat)

Equations

• AddGroupCat.forget_corepresentable = ⋯

instance AddCommGroupCat.forget_corepresentable : CategoryTheory.Functor.Corepresentable (CategoryTheory.forget AddCommGroupCat)

Equations

• AddCommGroupCat.forget_corepresentable = ⋯