Restrictions of continuous linear maps to submodules #

In this file, we collect the various operations of restrictions of ContinuousLinearMaps to subspaces of the domain/codomain.

Main definitions #

Submodule.subtypeL S is the inclusion map S →L[R] M when S : Submodule R M. In other words, it is Submodule.subtype S bundled as a ContinuousLinearMap.
ContinuousLinearMap.domRestrict f S is the map S →SL[σ] N obtained by restricting f : M →SL[σ] N to a subspace S of the domain. This is the continuous version of LinearMap.domRestrict.
ContinuousLinearMap.codRestrict f S h is the map M →SL[σ] S obtained by co-restricting f : M →SL[σ] N to a subspace S of the codomain; this requires a proof h that all values of f indeed belong to S. This is the continuous version of LinearMap.codRestrict.
ContinuousLinearMap.rangeRestrict f is an abbreviation for f.codRestrict f.range ⋯ : M →SL[σ] f.range. This is the continuous version of LinearMap.rangeRestrict.
ContinuousLinearMap.restrict f h is the map S →SL[σ] T obtained by restricting from f : M →SL[σ] N and a proof h that f maps S inside T. This is the continuous version of LinearMap.restrict.

source

def Submodule.subtypeL {R : Type u_1} [Semiring R] {M : Type u_2} [TopologicalSpace M] [AddCommMonoid M] [Module R M] (p : Submodule R M) :

↥p →L[R] M

Submodule.subtype as a ContinuousLinearMap.

Equations

p.subtypeL = { toLinearMap := p.subtype, cont := ⋯ }

Instances For

source

@[simp]

theorem Submodule.toLinearMap_subtypeL {R : Type u_1} [Semiring R] {M : Type u_2} [TopologicalSpace M] [AddCommMonoid M] [Module R M] (p : Submodule R M) :

↑p.subtypeL = p.subtype

source

@[simp]

theorem Submodule.coe_subtypeL {R : Type u_1} [Semiring R] {M : Type u_2} [TopologicalSpace M] [AddCommMonoid M] [Module R M] (p : Submodule R M) :

⇑p.subtypeL = ⇑p.subtype

source

@[deprecated Submodule.coe_subtypeL (since := "2026-05-06")]

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

⇑p.subtypeL = ⇑p.subtype

Alias of Submodule.coe_subtypeL.

source

theorem Submodule.subtypeL_apply {R : Type u_1} [Semiring R] {M : Type u_2} [TopologicalSpace M] [AddCommMonoid M] [Module R M] (p : Submodule R M) (x : ↥p) :

p.subtypeL x = ↑x

source

@[deprecated Submodule.range_subtype (since := "2026-05-06")]

theorem Submodule.range_subtypeL {R : Type u_1} [Semiring R] {M : Type u_2} [TopologicalSpace M] [AddCommMonoid M] [Module R M] (p : Submodule R M) :

(↑p.subtypeL).range = p

source

@[deprecated Submodule.ker_subtype (since := "2026-05-06")]

theorem Submodule.ker_subtypeL {R : Type u_1} [Semiring R] {M : Type u_2} [TopologicalSpace M] [AddCommMonoid M] [Module R M] (p : Submodule R M) :

(↑p.subtypeL).ker = ⊥

source

def ContinuousLinearMap.domRestrict {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} {M₂ : Type u_5} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R₁ M₁] [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₂ M₂] (f : M₁ →SL[σ₁₂] M₂) (p : Submodule R₁ M₁) :

↥p →SL[σ₁₂] 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 ∘SL p.subtypeL

Instances For

source

@[simp]

theorem ContinuousLinearMap.domRestrict_apply {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} {M₂ : Type u_5} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R₁ M₁] [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₂ M₂] (f : M₁ →SL[σ₁₂] M₂) (p : Submodule R₁ M₁) (x : ↥p) :

(f.domRestrict p) x = f ↑x

