Submodules of a module #

In this file we define

Submodule R M : a subset of a Module M that contains zero and is closed with respect to addition and scalar multiplication.
Subspace k M : an abbreviation for Submodule assuming that k is a Field.

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 :

Type v

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 ∈ self.carrier → b ∈ self.carrier → a + b ∈ self.carrier
zero_mem' : 0 ∈ self.carrier
smul_mem' (c : R) {x : M} : x ∈ self.carrier → c • x ∈ self.carrier

Instances For

source

instance Submodule.setLike {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] :

SetLike (Submodule R M) M

Equations

source

@[simp]

theorem Submodule.carrier_eq_coe {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] (s : Submodule R M) :

s.carrier = ↑s

source

def Submodule.ofClass {S : Type u_1} {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [SetLike S M] [AddSubmonoidClass S M] [SMulMemClass S R M] (s : S) :

Submodule R M

The actual Submodule obtained from an element of a SMulMemClass and AddSubmonoidClass.

Equations

Instances For

source

@[simp]

theorem Submodule.coe_ofClass {S : Type u_1} {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [SetLike S M] [AddSubmonoidClass S M] [SMulMemClass S R M] (s : S) :

↑(ofClass s) = ↑s

source

@[instance 100]

instance Submodule.instCanLiftSetCoeAndMemOfNatForallForallForallForallHAddForallForallForallHSMul {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] :

CanLift (Set M) (Submodule R M) SetLike.coe fun (s : Set M) => 0 ∈ s ∧ (∀ {x y : M}, x ∈ s → y ∈ s → x + y ∈ s) ∧ ∀ (r : R) {x : M}, x ∈ s → r • x ∈ s

source

instance Submodule.addSubmonoidClass {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] :

AddSubmonoidClass (Submodule R M) M

source

instance Submodule.smulMemClass {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] :

SMulMemClass (Submodule R M) R M

source

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

source

@[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.carrier → c • x ∈ S.carrier) :

x ∈ { toAddSubmonoid := S, smul_mem' := h } ↔ x ∈ S

source

@[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.carrier → c • x ∈ S.carrier) :

↑{ toAddSubmonoid := S, smul_mem' := h } = ↑S

source

@[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.carrier → c • x ∈ p.carrier) :

{ toAddSubmonoid := p.toAddSubmonoid, smul_mem' := h } = p

source

@[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.carrier → c • x ∈ S.carrier) (h' : ∀ (c : R) {x : M}, x ∈ S'.carrier → c • x ∈ S'.carrier) :

{ toAddSubmonoid := S, smul_mem' := h } ≤ { toAddSubmonoid := S', smul_mem' := h' } ↔ S ≤ S'

source

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

source

theorem Submodule.ext_iff {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] {p q : Submodule R M} :

p = q ↔ ∀ (x : M), x ∈ p ↔ x ∈ q

source

@[deprecated SetLike.coe_set_eq (since := "2025-04-20")]

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

source

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) :

Submodule R M

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

Equations

Instances For

source

@[simp]

theorem Submodule.coe_copy {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) (s : Set M) (hs : s = ↑p) :

↑(p.copy s hs) = s

source

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

source

theorem Submodule.toAddSubmonoid_injective {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] :

Function.Injective toAddSubmonoid

source

@[simp]

theorem Submodule.toAddSubmonoid_inj {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] {p q : Submodule R M} :

p.toAddSubmonoid = q.toAddSubmonoid ↔ p = q

source

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

source

theorem Submodule.toSubMulAction_injective {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] :

Function.Injective toSubMulAction

source

theorem Submodule.toSubMulAction_inj {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] {p q : Submodule R M} :

p.toSubMulAction = q.toSubMulAction ↔ p = q

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

@[simp]

theorem Submodule.smul_mem_iff'' {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) {r : R} {x : M} [Invertible r] :

r • x ∈ p ↔ x ∈ p

source

theorem Submodule.smul_mem_iff_of_isUnit {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) {r : R} {x : M} (hr : IsUnit r) :

r • x ∈ p ↔ x ∈ p

source

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

source

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

source

instance Submodule.inhabited {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) :

Inhabited ↥p

Equations

source

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

source

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

source

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

source

theorem Submodule.nonempty {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) :

(↑p).Nonempty

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

instance Submodule.addCommMonoid {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) :

AddCommMonoid ↥p

Equations

source

instance Submodule.isLeftCancelAdd {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) [IsLeftCancelAdd M] :

IsLeftCancelAdd ↥p

source

instance Submodule.isRightCancelAdd {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) [IsRightCancelAdd M] :

IsRightCancelAdd ↥p

source

instance Submodule.isCancelAdd {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) [IsCancelAdd M] :

IsCancelAdd ↥p

source

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

source

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

source

instance Submodule.addSubgroupClass {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] :

AddSubgroupClass (Submodule R M) M

source

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

source

def Submodule.toAddSubgroup {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] {module_M : Module R M} (p : Submodule R M) :

AddSubgroup M

Reinterpret a submodule as an additive subgroup.

Equations

Instances For

source

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

source

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

source

theorem Submodule.toAddSubgroup_injective {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] {module_M : Module R M} :

Function.Injective toAddSubgroup

source

@[simp]

theorem Submodule.toAddSubgroup_inj {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'

source

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 ∈ p → y ∈ p → x - y ∈ p

source

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

source

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)

source

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)

source

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

source

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

source

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

source

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

source

instance Submodule.addCommGroup {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] {module_M : Module R M} (p : Submodule R M) :

AddCommGroup ↥p

Equations

source

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

source

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

Documentation

Mathlib.Algebra.Module.Submodule.Defs

Submodules of a module #

Tags #