Extensionality of monoid homs from ℕ

theorem ext_nat' {A : Type u_3} {F : Type u_5} [FunLike F ℕ A] [AddMonoid A] [AddMonoidHomClass F ℕ A] (f g : F) (h : f 1 = g 1) : f = g

theorem AddMonoidHom.ext_nat {A : Type u_3} [AddMonoid A] {f g : ℕ →+ A} : f 1 = g 1 → f = g

def multiplesHom (M : Type u_2) [AddMonoid M] : M ≃ (ℕ →+ M)

Additive homomorphisms from ℕ are defined by the image of 1.

Equations

• multiplesHom M = { toFun := fun (x : M) => { toFun := fun (n : ℕ) => n • x, map_zero' := ⋯, map_add' := ⋯ }, invFun := fun (f : ℕ →+ M) => f 1, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem multiplesHom_apply {M : Type u_2} [AddMonoid M] (x : M) (n : ℕ) : ((multiplesHom M) x) n = n • x

@[simp]

theorem multiplesHom_symm_apply {M : Type u_2} [AddMonoid M] (f : ℕ →+ M) : (multiplesHom M).symm f = f 1

theorem AddMonoidHom.apply_nat {M : Type u_2} [AddMonoid M] (f : ℕ →+ M) (n : ℕ) : f n = n • f 1

def powersHom (M : Type u_2) [Monoid M] : M ≃ (Multiplicative ℕ →* M)

Monoid homomorphisms from Multiplicative ℕ are defined by the image of Multiplicative.ofAdd 1.

Equations

• powersHom M = Additive.ofMul.trans ((multiplesHom (Additive M)).trans AddMonoidHom.toMultiplicative'')

@[simp]

theorem powersHom_apply {M : Type u_2} [Monoid M] (x : M) (n : Multiplicative ℕ) : ((powersHom M) x) n = x ^ Multiplicative.toAdd n

@[simp]

theorem powersHom_symm_apply {M : Type u_2} [Monoid M] (f : Multiplicative ℕ →* M) : (powersHom M).symm f = f (Multiplicative.ofAdd 1)

theorem MonoidHom.apply_mnat {M : Type u_2} [Monoid M] (f : Multiplicative ℕ →* M) (n : Multiplicative ℕ) : f n = f (Multiplicative.ofAdd 1) ^ Multiplicative.toAdd n

theorem MonoidHom.ext_mnat {M : Type u_2} [Monoid M] ⦃f g : Multiplicative ℕ →* M⦄ (h : f (Multiplicative.ofAdd 1) = g (Multiplicative.ofAdd 1)) : f = g

def multiplesAddHom (M : Type u_2) [AddCommMonoid M] : M ≃+ (ℕ →+ M)

If M is commutative, multiplesHom is an additive equivalence.

Equations

• multiplesAddHom M = { toEquiv := multiplesHom M, map_add' := ⋯ }

@[simp]

theorem multiplesAddHom_apply {M : Type u_2} [AddCommMonoid M] (x : M) (n : ℕ) : ((multiplesAddHom M) x) n = n • x

@[simp]

theorem multiplesAddHom_symm_apply {M : Type u_2} [AddCommMonoid M] (f : ℕ →+ M) : (multiplesAddHom M).symm f = f 1

def powersMulHom (M : Type u_2) [CommMonoid M] : M ≃* (Multiplicative ℕ →* M)

If M is commutative, powersHom is a multiplicative equivalence.

Equations

• powersMulHom M = { toEquiv := powersHom M, map_mul' := ⋯ }

@[simp]

theorem powersMulHom_apply {M : Type u_2} [CommMonoid M] (x : M) (n : Multiplicative ℕ) : ((powersMulHom M) x) n = x ^ Multiplicative.toAdd n

@[simp]

theorem powersMulHom_symm_apply {M : Type u_2} [CommMonoid M] (f : Multiplicative ℕ →* M) : (powersMulHom M).symm f = f (Multiplicative.ofAdd 1)