Modules over ℕ and ℤ

This file concerns modules where the scalars are the natural numbers or the integers.

Main definitions

• AddCommMonoid.toNatModule: any AddCommMonoid is (uniquely) a module over the naturals.
• AddCommGroup.toIntModule: any AddCommGroup is a module over the integers.

Main results

• AddCommMonoid.uniqueNatModule: there is an unique AddCommMonoid ℕ M structure for any M

Tags

semimodule, module, vector space

instance AddCommMonoid.toNatModule {M : Type u_3} [AddCommMonoid M] : Module ℕ M

Equations

• AddCommMonoid.toNatModule = { toSMul := AddMonoid.toNatSMul, one_smul := ⋯, mul_smul := ⋯, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯ }

instance AddCommGroup.toIntModule (M : Type u_3) [AddCommGroup M] : Module ℤ M

Equations

• AddCommGroup.toIntModule M = { toSMul := SubNegMonoid.toZSMul, one_smul := ⋯, mul_smul := ⋯, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯ }

@[reducible, inline]

abbrev Module.addCommMonoidToAddCommGroup (R : Type u_1) {M : Type u_3} [Ring R] [AddCommMonoid M] [Module R M] : AddCommGroup M

An AddCommMonoid that is a Module over a Ring carries a natural AddCommGroup structure. See note [reducible non-instances].

Equations

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

theorem Nat.cast_smul_eq_nsmul (R : Type u_1) {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] (n : ℕ) (b : M) : ↑n • b = n • b

nsmul is equal to any other module structure via a cast.

theorem ofNat_smul_eq_nsmul (R : Type u_1) {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] (n : ℕ) [n.AtLeastTwo] (b : M) : OfNat.ofNat n • b = OfNat.ofNat n • b

nsmul is equal to any other module structure via a cast.

theorem nat_smul_eq_nsmul {M : Type u_3} [AddCommMonoid M] (h : Module ℕ M) (n : ℕ) (x : M) : SMul.smul n x = n • x

Convert back any exotic ℕ-smul to the canonical instance. This should not be needed since in mathlib all AddCommMonoids should normally have exactly one ℕ-module structure by design.

def AddCommMonoid.uniqueNatModule {M : Type u_3} [AddCommMonoid M] : Unique (Module ℕ M)

All ℕ-module structures are equal. Not an instance since in mathlib all AddCommMonoid should normally have exactly one ℕ-module structure by design.

Equations

• AddCommMonoid.uniqueNatModule = { default := inferInstance, uniq := ⋯ }

instance AddCommMonoid.subsingletonNatModule {M : Type u_3} [AddCommMonoid M] : Subsingleton (Module ℕ M)

All ℕ-module structures are equal. See also AddCommMoniod.uniqueNatModule.

instance AddCommMonoid.nat_isScalarTower {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] : IsScalarTower ℕ R M

theorem map_natCast_smul {M : Type u_3} {M₂ : Type u_4} [AddCommMonoid M] [AddCommMonoid M₂] {F : Type u_5} [FunLike F M M₂] [AddMonoidHomClass F M M₂] (f : F) (R : Type u_6) (S : Type u_7) [Semiring R] [Semiring S] [Module R M] [Module S M₂] (x : ℕ) (a : M) : f (↑x • a) = ↑x • f a

theorem Nat.smul_one_eq_cast {R : Type u_5} [NonAssocSemiring R] (m : ℕ) : m • 1 = ↑m

theorem Int.smul_one_eq_cast {R : Type u_5} [NonAssocRing R] (m : ℤ) : m • 1 = ↑m

theorem Int.cast_smul_eq_zsmul (R : Type u_1) {M : Type u_3} [Ring R] [AddCommGroup M] [Module R M] (n : ℤ) (b : M) : ↑n • b = n • b

zsmul is equal to any other module structure via a cast.

theorem int_smul_eq_zsmul {M : Type u_3} [AddCommGroup M] (h : Module ℤ M) (n : ℤ) (x : M) : SMul.smul n x = n • x

Convert back any exotic ℤ-smul to the canonical instance. This should not be needed since in mathlib all AddCommGroups should normally have exactly one ℤ-module structure by design.

def AddCommGroup.uniqueIntModule {M : Type u_3} [AddCommGroup M] : Unique (Module ℤ M)

All ℤ-module structures are equal. Not an instance since in mathlib all AddCommGroup should normally have exactly one ℤ-module structure by design.

Equations

• AddCommGroup.uniqueIntModule = { default := inferInstance, uniq := ⋯ }

instance AddCommMonoid.subsingletonIntModule {M : Type u_3} [AddCommMonoid M] : Subsingleton (Module ℤ M)

All ℤ-module structures are equal. See also AddCommGroup.uniqueIntModule.

theorem map_intCast_smul {M : Type u_3} {M₂ : Type u_4} [AddCommGroup M] [AddCommGroup M₂] {F : Type u_5} [FunLike F M M₂] [AddMonoidHomClass F M M₂] (f : F) (R : Type u_6) (S : Type u_7) [Ring R] [Ring S] [Module R M] [Module S M₂] (x : ℤ) (a : M) : f (↑x • a) = ↑x • f a

instance AddCommGroup.intIsScalarTower {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] : IsScalarTower ℤ R M