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 : Type v

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

  The carrier set is closed under scalar multiplication.

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.

@[reducible]

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

Reinterpret a Submodule as a SubMulAction.

Equations

• Submodule.toSubMulAction self = { carrier := self.carrier, smul_mem' := (_ : ∀ (c : R) {x : M}, x ∈ self.carrier → c • x ∈ self.carrier) }

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

Equations

• Submodule.setLike = { coe := fun s => s.carrier, coe_injective' := (_ : ∀ (p q : Submodule R M), (fun s => s.carrier) p = (fun s => s.carrier) q → p = q) }

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

Equations

• @Submodule.addSubmonoidClass = @Submodule.addSubmonoidClass.proof_1

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

Equations

• @Submodule.smulMemClass = @Submodule.smulMemClass.proof_1

@[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.carrier → c • 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.carrier → c • 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.carrier → c • 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.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'

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) : Submodule R M

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.

@[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_eq {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] {p : Submodule R M} {q : Submodule R M} : Submodule.toSubMulAction p = Submodule.toSubMulAction q ↔ p = q

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) : ↑(Submodule.toSubMulAction p) = ↑p

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 { x // x ∈ S' }

A submodule of a Module is a Module.

Equations

• SMulMemClass.toModule S' = Function.Injective.module R (AddSubmonoidClass.subtype S') (_ : Function.Injective fun a => ↑a) (_ : ∀ (r : R) (x : { x // x ∈ S' }), ↑(r • x) = r • ↑x)

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' { x // x ∈ 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

• SMulMemClass.toModule' S R' R A s = SMulMemClass.toModule s

def SMulMemClass.subtype {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) : { x // x ∈ S' } →ₗ[R] M

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

Equations

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

@[simp]

theorem SMulMemClass.coeSubtype {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) : ↑(SMulMemClass.subtype S') = Subtype.val

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} : (∀ (c : ι), c ∈ t → 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 : ∀ (c : ι), c ∈ t → 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 { x // x ∈ p }

Equations

• Submodule.add p = { add := fun x y => { 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 { x // x ∈ p }

Equations

• Submodule.zero p = { zero := { val := 0, property := (_ : 0 ∈ p) } }

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

Equations

• Submodule.inhabited p = { 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 { x // x ∈ p }

Equations

• Submodule.smul p = { smul := fun c x => { val := c • ↑x, property := (_ : c • ↑x ∈ p) } }

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 { x // x ∈ p }

Equations

• @Submodule.isScalarTower = @Submodule.isScalarTower.proof_1

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' { x // x ∈ p }

Equations

• @Submodule.isScalarTower' = @Submodule.isScalarTower'.proof_1

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] : IsCentralScalar S { x // x ∈ p }

Equations

• @Submodule.isCentralScalar = @Submodule.isCentralScalar.proof_1

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

@[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 : { x // 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 : { x // x ∈ p }) (y : { x // x ∈ 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 : { x // 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 : { x // 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 : { x // 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) : AddCommMonoid { x // x ∈ p }

Equations

• Submodule.addCommMonoid p = let src := AddSubmonoid.toAddCommMonoid p.toAddSubmonoid; AddCommMonoid.mk (_ : ∀ (a b : { x // x ∈ p.toAddSubmonoid }), a + b = b + a)

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 { x // x ∈ 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 { x // x ∈ p }

Equations

• Submodule.module p = Submodule.module' p

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] : NoZeroSMulDivisors R { x // x ∈ p }

Equations

• @Submodule.noZeroSMulDivisors = @Submodule.noZeroSMulDivisors.proof_1

def Submodule.subtype {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) : { x // x ∈ p } →ₗ[R] M

Embedding of a submodule p to the ambient space M.

Equations

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

theorem Submodule.subtype_apply {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) (x : { x // x ∈ p }) : ↑(Submodule.subtype p) x = ↑x

@[simp]

theorem Submodule.coeSubtype {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) : ↑(Submodule.subtype p) = Subtype.val

theorem Submodule.injective_subtype {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) : Function.Injective ↑(Submodule.subtype p)

theorem Submodule.coe_sum {R : Type u} {M : Type v} {ι : Type w} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) (x : ι → { x // x ∈ p }) (s : Finset ι) : ↑(Finset.sum s fun i => x i) = Finset.sum s fun i => ↑(x i)

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

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 add_group.to_add_action, enabling s +ᵥ m as an alias for ↑s + m.

instance Submodule.instVAddSubtypeMemSubmoduleInstMembershipSetLike {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) {α : Type u_1} [VAdd M α] : VAdd { x // x ∈ p } α

Equations

• Submodule.instVAddSubtypeMemSubmoduleInstMembershipSetLike p = AddSubmonoid.vadd p.toAddSubmonoid

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 { x // x ∈ p } α β

Equations

• @Submodule.vaddCommClass = @Submodule.vaddCommClass.proof_1

instance Submodule.instFaithfulVAddSubtypeMemSubmoduleInstMembershipSetLikeInstVAddSubtypeMemSubmoduleInstMembershipSetLike {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) {α : Type u_1} [VAdd M α] [FaithfulVAdd M α] : FaithfulVAdd { x // x ∈ p } α

Equations

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

instance Submodule.instAddActionSubtypeMemSubmoduleInstMembershipSetLikeToAddMonoidToAddMonoidToAddSubmonoid {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) {α : Type u_1} [AddAction M α] : AddAction { x // x ∈ p } α

The action by a submodule is the action by the underlying module.

Equations

• Submodule.instAddActionSubtypeMemSubmoduleInstMembershipSetLikeToAddMonoidToAddMonoidToAddSubmonoid p = AddAction.compHom α (LinearMap.toAddMonoidHom (Submodule.subtype p))

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 : { x // x ∈ 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) : 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

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

@[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) : ↑(Submodule.restrictScalars S V) = ↑V

@[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) : m ∈ Submodule.restrictScalars S V ↔ m ∈ V

@[simp]

theorem Submodule.restrictScalars_self {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] (V : Submodule R M) : Submodule.restrictScalars R V = V

theorem Submodule.restrictScalars_injective (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] : Function.Injective (Submodule.restrictScalars S)

@[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} : Submodule.restrictScalars S V₁ = Submodule.restrictScalars S V₂ ↔ V₁ = V₂

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) : Module R { x // x ∈ Submodule.restrictScalars S p }

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

Equations

• Submodule.restrictScalars.origModule S R M p = inferInstance

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) : IsScalarTower S R { x // x ∈ Submodule.restrictScalars S p }

Equations

• Submodule.restrictScalars.isScalarTower = Submodule.restrictScalars.isScalarTower.proof_1

@[simp]

theorem Submodule.restrictScalarsEmbedding_apply (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) : ↑(Submodule.restrictScalarsEmbedding S R M) V = Submodule.restrictScalars S V

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] : Submodule R M ↪o Submodule S 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.

@[simp]

theorem Submodule.restrictScalarsEquiv_symm_apply (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) : ∀ (a : { x // x ∈ p }), ↑(LinearEquiv.symm (Submodule.restrictScalarsEquiv S R M p)) a = a

@[simp]

theorem Submodule.restrictScalarsEquiv_apply (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) : ∀ (a : { x // x ∈ p }), ↑(Submodule.restrictScalarsEquiv S R M p) a = a

def Submodule.restrictScalarsEquiv (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) : { x // x ∈ Submodule.restrictScalars S p } ≃ₗ[R] { x // x ∈ 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

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

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

Equations

• @Submodule.addSubgroupClass = @Submodule.addSubgroupClass.proof_1

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

Reinterpret a submodule as an additive subgroup.

Equations

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

@[simp]

theorem Submodule.coe_toAddSubgroup {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] {module_M : Module R M} (p : Submodule R M) : ↑(Submodule.toAddSubgroup p) = ↑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 ∈ Submodule.toAddSubgroup p ↔ 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 : Submodule R M) (p' : Submodule R M) : Submodule.toAddSubgroup p = Submodule.toAddSubgroup p' ↔ p = p'

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) : Submodule.toAddSubgroup p ≤ Submodule.toAddSubgroup p' ↔ p ≤ p'

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 ∈ p → y ∈ p → x - 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 : { x // 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 : { x // x ∈ p }) (y : { x // x ∈ 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) : AddCommGroup { x // x ∈ p }

Equations

• Submodule.addCommGroup p = let src := AddSubgroup.toAddCommGroup (Submodule.toAddSubgroup p); AddCommGroup.mk (_ : ∀ (a b : { x // x ∈ Submodule.toAddSubgroup p }), a + b = b + a)

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) (y : M), y ∈ N → c • x + y = 0 → c = 0) : ¬x ∈ N

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) (y : M), y ∈ N → c • x + y = 0 → c = 0) : x ≠ 0

instance Submodule.toOrderedAddCommMonoid {R : Type u} [Semiring R] {M : Type u_1} [OrderedAddCommMonoid M] [Module R M] (S : Submodule R M) : OrderedAddCommMonoid { x // x ∈ S }

A submodule of an OrderedAddCommMonoid is an OrderedAddCommMonoid.

Equations

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

instance Submodule.toLinearOrderedAddCommMonoid {R : Type u} [Semiring R] {M : Type u_1} [LinearOrderedAddCommMonoid M] [Module R M] (S : Submodule R M) : LinearOrderedAddCommMonoid { x // x ∈ S }

A submodule of a LinearOrderedAddCommMonoid is a LinearOrderedAddCommMonoid.

Equations

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

instance Submodule.toOrderedCancelAddCommMonoid {R : Type u} [Semiring R] {M : Type u_1} [OrderedCancelAddCommMonoid M] [Module R M] (S : Submodule R M) : OrderedCancelAddCommMonoid { x // x ∈ S }

A submodule of an OrderedCancelAddCommMonoid is an OrderedCancelAddCommMonoid.

Equations

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

instance Submodule.toLinearOrderedCancelAddCommMonoid {R : Type u} [Semiring R] {M : Type u_1} [LinearOrderedCancelAddCommMonoid M] [Module R M] (S : Submodule R M) : LinearOrderedCancelAddCommMonoid { x // x ∈ S }

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) : OrderedAddCommGroup { x // x ∈ S }

A submodule of an OrderedAddCommGroup is an OrderedAddCommGroup.

Equations

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

instance Submodule.toLinearOrderedAddCommGroup {R : Type u} [Ring R] {M : Type u_1} [LinearOrderedAddCommGroup M] [Module R M] (S : Submodule R M) : LinearOrderedAddCommGroup { x // x ∈ S }

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] : Type v

Subspace of a vector space. Defined to equal Submodule.

Equations

• Subspace R M = Submodule R M