extension_property_addMonoidHom — Mathlib

English

If Q is Baer over the integers, then for any injective AddMonoidHom f, and any AddMonoidHom g: M → Q, there exists a Baer extension h: N → Q with h ∘ f = g.

Русский

Если Q является Баером над целыми, то для любого инъективного отображения AddMonoidHom f и любого гомоморфизма g: M → Q существует расширение h: N → Q с условием h ∘ f = g.

LaTeX

$$$ \\exists h: N \\to Q, h \\circ f = g $$$

Lean4

theorem extension_property_addMonoidHom (h : Module.Baer ℤ Q) (f : M →+ N) (hf : Function.Injective f) (g : M →+ Q) :
    ∃ h : N →+ Q, h.comp f = g :=
  have ⟨g', hg'⟩ := h.extension_property f.toIntLinearMap hf g.toIntLinearMap
  ⟨g', congr(LinearMap.toAddMonoidHom $hg')⟩

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