Mathlib.Algebra.Module.NatInt

Module docstring

{"# Modules over ℕ and ℤ

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

Main definitions

AddCommGroup.toNatModule: any AddCommMonoid is (uniquely) a module over the naturals. TODO: this name is not right!
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 "}

AddCommGroup.toNatModule instance

: Module ℕ M

Full source

instance AddCommGroup.toNatModule : Module ℕ M where
  one_smul := one_nsmul
  mul_smul m n a := mul_nsmul' a m n
  smul_add n a b := nsmul_add a b n
  smul_zero := nsmul_zero
  zero_smul := zero_nsmul
  add_smul r s x := add_nsmul x r s

Natural Number Module Structure on Additive Commutative Groups

Informal description

Every additive commutative group $M$ is naturally a module over the natural numbers $\mathbb{N}$, where the scalar multiplication is defined by repeated addition.

AddCommGroup.toIntModule instance

: Module ℤ M

Full source

instance AddCommGroup.toIntModule : Module ℤ M where
  one_smul := one_zsmul
  mul_smul m n a := mul_zsmul a m n
  smul_add n a b := zsmul_add a b n
  smul_zero := zsmul_zero
  zero_smul := zero_zsmul
  add_smul r s x := add_zsmul x r s

Additive Commutative Groups as $\mathbb{Z}$-Modules

Informal description

Every additive commutative group $M$ is canonically a $\mathbb{Z}$-module, where the scalar multiplication is given by the group's addition structure.

Module.addCommMonoidToAddCommGroup abbrev

[Ring R] [AddCommMonoid M] [Module R M] : AddCommGroup M

Full source

/-- An `AddCommMonoid` that is a `Module` over a `Ring` carries a natural `AddCommGroup`
structure.
See note [reducible non-instances]. -/
abbrev Module.addCommMonoidToAddCommGroup
    [Ring R] [AddCommMonoid M] [Module R M] : AddCommGroup M :=
  { (inferInstance : AddCommMonoid M) with
    neg := fun a => (-1 : R) • a
    neg_add_cancel := fun a =>
      show (-1 : R) • a + a = 0 by
        nth_rw 2 [← one_smul R a]
        rw [← add_smul, neg_add_cancel, zero_smul]
    zsmul := fun z a => (z : R) • a
    zsmul_zero' := fun a => by simpa only [Int.cast_zero] using zero_smul R a
    zsmul_succ' := fun z a => by simp [add_comm, add_smul]
    zsmul_neg' := fun z a => by simp [← smul_assoc, neg_one_smul] }

Additive Commutative Group Structure Induced by Module over a Ring

Informal description

Given a ring $R$, an additive commutative monoid $M$, and a module structure of $M$ over $R$, the monoid $M$ naturally carries the structure of an additive commutative group.

Nat.cast_smul_eq_nsmul theorem

(n : ℕ) (b : M) : (n : R) • b = n • b

Full source

/-- `nsmul` is equal to any other module structure via a cast. -/
@[norm_cast]
lemma Nat.cast_smul_eq_nsmul (n : ℕ) (b : M) : (n : R) • b = n • b := by
  induction n with
  | zero => rw [Nat.cast_zero, zero_smul, zero_smul]
  | succ n ih => rw [Nat.cast_succ, add_smul, add_smul, one_smul, ih, one_smul]

Natural Number Scalar Multiplication via Cast: $(n : R) \cdot b = n \cdot b$

Informal description

For any natural number $n$ and any element $b$ in an additive commutative monoid $M$ with a module structure over a ring $R$, the scalar multiplication of $n$ (viewed as an element of $R$) with $b$ is equal to the $n$-fold addition of $b$, i.e., $(n : R) \cdot b = n \cdot b$.

ofNat_smul_eq_nsmul theorem

(n : ℕ) [n.AtLeastTwo] (b : M) : (ofNat(n) : R) • b = ofNat(n) • b

Full source

/-- `nsmul` is equal to any other module structure via a cast. -/
lemma ofNat_smul_eq_nsmul (n : ℕ) [n.AtLeastTwo] (b : M) :
    (ofNat(n) : R) • b = ofNat(n) • b := Nat.cast_smul_eq_nsmul ..

Scalar Multiplication of Numerals via Cast Equals Repeated Addition

Informal description

For any natural number $n \geq 2$ and any element $b$ in an additive commutative monoid $M$ with a module structure over a ring $R$, the scalar multiplication of the numeral $n$ (interpreted in $R$) with $b$ is equal to the $n$-fold addition of $b$, i.e., $(n : R) \cdot b = n \cdot b$.

nat_smul_eq_nsmul theorem

(h : Module ℕ M) (n : ℕ) (x : M) : @SMul.smul ℕ M h.toSMul n x = n • x

Full source

/-- Convert back any exotic `ℕ`-smul to the canonical instance. This should not be needed since in
mathlib all `AddCommMonoid`s should normally have exactly one `ℕ`-module structure by design.
-/
theorem nat_smul_eq_nsmul (h : Module ℕ M) (n : ℕ) (x : M) : @SMul.smul ℕ M h.toSMul n x = n • x :=
  Nat.cast_smul_eq_nsmul ..

Natural Number Scalar Multiplication Equals Repeated Addition in $\mathbb{N}$-Modules

Informal description

For any $\mathbb{N}$-module structure $h$ on an additive commutative monoid $M$, the scalar multiplication of a natural number $n$ and an element $x \in M$ under $h$ is equal to the $n$-fold addition of $x$, i.e., $n \cdot x = n \bullet x$.

AddCommMonoid.uniqueNatModule definition

: Unique (Module ℕ M)

Full source

/-- All `ℕ`-module structures are equal. Not an instance since in mathlib all `AddCommMonoid`
should normally have exactly one `ℕ`-module structure by design. -/
def AddCommMonoid.uniqueNatModule : Unique (Module ℕ M) where
  default := by infer_instance
  uniq P := (Module.ext' P _) fun n => by convert nat_smul_eq_nsmul P n

Uniqueness of natural number module structure on additive commutative monoids

Informal description

For any additive commutative monoid $M$, there is a unique $\mathbb{N}$-module structure on $M$ where the scalar multiplication is given by repeated addition.

AddCommMonoid.nat_isScalarTower instance

: IsScalarTower ℕ R M

Full source

instance AddCommMonoid.nat_isScalarTower : IsScalarTower ℕ R M where
  smul_assoc n x y := by
    induction n with
    | zero => simp only [zero_smul]
    | succ n ih => simp only [add_smul, one_smul, ih]

Natural Number Scalar Multiplication Tower Property for Additive Commutative Monoids

Informal description

For any additive commutative monoid $M$ and any semiring $R$ acting on $M$, the scalar multiplication operations of $\mathbb{N}$ on $R$ and $R$ on $M$ form a scalar tower with $\mathbb{N}$ acting on $M$. That is, for any $n \in \mathbb{N}$, $r \in R$, and $m \in M$, we have $(n \cdot r) \cdot m = n \cdot (r \cdot m)$.

map_natCast_smul theorem

 [AddCommMonoid M] [AddCommMonoid M₂] {F : Type*} [FunLike F M M₂] [AddMonoidHomClass F M M₂] (f : F) (R S : Type*)
  [Semiring R] [Semiring S] [Module R M] [Module S M₂] (x : ℕ) (a : M) : f ((x : R) • a) = (x : S) • f a

Full source

theorem map_natCast_smul [AddCommMonoid M] [AddCommMonoid M₂] {F : Type*} [FunLike F M M₂]
    [AddMonoidHomClass F M M₂] (f : F) (R S : Type*) [Semiring R] [Semiring S] [Module R M]
    [Module S M₂] (x : ℕ) (a : M) : f ((x : R) • a) = (x : S) • f a := by
  simp only [Nat.cast_smul_eq_nsmul, AddMonoidHom.map_nsmul, map_nsmul]

Natural Number Scalar Multiplication Commutes with Additive Monoid Homomorphisms

Informal description

Let $M$ and $M_2$ be additive commutative monoids, and let $F$ be a type of functions from $M$ to $M_2$ that are additive monoid homomorphisms. For any semirings $R$ and $S$ with module structures on $M$ and $M_2$ respectively, any natural number $x$, and any element $a \in M$, we have that the homomorphism $f$ commutes with scalar multiplication via the natural number embedding: \[ f((x : R) \cdot a) = (x : S) \cdot f(a). \]

Nat.smul_one_eq_cast theorem

{R : Type*} [NonAssocSemiring R] (m : ℕ) : m • (1 : R) = ↑m

Full source

theorem Nat.smul_one_eq_cast {R : Type*} [NonAssocSemiring R] (m : ℕ) : m • (1 : R) = ↑m := by
  rw [nsmul_eq_mul, mul_one]

Scalar Multiplication of One Equals Natural Number Embedding in Non-Associative Semiring

Informal description

For any natural number $m$ and any element $1$ in a non-associative semiring $R$, the scalar multiplication $m \cdot 1$ equals the canonical embedding of $m$ into $R$, i.e., $m \cdot 1 = m$.

Int.smul_one_eq_cast theorem

{R : Type*} [NonAssocRing R] (m : ℤ) : m • (1 : R) = ↑m

Full source

theorem Int.smul_one_eq_cast {R : Type*} [NonAssocRing R] (m : ℤ) : m • (1 : R) = ↑m := by
  rw [zsmul_eq_mul, mul_one]

Scalar Multiplication of One Equals Integer Embedding in Non-Associative Ring

Informal description

For any integer $m$ and any element $1$ in a non-associative ring $R$, the scalar multiplication $m \cdot 1$ equals the canonical embedding of $m$ into $R$, i.e., $m \cdot 1 = m$.