extension_property — Mathlib

English

For P with abelian group structure and an R-module structure, given an injective f: N → M and any g: N → P, there exists h: M → P with h ∘ f = g.

Русский

Для абелевой группы P и R-модуля P, при инъективном f: N → M и любом g: N → P найдётся h: M → P такой, что h ∘ f = g.

LaTeX

$$For f : N →ₗ[R] M with hf injective, ∀ g : N →ₗ[R] P, ∃ h : M →ₗ[R] P, h ∘ f = g$$

Lean4

theorem extension_property {P} [AddCommGroup P] [Module R P] (f : N →ₗ[R] M) (hf : Function.Injective f)
    (g : N →ₗ[R] P) : ∃ h : M →ₗ[R] P, h ∘ₗ f = g :=
  have ⟨m, compl⟩ := exists_isCompl (LinearMap.range f)
  ⟨g ∘ₗ f.linearProjOfIsCompl _ hf compl, by ext; simp⟩

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