English
In a setting of a normed ring, a linear map is a unit if and only if it is bijective.
Русский
В обстановке нормированного кольца линейное отображение является единицей тогда и только тогда, когда оно биективно.
LaTeX
$$$\\text{IsUnit}(f) \\iff \\text{Bijective}(f)$$$
Lean4
/-- Intermediate definition used to show
`ContinuousLinearMap.closed_complemented_range_of_isCompl_of_ker_eq_bot`.
This is `f.coprod G.subtypeL` as a `ContinuousLinearEquiv`. -/
noncomputable def 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 = ⊥) :
(E × G) ≃L[𝕜] F :=
ContinuousLinearEquiv.ofBijective (f.coprod G.subtypeL)
(by
rw [ker_coprod_of_disjoint_range]
· rw [hker, Submodule.ker_subtypeL, Submodule.prod_bot]
· rw [Submodule.range_subtypeL]
exact h.disjoint)
(by simp only [range_coprod, Submodule.range_subtypeL, h.sup_eq_top])
