Documentation

Mathlib.Algebra.Category.Grp.ForgetCorepresentable

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.

@[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.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.fromMultiplicativeIntEquiv_apply (α : Type u) [Group α] (φ : Multiplicative →* α) :
(MonoidHom.fromMultiplicativeIntEquiv α) φ = φ (Multiplicative.ofAdd 1)

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

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

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

Equations
@[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.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
@[simp]
theorem AddMonoidHom.fromIntEquiv_apply (α : Type u) [AddGroup α] (φ : →+ α) :
@[simp]
def AddMonoidHom.fromIntEquiv (α : Type u) [AddGroup α] :
( →+ α) α

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

Equations
@[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_1 : ULift.{u, 0} ), ((AddMonoidHom.fromULiftIntEquiv α).symm a) a_1 = AddEquiv.ulift a_1 a

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

Equations