English
Let f: E →L[F] be a continuous linear map between normed spaces. Let G be a submodule of F such that the range of f is complemented by G (so F is the direct sum of range(f) and G). If ker f = {0}, then Range(f) equals the image of the direct product ⊤_E × ⊥_G under the canonical coprod map, i.e. Range(f) = ((⊤ : Submodule 𝕜 E).prod (⊥ : Submodule 𝕜 G)).map (f.coprodSubtypeLEquivOfIsCompl h hker).
Русский
Пусть f: E →L[𝕜] F — непрерывное линейное отображение между нормированными пространствами. Пусть G — подпространство F такое, что L = range(f) является дополнением к G (то есть F распадается как прямая сумма range(f) ⊕ G). Если ядро f тривиально, то образ f совпадает с образом прямой суммы E × G под каноническим копрод-переносом: range(f) = ((⊤ : Submodule 𝕜 E).prod (⊥ : Submodule 𝕜 G)).map (f.coprodSubtypeLEquivOfIsCompl h hker).
LaTeX
$$$\operatorname{range}(f) = \big( (\top_E : Submodule_𝕜 E) \prod (\bot_G : Submodule_𝕜 G) \big).map\Bigl( f.coprodSubtypeLEquivOfIsCompl\;h\;hker : E \times G \to_ℒ[𝕜] F \Bigr)$$$
Lean4
theorem range_eq_map_coprodSubtypeLEquivOfIsCompl {F : Type*} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F]
(f : E →L[𝕜] F) {G : Submodule 𝕜 F} (h : IsCompl (LinearMap.range f) G) [CompleteSpace G] (hker : ker f = ⊥) :
LinearMap.range f =
((⊤ : Submodule 𝕜 E).prod (⊥ : Submodule 𝕜 G)).map (f.coprodSubtypeLEquivOfIsCompl h hker : E × G →ₗ[𝕜] F) :=
by
rw [coprodSubtypeLEquivOfIsCompl, ContinuousLinearEquiv.coe_ofBijective, coe_coprod, LinearMap.coprod_map_prod,
Submodule.map_bot, sup_bot_eq, Submodule.map_top]
rfl
/- TODO: remove the assumption `f.ker = ⊥` in the next lemma, by using the map induced by `f` on
`E / f.ker`, once we have quotient normed spaces. -/
