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 a unique AddCommMonoid ℕ M structure for any M

Tags

semimodule, module, vector space

instance instMulActionNatOfAddMonoid {M : Type u_3} [AddMonoid M] : MulAction ℕ M

instance instSMulWithZeroNat {M : Type u_3} [AddMonoid M] : SMulWithZero ℕ M

instance instMulActionIntOfSubtractionMonoid {M : Type u_3} [SubtractionMonoid M] : MulAction ℤ M

instance instSMulWithZeroInt {M : Type u_3} [SubtractionMonoid M] : SMulWithZero ℤ M

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

theorem DistribSMul.toAddMonoidHom_eq_nsmulAddMonoidHom {M : Type u_3} [AddCommMonoid M] : toAddMonoidHom M = nsmulAddMonoidHom

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

theorem DistribSMul.toAddMonoidHom_eq_zsmulAddGroupHom (M : Type u_3) [AddCommGroup M] : toAddMonoidHom M = zsmulAddGroupHom

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

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.

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.

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

theorem CharZero.of_module {R : Type u_1} (M : Type u_3) [Semiring R] [AddCommMonoidWithOne M] [CharZero M] [Module R M] : CharZero R

If M is an R-module with one and M has characteristic zero, then R has characteristic zero as well. Usually M is an R-algebra.