English
For any y and r, if hr is a proof that r · y lies in the domain, then extendIdealTo(i,f,h,y)(r) equals the maximal extension evaluated at r · y.
Русский
Для любого y и r, если hr доказывает, что r · y лежит в области определения, то extendIdealTo(i,f,h,y)(r) равно значению максимального расширения на r · y.
LaTeX
$$$ ExtendIdealTo(i,f,h,y)(r) = (extensionOfMax(i,f)).toLinearPMap( \\langle r \\cdot y, hr \\rangle ) $$$
Lean4
protected theorem extension_property (h : Module.Baer R Q) (f : M →ₗ[R] N) (hf : Function.Injective f) (g : M →ₗ[R] Q) :
∃ h, h ∘ₗ f = g :=
haveI : Fact (Function.Injective f) := ⟨hf⟩
Exists.intro
{ toFun := ((extensionOfMax f g).toLinearPMap ⟨·, (extensionOfMax_to_submodule_eq_top f g h).symm ▸ ⟨⟩⟩)
map_add' := fun x y ↦ by rw [← LinearPMap.map_add]; congr
map_smul' := fun r x ↦ by rw [← LinearPMap.map_smul]; dsimp } <|
LinearMap.ext fun x ↦ ((extensionOfMax f g).is_extension x).symm