source

@[simp]

theorem ContinuousLinearMap.toLinearMap_domRestrict {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} {M₂ : Type u_5} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R₁ M₁] [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₂ M₂] (f : M₁ →SL[σ₁₂] M₂) (p : Submodule R₁ M₁) :

↑(f.domRestrict p) = (↑f).domRestrict p

source

theorem ContinuousLinearMap.coe_domRestrict {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} {M₂ : Type u_5} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R₁ M₁] [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₂ M₂] (f : M₁ →SL[σ₁₂] M₂) (p : Submodule R₁ M₁) :

⇑(f.domRestrict p) = (↑p).restrict ⇑f

source

def ContinuousLinearMap.codRestrict {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} {M₂ : Type u_5} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R₁ M₁] [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₂ M₂] (f : M₁ →SL[σ₁₂] M₂) (p : Submodule R₂ M₂) (h : ∀ (x : M₁), f x ∈ p) :

M₁ →SL[σ₁₂] ↥p

Restrict codomain of a continuous linear map.

Equations

f.codRestrict p h = { toLinearMap := LinearMap.codRestrict p (↑f) h, cont := ⋯ }

Instances For

source

@[simp]

theorem ContinuousLinearMap.toLinearMap_codRestrict {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} {M₂ : Type u_5} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R₁ M₁] [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₂ M₂] (f : M₁ →SL[σ₁₂] M₂) (p : Submodule R₂ M₂) (h : ∀ (x : M₁), f x ∈ p) :

↑(f.codRestrict p h) = LinearMap.codRestrict p (↑f) h

source

theorem ContinuousLinearMap.coe_codRestrict {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} {M₂ : Type u_5} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R₁ M₁] [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₂ M₂] (f : M₁ →SL[σ₁₂] M₂) (p : Submodule R₂ M₂) (h : ∀ (x : M₁), f x ∈ p) :

⇑(f.codRestrict p h) = Set.codRestrict (⇑f) (↑p) h

source

@[simp]

theorem ContinuousLinearMap.coe_codRestrict_apply {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} {M₂ : Type u_5} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R₁ M₁] [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₂ M₂] (f : M₁ →SL[σ₁₂] M₂) (p : Submodule R₂ M₂) (h : ∀ (x : M₁), f x ∈ p) (x : M₁) :

↑((f.codRestrict p h) x) = f x

source

theorem ContinuousLinearMap.ker_codRestrict {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} {M₂ : Type u_5} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R₁ M₁] [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₂ M₂] (f : M₁ →SL[σ₁₂] M₂) (p : Submodule R₂ M₂) (h : ∀ (x : M₁), f x ∈ p) :

(↑(f.codRestrict p h)).ker = (↑f).ker

source

@[simp]

theorem ContinuousLinearMap.domRestrict_comp_codRestrict {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [Semiring R₁] [Semiring R₂] [Semiring R₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] {M₁ : Type u_4} {M₂ : Type u_5} {M₃ : Type u_6} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R₁ M₁] [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₂ M₂] [TopologicalSpace M₃] [AddCommMonoid M₃] [Module R₃ M₃] (g : M₂ →SL[σ₂₃] M₃) (f : M₁ →SL[σ₁₂] M₂) (p : Submodule R₂ M₂) (h : ∀ (x : M₁), f x ∈ p) :

g.domRestrict p ∘SL f.codRestrict p h = g ∘SL f

source

@[reducible, inline]

abbrev ContinuousLinearMap.rangeRestrict {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} {M₂ : Type u_5} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R₁ M₁] [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₂ M₂] [RingHomSurjective σ₁₂] (f : M₁ →SL[σ₁₂] M₂) :

M₁ →SL[σ₁₂] ↥(↑f).range

Restrict the codomain of a continuous linear map f to f.range.

Equations

f.rangeRestrict = f.codRestrict (↑f).range ⋯

