Modules over a ring

In this file we define

• Module R M : an additive commutative monoid M is a Module over a Semiring R if for r : R and x : M their "scalar multiplication" r • x : M is defined, and the operation • satisfies some natural associativity and distributivity axioms similar to those on a ring.

Implementation notes

In typical mathematical usage, our definition of Module corresponds to "semimodule", and the word "module" is reserved for Module R M where R is a Ring and M an AddCommGroup. If R is a Field and M an AddCommGroup, M would be called an R-vector space. Since those assumptions can be made by changing the typeclasses applied to R and M, without changing the axioms in Module, mathlib calls everything a Module.

In older versions of mathlib3, we had separate abbreviations for semimodules and vector spaces. This caused inference issues in some cases, while not providing any real advantages, so we decided to use a canonical Module typeclass throughout.

Tags

semimodule, module, vector space

theorem Module.ext_iff {R : Type u} {M : Type v} : ∀ {inst : Semiring R} {inst_1 : AddCommMonoid M} {x y : Module R M}, x = y ↔ SMul.smul = SMul.smul

theorem Module.ext {R : Type u} {M : Type v} : ∀ {inst : Semiring R} {inst_1 : AddCommMonoid M} {x y : Module R M}, SMul.smul = SMul.smul → x = y

class Module (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] extends DistribMulAction : Type (max u v)

A module is a generalization of vector spaces to a scalar semiring. It consists of a scalar semiring R and an additive monoid of "vectors" M, connected by a "scalar multiplication" operation r • x : M (where r : R and x : M) with some natural associativity and distributivity axioms similar to those on a ring.

• smul : R → M → M
• one_smul : ∀ (b : M), 1 • b = b
• mul_smul : ∀ (x y : R) (b : M), (x * y) • b = x • y • b
• smul_zero : ∀ (a : R), a • 0 = 0
• smul_add : ∀ (a : R) (x y : M), a • (x + y) = a • x + a • y
• add_smul : ∀ (r s : R) (x : M), (r + s) • x = r • x + s • x

  Scalar multiplication distributes over addition from the right.

• zero_smul : ∀ (x : M), 0 • x = 0

  Scalar multiplication by zero gives zero.

theorem Module.add_smul {R : Type u} {M : Type v} : ∀ {inst : Semiring R} {inst_1 : AddCommMonoid M} [self : Module R M] (r s : R) (x : M), (r + s) • x = r • x + s • x

Scalar multiplication distributes over addition from the right.

theorem Module.zero_smul {R : Type u} {M : Type v} : ∀ {inst : Semiring R} {inst_1 : AddCommMonoid M} [self : Module R M] (x : M), 0 • x = 0

Scalar multiplication by zero gives zero.

@[instance 100]

instance Module.toMulActionWithZero {R : Type u_5} {M : Type u_6} : {x : Semiring R} → {x_1 : AddCommMonoid M} → [inst : Module R M] → MulActionWithZero R M

A module over a semiring automatically inherits a MulActionWithZero structure.

Equations

• Module.toMulActionWithZero = MulActionWithZero.mk ⋯ ⋯

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

Equations

• AddCommGroup.toNatModule = Module.mk ⋯ ⋯

theorem add_smul {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] (r : R) (s : R) (x : M) : (r + s) • x = r • x + s • x

