Documentation

Mathlib.Algebra.Module.Submodule.Basic

Submodules of a module #

In this file we define

Tags #

submodule, subspace, linear map

structure Submodule (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] extends AddSubmonoid :

A submodule of a module is one which is closed under vector operations. This is a sufficient condition for the subset of vectors in the submodule to themselves form a module.

  • carrier : Set M
  • add_mem' : ∀ {a b : M}, a s.carrierb s.carriera + b s.carrier
  • zero_mem' : 0 s.carrier
  • smul_mem' : ∀ (c : R) {x : M}, x s.carrierc x s.carrier

    The carrier set is closed under scalar multiplication.

Instances For
    @[reducible]
    abbrev Submodule.toSubMulAction {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] (self : Submodule R M) :

    Reinterpret a Submodule as a SubMulAction.

    Equations
    Instances For
      instance Submodule.setLike {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] :
      Equations
      • One or more equations did not get rendered due to their size.
      instance Submodule.smulMemClass {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] :
      Equations
      @[simp]
      theorem Submodule.mem_toAddSubmonoid {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) (x : M) :
      x p.toAddSubmonoid x p
      @[simp]
      theorem Submodule.mem_mk {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] {S : AddSubmonoid M} {x : M} (h : ∀ (c : R) {x : M}, x S.carrierc x S.carrier) :
      x { toAddSubmonoid := S, smul_mem' := h } x S
      @[simp]
      theorem Submodule.coe_set_mk {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] (S : AddSubmonoid M) (h : ∀ (c : R) {x : M}, x S.carrierc x S.carrier) :
      { toAddSubmonoid := S, smul_mem' := h } = S
      @[simp]
      theorem Submodule.eta {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] {p : Submodule R M} (h : ∀ (c : R) {x : M}, x p.carrierc x p.carrier) :
      { toAddSubmonoid := p.toAddSubmonoid, smul_mem' := h } = p
      @[simp]
      theorem Submodule.mk_le_mk {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] {S : AddSubmonoid M} {S' : AddSubmonoid M} (h : ∀ (c : R) {x : M}, x S.carrierc x S.carrier) (h' : ∀ (c : R) {x : M}, x S'.carrierc x S'.carrier) :
      { toAddSubmonoid := S, smul_mem' := h } { toAddSubmonoid := S', smul_mem' := h' } S S'
      theorem Submodule.ext {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] {p : Submodule R M} {q : Submodule R M} (h : ∀ (x : M), x p x q) :
      p = q
      @[simp]
      theorem Submodule.carrier_inj {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] {p : Submodule R M} {q : Submodule R M} :
      p.carrier = q.carrier p = q
      def Submodule.copy {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) (s : Set M) (hs : s = p) :

      Copy of a submodule with a new carrier equal to the old one. Useful to fix definitional equalities.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        @[simp]
        theorem Submodule.coe_copy {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] (S : Submodule R M) (s : Set M) (hs : s = S) :
        (Submodule.copy S s hs) = s
        theorem Submodule.copy_eq {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] (S : Submodule R M) (s : Set M) (hs : s = S) :
        Submodule.copy S s hs = S
        theorem Submodule.toAddSubmonoid_injective {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] :
        Function.Injective Submodule.toAddSubmonoid
        @[simp]
        theorem Submodule.toAddSubmonoid_eq {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] {p : Submodule R M} {q : Submodule R M} :
        p.toAddSubmonoid = q.toAddSubmonoid p = q
        theorem Submodule.toAddSubmonoid_strictMono {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] :
        StrictMono Submodule.toAddSubmonoid
        theorem Submodule.toAddSubmonoid_le {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] {p : Submodule R M} {q : Submodule R M} :
        p.toAddSubmonoid q.toAddSubmonoid p q
        theorem Submodule.toAddSubmonoid_mono {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] :
        Monotone Submodule.toAddSubmonoid
        @[simp]
        theorem Submodule.coe_toAddSubmonoid {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) :
        p.toAddSubmonoid = p
        theorem Submodule.toSubMulAction_injective {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] :
        Function.Injective Submodule.toSubMulAction
        theorem Submodule.toSubMulAction_strictMono {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] :
        StrictMono Submodule.toSubMulAction
        theorem Submodule.toSubMulAction_mono {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] :
        Monotone Submodule.toSubMulAction
        @[simp]
        theorem Submodule.coe_toSubMulAction {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) :
        instance SMulMemClass.toModule {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] {A : Type u_1} [SetLike A M] [AddSubmonoidClass A M] [SMulMemClass A R M] (S' : A) :
        Module R S'

        A submodule of a Module is a Module.

        Equations
        def SMulMemClass.toModule' (S : Type u_2) (R' : Type u_3) (R : Type u_4) (A : Type u_5) [Semiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Semiring R'] [SMul R' R] [Module R' A] [IsScalarTower R' R A] [SetLike S A] [AddSubmonoidClass S A] [SMulMemClass S R A] (s : S) :
        Module R' s

        This can't be an instance because Lean wouldn't know how to find R, but we can still use this to manually derive Module on specific types.

        Equations
        Instances For
          theorem Submodule.mem_carrier {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) {x : M} :
          x p.carrier x p
          @[simp]
          theorem Submodule.zero_mem {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) :
          0 p
          theorem Submodule.add_mem {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) {x : M} {y : M} (h₁ : x p) (h₂ : y p) :
          x + y p
          theorem Submodule.smul_mem {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) {x : M} (r : R) (h : x p) :
          r x p
          theorem Submodule.smul_of_tower_mem {S : Type u'} {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) {x : M} [SMul S R] [SMul S M] [IsScalarTower S R M] (r : S) (h : x p) :
          r x p
          theorem Submodule.sum_mem {R : Type u} {M : Type v} {ι : Type w} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) {t : Finset ι} {f : ιM} :
          (ct, f c p)(Finset.sum t fun (i : ι) => f i) p
          theorem Submodule.sum_smul_mem {R : Type u} {M : Type v} {ι : Type w} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) {t : Finset ι} {f : ιM} (r : ιR) (hyp : ct, f c p) :
          (Finset.sum t fun (i : ι) => r i f i) p
          @[simp]
          theorem Submodule.smul_mem_iff' {G : Type u''} {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) {x : M} [Group G] [MulAction G M] [SMul G R] [IsScalarTower G R M] (g : G) :
          g x p x p
          instance Submodule.add {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) :
          Add p
          Equations
          • Submodule.add p = { add := fun (x y : p) => { val := x + y, property := (_ : x + y p) } }
          instance Submodule.zero {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) :
          Zero p
          Equations
          instance Submodule.inhabited {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) :
          Equations
          instance Submodule.smul {S : Type u'} {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) [SMul S R] [SMul S M] [IsScalarTower S R M] :
          SMul S p
          Equations
          instance Submodule.isScalarTower {S : Type u'} {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) [SMul S R] [SMul S M] [IsScalarTower S R M] :
          IsScalarTower S R p
          Equations
          instance Submodule.isScalarTower' {S : Type u'} {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) {S' : Type u_1} [SMul S R] [SMul S M] [SMul S' R] [SMul S' M] [SMul S S'] [IsScalarTower S' R M] [IsScalarTower S S' M] [IsScalarTower S R M] :
          IsScalarTower S S' p
          Equations
          instance Submodule.isCentralScalar {S : Type u'} {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) [SMul S R] [SMul S M] [IsScalarTower S R M] [SMul Sᵐᵒᵖ R] [SMul Sᵐᵒᵖ M] [IsScalarTower Sᵐᵒᵖ R M] [IsCentralScalar S M] :
          Equations
          theorem Submodule.nonempty {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) :
          @[simp]
          theorem Submodule.mk_eq_zero {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) {x : M} (h : x p) :
          { val := x, property := h } = 0 x = 0
          theorem Submodule.coe_eq_zero {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} {p : Submodule R M} {x : p} :
          x = 0 x = 0
          @[simp]
          theorem Submodule.coe_add {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} {p : Submodule R M} (x : p) (y : p) :
          (x + y) = x + y
          @[simp]
          theorem Submodule.coe_zero {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} {p : Submodule R M} :
          0 = 0
          theorem Submodule.coe_smul {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} {p : Submodule R M} (r : R) (x : p) :
          (r x) = r x
          @[simp]
          theorem Submodule.coe_smul_of_tower {S : Type u'} {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} {p : Submodule R M} [SMul S R] [SMul S M] [IsScalarTower S R M] (r : S) (x : p) :
          (r x) = r x
          theorem Submodule.coe_mk {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} {p : Submodule R M} (x : M) (hx : x p) :
          { val := x, property := hx } = x
          theorem Submodule.coe_mem {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} {p : Submodule R M} (x : p) :
          x p
          instance Submodule.addCommMonoid {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) :
          Equations
          instance Submodule.module' {S : Type u'} {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) [Semiring S] [SMul S R] [Module S M] [IsScalarTower S R M] :
          Module S p
          Equations
          • One or more equations did not get rendered due to their size.
          instance Submodule.module {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) :
          Module R p
          Equations
          instance Submodule.noZeroSMulDivisors {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) [NoZeroSMulDivisors R M] :
          Equations

          Additive actions by Submodules #

          These instances transfer the action by an element m : M of an R-module M written as m +ᵥ a onto the action by an element s : S of a submodule S : Submodule R M such that s +ᵥ a = (s : M) +ᵥ a. These instances work particularly well in conjunction with AddGroup.toAddAction, enabling s +ᵥ m as an alias for ↑s + m.

          instance Submodule.vaddCommClass {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) {α : Type u_1} {β : Type u_2} [VAdd M β] [VAdd α β] [VAddCommClass M α β] :
          VAddCommClass (p) α β
          Equations
          Equations
          theorem Submodule.vadd_def {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} {p : Submodule R M} {α : Type u_1} [VAdd M α] (g : p) (m : α) :
          g +ᵥ m = g +ᵥ m
          def Submodule.restrictScalars (S : Type u') {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Semiring S] [Module S M] [Module R M] [SMul S R] [IsScalarTower S R M] (V : Submodule R M) :

          V.restrict_scalars S is the S-submodule of the S-module given by restriction of scalars, corresponding to V, an R-submodule of the original R-module.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            @[simp]
            theorem Submodule.coe_restrictScalars (S : Type u') {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Semiring S] [Module S M] [Module R M] [SMul S R] [IsScalarTower S R M] (V : Submodule R M) :
            @[simp]
            theorem Submodule.restrictScalars_mem (S : Type u') {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Semiring S] [Module S M] [Module R M] [SMul S R] [IsScalarTower S R M] (V : Submodule R M) (m : M) :
            @[simp]
            @[simp]
            theorem Submodule.restrictScalars_inj (S : Type u') (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Semiring S] [Module S M] [Module R M] [SMul S R] [IsScalarTower S R M] {V₁ : Submodule R M} {V₂ : Submodule R M} :
            instance Submodule.restrictScalars.origModule (S : Type u') (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Semiring S] [Module S M] [Module R M] [SMul S R] [IsScalarTower S R M] (p : Submodule R M) :

            Even though p.restrictScalars S has type Submodule S M, it is still an R-module.

            Equations
            instance Submodule.restrictScalars.isScalarTower (S : Type u') (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Semiring S] [Module S M] [Module R M] [SMul S R] [IsScalarTower S R M] (p : Submodule R M) :
            Equations
            def Submodule.restrictScalarsEmbedding (S : Type u') (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Semiring S] [Module S M] [Module R M] [SMul S R] [IsScalarTower S R M] :

            restrictScalars S is an embedding of the lattice of R-submodules into the lattice of S-submodules.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              instance Submodule.addSubgroupClass {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] :
              Equations
              theorem Submodule.neg_mem {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] {module_M : Module R M} (p : Submodule R M) {x : M} (hx : x p) :
              -x p
              def Submodule.toAddSubgroup {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] {module_M : Module R M} (p : Submodule R M) :

              Reinterpret a submodule as an additive subgroup.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                @[simp]
                theorem Submodule.coe_toAddSubgroup {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] {module_M : Module R M} (p : Submodule R M) :
                @[simp]
                theorem Submodule.mem_toAddSubgroup {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] {module_M : Module R M} (p : Submodule R M) {x : M} :
                theorem Submodule.toAddSubgroup_injective {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] {module_M : Module R M} :
                Function.Injective Submodule.toAddSubgroup
                @[simp]
                theorem Submodule.toAddSubgroup_eq {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] {module_M : Module R M} (p : Submodule R M) (p' : Submodule R M) :
                theorem Submodule.toAddSubgroup_strictMono {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] {module_M : Module R M} :
                StrictMono Submodule.toAddSubgroup
                theorem Submodule.toAddSubgroup_le {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] {module_M : Module R M} (p : Submodule R M) (p' : Submodule R M) :
                theorem Submodule.toAddSubgroup_mono {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] {module_M : Module R M} :
                Monotone Submodule.toAddSubgroup
                theorem Submodule.sub_mem {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] {module_M : Module R M} (p : Submodule R M) {x : M} {y : M} :
                x py px - y p
                theorem Submodule.neg_mem_iff {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] {module_M : Module R M} (p : Submodule R M) {x : M} :
                -x p x p
                theorem Submodule.add_mem_iff_left {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] {module_M : Module R M} (p : Submodule R M) {x : M} {y : M} :
                y p(x + y p x p)
                theorem Submodule.add_mem_iff_right {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] {module_M : Module R M} (p : Submodule R M) {x : M} {y : M} :
                x p(x + y p y p)
                theorem Submodule.coe_neg {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] {module_M : Module R M} (p : Submodule R M) (x : p) :
                (-x) = -x
                theorem Submodule.coe_sub {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] {module_M : Module R M} (p : Submodule R M) (x : p) (y : p) :
                (x - y) = x - y
                theorem Submodule.sub_mem_iff_left {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] {module_M : Module R M} (p : Submodule R M) {x : M} {y : M} (hy : y p) :
                x - y p x p
                theorem Submodule.sub_mem_iff_right {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] {module_M : Module R M} (p : Submodule R M) {x : M} {y : M} (hx : x p) :
                x - y p y p
                instance Submodule.addCommGroup {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] {module_M : Module R M} (p : Submodule R M) :
                Equations
                theorem Submodule.neg_coe {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] {module_M : Module R M} (p : Submodule R M) :
                -p = p
                theorem Submodule.not_mem_of_ortho {R : Type u} {M : Type v} [Ring R] [IsDomain R] [AddCommGroup M] [Module R M] {x : M} {N : Submodule R M} (ortho : ∀ (c : R), yN, c x + y = 0c = 0) :
                xN
                theorem Submodule.ne_zero_of_ortho {R : Type u} {M : Type v} [Ring R] [IsDomain R] [AddCommGroup M] [Module R M] {x : M} {N : Submodule R M} (ortho : ∀ (c : R), yN, c x + y = 0c = 0) :
                x 0

                A submodule of an OrderedAddCommMonoid is an OrderedAddCommMonoid.

                Equations
                • One or more equations did not get rendered due to their size.

                A submodule of a LinearOrderedAddCommMonoid is a LinearOrderedAddCommMonoid.

                Equations
                • One or more equations did not get rendered due to their size.

                A submodule of an OrderedCancelAddCommMonoid is an OrderedCancelAddCommMonoid.

                Equations
                • One or more equations did not get rendered due to their size.

                A submodule of a LinearOrderedCancelAddCommMonoid is a LinearOrderedCancelAddCommMonoid.

                Equations
                • One or more equations did not get rendered due to their size.
                instance Submodule.toOrderedAddCommGroup {R : Type u} [Ring R] {M : Type u_1} [OrderedAddCommGroup M] [Module R M] (S : Submodule R M) :

                A submodule of an OrderedAddCommGroup is an OrderedAddCommGroup.

                Equations
                • One or more equations did not get rendered due to their size.

                A submodule of a LinearOrderedAddCommGroup is a LinearOrderedAddCommGroup.

                Equations
                • One or more equations did not get rendered due to their size.
                theorem Submodule.smul_mem_iff {S : Type u'} {R : Type u} {M : Type v} [DivisionSemiring S] [Semiring R] [AddCommMonoid M] [Module R M] [SMul S R] [Module S M] [IsScalarTower S R M] (p : Submodule R M) {s : S} {x : M} (s0 : s 0) :
                s x p x p
                @[inline, reducible]
                abbrev Subspace (R : Type u) (M : Type v) [DivisionRing R] [AddCommGroup M] [Module R M] :

                Subspace of a vector space. Defined to equal Submodule.

                Equations
                Instances For