# Documentation

Mathlib.Algebra.Module.Submodule.LinearMap

# Linear maps involving submodules of a module #

In this file we define a number of linear maps involving submodules of a module.

## Main declarations #

• Submodule.subtype: Embedding of a submodule p to the ambient space M as a Submodule.
• LinearMap.domRestrict: The restriction of a semilinear map f : M → M₂ to a submodule p ⊆ M as a semilinear map p → M₂.
• LinearMap.restrict: The restriction of a linear map f : M → M₁ to a submodule p ⊆ M and q ⊆ M₁ (if q contains the codomain).
• Submodule.inclusion: the inclusion p ⊆ p' of submodules p and p' as a linear map.

## Tags #

submodule, subspace, linear map

def SMulMemClass.subtype {R : Type u} {M : Type v} [] [] [Module R M] {A : Type u_1} [SetLike A M] [] [SMulMemClass A R M] (S' : A) :
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.
Instances For
@[simp]
theorem SMulMemClass.coeSubtype {R : Type u} {M : Type v} [] [] [Module R M] {A : Type u_1} [SetLike A M] [] [SMulMemClass A R M] (S' : A) :
() = Subtype.val
def Submodule.subtype {R : Type u} {M : Type v} [] [] {module_M : Module R M} (p : ) :
p →ₗ[R] M

Embedding of a submodule p to the ambient space M.

Equations
• = { toAddHom := { toFun := Subtype.val, map_add' := (_ : ∀ (a a_1 : p), a + a_1 = a + a_1) }, map_smul' := (_ : ∀ (a : R) (a_1 : p), a a_1 = a a_1) }
Instances For
theorem Submodule.subtype_apply {R : Type u} {M : Type v} [] [] {module_M : Module R M} (p : ) (x : p) :
x = x
@[simp]
theorem Submodule.coeSubtype {R : Type u} {M : Type v} [] [] {module_M : Module R M} (p : ) :
= Subtype.val
theorem Submodule.injective_subtype {R : Type u} {M : Type v} [] [] {module_M : Module R M} (p : ) :
theorem Submodule.coe_sum {R : Type u} {M : Type v} {ι : Type w} [] [] {module_M : Module R M} (p : ) (x : ιp) (s : ) :
(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.

instance Submodule.instAddActionSubtypeMemSubmoduleInstMembershipSetLikeToAddMonoidToAddMonoidToAddSubmonoid {R : Type u} {M : Type v} [] [] {module_M : Module R M} (p : ) {α : Type u_1} [] :

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

Equations
@[simp]
theorem Submodule.restrictScalarsEquiv_symm_apply (S : Type u') (R : Type u) (M : Type v) [] [] [] [Module S M] [Module R M] [SMul S R] [] (p : ) :
∀ (a : p), () a = a
@[simp]
theorem Submodule.restrictScalarsEquiv_apply (S : Type u') (R : Type u) (M : Type v) [] [] [] [Module S M] [Module R M] [SMul S R] [] (p : ) :
∀ (a : p), () a = a
def Submodule.restrictScalarsEquiv (S : Type u') (R : Type u) (M : Type v) [] [] [] [Module S M] [Module R M] [SMul S R] [] (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
• One or more equations did not get rendered due to their size.
Instances For
def LinearMap.domRestrict {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} (f : M →ₛₗ[σ₁₂] M₂) (p : ) :
p →ₛₗ[σ₁₂] M₂

The restriction of a linear map f : M → M₂ to a submodule p ⊆ M gives a linear map p → M₂.

Equations
Instances For
@[simp]
theorem LinearMap.domRestrict_apply {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} (f : M →ₛₗ[σ₁₂] M₂) (p : ) (x : p) :
() x = f x
def LinearMap.codRestrict {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} (p : Submodule R₂ M₂) (f : M →ₛₗ[σ₁₂] M₂) (h : ∀ (c : M), f c p) :
M →ₛₗ[σ₁₂] p

A linear map f : M₂ → M whose values lie in a submodule p ⊆ M can be restricted to a linear map M₂ → p.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem LinearMap.codRestrict_apply {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} (p : Submodule R₂ M₂) (f : M →ₛₗ[σ₁₂] M₂) {h : ∀ (c : M), f c p} (x : M) :
(() x) = f x
@[simp]
theorem LinearMap.comp_codRestrict {R : Type u_1} {R₂ : Type u_3} {R₃ : Type u_4} {M : Type u_5} {M₂ : Type u_7} {M₃ : Type u_8} [] [Semiring R₂] [Semiring R₃] [] [] [] [Module R M] [Module R₂ M₂] [Module R₃ M₃] {σ₁₂ : R →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (f : M →ₛₗ[σ₁₂] M₂) (g : M₂ →ₛₗ[σ₂₃] M₃) (p : Submodule R₃ M₃) (h : ∀ (b : M₂), g b p) :
LinearMap.comp () f = LinearMap.codRestrict p () (_ : ∀ (x : M), g (f x) p)
@[simp]
theorem LinearMap.subtype_comp_codRestrict {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} (f : M →ₛₗ[σ₁₂] M₂) (p : Submodule R₂ M₂) (h : ∀ (b : M), f b p) :
= f
def LinearMap.restrict {R : Type u_1} {M : Type u_5} {M₁ : Type u_6} [] [] [] [Module R M] [Module R M₁] (f : M →ₗ[R] M₁) {p : } {q : Submodule R M₁} (hf : xp, f x q) :
p →ₗ[R] q

Restrict domain and codomain of a linear map.

Equations
Instances For
@[simp]
theorem LinearMap.restrict_coe_apply {R : Type u_1} {M : Type u_5} {M₁ : Type u_6} [] [] [] [Module R M] [Module R M₁] (f : M →ₗ[R] M₁) {p : } {q : Submodule R M₁} (hf : xp, f x q) (x : p) :
(() x) = f x
theorem LinearMap.restrict_apply {R : Type u_1} {M : Type u_5} {M₁ : Type u_6} [] [] [] [Module R M] [Module R M₁] {f : M →ₗ[R] M₁} {p : } {q : Submodule R M₁} (hf : xp, f x q) (x : p) :
() x = { val := f x, property := (_ : f x q) }
theorem LinearMap.restrict_comp {R : Type u_1} {M : Type u_5} [] [] [Module R M] {M₂ : Type u_10} {M₃ : Type u_11} [] [] [Module R M₂] [Module R M₃] {p : } {p₂ : Submodule R M₂} {p₃ : Submodule R M₃} {f : M →ₗ[R] M₂} {g : M₂ →ₗ[R] M₃} (hf : Set.MapsTo f p p₂) (hg : Set.MapsTo g p₂ p₃) (hfg : optParam (Set.MapsTo () p p₃) (_ : Set.MapsTo (g fun (x : M) => f x) p p₃)) :
theorem LinearMap.restrict_commute {R : Type u_1} {M : Type u_5} [] [] [Module R M] {f : M →ₗ[R] M} {g : M →ₗ[R] M} (h : Commute f g) {p : } (hf : Set.MapsTo f p p) (hg : Set.MapsTo g p p) :
Commute () ()
theorem LinearMap.subtype_comp_restrict {R : Type u_1} {M : Type u_5} {M₁ : Type u_6} [] [] [] [Module R M] [Module R M₁] {f : M →ₗ[R] M₁} {p : } {q : Submodule R M₁} (hf : xp, f x q) :
theorem LinearMap.restrict_eq_codRestrict_domRestrict {R : Type u_1} {M : Type u_5} {M₁ : Type u_6} [] [] [] [Module R M] [Module R M₁] {f : M →ₗ[R] M₁} {p : } {q : Submodule R M₁} (hf : xp, f x q) :
= LinearMap.codRestrict q () (_ : ∀ (x : p), f x q)
theorem LinearMap.restrict_eq_domRestrict_codRestrict {R : Type u_1} {M : Type u_5} {M₁ : Type u_6} [] [] [] [Module R M] [Module R M₁] {f : M →ₗ[R] M₁} {p : } {q : Submodule R M₁} (hf : ∀ (x : M), f x q) :
LinearMap.restrict f (_ : xp, f x q) =
instance LinearMap.uniqueOfLeft {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [] :
Unique (M →ₛₗ[σ₁₂] M₂)
Equations
instance LinearMap.uniqueOfRight {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [] :
Unique (M →ₛₗ[σ₁₂] M₂)
Equations
@[simp]
theorem LinearMap.evalAddMonoidHom_apply {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} (a : M) (f : M →ₛₗ[σ₁₂] M₂) :
= f a
def LinearMap.evalAddMonoidHom {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} (a : M) :
(M →ₛₗ[σ₁₂] M₂) →+ M₂

Evaluation of a σ₁₂-linear map at a fixed a, as an AddMonoidHom.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem LinearMap.toAddMonoidHom'_apply {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} (f : M →ₛₗ[σ₁₂] M₂) :
def LinearMap.toAddMonoidHom' {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} :
(M →ₛₗ[σ₁₂] M₂) →+ M →+ M₂

LinearMap.toAddMonoidHom promoted to an AddMonoidHom.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem LinearMap.sum_apply {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} {ι : Type u_9} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} (t : ) (f : ιM →ₛₗ[σ₁₂] M₂) (b : M) :
(Finset.sum t fun (d : ι) => f d) b = Finset.sum t fun (d : ι) => (f d) b
instance LinearMap.instNontrivialEnd {R : Type u_1} {M : Type u_5} [] [] [Module R M] [] :
Equations
@[simp]
theorem LinearMap.coeFn_sum {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {ι : Type u_10} (t : ) (f : ιM →ₛₗ[σ₁₂] M₂) :
(Finset.sum t fun (i : ι) => f i) = Finset.sum t fun (i : ι) => (f i)
theorem LinearMap.submodule_pow_eq_zero_of_pow_eq_zero {R : Type u_1} {M : Type u_5} [] [] [Module R M] {N : } {g : Module.End R N} {G : } (h : ) {k : } (hG : G ^ k = 0) :
g ^ k = 0
theorem LinearMap.pow_apply_mem_of_forall_mem {R : Type u_1} {M : Type u_5} [] [] [Module R M] {f' : M →ₗ[R] M} {p : } (n : ) (h : xp, f' x p) (x : M) (hx : x p) :
(f' ^ n) x p
theorem LinearMap.pow_restrict {R : Type u_1} {M : Type u_5} [] [] [Module R M] {f' : M →ₗ[R] M} {p : } (n : ) (h : xp, f' x p) (h' : optParam (xp, (f' ^ n) x p) (_ : xp, (f' ^ n) x p)) :
^ n = LinearMap.restrict (f' ^ n) h'
def LinearMap.domRestrict' {R : Type u_1} {M : Type u_5} {M₂ : Type u_7} [] [] [] [Module R M] [Module R M₂] (p : ) :
(M →ₗ[R] M₂) →ₗ[R] p →ₗ[R] M₂

Alternative version of domRestrict as a linear map.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem LinearMap.domRestrict'_apply {R : Type u_1} {M : Type u_5} {M₂ : Type u_7} [] [] [] [Module R M] [Module R M₂] (f : M →ₗ[R] M₂) (p : ) (x : p) :
() x = f x
def Submodule.inclusion {R : Type u_1} {M : Type u_2} [] [] [Module R M] {p : } {p' : } (h : p p') :
p →ₗ[R] p'

If two submodules p and p' satisfy p ⊆ p', then inclusion p p' is the linear map version of this inclusion.

Equations
Instances For
@[simp]
theorem Submodule.coe_inclusion {R : Type u_1} {M : Type u_2} [] [] [Module R M] {p : } {p' : } (h : p p') (x : p) :
( x) = x
theorem Submodule.inclusion_apply {R : Type u_1} {M : Type u_2} [] [] [Module R M] {p : } {p' : } (h : p p') (x : p) :
x = { val := x, property := (_ : x p') }
theorem Submodule.inclusion_injective {R : Type u_1} {M : Type u_2} [] [] [Module R M] {p : } {p' : } (h : p p') :
theorem Submodule.subtype_comp_inclusion {R : Type u_1} {M : Type u_2} [] [] [Module R M] (p : ) (q : ) (h : p q) :