English
There is a canonical extension of the map f to the joined space M ⊔ ⟨y⟩, given by x ↦ f x + φ of the y-component; this extension is itself an extension of f and sits inside a larger maximal extension.
Русский
Существует каноническое продолжение отображения f к объединённому пространству M ⊔ ⟨y⟩, заданное как x ↦ f(x) + φ(component) y; это продолжение является продолжением f и находится в большем максимальном расширении.
LaTeX
$$$ extensionOfMaxAdjoin(i,f,h,y) : ExtensionOf i f \\quad \\text{is an extension of } f $$$
Lean4
/-- The linear map `M ⊔ ⟨y⟩ ⟶ Q` by `x + r • y ↦ f x + φ r` is an extension of `f` -/
def extensionOfMaxAdjoin (h : Module.Baer R Q) (y : N) : ExtensionOf i f
where
domain := supExtensionOfMaxSingleton i f y
le := le_trans (extensionOfMax i f).le le_sup_left
toFun :=
{ toFun := ExtensionOfMaxAdjoin.extensionToFun i f h
map_add' := fun a b =>
by
have eq1 :
↑a + ↑b =
↑(ExtensionOfMaxAdjoin.fst i a + ExtensionOfMaxAdjoin.fst i b) +
(ExtensionOfMaxAdjoin.snd i a + ExtensionOfMaxAdjoin.snd i b) • y :=
by
rw [ExtensionOfMaxAdjoin.eqn, ExtensionOfMaxAdjoin.eqn, add_smul, Submodule.coe_add]
ac_rfl
rw [ExtensionOfMaxAdjoin.extensionToFun_wd (y := y) i f h (a + b) _ _ eq1, LinearPMap.map_add, map_add]
unfold ExtensionOfMaxAdjoin.extensionToFun
abel
map_smul' := fun r a => by
dsimp
have eq1 : r • (a : N) = ↑(r • ExtensionOfMaxAdjoin.fst i a) + (r • ExtensionOfMaxAdjoin.snd i a) • y :=
by
rw [ExtensionOfMaxAdjoin.eqn, smul_add, smul_eq_mul, mul_smul]
rfl
rw [ExtensionOfMaxAdjoin.extensionToFun_wd i f h (r • a :) _ _ eq1, LinearMap.map_smul, LinearPMap.map_smul, ←
smul_add]
congr }
is_extension
m := by
dsimp
rw [(extensionOfMax i f).is_extension, ExtensionOfMaxAdjoin.extensionToFun_wd i f h _ ⟨i m, _⟩ 0 _, map_zero,
add_zero]
simp
