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

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.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

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 AddMonoid.End.natCast_def {M : Type u_3} [AddCommMonoid M] (n : ℕ) : ↑n = (DistribMulAction.toAddMonoidEnd ℕ M) n

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

@[simp]

theorem invOf_two_smul_add_invOf_two_smul (R : Type u_1) {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [Invertible 2] (x : M) : ⅟2 • x + ⅟2 • 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 ⋯ ⋯

def Module.toAddMonoidEnd (R : Type u_1) (M : Type u_3) [Semiring R] [AddCommMonoid M] [Module R M] : R →+* AddMonoid.End M

(•) as an AddMonoidHom.

This is a stronger version of DistribMulAction.toAddMonoidEnd

Equations

• Module.toAddMonoidEnd R M = { toMonoidHom := DistribMulAction.toAddMonoidEnd R M, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem Module.toAddMonoidEnd_apply_apply (R : Type u_1) (M : Type u_3) [Semiring R] [AddCommMonoid M] [Module R M] (x : R) : ∀ (x2 : M), ((Module.toAddMonoidEnd R M) x) x2 = x • x2

def smulAddHom (R : Type u_1) (M : Type u_3) [Semiring R] [AddCommMonoid M] [Module R M] : R →+ M →+ M

A convenience alias for Module.toAddMonoidEnd as an AddMonoidHom, usually to allow the use of AddMonoidHom.flip.

Equations

• smulAddHom R M = (Module.toAddMonoidEnd R M).toAddMonoidHom

@[simp]

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

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 AddMonoid.End.intCast_def (M : Type u_3) [AddCommGroup M] (z : ℤ) : ↑z = (DistribMulAction.toAddMonoidEnd ℤ M) z

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 ⋯ ⋯

@[instance 910]

instance Semiring.toOppositeModule {R : Type u_1} [Semiring R] : Module Rᵐᵒᵖ R

Like Semiring.toModule, but multiplies on the right.

Equations

• Semiring.toOppositeModule = 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

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' := ⋯ }

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

@[deprecated Int.cast_smul_eq_zsmul]

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

Alias of Int.cast_smul_eq_zsmul.

---

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

@[deprecated Int.cast_smul_eq_zsmul]

theorem zsmul_eq_smul_cast (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 := ⋯ }

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

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

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

Equations

• ⋯ = ⋯

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.