surjective_linearMapComp_left — Mathlib

English

If P is projective, then precomposition with a surjective f: M →ₗ[R] P induces a surjective map on the Hom-sets: for every h: N →ₗ[R] P there exists g: N →ₗ[R] M with f ∘ g = h.

Русский

Если P проективен, то предкомпозиция с сюръективным отображением f: M →ₗ[R] P индуцирует сюръективное отображение между множествами гомоморфизмов: для каждого h: N →ₗ[R] P существует g: N →ₗ[R] M такой, что f ∘ g = h.

LaTeX

$$$$ \\forall h: N \\to P, \\; \\exists g: N \\to M, \\; f \\circ g = h. $$$$

Lean4

theorem _root_.Function.Surjective.surjective_linearMapComp_left [Projective R P] {f : M →ₗ[R] P}
    (hf_surj : Surjective f) : Surjective (fun g : N →ₗ[R] M ↦ f.comp g) :=
  surjective_comp_left_of_exists_rightInverse <|
    f.exists_rightInverse_of_surjective <| range_eq_top_of_surjective f hf_surj

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