Instances For

source

theorem ContinuousLinearMap.toLinearMap_rangeRestrict {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} {M₂ : Type u_5} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R₁ M₁] [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₂ M₂] [RingHomSurjective σ₁₂] (f : M₁ →SL[σ₁₂] M₂) :

↑f.rangeRestrict = (↑f).rangeRestrict

source

@[simp]

theorem ContinuousLinearMap.coe_rangeRestrict {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} {M₂ : Type u_5} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R₁ M₁] [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₂ M₂] [RingHomSurjective σ₁₂] (f : M₁ →SL[σ₁₂] M₂) :

⇑f.rangeRestrict = Set.rangeFactorization ⇑f

source

def ContinuousLinearMap.restrict {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} {M₂ : Type u_5} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R₁ M₁] [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₂ M₂] (f : M₁ →SL[σ₁₂] M₂) {p : Submodule R₁ M₁} {q : Submodule R₂ M₂} (h : ∀ x ∈ p, f x ∈ q) :

↥p →SL[σ₁₂] ↥q

Restrict codomain of a continuous linear map.

Equations

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

Instances For

source

@[simp]

theorem ContinuousLinearMap.toLinearMap_restrict {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} {M₂ : Type u_5} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R₁ M₁] [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₂ M₂] {f : M₁ →SL[σ₁₂] M₂} {p : Submodule R₁ M₁} {q : Submodule R₂ M₂} (h : ∀ x ∈ p, f x ∈ q) :

↑(f.restrict h) = (↑f).restrict h

source

@[simp]

theorem ContinuousLinearMap.coe_restrict_apply {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} {M₂ : Type u_5} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R₁ M₁] [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₂ M₂] {f : M₁ →SL[σ₁₂] 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 ContinuousLinearMap.restrict_apply {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} {M₂ : Type u_5} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R₁ M₁] [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₂ M₂] {f : M₁ →SL[σ₁₂] 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 ContinuousLinearMap.restrict_comp {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [Semiring R₁] [Semiring R₂] [Semiring R₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] {M₁ : Type u_4} {M₂ : Type u_5} {M₃ : Type u_6} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R₁ M₁] [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₂ M₂] [TopologicalSpace M₃] [AddCommMonoid M₃] [Module R₃ M₃] {p : Submodule R₁ M₁} {p₂ : Submodule R₂ M₂} {p₃ : Submodule R₃ M₃} {f : M₁ →SL[σ₁₂] M₂} {g : M₂ →SL[σ₂₃] M₃} (hf : Set.MapsTo ⇑f ↑p ↑p₂) (hg : Set.MapsTo ⇑g ↑p₂ ↑p₃) (hfg : Set.MapsTo ⇑(g ∘SL f) ↑p ↑p₃ := ⋯) :

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

source

theorem ContinuousLinearMap.subtypeL_comp_restrict {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} {M₂ : Type u_5} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R₁ M₁] [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₂ M₂] {f : M₁ →SL[σ₁₂] M₂} {p : Submodule R₁ M₁} {q : Submodule R₂ M₂} (hf : ∀ x ∈ p, f x ∈ q) :

q.subtypeL ∘SL f.restrict hf = f.domRestrict p

source

theorem ContinuousLinearMap.restrict_eq_codRestrict_domRestrict {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} {M₂ : Type u_5} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R₁ M₁] [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₂ M₂] {f : M₁ →SL[σ₁₂] M₂} {p : Submodule R₁ M₁} {q : Submodule R₂ M₂} (hf : ∀ x ∈ p, f x ∈ q) :

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

source

theorem ContinuousLinearMap.restrict_eq_domRestrict_codRestrict {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} {M₂ : Type u_5} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R₁ M₁] [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₂ M₂] {f : M₁ →SL[σ₁₂] M₂} {p : Submodule R₁ M₁} {q : Submodule R₂ M₂} (hf : ∀ (x : M₁), f x ∈ q) :

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

