extendIdealTo — Mathlib

English

Assuming Q is Baer, the map from the ideal I_y to Q extends to a linear map φ: R → Q. That is, the restriction of φ to I_y coincides with idealTo, and φ is defined on all of R by Baer's property.

Русский

Пусть Q является Баером. Отображение от идеала I_y к Q расширяется до линейного отображения φ: R → Q, причём ограничение φ на I_y совпадает с idealTo, а φ определено на всём R по свойству Баера.

LaTeX

$$$ \\exists \\phi : R \\to Q \\text{ linear, such that } \\phi|_{I_y} = idealTo(i,f,y) $$$

Lean4

/-- Since we assumed `Q` being Baer, the linear map `x ↦ f' (x • y) : I ⟶ Q` extends to `R ⟶ Q`,
call this extended map `φ` -/
def extendIdealTo (h : Module.Baer R Q) (y : N) : R →ₗ[R] Q :=
  (h (ExtensionOfMaxAdjoin.ideal i f y) (ExtensionOfMaxAdjoin.idealTo i f y)).choose

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