Submodules of a module #
This file contains basic results on submodules that require further theory to be defined. As such it is a good target for organizing and splitting further.
Tags #
submodule, subspace, linear map
theorem
Submodule.toAddSubmonoid_strictMono
{R : Type u}
{M : Type v}
[Semiring R]
[AddCommMonoid M]
[Module R M]
:
theorem
Submodule.toAddSubmonoid_le
{R : Type u}
{M : Type v}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{p q : Submodule R M}
:
theorem
Submodule.toAddSubmonoid_mono
{R : Type u}
{M : Type v}
[Semiring R]
[AddCommMonoid M]
[Module R M]
:
theorem
Submodule.toSubMulAction_strictMono
{R : Type u}
{M : Type v}
[Semiring R]
[AddCommMonoid M]
[Module R M]
:
theorem
Submodule.toSubMulAction_mono
{R : Type u}
{M : Type v}
[Semiring R]
[AddCommMonoid M]
[Module R M]
:
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 ↥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 ↥p
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 AddGroup.toAddAction, enabling
s +ᵥ m as an alias for ↑s + m.
instance
Submodule.instVAddSubtypeMem
{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 (↥p) α
Equations
- p.instVAddSubtypeMem = p.vadd
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 (↥p) α β
instance
Submodule.instFaithfulVAddSubtypeMem
{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 (↥p) α
theorem
Submodule.toAddSubgroup_strictMono
{R : Type u}
{M : Type v}
[Ring R]
[AddCommGroup M]
{module_M : Module R M}
:
theorem
Submodule.toAddSubgroup_le
{R : Type u}
{M : Type v}
[Ring R]
[AddCommGroup M]
{module_M : Module R M}
(p p' : Submodule R M)
:
theorem
Submodule.toAddSubgroup_mono
{R : Type u}
{M : Type v}
[Ring R]
[AddCommGroup M]
{module_M : Module R M}
:
theorem
GCongr.Submodule.toAddSubgroup_le
{R : Type u}
{M : Type v}
[Ring R]
[AddCommGroup M]
{module_M : Module R M}
(p p' : Submodule R M)
:
p ≤ p' → p.toAddSubgroup ≤ p'.toAddSubgroup
Alias of the reverse direction of Submodule.toAddSubgroup_le.
theorem
Submodule.neg_coe
{R : Type u}
{M : Type v}
[Ring R]
[AddCommGroup M]
{module_M : Module R M}
(p : Submodule R M)
:
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)
: