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} [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

SMulMemClass.subtype S' = { toFun := Subtype.val, map_add' := ⋯, map_smul' := ⋯ }

Instances For

source

@[simp]

theorem SMulMemClass.subtype_apply {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 : ↥S') :

(SMulMemClass.subtype S') x = ↑x

source

theorem SMulMemClass.subtype_injective {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) :

Function.Injective ⇑(SMulMemClass.subtype S')

source

@[simp]

theorem SMulMemClass.coe_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) :

⇑(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

p.subtype = { toFun := Subtype.val, map_add' := ⋯, map_smul' := ⋯ }

Instances For

source

@[simp]

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

p.subtype x = ↑x

source

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

Function.Injective ⇑p.subtype

source

@[simp]

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

⇑p.subtype = 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 ⇑p.subtype

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 ι) :

↑(∑ i ∈ s, x i) = ∑ i ∈ s, ↑(x i)

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

source

instance Submodule.instAddActionSubtypeMem {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

p.instAddActionSubtypeMem = AddAction.compHom α p.subtype.toAddMonoidHom

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

f.domRestrict p = f ∘ₛₗ p.subtype

Instances For

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

(f.domRestrict 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.

See also LinearMap.codLift.

Equations

LinearMap.codRestrict p f h = { toFun := fun (c : M) => ⟨f c, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }

Instances For

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

↑((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) :

codRestrict p g h ∘ₛₗ f = codRestrict p (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) :

p.subtype ∘ₛₗ codRestrict p f h = f

source

noncomputable def LinearMap.codLift {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₂) {M₂' : Type u_10} [AddCommMonoid M₂'] [Module R₂ M₂'] (p : M₂' →ₗ[R₂] M₂) (hp : Function.Injective ⇑p) (h : ∀ (c : M), f c ∈ Set.range ⇑p) :

M →ₛₗ[σ₁₂] M₂'

A linear map f : M → M₂ whose values lie in the image of an injective linear map p : M₂' → M₂ admits a unique lift to a linear map M → M₂'.

Equations

f.codLift p hp h = { toFun := fun (c : M) => Exists.choose ⋯, map_add' := ⋯, map_smul' := ⋯ }

Instances For

source

@[simp]

theorem LinearMap.codLift_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₂) {M₂' : Type u_10} [AddCommMonoid M₂'] [Module R₂ M₂'] (p : M₂' →ₗ[R₂] M₂) (hp : Function.Injective ⇑p) (h : ∀ (c : M), f c ∈ Set.range ⇑p) (x : M) :

(f.codLift p hp h) x = Exists.choose ⋯

source

@[simp]

theorem LinearMap.comp_codLift {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₂) {M₂' : Type u_10} [AddCommMonoid M₂'] [Module R₂ M₂'] (p : M₂' →ₗ[R₂] M₂) (hp : Function.Injective ⇑p) (h : ∀ (c : M), f c ∈ Set.range ⇑p) :

p ∘ₛₗ f.codLift p hp 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

f.restrict hf = LinearMap.codRestrict q (f.domRestrict p) ⋯

Instances For

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

↑((f.restrict 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) :

(f.restrict hf) x = ⟨f ↑x, ⋯⟩

source

theorem LinearMap.restrict_sub {R : Type u_10} {M : Type u_11} {M₁ : Type u_12} [Ring R] [AddCommGroup M] [AddCommGroup M₁] [Module R M] [Module R M₁] {p : Submodule R M} {q : Submodule R M₁} {f g : M →ₗ[R] M₁} (hf : Set.MapsTo ⇑f ↑p ↑q) (hg : Set.MapsTo ⇑g ↑p ↑q) (hfg : Set.MapsTo ⇑(f - g) ↑p ↑q := ⋯) :

f.restrict hf - g.restrict hg = (f - g).restrict hfg

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 : Set.MapsTo ⇑(g ∘ₗ f) ↑p ↑p₃ := ⋯) :

(g ∘ₗ f).restrict hfg = g.restrict hg ∘ₗ f.restrict hf

source

theorem LinearMap.restrict_smul_one {R : Type u_10} {M : Type u_11} [CommSemiring R] [AddCommMonoid M] [Module R M] {p : Submodule R M} (μ : R) (h : ∀ x ∈ p, (μ • 1) x ∈ p := ⋯) :

restrict (μ • 1) h = μ • 1

source

theorem LinearMap.restrict_commute {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {f 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 (f.restrict hf) (g.restrict 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) :

q.subtype ∘ₗ f.restrict hf = f.domRestrict 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) :

f.restrict hf = codRestrict q (f.domRestrict 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) :

f.restrict ⋯ = (codRestrict q f hf).domRestrict p

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

(∑ d ∈ t, f d) b = ∑ d ∈ t, (f d) b

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₂) :

⇑(∑ i ∈ t, f i) = ∑ i ∈ t, ⇑(f i)

source

theorem Module.End.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 : End R ↥N} {G : End R M} (h : G ∘ₗ N.subtype = N.subtype ∘ₗ g) {k : ℕ} (hG : G ^ k = 0) :

g ^ k = 0

source

theorem Module.End.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 Module.End.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' : ∀ x ∈ p, (f' ^ n) x ∈ p := ⋯) :

f'.restrict h ^ n = (f' ^ n).restrict 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

LinearMap.domRestrict' p = { toFun := fun (φ : M →ₗ[R] M₂) => φ.domRestrict p, map_add' := ⋯, map_smul' := ⋯ }

Instances For

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

((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 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

Submodule.inclusion h = LinearMap.codRestrict p' p.subtype ⋯

Instances For

source

@[simp]

theorem Submodule.coe_inclusion {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {p p' : Submodule R M} (h : p ≤ p') (x : ↥p) :

↑((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 p' : Submodule R M} (h : p ≤ p') (x : ↥p) :

(inclusion h) x = ⟨↑x, ⋯⟩

source

theorem Submodule.inclusion_injective {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {p p' : Submodule R M} (h : p ≤ p') :

Function.Injective ⇑(inclusion h)

source

theorem Submodule.subtype_comp_inclusion {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] (p q : Submodule R M) (h : p ≤ q) :

q.subtype ∘ₗ inclusion h = p.subtype

Documentation

Mathlib.Algebra.Module.Submodule.LinearMap

Linear maps involving submodules of a module #

Main declarations #

Tags #