exists_rightInverse_of_surjective

English

If P is projective and f: M →ₗ[R] P is surjective, there exists a linear map g: P →ₗ[R] M such that f ∘ g = id_P.

Русский

Если P проективен и f: M →ₗ[R] P сюръективно, то существует линейное отображение g: P →ₗ[R] M such that f ∘ g = id_P.

LaTeX

$$$$ \\exists g: M \\to P, \\; f \\circ g = \\mathrm{id}_P. $$$$

Lean4

theorem _root_.LinearMap.exists_rightInverse_of_surjective [Projective R P] (f : M →ₗ[R] P) (hf_surj : range f = ⊤) :
    ∃ g : P →ₗ[R] M, f ∘ₗ g = LinearMap.id :=
  projective_lifting_property f (.id : P →ₗ[R] P) (LinearMap.range_eq_top.1 hf_surj)

Похожие утверждения