Norm estimates on quotient modules

Descending a continuous semilinear map through a submodule contained in its kernel preserves its operator norm. Equivalently, precomposition with the quotient projection preserves operator norms. These facts apply to seminormed spaces and arbitrary submodules, and supply the metric part of the duality between a quotient and the annihilator of its defining submodule. The quotient projection is moreover a metric quotient map: it has norm at most one and lifts every vector of norm less than r to a vector of norm less than r. A closed-subspace quotient has a chosen bounded nonlinear right inverse with public bound constant two (Submodule.quotientRightInverse, Submodule.quotientRightInverse_nnnorm).

The quotient module also inherits a contractive action of a possibly noncommutative seminormed ring. In particular, this applies to quotients of a normed ring by left ideals.

The estimates reuse Mathlib's quotient norm and quotient lift for bounded additive homomorphisms.

theorem Submodule.norm_liftQL_le {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {F : Type u_4} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜₂ F] {σ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ] (S : Submodule 𝕜 E) (f : E →SL[σ] F) (h : S ≤ (↑f).ker) : ‖S.liftQL f h‖ ≤ ‖f‖

Descending through a quotient does not increase the operator norm.

@[simp]

theorem Submodule.norm_comp_mkQL {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {F : Type u_4} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜₂ F] {σ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ] (S : Submodule 𝕜 E) (f : E ⧸ S →SL[σ] F) : ‖f ∘SL S.mkQL‖ = ‖f‖

Precomposition with the quotient projection preserves the operator norm.

@[simp]

theorem Submodule.norm_liftQL {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {F : Type u_4} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜₂ F] {σ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ] (S : Submodule 𝕜 E) (f : E →SL[σ] F) (h : S ≤ (↑f).ker) : ‖S.liftQL f h‖ = ‖f‖

Descending through a quotient preserves the operator norm.

theorem Submodule.norm_mkQL_le {𝕜 : Type u_1} {E : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] (S : Submodule 𝕜 E) : ‖S.mkQL‖ ≤ 1

The quotient projection has operator norm at most one.

theorem Submodule.ball_subset_image_mkQL_ball {𝕜 : Type u_1} {E : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] (S : Submodule 𝕜 E) (r : ℝ) : Metric.ball 0 r ⊆ ⇑S.mkQL '' Metric.ball 0 r

The quotient projection lifts every vector of norm less than r to a vector of norm less than r. With Submodule.norm_mkQL_le, this says that it is a metric quotient map.

instance Submodule.Quotient.isBoundedSMul {R : Type u_1} {E : Type u_2} [SeminormedRing R] [SeminormedAddCommGroup E] [Module R E] [IsBoundedSMul R E] (S : Submodule R E) : IsBoundedSMul R (E ⧸ S)

The quotient action of a seminormed ring is contractive whenever the original action is. The ring need not be commutative, and the submodule need not be closed.

noncomputable def Submodule.quotientRightInverse {𝕜 : Type u_1} {F : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (W : Submodule 𝕜 F) [IsClosed ↑W] : W.mkQL.NonlinearRightInverse

The quotient norm gives a right inverse of bound 2 for a closed-subspace quotient.

@[simp]

theorem Submodule.quotientRightInverse_nnnorm {𝕜 : Type u_1} {F : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (W : Submodule 𝕜 F) [IsClosed ↑W] : W.quotientRightInverse.nnnorm = 2

The chosen quotient lift has the public uniform bound constant two.