extension_property — Mathlib

English

Baer's criterion for injective modules: given an injective M and a map f: P → P' with f injective, every linear map g: P → M extends to some h: P' → M, i.e., h ∘ f = g.

Русский

Критерий Баера для инъективных модулей: если M инъективен и есть инъективное отображение f: P → P', то каждый линейный отображение g: P → M может быть продолжено до h: P' → M, причём h ∘ f = g.

LaTeX

$$$ \\exists h : P' \\to M, h \\circ f = g $$$

Lean4

theorem extension_property (f : P →ₗ[R] P') (hf : Function.Injective f) (g : P →ₗ[R] M) :
    ∃ h : P' →ₗ[R] M, h ∘ₗ f = g :=
  (Module.Baer.of_injective inj).extension_property f hf g

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