algebra.module.submodule.basic

@[class]

structure submodule_class (S : Type u_1) (R : out_param (Type u_2)) (M : Type u_3) [add_zero_class M] [has_smul R M] [set_like S M] [add_submonoid_class S M] :

Type

smul_mem : ∀ {s : S} (r : R) {m : M}, m ∈ s → r • m ∈ s

submodule_class S R M says S is a type of submodules s ≤ M.

Note that only R is marked as out_param since M is already supplied by the set_like class.

Instances of this typeclass

submodule.submodule_class

Instances of other typeclasses for submodule_class

submodule_class.has_sizeof_inst

source

@[instance]

def submodule_class.to_smul_mem_class (S : Type u_1) (R : out_param (Type u_2)) (M : Type u_3) [add_zero_class M] [has_smul R M] [set_like S M] [add_submonoid_class S M] [self : submodule_class S R M] :

smul_mem_class S R M

source

def submodule.to_add_submonoid {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [module R M] (self : submodule R M) :

add_submonoid M

Reinterpret a submodule as an add_submonoid.

source

structure submodule (R : Type u) (M : Type v) [semiring R] [add_comm_monoid M] [module R M] :

Type v

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

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 submodule

source

def submodule.to_sub_mul_action {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [module R M] (self : submodule R M) :

sub_mul_action R M

Reinterpret a submodule as an sub_mul_action.

source

@[protected, instance]

def submodule.set_like {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [module R M] :

set_like (submodule R M) M

Equations

submodule.set_like = {coe := submodule.carrier _inst_3, coe_injective' := _}

source

@[protected, instance]

def submodule.add_submonoid_class {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [module R M] :

add_submonoid_class (submodule R M) M

source

@[protected, instance]

def submodule.submodule_class {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [module R M] :

submodule_class (submodule R M) R M

Equations

submodule.submodule_class = {smul_mem := _}

source

@[simp]

theorem submodule.mem_to_add_submonoid {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [module R M] (p : submodule R M) (x : M) :

x ∈ p.to_add_submonoid ↔ x ∈ p

source

@[simp]

theorem submodule.mem_mk {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [module R M] {S : set M} {x : M} (h₁ : ∀ {a b : M}, a ∈ S → b ∈ S → a + b ∈ S) (h₂ : 0 ∈ S) (h₃ : ∀ (c : R) {x : M}, x ∈ S → c • x ∈ S) :

x ∈ {carrier := S, add_mem' := h₁, zero_mem' := h₂, smul_mem' := h₃} ↔ x ∈ S

source

@[simp]

theorem submodule.coe_set_mk {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [module R M] (S : set M) (h₁ : ∀ {a b : M}, a ∈ S → b ∈ S → a + b ∈ S) (h₂ : 0 ∈ S) (h₃ : ∀ (c : R) {x : M}, x ∈ S → c • x ∈ S) :

↑{carrier := S, add_mem' := h₁, zero_mem' := h₂, smul_mem' := h₃} = S

source

@[simp]

theorem submodule.mk_le_mk {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [module R M] {S S' : set M} (h₁ : ∀ {a b : M}, a ∈ S → b ∈ S → a + b ∈ S) (h₂ : 0 ∈ S) (h₃ : ∀ (c : R) {x : M}, x ∈ S → c • x ∈ S) (h₁' : ∀ {a b : M}, a ∈ S' → b ∈ S' → a + b ∈ S') (h₂' : 0 ∈ S') (h₃' : ∀ (c : R) {x : M}, x ∈ S' → c • x ∈ S') :

{carrier := S, add_mem' := h₁, zero_mem' := h₂, smul_mem' := h₃} ≤ {carrier := S', add_mem' := h₁', zero_mem' := h₂', smul_mem' := h₃'} ↔ S ⊆ S'

source

@[ext]

theorem submodule.ext {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [module R M] {p q : submodule R M} (h : ∀ (x : M), x ∈ p ↔ x ∈ q) :

p = q

source

@[protected]

def submodule.copy {R : Type u} {M : Type v} [semiring R] [add_comm_monoid 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

p.copy s hs = {carrier := s, add_mem' := _, zero_mem' := _, smul_mem' := _}

source

@[simp]

theorem submodule.coe_copy {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [module R M] (S : submodule R M) (s : set M) (hs : s = ↑S) :

↑(S.copy s hs) = s

source

theorem submodule.copy_eq {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [module R M] (S : submodule R M) (s : set M) (hs : s = ↑S) :

S.copy s hs = S

source

theorem submodule.to_add_submonoid_injective {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [module R M] :

function.injective submodule.to_add_submonoid

source

@[simp]

theorem submodule.to_add_submonoid_eq {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [module R M] {p q : submodule R M} :

p.to_add_submonoid = q.to_add_submonoid ↔ p = q

source

theorem submodule.to_add_submonoid_strict_mono {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [module R M] :

strict_mono submodule.to_add_submonoid

source

theorem submodule.to_add_submonoid_le {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [module R M] {p q : submodule R M} :

p.to_add_submonoid ≤ q.to_add_submonoid ↔ p ≤ q

source

theorem submodule.to_add_submonoid_mono {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [module R M] :

monotone submodule.to_add_submonoid

source

@[simp]

theorem submodule.coe_to_add_submonoid {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [module R M] (p : submodule R M) :

↑(p.to_add_submonoid) = ↑p

source

theorem submodule.to_sub_mul_action_injective {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [module R M] :

function.injective submodule.to_sub_mul_action

source

@[simp]

theorem submodule.to_sub_mul_action_eq {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [module R M] {p q : submodule R M} :

p.to_sub_mul_action = q.to_sub_mul_action ↔ p = q

source

theorem submodule.to_sub_mul_action_strict_mono {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [module R M] :

strict_mono submodule.to_sub_mul_action

source

theorem submodule.to_sub_mul_action_mono {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [module R M] :

monotone submodule.to_sub_mul_action

source

@[simp]

theorem submodule.coe_to_sub_mul_action {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [module R M] (p : submodule R M) :

↑(p.to_sub_mul_action) = ↑p

source

@[protected, instance]

def submodule_class.to_module {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [module R M] {A : Type u_1} [set_like A M] [add_submonoid_class A M] [hA : submodule_class A R M] (S' : A) :

module R ↥S'

A submodule of a module is a module.

Equations

submodule_class.to_module S' = function.injective.module R (add_submonoid_class.subtype S') _ _

source

@[protected]

def submodule_class.subtype {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [module R M] {A : Type u_1} [set_like A M] [add_submonoid_class A M] [hA : submodule_class A R M] (S' : A) :

↥S' →ₗ[R] M

The natural R-linear map from a submodule of an R-module M to M.

Equations

submodule_class.subtype S' = {to_fun := coe coe_to_lift, map_add' := _, map_smul' := _}

source

@[protected, simp]

theorem submodule_class.coe_subtype {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [module R M] {A : Type u_1} [set_like A M] [add_submonoid_class A M] [hA : submodule_class A R M] (S' : A) :

⇑(submodule_class.subtype S') = coe

source

@[simp]

theorem submodule.mem_carrier {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] {module_M : module R M} (p : submodule R M) {x : M} :

x ∈ p.carrier ↔ x ∈ ↑p

source

@[protected, simp]

theorem submodule.zero_mem {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] {module_M : module R M} (p : submodule R M) :

0 ∈ p

source

@[protected]

theorem submodule.add_mem {R : Type u} {M : Type v} [semiring R] [add_comm_monoid 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] [add_comm_monoid 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] [add_comm_monoid M] {module_M : module R M} (p : submodule R M) {x : M} [has_smul S R] [has_smul S M] [is_scalar_tower S R M] (r : S) (h : x ∈ p) :

r • x ∈ p

source

@[protected]

theorem submodule.sum_mem {R : Type u} {M : Type v} {ι : Type w} [semiring R] [add_comm_monoid M] {module_M : module R M} (p : submodule R M) {t : finset ι} {f : ι → M} :

(∀ (c : ι), c ∈ t → f c ∈ p) → t.sum (λ (i : ι), f i) ∈ p

source

theorem submodule.sum_smul_mem {R : Type u} {M : Type v} {ι : Type w} [semiring R] [add_comm_monoid M] {module_M : module R M} (p : submodule R M) {t : finset ι} {f : ι → M} (r : ι → R) (hyp : ∀ (c : ι), c ∈ t → f c ∈ p) :

t.sum (λ (i : ι), r i • f i) ∈ p

source

@[simp]

theorem submodule.smul_mem_iff' {G : Type u''} {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] {module_M : module R M} (p : submodule R M) {x : M} [group G] [mul_action G M] [has_smul G R] [is_scalar_tower G R M] (g : G) :

g • x ∈ p ↔ x ∈ p

source

@[protected, instance]

def submodule.has_add {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] {module_M : module R M} (p : submodule R M) :

has_add ↥p

Equations

p.has_add = {add := λ (x y : ↥p), ⟨x.val + y.val, _⟩}

source

@[protected, instance]

def submodule.has_zero {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] {module_M : module R M} (p : submodule R M) :

has_zero ↥p

Equations

p.has_zero = {zero := ⟨0, _⟩}

source

@[protected, instance]

def submodule.inhabited {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] {module_M : module R M} (p : submodule R M) :

inhabited ↥p

Equations

p.inhabited = {default := 0}

source

@[protected, instance]

def submodule.has_smul {S : Type u'} {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] {module_M : module R M} (p : submodule R M) [has_smul S R] [has_smul S M] [is_scalar_tower S R M] :

has_smul S ↥p

Equations

p.has_smul = {smul := λ (c : S) (x : ↥p), ⟨c • x.val, _⟩}

source

@[protected, instance]

def submodule.is_scalar_tower {S : Type u'} {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] {module_M : module R M} (p : submodule R M) [has_smul S R] [has_smul S M] [is_scalar_tower S R M] :

is_scalar_tower S R ↥p

source

@[protected, instance]

def submodule.is_scalar_tower' {S : Type u'} {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] {module_M : module R M} (p : submodule R M) {S' : Type u_1} [has_smul S R] [has_smul S M] [has_smul S' R] [has_smul S' M] [has_smul S S'] [is_scalar_tower S' R M] [is_scalar_tower S S' M] [is_scalar_tower S R M] :

is_scalar_tower S S' ↥p

source

@[protected, instance]

def submodule.is_central_scalar {S : Type u'} {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] {module_M : module R M} (p : submodule R M) [has_smul S R] [has_smul S M] [is_scalar_tower S R M] [has_smul Sᵐᵒᵖ R] [has_smul Sᵐᵒᵖ M] [is_scalar_tower Sᵐᵒᵖ R M] [is_central_scalar S M] :

is_central_scalar S ↥p

source

@[protected]

theorem submodule.nonempty {R : Type u} {M : Type v} [semiring R] [add_comm_monoid 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] [add_comm_monoid M] {module_M : module R M} (p : submodule R M) {x : M} (h : x ∈ p) :

⟨x, h⟩ = 0 ↔ x = 0

source

@[simp, norm_cast]

theorem submodule.coe_eq_zero {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] {module_M : module R M} {p : submodule R M} {x : ↥p} :

↑x = 0 ↔ x = 0

source

@[simp, norm_cast]

theorem submodule.coe_add {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] {module_M : module R M} {p : submodule R M} (x y : ↥p) :

↑(x + y) = ↑x + ↑y

source

@[simp, norm_cast]

theorem submodule.coe_zero {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] {module_M : module R M} {p : submodule R M} :

↑0 = 0

source

@[norm_cast]

theorem submodule.coe_smul {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] {module_M : module R M} {p : submodule R M} (r : R) (x : ↥p) :

↑(r • x) = r • ↑x

source

@[simp, norm_cast]

theorem submodule.coe_smul_of_tower {S : Type u'} {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] {module_M : module R M} {p : submodule R M} [has_smul S R] [has_smul S M] [is_scalar_tower S R M] (r : S) (x : ↥p) :

↑(r • x) = r • ↑x

source

@[simp, norm_cast]

theorem submodule.coe_mk {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] {module_M : module R M} {p : submodule R M} (x : M) (hx : x ∈ p) :

↑⟨x, hx⟩ = x

source

@[simp]

theorem submodule.coe_mem {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] {module_M : module R M} {p : submodule R M} (x : ↥p) :

↑x ∈ p

source

@[protected, instance]

def submodule.add_comm_monoid {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] {module_M : module R M} (p : submodule R M) :

add_comm_monoid ↥p

Equations

p.add_comm_monoid = {add := has_add.add p.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := add_comm_monoid.nsmul p.to_add_submonoid.to_add_comm_monoid, nsmul_zero' := _, nsmul_succ' := _, add_comm := _}

source

@[protected, instance]

def submodule.module' {S : Type u'} {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] {module_M : module R M} (p : submodule R M) [semiring S] [has_smul S R] [module S M] [is_scalar_tower S R M] :

module S ↥p

Equations

p.module' = {to_distrib_mul_action := {to_mul_action := {to_has_smul := {smul := has_smul.smul p.has_smul}, one_smul := _, mul_smul := _}, smul_zero := _, smul_add := _}, add_smul := _, zero_smul := _}

source

@[protected, instance]

def submodule.module {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] {module_M : module R M} (p : submodule R M) :

module R ↥p

Equations

p.module = p.module'

source

@[protected, instance]

def submodule.no_zero_smul_divisors {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] {module_M : module R M} (p : submodule R M) [no_zero_smul_divisors R M] :

no_zero_smul_divisors R ↥p

source

@[protected]

def submodule.subtype {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] {module_M : module R M} (p : submodule R M) :

↥p →ₗ[R] M

Embedding of a submodule p to the ambient space M.

Equations

p.subtype = {to_fun := coe coe_to_lift, map_add' := _, map_smul' := _}

source

theorem submodule.subtype_apply {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] {module_M : module R M} (p : submodule R M) (x : ↥p) :

⇑(p.subtype) x = ↑x

source

@[simp]

theorem submodule.coe_subtype {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] {module_M : module R M} (p : submodule R M) :

⇑(p.subtype) = coe

source

theorem submodule.injective_subtype {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] {module_M : module R M} (p : submodule R M) :

function.injective ⇑(p.subtype)

source

@[simp]

theorem submodule.coe_sum {R : Type u} {M : Type v} {ι : Type w} [semiring R] [add_comm_monoid M] {module_M : module R M} (p : submodule R M) (x : ι → ↥p) (s : finset ι) :

↑(s.sum (λ (i : ι), x i)) = s.sum (λ (i : ι), ↑(x i))

Note the add_submonoid version of this lemma is called add_submonoid.coe_finset_sum.

source

def submodule.restrict_scalars (S : Type u') {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semiring S] [module S M] [module R M] [has_smul S R] [is_scalar_tower S R M] (V : submodule R M) :

submodule S 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

submodule.restrict_scalars S V = {carrier := ↑V, add_mem' := _, zero_mem' := _, smul_mem' := _}

Instances for ↥submodule.restrict_scalars

source

@[simp]

theorem submodule.coe_restrict_scalars (S : Type u') {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semiring S] [module S M] [module R M] [has_smul S R] [is_scalar_tower S R M] (V : submodule R M) :

↑(submodule.restrict_scalars S V) = ↑V

source

@[simp]

theorem submodule.restrict_scalars_mem (S : Type u') {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semiring S] [module S M] [module R M] [has_smul S R] [is_scalar_tower S R M] (V : submodule R M) (m : M) :

m ∈ submodule.restrict_scalars S V ↔ m ∈ V

source

@[simp]

theorem submodule.restrict_scalars_self {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [module R M] (V : submodule R M) :

submodule.restrict_scalars R V = V

source

theorem submodule.restrict_scalars_injective (S : Type u') (R : Type u) (M : Type v) [semiring R] [add_comm_monoid M] [semiring S] [module S M] [module R M] [has_smul S R] [is_scalar_tower S R M] :

function.injective (submodule.restrict_scalars S)

source

@[simp]

theorem submodule.restrict_scalars_inj (S : Type u') (R : Type u) (M : Type v) [semiring R] [add_comm_monoid M] [semiring S] [module S M] [module R M] [has_smul S R] [is_scalar_tower S R M] {V₁ V₂ : submodule R M} :

submodule.restrict_scalars S V₁ = submodule.restrict_scalars S V₂ ↔ V₁ = V₂

source

@[protected, instance]

def submodule.restrict_scalars.orig_module (S : Type u') (R : Type u) (M : Type v) [semiring R] [add_comm_monoid M] [semiring S] [module S M] [module R M] [has_smul S R] [is_scalar_tower S R M] (p : submodule R M) :

module R ↥(submodule.restrict_scalars S p)

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

Equations

submodule.restrict_scalars.orig_module S R M p = p.module

source

@[protected, instance]

def submodule.restrict_scalars.is_scalar_tower (S : Type u') (R : Type u) (M : Type v) [semiring R] [add_comm_monoid M] [semiring S] [module S M] [module R M] [has_smul S R] [is_scalar_tower S R M] (p : submodule R M) :

is_scalar_tower S R ↥(submodule.restrict_scalars S p)

source

def submodule.restrict_scalars_embedding (S : Type u') (R : Type u) (M : Type v) [semiring R] [add_comm_monoid M] [semiring S] [module S M] [module R M] [has_smul S R] [is_scalar_tower S R M] :

submodule R M ↪o submodule S M

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

Equations

submodule.restrict_scalars_embedding S R M = {to_embedding := {to_fun := submodule.restrict_scalars S _inst_7, inj' := _}, map_rel_iff' := _}

source

@[simp]

theorem submodule.restrict_scalars_embedding_apply (S : Type u') (R : Type u) (M : Type v) [semiring R] [add_comm_monoid M] [semiring S] [module S M] [module R M] [has_smul S R] [is_scalar_tower S R M] (V : submodule R M) :

⇑(submodule.restrict_scalars_embedding S R M) V = submodule.restrict_scalars S V

source

def submodule.restrict_scalars_equiv (S : Type u') (R : Type u) (M : Type v) [semiring R] [add_comm_monoid M] [semiring S] [module S M] [module R M] [has_smul S R] [is_scalar_tower S R M] (p : submodule R M) :

↥(submodule.restrict_scalars S p) ≃ₗ[R] ↥p

Turning p : submodule R M into an S-submodule gives the same module structure as turning it into a type and adding a module structure.

Equations

submodule.restrict_scalars_equiv S R M p = {to_fun := id ↥(submodule.restrict_scalars S p), map_add' := _, map_smul' := _, inv_fun := id ↥p, left_inv := _, right_inv := _}

source

@[simp]

theorem submodule.restrict_scalars_equiv_apply (S : Type u') (R : Type u) (M : Type v) [semiring R] [add_comm_monoid M] [semiring S] [module S M] [module R M] [has_smul S R] [is_scalar_tower S R M] (p : submodule R M) (a : ↥(submodule.restrict_scalars S p)) :

⇑(submodule.restrict_scalars_equiv S R M p) a = a

source

@[simp]

theorem submodule.restrict_scalars_equiv_symm_apply (S : Type u') (R : Type u) (M : Type v) [semiring R] [add_comm_monoid M] [semiring S] [module S M] [module R M] [has_smul S R] [is_scalar_tower S R M] (p : submodule R M) (a : ↥p) :

⇑((submodule.restrict_scalars_equiv S R M p).symm) a = a

source

@[protected, instance]

def submodule.add_subgroup_class {R : Type u} {M : Type v} [ring R] [add_comm_group M] [module R M] :

add_subgroup_class (submodule R M) M

source

@[protected]

theorem submodule.neg_mem {R : Type u} {M : Type v} [ring R] [add_comm_group M] {module_M : module R M} (p : submodule R M) {x : M} (hx : x ∈ p) :

-x ∈ p

source

def submodule.to_add_subgroup {R : Type u} {M : Type v} [ring R] [add_comm_group M] {module_M : module R M} (p : submodule R M) :

add_subgroup M

Reinterpret a submodule as an additive subgroup.

Equations

p.to_add_subgroup = {carrier := p.to_add_submonoid.carrier, add_mem' := _, zero_mem' := _, neg_mem' := _}

source

@[simp]

theorem submodule.coe_to_add_subgroup {R : Type u} {M : Type v} [ring R] [add_comm_group M] {module_M : module R M} (p : submodule R M) :

↑(p.to_add_subgroup) = ↑p

source

@[simp]

theorem submodule.mem_to_add_subgroup {R : Type u} {M : Type v} [ring R] [add_comm_group M] {module_M : module R M} (p : submodule R M) {x : M} :

x ∈ p.to_add_subgroup ↔ x ∈ p

source

theorem submodule.to_add_subgroup_injective {R : Type u} {M : Type v} [ring R] [add_comm_group M] {module_M : module R M} :

function.injective submodule.to_add_subgroup

source

@[simp]

theorem submodule.to_add_subgroup_eq {R : Type u} {M : Type v} [ring R] [add_comm_group M] {module_M : module R M} (p p' : submodule R M) :

p.to_add_subgroup = p'.to_add_subgroup ↔ p = p'

source

theorem submodule.to_add_subgroup_strict_mono {R : Type u} {M : Type v} [ring R] [add_comm_group M] {module_M : module R M} :

strict_mono submodule.to_add_subgroup

source

theorem submodule.to_add_subgroup_le {R : Type u} {M : Type v} [ring R] [add_comm_group M] {module_M : module R M} (p p' : submodule R M) :

p.to_add_subgroup ≤ p'.to_add_subgroup ↔ p ≤ p'

source

theorem submodule.to_add_subgroup_mono {R : Type u} {M : Type v} [ring R] [add_comm_group M] {module_M : module R M} :

monotone submodule.to_add_subgroup

source

@[protected]

theorem submodule.sub_mem {R : Type u} {M : Type v} [ring R] [add_comm_group M] {module_M : module R M} (p : submodule R M) {x y : M} :

x ∈ p → y ∈ p → x - y ∈ p

source

@[protected]

theorem submodule.neg_mem_iff {R : Type u} {M : Type v} [ring R] [add_comm_group M] {module_M : module R M} (p : submodule R M) {x : M} :

-x ∈ p ↔ x ∈ p

source

@[protected]

theorem submodule.add_mem_iff_left {R : Type u} {M : Type v} [ring R] [add_comm_group M] {module_M : module R M} (p : submodule R M) {x y : M} :

y ∈ p → (x + y ∈ p ↔ x ∈ p)

source

@[protected]

theorem submodule.add_mem_iff_right {R : Type u} {M : Type v} [ring R] [add_comm_group M] {module_M : module R M} (p : submodule R M) {x y : M} :

x ∈ p → (x + y ∈ p ↔ y ∈ p)

source

@[protected]

theorem submodule.coe_neg {R : Type u} {M : Type v} [ring R] [add_comm_group M] {module_M : module R M} (p : submodule R M) (x : ↥p) :

↑-x = -↑x

source

@[protected]

theorem submodule.coe_sub {R : Type u} {M : Type v} [ring R] [add_comm_group 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] [add_comm_group 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] [add_comm_group M] {module_M : module R M} (p : submodule R M) {x y : M} (hx : x ∈ p) :

x - y ∈ p ↔ y ∈ p

source

@[protected, instance]

def submodule.add_comm_group {R : Type u} {M : Type v} [ring R] [add_comm_group M] {module_M : module R M} (p : submodule R M) :

add_comm_group ↥p

Equations

p.add_comm_group = {add := has_add.add p.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := add_comm_group.nsmul p.to_add_subgroup.to_add_comm_group, nsmul_zero' := _, nsmul_succ' := _, neg := has_neg.neg add_subgroup_class.has_neg, sub := add_comm_group.sub p.to_add_subgroup.to_add_comm_group, sub_eq_add_neg := _, zsmul := add_comm_group.zsmul p.to_add_subgroup.to_add_comm_group, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _}

source

theorem submodule.not_mem_of_ortho {R : Type u} {M : Type v} [ring R] [is_domain R] [add_comm_group M] [module R M] {x : M} {N : submodule R M} (ortho : ∀ (c : R) (y : M), y ∈ N → c • x + y = 0 → c = 0) :

x ∉ N

source

theorem submodule.ne_zero_of_ortho {R : Type u} {M : Type v} [ring R] [is_domain R] [add_comm_group M] [module R M] {x : M} {N : submodule R M} (ortho : ∀ (c : R) (y : M), y ∈ N → c • x + y = 0 → c = 0) :

x ≠ 0

source

@[protected, instance]

def submodule.to_ordered_add_comm_monoid {R : Type u} [semiring R] {M : Type u_1} [ordered_add_comm_monoid M] [module R M] (S : submodule R M) :

ordered_add_comm_monoid ↥S

A submodule of an ordered_add_comm_monoid is an ordered_add_comm_monoid.

Equations

S.to_ordered_add_comm_monoid = function.injective.ordered_add_comm_monoid coe _ _ _ _

source

@[protected, instance]

def submodule.to_linear_ordered_add_comm_monoid {R : Type u} [semiring R] {M : Type u_1} [linear_ordered_add_comm_monoid M] [module R M] (S : submodule R M) :

linear_ordered_add_comm_monoid ↥S

A submodule of a linear_ordered_add_comm_monoid is a linear_ordered_add_comm_monoid.

Equations

S.to_linear_ordered_add_comm_monoid = function.injective.linear_ordered_add_comm_monoid coe _ _ _ _ _ _

source

@[protected, instance]

def submodule.to_ordered_cancel_add_comm_monoid {R : Type u} [semiring R] {M : Type u_1} [ordered_cancel_add_comm_monoid M] [module R M] (S : submodule R M) :

ordered_cancel_add_comm_monoid ↥S

A submodule of an ordered_cancel_add_comm_monoid is an ordered_cancel_add_comm_monoid.

Equations

S.to_ordered_cancel_add_comm_monoid = function.injective.ordered_cancel_add_comm_monoid coe _ _ _ _

source

@[protected, instance]

def submodule.to_linear_ordered_cancel_add_comm_monoid {R : Type u} [semiring R] {M : Type u_1} [linear_ordered_cancel_add_comm_monoid M] [module R M] (S : submodule R M) :

linear_ordered_cancel_add_comm_monoid ↥S

A submodule of a linear_ordered_cancel_add_comm_monoid is a linear_ordered_cancel_add_comm_monoid.

Equations

S.to_linear_ordered_cancel_add_comm_monoid = function.injective.linear_ordered_cancel_add_comm_monoid coe _ _ _ _ _ _

source

@[protected, instance]

def submodule.to_ordered_add_comm_group {R : Type u} [ring R] {M : Type u_1} [ordered_add_comm_group M] [module R M] (S : submodule R M) :

ordered_add_comm_group ↥S

A submodule of an ordered_add_comm_group is an ordered_add_comm_group.

Equations

S.to_ordered_add_comm_group = function.injective.ordered_add_comm_group coe _ _ _ _ _ _ _

source

@[protected, instance]

def submodule.to_linear_ordered_add_comm_group {R : Type u} [ring R] {M : Type u_1} [linear_ordered_add_comm_group M] [module R M] (S : submodule R M) :

linear_ordered_add_comm_group ↥S

A submodule of a linear_ordered_add_comm_group is a linear_ordered_add_comm_group.

Equations

S.to_linear_ordered_add_comm_group = function.injective.linear_ordered_add_comm_group coe _ _ _ _ _ _ _ _ _

source

theorem submodule.smul_mem_iff {S : Type u'} {R : Type u} {M : Type v} [division_ring S] [semiring R] [add_comm_monoid M] [module R M] [has_smul S R] [module S M] [is_scalar_tower S R M] (p : submodule R M) {s : S} {x : M} (s0 : s ≠ 0) :

s • x ∈ p ↔ x ∈ p

source

@[reducible]

def subspace (R : Type u) (M : Type v) [division_ring R] [add_comm_group M] [module R M] :

Type v

Subspace of a vector space. Defined to equal submodule.

mathlib documentation

Submodules of a module #

Tags #