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.

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 := ⋯ }

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

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

@[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.

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

theorem Submodule.isEmbedding_subtype {R : Type u_1} [Semiring R] {M : Type u_2} [TopologicalSpace M] [AddCommMonoid M] [Module R M] (p : Submodule R M) : Topology.IsEmbedding ⇑p.subtype

theorem Submodule.isEmbedding_subtypeL {R : Type u_1} [Semiring R] {M : Type u_2} [TopologicalSpace M] [AddCommMonoid M] [Module R M] (p : Submodule R M) : Topology.IsEmbedding ⇑p.subtypeL

theorem Submodule.isClosedEmbedding_subtype {R : Type u_1} [Semiring R] {M : Type u_2} [TopologicalSpace M] [AddCommMonoid M] [Module R M] (p : Submodule R M) (hp : IsClosed ↑p) : Topology.IsClosedEmbedding ⇑p.subtype

theorem Submodule.isClosedEmbedding_subtypeL {R : Type u_1} [Semiring R] {M : Type u_2} [TopologicalSpace M] [AddCommMonoid M] [Module R M] (p : Submodule R M) (hp : IsClosed ↑p) : Topology.IsClosedEmbedding ⇑p.subtypeL

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

@[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 = ⊥

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

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

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

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).domRestrict ⇑f

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 := ⋯ }

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

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

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

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

@[simp]

theorem ContinuousLinearMap.subtypeL_comp_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) : p.subtypeL ∘SL f.codRestrict p h = f

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

@[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 ⋯

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

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

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 ⋯

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

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

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, ⋯⟩

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

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

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 ⋯

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

def ContinuousLinearMap.projKerOfRightInverse {R₁ : Type u_1} {R₂ : Type u_2} [Ring R₁] [Ring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [RingHomInvPair σ₁₂ σ₂₁] {M₁ : Type u_3} {M₂ : Type u_4} [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 ⋯

@[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_3} {M₂ : Type u_4} [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)

@[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_3} {M₂ : Type u_4} [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

@[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_3} {M₂ : Type u_4} [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