English
One can define a linear map from the sum M ⊔ ⟨y⟩ to Q by sending x + r y to f(x) + φ(r). This gives a well-defined extension to the joined space.
Русский
Можно определить линейное отображение от объединения M ⊔ ⟨y⟩ в Q, послав x + r y в f(x) + φ(r). Это образует корректное продолжение на присоединённое пространство.
LaTeX
$$$ extensionToFun(h) : (supExtensionOfMaxSingleton i f y) \\to Q \\\\; x \\mapsto (extensionOfMax i f).toLinearPMap (ExtensionOfMaxAdjoin.fst i x) + ExtensionOfMaxAdjoin.extendIdealTo i f h y (ExtensionOfMaxAdjoin.snd i x) $$$
Lean4
/-- We can finally define a linear map `M ⊔ ⟨y⟩ ⟶ Q` by `x + r • y ↦ f x + φ r`
-/
def extensionToFun (h : Module.Baer R Q) {y : N} : supExtensionOfMaxSingleton i f y → Q := fun x =>
(extensionOfMax i f).toLinearPMap (ExtensionOfMaxAdjoin.fst i x) +
ExtensionOfMaxAdjoin.extendIdealTo i f h y (ExtensionOfMaxAdjoin.snd i x)