source

def ContinuousLinearMap.projKerOfRightInverse {R₁ : Type u_1} {R₂ : Type u_2} [Ring R₁] [Ring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [RingHomInvPair σ₁₂ σ₂₁] {M₁ : Type u_4} {M₂ : Type u_5} [TopologicalSpace M₁] [AddCommGroup M₁] [Module R₁ M₁] [TopologicalSpace M₂] [AddCommGroup M₂] [Module R₂ M₂] [IsTopologicalAddGroup M₁] (f₁ : M₁ →SL[σ₁₂] M₂) (f₂ : M₂ →SL[σ₂₁] M₁) (h : Function.RightInverse ⇑f₂ ⇑f₁) :

M₁ →L[R₁] ↥(↑f₁).ker

Given a right inverse f₂ : M₂ →L[R] M₁ to f₁ : M₁ →L[R] M₂, projKerOfRightInverse f₁ f₂ h is the projection M₁ →L[R] LinearMap.ker f₁ along LinearMap.range f₂.

Equations

f₁.projKerOfRightInverse f₂ h = (ContinuousLinearMap.id R₁ M₁ - f₂ ∘SL f₁).codRestrict (↑f₁).ker ⋯

Instances For

source

@[simp]

theorem ContinuousLinearMap.coe_projKerOfRightInverse_apply {R₁ : Type u_1} {R₂ : Type u_2} [Ring R₁] [Ring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [RingHomInvPair σ₁₂ σ₂₁] {M₁ : Type u_4} {M₂ : Type u_5} [TopologicalSpace M₁] [AddCommGroup M₁] [Module R₁ M₁] [TopologicalSpace M₂] [AddCommGroup M₂] [Module R₂ M₂] [IsTopologicalAddGroup M₁] (f₁ : M₁ →SL[σ₁₂] M₂) (f₂ : M₂ →SL[σ₂₁] M₁) (h : Function.RightInverse ⇑f₂ ⇑f₁) (x : M₁) :

↑((f₁.projKerOfRightInverse f₂ h) x) = x - f₂ (f₁ x)

source

@[simp]

theorem ContinuousLinearMap.projKerOfRightInverse_apply_idem {R₁ : Type u_1} {R₂ : Type u_2} [Ring R₁] [Ring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [RingHomInvPair σ₁₂ σ₂₁] {M₁ : Type u_4} {M₂ : Type u_5} [TopologicalSpace M₁] [AddCommGroup M₁] [Module R₁ M₁] [TopologicalSpace M₂] [AddCommGroup M₂] [Module R₂ M₂] [IsTopologicalAddGroup M₁] (f₁ : M₁ →SL[σ₁₂] M₂) (f₂ : M₂ →SL[σ₂₁] M₁) (h : Function.RightInverse ⇑f₂ ⇑f₁) (x : ↥(↑f₁).ker) :

(f₁.projKerOfRightInverse f₂ h) ↑x = x

source

@[simp]

theorem ContinuousLinearMap.projKerOfRightInverse_comp_inv {R₁ : Type u_1} {R₂ : Type u_2} [Ring R₁] [Ring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [RingHomInvPair σ₁₂ σ₂₁] {M₁ : Type u_4} {M₂ : Type u_5} [TopologicalSpace M₁] [AddCommGroup M₁] [Module R₁ M₁] [TopologicalSpace M₂] [AddCommGroup M₂] [Module R₂ M₂] [IsTopologicalAddGroup M₁] (f₁ : M₁ →SL[σ₁₂] M₂) (f₂ : M₂ →SL[σ₂₁] M₁) (h : Function.RightInverse ⇑f₂ ⇑f₁) (y : M₂) :

(f₁.projKerOfRightInverse f₂ h) (f₂ y) = 0

Documentation

Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Restrict

Restrictions of continuous linear maps to submodules #

Main definitions #