Documentation

Mathlib.Algebra.Module.Basic

Modules over a ring #

In this file we define

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 semimodule and vector_space abbreviations. 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 {R : Type u} {M : Type v} :
∀ {inst : Semiring R} {inst_1 : AddCommMonoid M} (x y : Module R M), SMul.smul = SMul.smulx = y
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
class Module (R : Type u) (M : Type v) [inst : Semiring R] [inst : AddCommMonoid M] extends DistribMulAction :
Type (maxuv)
  • Scalar multiplication distributes over addition from the right.

    add_smul : ∀ (r s : R) (x : M), (r + s) x = r x + s x
  • Scalar multiplication by zero gives zero.

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

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.

Instances
    instance Module.toMulActionWithZero {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] :

    A module over a semiring automatically inherits a MulActionWithZero structure.

    Equations
    instance AddCommMonoid.natModule {M : Type u_1} [inst : AddCommMonoid M] :
    Equations
    theorem add_smul {R : Type u_2} {M : Type u_1} [inst : Semiring R] [inst : AddCommMonoid M] [inst : 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_2} [inst : Semiring R] [inst : AddCommMonoid M] [inst : 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_1} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] (x : M) :
    2 x = x + x
    theorem two_smul' (R : Type u_2) {M : Type u_1} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] (x : M) :
    2 x = bit0 x
    @[simp]
    theorem inv_of_two_smul_add_inv_of_two_smul (R : Type u_1) {M : Type u_2} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] [inst : Invertible 2] (x : M) :
    2 x + 2 x = x
    def Function.Injective.module (R : Type u_1) {M : Type u_2} {M₂ : Type u_3} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] [inst : AddCommMonoid M₂] [inst : 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
    • One or more equations did not get rendered due to their size.
    def Function.Surjective.module (R : Type u_1) {M : Type u_2} {M₂ : Type u_3} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] [inst : AddCommMonoid M₂] [inst : 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.

    Equations
    • One or more equations did not get rendered due to their size.
    def Function.Surjective.moduleLeft {R : Type u_1} {S : Type u_2} {M : Type u_3} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] [inst : Semiring S] [inst : 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→+* S.

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

    Equations
    • One or more equations did not get rendered due to their size.
    def Module.compHom {R : Type u_1} {S : Type u_2} (M : Type u_3) [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] [inst : 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
    • One or more equations did not get rendered due to their size.
    @[simp]
    theorem Module.toAddMonoidEnd_apply_apply (R : Type u_1) (M : Type u_2) [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] (x : R) :
    ∀ (x : M), ↑(↑(Module.toAddMonoidEnd R M) x) x = x x
    def Module.toAddMonoidEnd (R : Type u_1) (M : Type u_2) [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] :

    (•) as an AddMonoidHom.

    This is a stronger version of DistribMulAction.toAddMonoidEnd

    Equations
    • One or more equations did not get rendered due to their size.
    def smulAddHom (R : Type u_1) (M : Type u_2) [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] :
    R →+ M →+ M

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

    Equations
    @[simp]
    theorem smulAddHom_apply {R : Type u_2} {M : Type u_1} [inst : Semiring R] [inst : AddCommMonoid M] [inst : 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_2} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] (x : M) (zero_eq_one : 0 = 1) :
    x = 0
    @[simp]
    theorem smul_add_one_sub_smul {M : Type u_2} [inst : AddCommMonoid M] {R : Type u_1} [inst : Ring R] [inst : Module R M] {r : R} {m : M} :
    r m + (1 - r) m = m
    def Module.addCommMonoidToAddCommGroup (R : Type u_1) {M : Type u_2} [inst : Ring R] [inst : AddCommMonoid M] [inst : Module R M] :

    An AddCommMonoid that is a Module over a Ring carries a natural AddCommGroup structure. See note [reducible non-instances].

    Equations
    instance AddCommGroup.intModule (M : Type u_1) [inst : AddCommGroup M] :
    Equations
    structure Module.Core (R : Type u_1) (M : Type u_2) [inst : Semiring R] [inst : AddCommGroup M] extends SMul :
    Type (maxu_1u_2)
    • Scalar multiplication distributes over addition from the left.

      smul_add : ∀ (r : R) (x y : M), r (x + y) = r x + r y
    • Scalar multiplication distributes over addition from the right.

      add_smul : ∀ (r s : R) (x : M), (r + s) x = r x + s x
    • Scalar multiplication distributes over multiplication from the right.

      mul_smul : ∀ (r s : R) (x : M), (r * s) x = r s x
    • Scalar multiplication by one is the identity.

      one_smul : ∀ (x : M), 1 x = x

    A structure containing most informations as in a module, except the fields zero_smul and smul_zero. As these fields can be deduced from the other ones when M is an AddCommGroup, this provides a way to construct a module structure by checking less properties, in Module.ofCore.

    Instances For
      def Module.ofCore {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst : AddCommGroup M] (H : Module.Core R M) :
      Module R M

      Define Module without proving zero_smul and smul_zero by using an auxiliary structure Module.Core, when the underlying space is an AddCommGroup.

      Equations
      theorem Convex.combo_eq_smul_sub_add {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst : AddCommGroup M] [inst : 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_1} [inst : Semiring R] {M : Type u_2} [inst : 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_1} [inst : Ring R] [inst : AddCommGroup M] [inst : Module R M] (r : R) (x : M) :
      -r x = -(r x)
      theorem neg_smul_neg {R : Type u_2} {M : Type u_1} [inst : Ring R] [inst : AddCommGroup M] [inst : Module R M] (r : R) (x : M) :
      -r -x = r x
      @[simp]
      theorem Units.neg_smul {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst : AddCommGroup M] [inst : Module R M] (u : Rˣ) (x : M) :
      -u x = -(u x)
      theorem neg_one_smul (R : Type u_2) {M : Type u_1} [inst : Ring R] [inst : AddCommGroup M] [inst : Module R M] (x : M) :
      -1 x = -x
      theorem sub_smul {R : Type u_2} {M : Type u_1} [inst : Ring R] [inst : AddCommGroup M] [inst : Module R M] (r : R) (s : R) (y : M) :
      (r - s) y = r y - s y
      theorem Module.subsingleton (R : Type u_1) (M : Type u_2) [inst : Semiring R] [inst : Subsingleton R] [inst : AddCommMonoid M] [inst : Module R 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_1) (M : Type u_2) [inst : Semiring R] [inst : Nontrivial M] [inst : AddCommMonoid M] [inst : Module R M] :

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

      instance Semiring.toModule {R : Type u_1} [inst : Semiring R] :
      Module R R
      Equations
      • Semiring.toModule = Module.mk (_ : ∀ (a b c : R), (a + b) * c = a * c + b * c) (_ : ∀ (a : R), 0 * a = 0)
      instance Semiring.toOppositeModule {R : Type u_1} [inst : Semiring R] :

      Like Semiring.toModule, but multiplies on the right.

      Equations
      • One or more equations did not get rendered due to their size.
      def RingHom.toModule {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst : Semiring S] (f : R →+* S) :
      Module R S

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

      Equations
      instance RingHom.applyDistribMulAction {R : Type u_1} [inst : Semiring R] :

      The tautological action by R →+* R→+* R on R.

      This generalizes Function.End.applyMulAction.

      Equations
      @[simp]
      theorem RingHom.smul_def {R : Type u_1} [inst : Semiring R] (f : R →+* R) (a : R) :
      f a = f a
      theorem nsmul_eq_smul_cast (R : Type u_2) {M : Type u_1} [inst : Semiring R] [inst : AddCommMonoid M] [inst : 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_1} [inst : 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.

      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 := (_ : ∀ (P : Module M), P = default) }
      theorem zsmul_eq_smul_cast (R : Type u_2) {M : Type u_1} [inst : Ring R] [inst : AddCommGroup M] [inst : 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_1} [inst : 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.

      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 := (_ : ∀ (P : Module M), P = default) }
      theorem map_int_cast_smul {M : Type u_1} {M₂ : Type u_2} [inst : AddCommGroup M] [inst : AddCommGroup M₂] {F : Type u_3} [inst : AddMonoidHomClass F M M₂] (f : F) (R : Type u_4) (S : Type u_5) [inst : Ring R] [inst : Ring S] [inst : Module R M] [inst : Module S M₂] (x : ) (a : M) :
      f (x a) = x f a
      theorem map_nat_cast_smul {M : Type u_1} {M₂ : Type u_2} [inst : AddCommMonoid M] [inst : AddCommMonoid M₂] {F : Type u_3} [inst : AddMonoidHomClass F M M₂] (f : F) (R : Type u_4) (S : Type u_5) [inst : Semiring R] [inst : Semiring S] [inst : Module R M] [inst : Module S M₂] (x : ) (a : M) :
      f (x a) = x f a
      theorem map_inv_int_cast_smul {M : Type u_1} {M₂ : Type u_2} [inst : AddCommGroup M] [inst : AddCommGroup M₂] {F : Type u_3} [inst : AddMonoidHomClass F M M₂] (f : F) (R : Type u_4) (S : Type u_5) [inst : DivisionRing R] [inst : DivisionRing S] [inst : Module R M] [inst : Module S M₂] (n : ) (x : M) :
      f ((n)⁻¹ x) = (n)⁻¹ f x
      theorem map_inv_nat_cast_smul {M : Type u_1} {M₂ : Type u_2} [inst : AddCommGroup M] [inst : AddCommGroup M₂] {F : Type u_3} [inst : AddMonoidHomClass F M M₂] (f : F) (R : Type u_4) (S : Type u_5) [inst : DivisionRing R] [inst : DivisionRing S] [inst : Module R M] [inst : Module S M₂] (n : ) (x : M) :
      f ((n)⁻¹ x) = (n)⁻¹ f x
      theorem map_rat_cast_smul {M : Type u_1} {M₂ : Type u_2} [inst : AddCommGroup M] [inst : AddCommGroup M₂] {F : Type u_3} [inst : AddMonoidHomClass F M M₂] (f : F) (R : Type u_4) (S : Type u_5) [inst : DivisionRing R] [inst : DivisionRing S] [inst : Module R M] [inst : Module S M₂] (c : ) (x : M) :
      f (c x) = c f x
      theorem map_rat_smul {M : Type u_1} {M₂ : Type u_2} [inst : AddCommGroup M] [inst : AddCommGroup M₂] [inst : Module M] [inst : Module M₂] {F : Type u_3} [inst : AddMonoidHomClass F M M₂] (f : F) (c : ) (x : M) :
      f (c x) = c f x
      instance subsingleton_rat_module (E : Type u_1) [inst : AddCommGroup E] :

      There can be at most one Module ℚ E structure on an additive commutative group.

      Equations
      theorem inv_int_cast_smul_eq {E : Type u_1} (R : Type u_2) (S : Type u_3) [inst : AddCommGroup E] [inst : DivisionRing R] [inst : DivisionRing S] [inst : Module R E] [inst : Module S E] (n : ) (x : E) :
      (n)⁻¹ x = (n)⁻¹ x

      If E is a vector space over two division rings R and S, then scalar multiplications agree on inverses of integer numbers in R and S.

      theorem inv_nat_cast_smul_eq {E : Type u_1} (R : Type u_2) (S : Type u_3) [inst : AddCommGroup E] [inst : DivisionRing R] [inst : DivisionRing S] [inst : Module R E] [inst : Module S E] (n : ) (x : E) :
      (n)⁻¹ x = (n)⁻¹ x

      If E is a vector space over two division rings R and S, then scalar multiplications agree on inverses of natural numbers in R and S.

      theorem inv_int_cast_smul_comm {α : Type u_1} {E : Type u_2} (R : Type u_3) [inst : AddCommGroup E] [inst : DivisionRing R] [inst : Monoid α] [inst : Module R E] [inst : DistribMulAction α E] (n : ) (s : α) (x : E) :
      (n)⁻¹ s x = s (n)⁻¹ x

      If E is a vector space over a division rings R and has a monoid action by α, then that action commutes by scalar multiplication of inverses of integers in R

      theorem inv_nat_cast_smul_comm {α : Type u_1} {E : Type u_2} (R : Type u_3) [inst : AddCommGroup E] [inst : DivisionRing R] [inst : Monoid α] [inst : Module R E] [inst : DistribMulAction α E] (n : ) (s : α) (x : E) :
      (n)⁻¹ s x = s (n)⁻¹ x

      If E is a vector space over a division rings R and has a monoid action by α, then that action commutes by scalar multiplication of inverses of natural numbers in R.

      theorem rat_cast_smul_eq {E : Type u_1} (R : Type u_2) (S : Type u_3) [inst : AddCommGroup E] [inst : DivisionRing R] [inst : DivisionRing S] [inst : Module R E] [inst : Module S E] (r : ) (x : E) :
      r x = r x

      If E is a vector space over two division rings R and S, then scalar multiplications agree on rational numbers in R and S.

      instance IsScalarTower.rat {R : Type u} {M : Type v} [inst : Ring R] [inst : AddCommGroup M] [inst : Module R M] [inst : Module R] [inst : Module M] :
      Equations
      instance SMulCommClass.rat {R : Type u} {M : Type v} [inst : Semiring R] [inst : AddCommGroup M] [inst : Module R M] [inst : Module M] :
      Equations
      instance SMulCommClass.rat' {R : Type u} {M : Type v} [inst : Semiring R] [inst : AddCommGroup M] [inst : Module R M] [inst : Module M] :
      Equations

      NoZeroSMulDivisors #

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

      class NoZeroSMulDivisors (R : Type u_1) (M : Type u_2) [inst : Zero R] [inst : Zero M] [inst : SMul R M] :
      • If scalar multiplication yields zero, either the scalar or the vector was zero.

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

      NoZeroSMulDivisors R M states that a scalar multiple is 0 only if either argument is 0. This 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.

      Instances
        theorem Function.Injective.noZeroSMulDivisors {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : Zero R] [inst : Zero M] [inst : Zero N] [inst : SMul R M] [inst : SMul R N] [inst : NoZeroSMulDivisors R N] (f : MN) (hf : Function.Injective f) (h0 : f 0 = 0) (hs : ∀ (c : R) (x : M), f (c x) = c f x) :

        Pullback a NoZeroSMulDivisors instance along an injective function.

        theorem smul_ne_zero {R : Type u_1} {M : Type u_2} [inst : Zero R] [inst : Zero M] [inst : SMul R M] [inst : 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_1} [inst : Zero R] [inst : Zero M] [inst : SMulWithZero R M] [inst : 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_1} [inst : Zero R] [inst : Zero M] [inst : SMulWithZero R M] [inst : NoZeroSMulDivisors R M] {c : R} {x : M} :
        c x 0 c 0 x 0
        theorem Nat.noZeroSMulDivisors (R : Type u_2) (M : Type u_1) [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] [inst : NoZeroSMulDivisors R M] [inst : CharZero R] :
        theorem two_nsmul_eq_zero (R : Type u_2) (M : Type u_1) [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] [inst : NoZeroSMulDivisors R M] [inst : CharZero R] {v : M} :
        2 v = 0 v = 0
        theorem CharZero.of_module (R : Type u_2) [inst : Semiring R] (M : Type u_1) [inst : AddCommMonoidWithOne M] [inst : CharZero M] [inst : Module R M] :

        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_1} (M : Type u_2) [inst : Semiring R] [inst : AddCommGroup M] [inst : Module R M] [inst : NoZeroSMulDivisors R M] {c : R} (hc : c 0) :
        Function.Injective ((fun x x_1 => x x_1) c)
        theorem smul_right_inj {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst : AddCommGroup M] [inst : Module R M] [inst : 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_1) [inst : Semiring R] [inst : AddCommGroup M] [inst : Module R M] [inst : NoZeroSMulDivisors R M] [inst : CharZero R] {v : M} :
        v = -v v = 0
        theorem neg_eq_self (R : Type u_2) (M : Type u_1) [inst : Semiring R] [inst : AddCommGroup M] [inst : Module R M] [inst : NoZeroSMulDivisors R M] [inst : CharZero R] {v : M} :
        -v = v v = 0
        theorem self_ne_neg (R : Type u_2) (M : Type u_1) [inst : Semiring R] [inst : AddCommGroup M] [inst : Module R M] [inst : NoZeroSMulDivisors R M] [inst : CharZero R] {v : M} :
        v -v v 0
        theorem neg_ne_self (R : Type u_2) (M : Type u_1) [inst : Semiring R] [inst : AddCommGroup M] [inst : Module R M] [inst : NoZeroSMulDivisors R M] [inst : CharZero R] {v : M} :
        -v v v 0
        theorem smul_left_injective (R : Type u_2) {M : Type u_1} [inst : Ring R] [inst : AddCommGroup M] [inst : Module R M] [inst : NoZeroSMulDivisors R M] {x : M} (hx : x 0) :
        Function.Injective fun c => c x
        instance GroupWithZero.toNoZeroSMulDivisors {R : Type u_1} {M : Type u_2} [inst : GroupWithZero R] [inst : AddMonoid M] [inst : DistribMulAction R M] :

        This instance applies to DivisionSemirings, in particular NNReal and NNRat.

        Equations
        theorem Nat.smul_one_eq_coe {R : Type u_1} [inst : Semiring R] (m : ) :
        m 1 = m
        theorem Int.smul_one_eq_coe {R : Type u_1} [inst : Ring R] (m : ) :
        m 1 = m