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.

instance Module.toMulActionWithZero {R : Type u_2} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] : MulActionWithZero R M

A module over a semiring automatically inherits a MulActionWithZero structure.

Equations

• Module.toMulActionWithZero = let __src := inferInstance; MulActionWithZero.mk ⋯ ⋯

instance AddCommMonoid.natModule {M : Type u_5} [AddCommMonoid M] : Module ℕ M

Equations

• AddCommMonoid.natModule = Module.mk ⋯ ⋯

theorem AddMonoid.End.natCast_def {M : Type u_5} [AddCommMonoid M] (n : ℕ) : ↑n = (DistribMulAction.toAddMonoidEnd ℕ M) n

theorem add_smul {R : Type u_2} {M : Type u_5} [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_2} {M : Type u_5} [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_2) {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (x : M) : 2 • x = x + x

@[deprecated]

theorem two_smul' (R : Type u_2) {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (x : M) : 2 • x = bit0 x

@[simp]

theorem invOf_two_smul_add_invOf_two_smul (R : Type u_2) {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [Invertible 2] (x : M) : ⅟2 • x + ⅟2 • x = x

@[reducible]

def Function.Injective.module (R : Type u_2) {M : Type u_5} {M₂ : Type u_6} [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 = let __src := Function.Injective.distribMulAction f hf smul; Module.mk ⋯ ⋯

@[reducible]

def Function.Surjective.module (R : Type u_2) {M : Type u_5} {M₂ : Type u_6} [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]

def Function.Surjective.moduleLeft {R : Type u_9} {S : Type u_10} {M : Type u_11} [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 = let __src := Function.Surjective.distribMulActionLeft (↑f) hf hsmul; Module.mk ⋯ ⋯

@[reducible]

def Module.compHom {R : Type u_2} {S : Type u_4} (M : Type u_5) [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 = let __src := MulActionWithZero.compHom M (RingHom.toMonoidWithZeroHom f); let __src_1 := DistribMulAction.compHom M ↑f; Module.mk ⋯ ⋯

@[simp]

theorem Module.toAddMonoidEnd_apply_apply (R : Type u_2) (M : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] (x : R) : ∀ (x_1 : M), ((Module.toAddMonoidEnd R M) x) x_1 = x • x_1

def Module.toAddMonoidEnd (R : Type u_2) (M : Type u_5) [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 = let __src := DistribMulAction.toAddMonoidEnd R M; { toMonoidHom := __src, map_zero' := ⋯, map_add' := ⋯ }

def smulAddHom (R : Type u_2) (M : Type u_5) [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 = RingHom.toAddMonoidHom (Module.toAddMonoidEnd R M)

@[simp]

theorem smulAddHom_apply {R : Type u_2} {M : Type u_5} [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_2} {M : Type u_5} [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_5} [AddCommMonoid M] {R : Type u_9} [Ring R] [Module R M] {r : R} {m : M} : r • m + (1 - r) • m = m

instance AddCommGroup.intModule (M : Type u_5) [AddCommGroup M] : Module ℤ M

Equations

• AddCommGroup.intModule M = Module.mk ⋯ ⋯

theorem AddMonoid.End.intCast_def (M : Type u_5) [AddCommGroup M] (z : ℤ) : ↑z = (DistribMulAction.toAddMonoidEnd ℤ M) z

theorem Convex.combo_eq_smul_sub_add {R : Type u_2} {M : Type u_5} [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_9} [Semiring R] {M : Type u_10} [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_2} {M : Type u_5} [Ring R] [AddCommGroup M] [Module R M] (r : R) (x : M) : -r • x = -(r • x)

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

@[simp]

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

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

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

@[reducible]

def Module.addCommMonoidToAddCommGroup (R : Type u_2) {M : Type u_5} [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 = let __src := inferInstance; AddCommGroup.mk ⋯

theorem Module.subsingleton (R : Type u_9) (M : Type u_10) [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_9) (M : Type u_10) [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 Semiring.toModule {R : Type u_2} [Semiring R] : Module R R

Equations

• Semiring.toModule = Module.mk ⋯ ⋯

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

Like Semiring.toModule, but multiplies on the right.

Equations

• Semiring.toOppositeModule = let __src := MonoidWithZero.toOppositeMulActionWithZero R; Module.mk ⋯ ⋯

def RingHom.toModule {R : Type u_2} {S : Type u_4} [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

• RingHom.toModule f = Module.compHom S f

@[simp]

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

def RingHom.smulOneHom {R : Type u_2} {S : Type u_4} [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 = let __spread.0 := MonoidHom.smulOneHom; { toMonoidHom := __spread.0, map_zero' := ⋯, map_add' := ⋯ }

def ringHomEquivModuleIsScalarTower {R : Type u_2} {S : Type u_4} [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 nsmul_eq_smul_cast (R : Type u_2) {M : Type u_5} [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_5} [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.natModule.unique {M : Type u_5} [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.natModule.unique = { toInhabited := { default := inferInstance }, uniq := ⋯ }

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

Equations

• ⋯ = ⋯

theorem zsmul_eq_smul_cast (R : Type u_2) {M : Type u_5} [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_5} [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.intModule.unique {M : Type u_5} [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.intModule.unique = { toInhabited := { default := inferInstance }, uniq := ⋯ }

theorem map_intCast_smul {M : Type u_5} {M₂ : Type u_6} [AddCommGroup M] [AddCommGroup M₂] {F : Type u_9} [FunLike F M M₂] [AddMonoidHomClass F M M₂] (f : F) (R : Type u_10) (S : Type u_11) [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_5} {M₂ : Type u_6} [AddCommMonoid M] [AddCommMonoid M₂] {F : Type u_9} [FunLike F M M₂] [AddMonoidHomClass F M M₂] (f : F) (R : Type u_10) (S : Type u_11) [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

• ⋯ = ⋯

NoZeroSMulDivisors

This section defines the NoZeroSMulDivisors class, and includes some tests for the vanishing of elements (especially in modules over division rings).

theorem noZeroSMulDivisors_iff (R : Type u_9) (M : Type u_10) [Zero R] [Zero M] [SMul R M] : NoZeroSMulDivisors R M ↔ ∀ {c : R} {x : M}, c • x = 0 → c = 0 ∨ x = 0

class NoZeroSMulDivisors (R : Type u_9) (M : Type u_10) [Zero R] [Zero M] [SMul R M] : Prop

NoZeroSMulDivisors R M states that a scalar multiple is 0 only if either argument is 0. This is a version of saying that M is torsion free, without assuming R is zero-divisor free.

The main application of NoZeroSMulDivisors R M, when M is a module, is the result smul_eq_zero: a scalar multiple is 0 iff either argument is 0.

It is a generalization of the NoZeroDivisors class to heterogeneous multiplication.

• eq_zero_or_eq_zero_of_smul_eq_zero : ∀ {c : R} {x : M}, c • x = 0 → c = 0 ∨ x = 0

  If scalar multiplication yields zero, either the scalar or the vector was zero.

theorem Function.Injective.noZeroSMulDivisors {R : Type u_9} {M : Type u_10} {N : Type u_11} [Zero R] [Zero M] [Zero N] [SMul R M] [SMul R N] [NoZeroSMulDivisors R N] (f : M → N) (hf : Function.Injective f) (h0 : f 0 = 0) (hs : ∀ (c : R) (x : M), f (c • x) = c • f x) : NoZeroSMulDivisors R M

Pullback a NoZeroSMulDivisors instance along an injective function.

instance NoZeroDivisors.toNoZeroSMulDivisors {R : Type u_2} [Zero R] [Mul R] [NoZeroDivisors R] : NoZeroSMulDivisors R R

Equations

• ⋯ = ⋯

theorem smul_ne_zero {R : Type u_2} {M : Type u_5} [Zero R] [Zero M] [SMul R M] [NoZeroSMulDivisors R M] {c : R} {x : M} (hc : c ≠ 0) (hx : x ≠ 0) : c • x ≠ 0

@[simp]

theorem smul_eq_zero {R : Type u_2} {M : Type u_5} [Zero R] [Zero M] [SMulWithZero R M] [NoZeroSMulDivisors R M] {c : R} {x : M} : c • x = 0 ↔ c = 0 ∨ x = 0

theorem smul_ne_zero_iff {R : Type u_2} {M : Type u_5} [Zero R] [Zero M] [SMulWithZero R M] [NoZeroSMulDivisors R M] {c : R} {x : M} : c • x ≠ 0 ↔ c ≠ 0 ∧ x ≠ 0

theorem smul_eq_zero_iff_left {R : Type u_2} {M : Type u_5} [Zero R] [Zero M] [SMulWithZero R M] [NoZeroSMulDivisors R M] {c : R} {x : M} (hx : x ≠ 0) : c • x = 0 ↔ c = 0

theorem smul_eq_zero_iff_right {R : Type u_2} {M : Type u_5} [Zero R] [Zero M] [SMulWithZero R M] [NoZeroSMulDivisors R M] {c : R} {x : M} (hc : c ≠ 0) : c • x = 0 ↔ x = 0

theorem smul_ne_zero_iff_left {R : Type u_2} {M : Type u_5} [Zero R] [Zero M] [SMulWithZero R M] [NoZeroSMulDivisors R M] {c : R} {x : M} (hx : x ≠ 0) : c • x ≠ 0 ↔ c ≠ 0

theorem smul_ne_zero_iff_right {R : Type u_2} {M : Type u_5} [Zero R] [Zero M] [SMulWithZero R M] [NoZeroSMulDivisors R M] {c : R} {x : M} (hc : c ≠ 0) : c • x ≠ 0 ↔ x ≠ 0

theorem Nat.noZeroSMulDivisors (R : Type u_2) (M : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] [NoZeroSMulDivisors R M] [CharZero R] : NoZeroSMulDivisors ℕ M

theorem two_nsmul_eq_zero (R : Type u_2) (M : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] [NoZeroSMulDivisors R M] [CharZero R] {v : M} : 2 • v = 0 ↔ v = 0

theorem CharZero.of_module (R : Type u_2) [Semiring R] (M : Type u_9) [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.

theorem smul_right_injective {R : Type u_2} (M : Type u_5) [Semiring R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] {c : R} (hc : c ≠ 0) : Function.Injective fun (x : M) => c • x

theorem smul_right_inj {R : Type u_2} {M : Type u_5} [Semiring R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] {c : R} (hc : c ≠ 0) {x : M} {y : M} : c • x = c • y ↔ x = y

theorem self_eq_neg (R : Type u_2) (M : Type u_5) [Semiring R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] [CharZero R] {v : M} : v = -v ↔ v = 0

theorem neg_eq_self (R : Type u_2) (M : Type u_5) [Semiring R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] [CharZero R] {v : M} : -v = v ↔ v = 0

theorem self_ne_neg (R : Type u_2) (M : Type u_5) [Semiring R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] [CharZero R] {v : M} : v ≠ -v ↔ v ≠ 0

theorem neg_ne_self (R : Type u_2) (M : Type u_5) [Semiring R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] [CharZero R] {v : M} : -v ≠ v ↔ v ≠ 0

theorem smul_left_injective (R : Type u_2) {M : Type u_5} [Ring R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] {x : M} (hx : x ≠ 0) : Function.Injective fun (c : R) => c • x

instance instNoZeroSMulDivisorsNatToZeroInstLinearOrderedCommMonoidWithZeroToZeroToNegZeroClassToSubNegZeroMonoidToSubtractionMonoidToDivisionAddCommMonoidToNatSMulToAddMonoidToSubNegMonoidToAddGroup {M : Type u_5} [AddCommGroup M] [NoZeroSMulDivisors ℤ M] : NoZeroSMulDivisors ℕ M

Equations

• ⋯ = ⋯

theorem NoZeroSMulDivisors.int_of_charZero (R : Type u_2) (M : Type u_5) [Ring R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] [CharZero R] : NoZeroSMulDivisors ℤ M

theorem CharZero.of_noZeroSMulDivisors (R : Type u_2) (M : Type u_5) [Ring R] [AddCommGroup M] [Module R M] [Nontrivial M] [NoZeroSMulDivisors ℤ M] : CharZero R

Only a ring of characteristic zero can can have a non-trivial module without additive or scalar torsion.

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

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