theorem Convex.combo_self {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {a : R} {b : R} (h : a + b = 1) (x : M) : a • x + b • x = x

theorem two_smul (R : Type u_1) {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] (x : M) : 2 • x = x + x

@[reducible, inline]

abbrev Function.Injective.module (R : Type u_1) {M : Type u_3} {M₂ : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M₂] [SMul R M₂] (f : M₂ →+ M) (hf : Function.Injective ⇑f) (smul : ∀ (c : R) (x : M₂), f (c • x) = c • f x) : Module R M₂

Pullback a Module structure along an injective additive monoid homomorphism. See note [reducible non-instances].

Equations

• Function.Injective.module R f hf smul = Module.mk ⋯ ⋯

@[reducible, inline]

abbrev Function.Surjective.module (R : Type u_1) {M : Type u_3} {M₂ : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M₂] [SMul R M₂] (f : M →+ M₂) (hf : Function.Surjective ⇑f) (smul : ∀ (c : R) (x : M), f (c • x) = c • f x) : Module R M₂

Pushforward a Module structure along a surjective additive monoid homomorphism. See note [reducible non-instances].

Equations

• Function.Surjective.module R f hf smul = Module.mk ⋯ ⋯

@[reducible, inline]

abbrev Function.Surjective.moduleLeft {R : Type u_5} {S : Type u_6} {M : Type u_7} [Semiring R] [AddCommMonoid M] [Module R M] [Semiring S] [SMul S M] (f : R →+* S) (hf : Function.Surjective ⇑f) (hsmul : ∀ (c : R) (x : M), f c • x = c • x) : Module S M

Push forward the action of R on M along a compatible surjective map f : R →+* S.

See also Function.Surjective.mulActionLeft and Function.Surjective.distribMulActionLeft.

Equations

• Function.Surjective.moduleLeft f hf hsmul = Module.mk ⋯ ⋯

@[reducible, inline]

abbrev Module.compHom {R : Type u_1} {S : Type u_2} (M : Type u_3) [Semiring R] [AddCommMonoid M] [Module R M] [Semiring S] (f : S →+* R) : Module S M

Compose a Module with a RingHom, with action f s • m.

See note [reducible non-instances].

Equations

• Module.compHom M f = Module.mk ⋯ ⋯

theorem Module.eq_zero_of_zero_eq_one {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] (x : M) (zero_eq_one : 0 = 1) : x = 0

@[simp]

theorem smul_add_one_sub_smul {M : Type u_3} [AddCommMonoid M] {R : Type u_5} [Ring R] [Module R M] {r : R} {m : M} : r • m + (1 - r) • m = m

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

Equations

• AddCommGroup.toIntModule M = Module.mk ⋯ ⋯

theorem Convex.combo_eq_smul_sub_add {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommGroup M] [Module R M] {x : M} {y : M} {a : R} {b : R} (h : a + b = 1) : a • x + b • y = b • (y - x) + x

theorem Module.ext' {R : Type u_5} [Semiring R] {M : Type u_6} [AddCommMonoid M] (P : Module R M) (Q : Module R M) (w : ∀ (r : R) (m : M), r • m = r • m) : P = Q

A variant of Module.ext that's convenient for term-mode.

@[simp]

theorem neg_smul {R : Type u_1} {M : Type u_3} [Ring R] [AddCommGroup M] [Module R M] (r : R) (x : M) : -r • x = -(r • x)

theorem neg_smul_neg {R : Type u_1} {M : Type u_3} [Ring R] [AddCommGroup M] [Module R M] (r : R) (x : M) : -r • -x = r • x

@[simp]

theorem Units.neg_smul {R : Type u_1} {M : Type u_3} [Ring R] [AddCommGroup M] [Module R M] (u : Rˣ) (x : M) : -u • x = -(u • x)

theorem neg_one_smul (R : Type u_1) {M : Type u_3} [Ring R] [AddCommGroup M] [Module R M] (x : M) : -1 • x = -x

theorem sub_smul {R : Type u_1} {M : Type u_3} [Ring R] [AddCommGroup M] [Module R M] (r : R) (s : R) (y : M) : (r - s) • y = r • y - s • y

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

• Module.addCommMonoidToAddCommGroup R = AddCommGroup.mk ⋯

theorem Module.subsingleton (R : Type u_5) (M : Type u_6) [Semiring R] [Subsingleton R] [AddCommMonoid M] [Module R M] : Subsingleton M

A module over a Subsingleton semiring is a Subsingleton. We cannot register this as an instance because Lean has no way to guess R.

theorem Module.nontrivial (R : Type u_5) (M : Type u_6) [Semiring R] [Nontrivial M] [AddCommMonoid M] [Module R M] : Nontrivial R

A semiring is Nontrivial provided that there exists a nontrivial module over this semiring.

@[instance 910]

instance Semiring.toModule {R : Type u_1} [Semiring R] : Module R R

Equations

• Semiring.toModule = Module.mk ⋯ ⋯

def RingHom.toModule {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] (f : R →+* S) : Module R S

A ring homomorphism f : R →+* M defines a module structure by r • x = f r * x.

Equations

• f.toModule = Module.compHom S f

@[simp]

theorem RingHom.smulOneHom_apply {R : Type u_1} {S : Type u_2} [Semiring R] [NonAssocSemiring S] [Module R S] [IsScalarTower R S S] (x : R) : RingHom.smulOneHom x = x • 1

def RingHom.smulOneHom {R : Type u_1} {S : Type u_2} [Semiring R] [NonAssocSemiring S] [Module R S] [IsScalarTower R S S] : R →+* S

If the module action of R on S is compatible with multiplication on S, then fun x ↦ x • 1 is a ring homomorphism from R to S.

This is the RingHom version of MonoidHom.smulOneHom.

When R is commutative, usually algebraMap should be preferred.

Equations

• RingHom.smulOneHom = { toMonoidHom := MonoidHom.smulOneHom, map_zero' := ⋯, map_add' := ⋯ }

def ringHomEquivModuleIsScalarTower {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] : (R →+* S) ≃ { _inst : Module R S // IsScalarTower R S S }

A homomorphism between semirings R and S can be equivalently specified by a R-module structure on S such that S/S/R is a scalar tower.

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.

@[deprecated Nat.cast_smul_eq_nsmul]

theorem nsmul_eq_smul_cast (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 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.nat_isScalarTower {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] : IsScalarTower ℕ R M

Equations

• ⋯ = ⋯

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

@[deprecated Nat.smul_one_eq_cast]

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

Alias of Nat.smul_one_eq_cast.

@[deprecated Int.smul_one_eq_cast]

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

Alias of Int.smul_one_eq_cast.