surjective_compr₂_of_exists_rightInverse

English

If f is surjective and there exists a right inverse g' of g with g ∘ g' = id, then f.compr₂ g is surjective.

Русский

Если f сюръективна и существует правая обратная для g, скажем g', такая что g ∘ g' = id, то f.compr₂ g сюръективна.

LaTeX

$$$\text{Surjective}(f) \to (\exists g' : Q \to P, g \circ g' = \mathrm{id}) \to \text{Surjective}(f.compr₂ g).$$$

Lean4

/-- A version of `Function.Surjective.comp` for composition of a bilinear map with a linear map. -/
theorem surjective_compr₂_of_exists_rightInverse (f : M →ₗ[R] Nₗ →ₗ[R] Pₗ) (g : Pₗ →ₗ[R] Qₗ) (hf : Surjective f)
    (hg : ∃ g' : Qₗ →ₗ[R] Pₗ, g.comp g' = LinearMap.id) : Surjective (f.compr₂ g) :=
  (surjective_comp_left_of_exists_rightInverse hg).comp hf

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