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 #

Tags #

submodule, subspace, linear map

source
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) :
↥S' →ₗ[R] M

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

Equations
source
@[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
source
def Submodule.subtype {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) :
↥p →ₗ[R] M

Embedding of a submodule p to the ambient space M.

Equations
  • Submodule.subtype p = { toAddHom := { toFun := Subtype.val, map_add' := ⋯ }, map_smul' := ⋯ }
source
theorem Submodule.subtype_apply {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) (x : ↥p) :
(Submodule.subtype p) x = ↑x
source
@[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
source
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)
source
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 : ι → ↥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.

source
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 (↥p) α

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

Equations
source
def LinearMap.domRestrict {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} (f : M →ₛₗ[σ₁₂] M₂) (p : Submodule R M) :
↥p →ₛₗ[σ₁₂] M₂

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

Equations
source
@[simp]
theorem LinearMap.domRestrict_apply {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} (f : M →ₛₗ[σ₁₂] M₂) (p : Submodule R M) (x : ↥p) :
(LinearMap.domRestrict f p) x = f ↑x
source
def LinearMap.codRestrict {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [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
  • LinearMap.codRestrict p f h = { toAddHom := { toFun := fun (c : M) => { val := f c, property := ⋯ }, map_add' := ⋯ }, map_smul' := ⋯ }
source
@[simp]
theorem LinearMap.codRestrict_apply {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} (p : Submodule R₂ M₂) (f : M →ₛₗ[σ₁₂] M₂) {h : ∀ (c : M), f c ∈ p} (x : M) :
↑((LinearMap.codRestrict p f h) x) = f x
source
@[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₂] [Semiring R₃] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [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 (LinearMap.codRestrict p g h) f = LinearMap.codRestrict p (LinearMap.comp g f) ⋯
source
@[simp]
theorem LinearMap.subtype_comp_codRestrict {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} (f : M →ₛₗ[σ₁₂] M₂) (p : Submodule R₂ M₂) (h : ∀ (b : M), f b ∈ p) :
LinearMap.comp (Submodule.subtype p) (LinearMap.codRestrict p f h) = f
source
def LinearMap.restrict {R : Type u_1} {M : Type u_5} {M₁ : Type u_6} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₁] [Module R M] [Module R M₁] (f : M →ₗ[R] M₁) {p : Submodule R M} {q : Submodule R M₁} (hf : ∀ x ∈ p, f x ∈ q) :
↥p →ₗ[R] ↥q

Restrict domain and codomain of a linear map.

Equations
source
@[simp]
theorem LinearMap.restrict_coe_apply {R : Type u_1} {M : Type u_5} {M₁ : Type u_6} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₁] [Module R M] [Module R M₁] (f : M →ₗ[R] M₁) {p : Submodule R M} {q : Submodule R M₁} (hf : ∀ x ∈ p, f x ∈ q) (x : ↥p) :
↑((LinearMap.restrict f hf) x) = f ↑x
source
theorem LinearMap.restrict_apply {R : Type u_1} {M : Type u_5} {M₁ : Type u_6} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₁] [Module R M] [Module R M₁] {f : M →ₗ[R] M₁} {p : Submodule R M} {q : Submodule R M₁} (hf : ∀ x ∈ p, f x ∈ q) (x : ↥p) :
(LinearMap.restrict f hf) x = { val := f ↑x, property := ⋯ }
source
theorem LinearMap.restrict_comp {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {M₂ : Type u_10} {M₃ : Type u_11} [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M₂] [Module R M₃] {p : Submodule R M} {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 ⇑(g ∘ₗ f) ↑p ↑p₃) ⋯) :
LinearMap.restrict (g ∘ₗ f) hfg = LinearMap.restrict g hg ∘ₗ LinearMap.restrict f hf
source
theorem LinearMap.restrict_commute {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {f : M →ₗ[R] M} {g : M →ₗ[R] M} (h : Commute f g) {p : Submodule R M} (hf : Set.MapsTo ⇑f ↑p ↑p) (hg : Set.MapsTo ⇑g ↑p ↑p) :
Commute (LinearMap.restrict f hf) (LinearMap.restrict g hg)
source
theorem LinearMap.subtype_comp_restrict {R : Type u_1} {M : Type u_5} {M₁ : Type u_6} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₁] [Module R M] [Module R M₁] {f : M →ₗ[R] M₁} {p : Submodule R M} {q : Submodule R M₁} (hf : ∀ x ∈ p, f x ∈ q) :
Submodule.subtype q ∘ₗ LinearMap.restrict f hf = LinearMap.domRestrict f p
source
theorem LinearMap.restrict_eq_codRestrict_domRestrict {R : Type u_1} {M : Type u_5} {M₁ : Type u_6} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₁] [Module R M] [Module R M₁] {f : M →ₗ[R] M₁} {p : Submodule R M} {q : Submodule R M₁} (hf : ∀ x ∈ p, f x ∈ q) :
LinearMap.restrict f hf = LinearMap.codRestrict q (LinearMap.domRestrict f p) ⋯
source
theorem LinearMap.restrict_eq_domRestrict_codRestrict {R : Type u_1} {M : Type u_5} {M₁ : Type u_6} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₁] [Module R M] [Module R M₁] {f : M →ₗ[R] M₁} {p : Submodule R M} {q : Submodule R M₁} (hf : ∀ (x : M), f x ∈ q) :
LinearMap.restrict f ⋯ = LinearMap.domRestrict (LinearMap.codRestrict q f hf) p
source
instance LinearMap.uniqueOfLeft {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [Subsingleton M] :
Unique (M →ₛₗ[σ₁₂] M₂)
Equations
source
instance LinearMap.uniqueOfRight {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [Subsingleton M₂] :
Unique (M →ₛₗ[σ₁₂] M₂)
Equations
source
@[simp]
theorem LinearMap.evalAddMonoidHom_apply {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} (a : M) (f : M →ₛₗ[σ₁₂] M₂) :
(LinearMap.evalAddMonoidHom a) f = f a
source
def LinearMap.evalAddMonoidHom {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [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
source
@[simp]
theorem LinearMap.toAddMonoidHom'_apply {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} (f : M →ₛₗ[σ₁₂] M₂) :
LinearMap.toAddMonoidHom' f = LinearMap.toAddMonoidHom f
source
def LinearMap.toAddMonoidHom' {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} :
(M →ₛₗ[σ₁₂] M₂) →+ M →+ M₂

LinearMap.toAddMonoidHom promoted to an AddMonoidHom.

Equations
  • LinearMap.toAddMonoidHom' = { toZeroHom := { toFun := LinearMap.toAddMonoidHom, map_zero' := ⋯ }, map_add' := ⋯ }
source
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] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} (t : Finset ι) (f : ι → M →ₛₗ[σ₁₂] M₂) (b : M) :
(Finset.sum t fun (d : ι) => f d) b = Finset.sum t fun (d : ι) => (f d) b
source
instance LinearMap.instNontrivialEnd {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [Nontrivial M] :
Nontrivial (Module.End R M)
Equations
  • ⋯ = ⋯
source
@[simp]
theorem LinearMap.coeFn_sum {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {ι : Type u_10} (t : Finset ι) (f : ι → M →ₛₗ[σ₁₂] M₂) :
⇑(Finset.sum t fun (i : ι) => f i) = Finset.sum t fun (i : ι) => ⇑(f i)
source
theorem LinearMap.submodule_pow_eq_zero_of_pow_eq_zero {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {N : Submodule R M} {g : Module.End R ↥N} {G : Module.End R M} (h : G ∘ₗ Submodule.subtype N = Submodule.subtype N ∘ₗ g) {k : ℕ} (hG : G ^ k = 0) :
g ^ k = 0
source
theorem LinearMap.pow_apply_mem_of_forall_mem {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {f' : M →ₗ[R] M} {p : Submodule R M} (n : ℕ) (h : ∀ x ∈ p, f' x ∈ p) (x : M) (hx : x ∈ p) :
(f' ^ n) x ∈ p
source
theorem LinearMap.pow_restrict {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {f' : M →ₗ[R] M} {p : Submodule R M} (n : ℕ) (h : ∀ x ∈ p, f' x ∈ p) (h' : optParam (∀ x ∈ p, (f' ^ n) x ∈ p) ⋯) :
LinearMap.restrict f' h ^ n = LinearMap.restrict (f' ^ n) h'
source
def LinearMap.domRestrict' {R : Type u_1} {M : Type u_5} {M₂ : Type u_7} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (p : Submodule R M) :
(M →ₗ[R] M₂) →ₗ[R] ↥p →ₗ[R] M₂

Alternative version of domRestrict as a linear map.

Equations
source
@[simp]
theorem LinearMap.domRestrict'_apply {R : Type u_1} {M : Type u_5} {M₂ : Type u_7} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (f : M →ₗ[R] M₂) (p : Submodule R M) (x : ↥p) :
((LinearMap.domRestrict' p) f) x = f ↑x
source
def Submodule.inclusion {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {p : Submodule R M} {p' : Submodule R M} (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
source
@[simp]
theorem Submodule.coe_inclusion {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {p : Submodule R M} {p' : Submodule R M} (h : p ≤ p') (x : ↥p) :
↑((Submodule.inclusion h) x) = ↑x
source
theorem Submodule.inclusion_apply {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {p : Submodule R M} {p' : Submodule R M} (h : p ≤ p') (x : ↥p) :
(Submodule.inclusion h) x = { val := ↑x, property := ⋯ }
source
theorem Submodule.inclusion_injective {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {p : Submodule R M} {p' : Submodule R M} (h : p ≤ p') :
Function.Injective ⇑(Submodule.inclusion h)
source
theorem Submodule.subtype_comp_inclusion {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) (q : Submodule R M) (h : p ≤ q) :
Submodule.subtype q ∘ₗ Submodule.inclusion h = Submodule.subtype p