Submodules of a module #
In this file we define
Submodule R M
: a subset of aModule
M
that contains zero and is closed with respect to addition and scalar multiplication.Subspace k M
: an abbreviation forSubmodule
assuming thatk
is aField
.
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.
Instances For
theorem
Submodule.addSubmonoidClass
{R : Type u}
{M : Type v}
[Semiring R]
[AddCommMonoid M]
[Module R M]
:
AddSubmonoidClass (Submodule R M) M
theorem
Submodule.smulMemClass
{R : Type u}
{M : Type v}
[Semiring R]
[AddCommMonoid M]
[Module R M]
:
SMulMemClass (Submodule R M) R M
@[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)
:
@[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.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)
:
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
- p.copy s hs = { carrier := s, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
Instances For
theorem
Submodule.toAddSubmonoid_injective
{R : Type u}
{M : Type v}
[Semiring R]
[AddCommMonoid M]
[Module R M]
:
Function.Injective 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
@[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
- SMulMemClass.toModule' S R' R A s = SMulMemClass.toModule s
Instances For
@[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.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)
:
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)
:
Inhabited ↥p
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
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.coe_zero
{R : Type u}
{M : Type v}
[Semiring R]
[AddCommMonoid M]
{module_M : Module R M}
{p : Submodule R M}
:
↑0 = 0
@[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)
:
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
- p.addCommMonoid = AddCommMonoid.mk ⋯
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.addSubgroupClass
{R : Type u}
{M : Type v}
[Ring R]
[AddCommGroup M]
[Module R M]
:
AddSubgroupClass (Submodule R M) M
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
theorem
Submodule.toAddSubgroup_injective
{R : Type u}
{M : Type v}
[Ring R]
[AddCommGroup M]
{module_M : Module R M}
:
Function.Injective Submodule.toAddSubgroup
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
- p.addCommGroup = AddCommGroup.mk ⋯
@[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
- SubmoduleClass.module' t = Module.mk ⋯ ⋯
@[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