Documentation

Mathlib.Algebra.Module.Submodule.Defs

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 M, SubMulAction R M :

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.

Instances For
    instance Submodule.setLike {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] :
    Equations
    • Submodule.setLike = { coe := fun (s : Submodule R M) => s.carrier, coe_injective' := }
    theorem Submodule.smulMemClass {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] :
    @[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 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 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 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
    • p.copy s hs = { carrier := s, add_mem' := , zero_mem' := , smul_mem' := }
    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) :
      (S.copy 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) :
      S.copy 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 q : Submodule R M} :
      p.toAddSubmonoid = q.toAddSubmonoid p = q
      @[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_eq {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] {p q : Submodule R M} :
      p.toSubMulAction = q.toSubMulAction p = q
      @[simp]
      theorem Submodule.coe_toSubMulAction {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) :
      p.toSubMulAction = p
      @[instance 75]
      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 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
        @[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
        • p.add = { add := fun (x y : p) => x + y, }
        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
        • p.zero = { zero := 0, }
        instance Submodule.inhabited {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) :
        Equations
        • p.inhabited = { default := 0 }
        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
        • p.smul = { smul := fun (c : S) (x : p) => c x, }
        theorem 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
        theorem 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
        theorem Submodule.nonempty {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) :
        (↑p).Nonempty
        @[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) :
        x, 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 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) :
        x, 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
        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
        • p.module = p.module'
        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
        • p.toAddSubgroup = { toAddSubmonoid := p.toAddSubmonoid, neg_mem' := }
        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) :
          p.toAddSubgroup = p
          @[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} :
          x p.toAddSubgroup x p
          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 p' : Submodule R M) :
          p.toAddSubgroup = p'.toAddSubgroup p = p'
          theorem Submodule.sub_mem {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] {module_M : Module R M} (p : Submodule R M) {x 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 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 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 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 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 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
          @[instance 75]
          instance SubmoduleClass.module' {S : Type u'} {R : Type u} {M : Type v} {T : Type u_1} [Semiring R] [AddCommMonoid M] [Semiring S] [Module R M] [SMul S R] [Module S M] [IsScalarTower S R M] [SetLike T M] [AddSubmonoidClass T M] [SMulMemClass T R M] (t : T) :
          Module S t
          Equations
          @[instance 75]
          instance SubmoduleClass.module {S : Type u'} {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] [SetLike S M] [AddSubmonoidClass S M] [SMulMemClass S R M] (s : S) :
          Module R s
          Equations